diff --git a/.project b/.project index 4477a83..e840b49 100644 --- a/.project +++ b/.project @@ -25,6 +25,11 @@ + + net.alloyggp.griddle.gdlValidator + + + org.eclipse.jdt.core.javanature diff --git a/war/root/games/amazonsSuicide_10x10/METADATA b/war/root/games/amazonsSuicide_10x10/METADATA new file mode 100644 index 0000000..42d4dae --- /dev/null +++ b/war/root/games/amazonsSuicide_10x10/METADATA @@ -0,0 +1,6 @@ +{ + "gameName": "Amazons Suicide (10x10)", + + "rulesheet": "amazonsSuicide_10x10.kif", + "stylesheet": "amazonsSuicide_10x10.xsl" +} \ No newline at end of file diff --git a/war/root/games/amazonsSuicide_10x10/amazonsSuicide_10x10.kif b/war/root/games/amazonsSuicide_10x10/amazonsSuicide_10x10.kif new file mode 100644 index 0000000..a5395e5 --- /dev/null +++ b/war/root/games/amazonsSuicide_10x10/amazonsSuicide_10x10.kif @@ -0,0 +1,192 @@ +; Amazons Suicide 10x10 (variant) +; +; In this version of Amazons, moving and firing an arrow occur on separate turns. +; This vastly speeds up rule simulation relative to the earlier GDL representation. +; +; As a suicide/misere variant, goal values are the opposite of normal Amazons. + +(role white) +(role black) + +; Bases and inputs + +(base (turn white move)) +(base (turn white fire)) +(base (turn black move)) +(base (turn black fire)) + +(<= (base (cell ?x ?y white)) + (index ?x) + (index ?y)) +(<= (base (cell ?x ?y black)) + (index ?x) + (index ?y)) +(<= (base (cell ?x ?y arrow)) + (index ?x) + (index ?y)) +(<= (base (justMoved ?x ?y)) + (index ?x) + (index ?y)) + +(<= (input ?player noop) + (role ?player)) +(<= (input ?player (move ?x1 ?y1 ?x2 ?y2)) + (role ?player) + (queenMove ?x1 ?y1 ?x2 ?y2)) +(<= (input ?player (fire ?x ?y)) + (role ?player) + (index ?x) + (index ?y)) + +; Initial state + +(init (cell 1 4 white)) +(init (cell 4 1 white)) +(init (cell 7 1 white)) +(init (cell 10 4 white)) +(init (cell 1 7 black)) +(init (cell 4 10 black)) +(init (cell 7 10 black)) +(init (cell 10 7 black)) + +(init (turn white move)) + +; Legal moves + +(<= (legal white noop) + (true (turn black ?any))) +(<= (legal black noop) + (true (turn white ?any))) + +(<= (legal ?player ?move) + (legalMove ?player ?move)) +(<= (legalMove ?player (move ?x1 ?y1 ?x2 ?y2)) + (true (turn ?player move)) + (true (cell ?x1 ?y1 ?player)) + (dir ?dir) + (openPath ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (legalMove ?player (fire ?x2 ?y2)) + (true (turn ?player fire)) + (true (justMoved ?x1 ?y1)) + (dir ?dir) + (openPath ?x1 ?y1 ?x2 ?y2 ?dir)) + +(<= (openPath ?x1 ?y1 ?x2 ?y2 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (not (occupied ?x2 ?y2))) +; Ideal recursive call would probably look like this, but hard for provers to handle right... +;(<= (openPath ?x1 ?y1 ?x3 ?y3 ?dir) +; (openPath ?x1 ?y1 ?x2 ?y2 ?dir) +; (oneInDir ?x2 ?y2 ?x3 ?y3 ?dir) +; (not (occupied ?x3 ?y3))) +; This is in a sense "quadratic", because we also need to compute versions of openPath +; that start with each intermediate coordinate +(<= (openPath ?x1 ?y1 ?x3 ?y3 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (not (occupied ?x2 ?y2)) + (openPath ?x2 ?y2 ?x3 ?y3 ?dir)) + +(<= (occupied ?x ?y) + (true (cell ?x ?y ?any))) + +; Game dynamics + +(<= (next (turn ?player fire)) + (true (turn ?player move))) +(<= (next (turn ?opponent move)) + (true (turn ?player fire)) + (opponent ?player ?opponent)) + +(<= (next (cell ?x2 ?y2 ?player)) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) +(<= (next (cell ?x ?y ?player)) + (true (cell ?x ?y ?player)) + (not (vacated ?x ?y))) +(<= (vacated ?x1 ?y1) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) +(<= (next (justMoved ?x2 ?y2)) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) + +(<= (next (cell ?x ?y arrow)) + (does ?player (fire ?x ?y))) + +; Game ending conditions +(<= terminal + (true (turn ?player ?any)) + (not (anyLegalMove ?player))) +(<= (anyLegalMove ?player) + (legal ?player ?move)) + +(<= (goal ?player 100) + (true (turn ?player ?any))) +(<= (goal ?player 0) + (true (turn ?opponent ?any)) + (opponent ?opponent ?player)) + +; Constants + +(index 1) +(index 2) +(index 3) +(index 4) +(index 5) +(index 6) +(index 7) +(index 8) +(index 9) +(index 10) +(nextIndex 1 2) +(nextIndex 2 3) +(nextIndex 3 4) +(nextIndex 4 5) +(nextIndex 5 6) +(nextIndex 6 7) +(nextIndex 7 8) +(nextIndex 8 9) +(nextIndex 9 10) + +(opponent white black) +(opponent black white) + +(dir n) +(dir ne) +(dir e) +(dir se) +(dir s) +(dir sw) +(dir w) +(dir nw) + +(<= (oneInDir ?x ?y1 ?x ?y2 n) + (index ?x) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x1 ?y1 ?x2 ?y2 ne) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x1 ?y ?x2 ?y e) + (nextIndex ?x1 ?x2) + (index ?y)) +(<= (oneInDir ?x1 ?y2 ?x2 ?y1 se) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x ?y2 ?x ?y1 s) + (index ?x) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x2 ?y2 ?x1 ?y1 sw) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x2 ?y ?x1 ?y w) + (nextIndex ?x1 ?x2) + (index ?y)) +(<= (oneInDir ?x2 ?y1 ?x1 ?y2 nw) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) + +(<= (queenMove ?x1 ?y1 ?x2 ?y2) + (dir ?dir) + (queenMoveDir ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (queenMoveDir ?x1 ?y1 ?x2 ?y2 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (queenMoveDir ?x1 ?y1 ?x3 ?y3 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (queenMoveDir ?x2 ?y2 ?x3 ?y3 ?dir)) diff --git a/war/root/games/amazonsSuicide_10x10/amazonsSuicide_10x10.xsl b/war/root/games/amazonsSuicide_10x10/amazonsSuicide_10x10.xsl new file mode 100644 index 0000000..2180b81 --- /dev/null +++ b/war/root/games/amazonsSuicide_10x10/amazonsSuicide_10x10.xsl @@ -0,0 +1,112 @@ + + + + + +
+ + + + + + + + +
+ + + + + + + + + + + + + + + background-color: #222 + + +
+ + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ + + \ No newline at end of file diff --git a/war/root/games/amazonsTorus_10x10/METADATA b/war/root/games/amazonsTorus_10x10/METADATA new file mode 100644 index 0000000..1b6390f --- /dev/null +++ b/war/root/games/amazonsTorus_10x10/METADATA @@ -0,0 +1,6 @@ +{ + "gameName": "Amazons Torus (10x10)", + + "rulesheet": "amazonsTorus_10x10.kif", + "stylesheet": "amazonsTorus_10x10.xsl" +} \ No newline at end of file diff --git a/war/root/games/amazonsTorus_10x10/amazonsTorus_10x10.kif b/war/root/games/amazonsTorus_10x10/amazonsTorus_10x10.kif new file mode 100644 index 0000000..bdb7de1 --- /dev/null +++ b/war/root/games/amazonsTorus_10x10/amazonsTorus_10x10.kif @@ -0,0 +1,191 @@ +; Amazons 10x10 (variant) +; +; In this version of Amazons, moving and firing an arrow occur on separate turns. +; This vastly speeds up rule simulation relative to the earlier GDL representation. + +(role white) +(role black) + +; Bases and inputs + +(base (turn white move)) +(base (turn white fire)) +(base (turn black move)) +(base (turn black fire)) + +(<= (base (cell ?x ?y white)) + (index ?x) + (index ?y)) +(<= (base (cell ?x ?y black)) + (index ?x) + (index ?y)) +(<= (base (cell ?x ?y arrow)) + (index ?x) + (index ?y)) +(<= (base (justMoved ?x ?y)) + (index ?x) + (index ?y)) + +(<= (input ?player noop) + (role ?player)) +(<= (input ?player (move ?x1 ?y1 ?x2 ?y2)) + (role ?player) + (queenMove ?x1 ?y1 ?x2 ?y2)) +(<= (input ?player (fire ?x ?y)) + (role ?player) + (index ?x) + (index ?y)) + +; Initial state + +(init (cell 1 4 white)) +(init (cell 4 1 white)) +(init (cell 7 1 white)) +(init (cell 10 4 white)) +(init (cell 1 7 black)) +(init (cell 4 10 black)) +(init (cell 7 10 black)) +(init (cell 10 7 black)) + +(init (turn white move)) + +; Legal moves + +(<= (legal white noop) + (true (turn black ?any))) +(<= (legal black noop) + (true (turn white ?any))) + +(<= (legal ?player ?move) + (legalMove ?player ?move)) +(<= (legalMove ?player (move ?x1 ?y1 ?x2 ?y2)) + (true (turn ?player move)) + (true (cell ?x1 ?y1 ?player)) + (dir ?dir) + (openPath ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (legalMove ?player (fire ?x2 ?y2)) + (true (turn ?player fire)) + (true (justMoved ?x1 ?y1)) + (dir ?dir) + (openPath ?x1 ?y1 ?x2 ?y2 ?dir)) + +(<= (openPath ?x1 ?y1 ?x2 ?y2 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (not (occupied ?x2 ?y2))) +; Ideal recursive call would probably look like this, but hard for provers to handle right... +;(<= (openPath ?x1 ?y1 ?x3 ?y3 ?dir) +; (openPath ?x1 ?y1 ?x2 ?y2 ?dir) +; (oneInDir ?x2 ?y2 ?x3 ?y3 ?dir) +; (not (occupied ?x3 ?y3))) +; This is in a sense "quadratic", because we also need to compute versions of openPath +; that start with each intermediate coordinate +(<= (openPath ?x1 ?y1 ?x3 ?y3 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (not (occupied ?x2 ?y2)) + (openPath ?x2 ?y2 ?x3 ?y3 ?dir)) + +(<= (occupied ?x ?y) + (true (cell ?x ?y ?any))) + +; Game dynamics + +(<= (next (turn ?player fire)) + (true (turn ?player move))) +(<= (next (turn ?opponent move)) + (true (turn ?player fire)) + (opponent ?player ?opponent)) + +(<= (next (cell ?x2 ?y2 ?player)) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) +(<= (next (cell ?x ?y ?player)) + (true (cell ?x ?y ?player)) + (not (vacated ?x ?y))) +(<= (vacated ?x1 ?y1) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) +(<= (next (justMoved ?x2 ?y2)) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) + +(<= (next (cell ?x ?y arrow)) + (does ?player (fire ?x ?y))) + +; Game ending conditions +(<= terminal + (true (turn ?player ?any)) + (not (anyLegalMove ?player))) +(<= (anyLegalMove ?player) + (legal ?player ?move)) + +(<= (goal ?player 0) + (true (turn ?player ?any))) +(<= (goal ?player 100) + (true (turn ?opponent ?any)) + (opponent ?opponent ?player)) + +; Constants + +(index 1) +(index 2) +(index 3) +(index 4) +(index 5) +(index 6) +(index 7) +(index 8) +(index 9) +(index 10) +(nextIndex 1 2) +(nextIndex 2 3) +(nextIndex 3 4) +(nextIndex 4 5) +(nextIndex 5 6) +(nextIndex 6 7) +(nextIndex 7 8) +(nextIndex 8 9) +(nextIndex 9 10) +(nextIndex 10 1) + +(opponent white black) +(opponent black white) + +(dir n) +(dir ne) +(dir e) +(dir se) +(dir s) +(dir sw) +(dir w) +(dir nw) + +(<= (oneInDir ?x ?y1 ?x ?y2 n) + (index ?x) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x1 ?y1 ?x2 ?y2 ne) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x1 ?y ?x2 ?y e) + (nextIndex ?x1 ?x2) + (index ?y)) +(<= (oneInDir ?x1 ?y2 ?x2 ?y1 se) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x ?y2 ?x ?y1 s) + (index ?x) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x2 ?y2 ?x1 ?y1 sw) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x2 ?y ?x1 ?y w) + (nextIndex ?x1 ?x2) + (index ?y)) +(<= (oneInDir ?x2 ?y1 ?x1 ?y2 nw) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) + +(<= (queenMove ?x1 ?y1 ?x2 ?y2) + (dir ?dir) + (queenMoveDir ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (queenMoveDir ?x1 ?y1 ?x2 ?y2 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (queenMoveDir ?x1 ?y1 ?x3 ?y3 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (queenMoveDir ?x2 ?y2 ?x3 ?y3 ?dir)) diff --git a/war/root/games/amazonsTorus_10x10/amazonsTorus_10x10.xsl b/war/root/games/amazonsTorus_10x10/amazonsTorus_10x10.xsl new file mode 100644 index 0000000..2180b81 --- /dev/null +++ b/war/root/games/amazonsTorus_10x10/amazonsTorus_10x10.xsl @@ -0,0 +1,112 @@ + + + + + +
+ + + + + + + + +
+ + + + + + + + + + + + + + + background-color: #222 + + +
+ + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ + + \ No newline at end of file diff --git a/war/root/games/amazons_10x10/METADATA b/war/root/games/amazons_10x10/METADATA new file mode 100644 index 0000000..a024800 --- /dev/null +++ b/war/root/games/amazons_10x10/METADATA @@ -0,0 +1,6 @@ +{ + "gameName": "Amazons (10x10)", + + "rulesheet": "amazons_10x10.kif", + "stylesheet": "amazons_10x10.xsl" +} \ No newline at end of file diff --git a/war/root/games/amazons_10x10/amazons_10x10.kif b/war/root/games/amazons_10x10/amazons_10x10.kif new file mode 100644 index 0000000..a2cda3a --- /dev/null +++ b/war/root/games/amazons_10x10/amazons_10x10.kif @@ -0,0 +1,190 @@ +; Amazons 10x10 (variant) +; +; In this version of Amazons, moving and firing an arrow occur on separate turns. +; This vastly speeds up rule simulation relative to the earlier GDL representation. + +(role white) +(role black) + +; Bases and inputs + +(base (turn white move)) +(base (turn white fire)) +(base (turn black move)) +(base (turn black fire)) + +(<= (base (cell ?x ?y white)) + (index ?x) + (index ?y)) +(<= (base (cell ?x ?y black)) + (index ?x) + (index ?y)) +(<= (base (cell ?x ?y arrow)) + (index ?x) + (index ?y)) +(<= (base (justMoved ?x ?y)) + (index ?x) + (index ?y)) + +(<= (input ?player noop) + (role ?player)) +(<= (input ?player (move ?x1 ?y1 ?x2 ?y2)) + (role ?player) + (queenMove ?x1 ?y1 ?x2 ?y2)) +(<= (input ?player (fire ?x ?y)) + (role ?player) + (index ?x) + (index ?y)) + +; Initial state + +(init (cell 1 4 white)) +(init (cell 4 1 white)) +(init (cell 7 1 white)) +(init (cell 10 4 white)) +(init (cell 1 7 black)) +(init (cell 4 10 black)) +(init (cell 7 10 black)) +(init (cell 10 7 black)) + +(init (turn white move)) + +; Legal moves + +(<= (legal white noop) + (true (turn black ?any))) +(<= (legal black noop) + (true (turn white ?any))) + +(<= (legal ?player ?move) + (legalMove ?player ?move)) +(<= (legalMove ?player (move ?x1 ?y1 ?x2 ?y2)) + (true (turn ?player move)) + (true (cell ?x1 ?y1 ?player)) + (dir ?dir) + (openPath ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (legalMove ?player (fire ?x2 ?y2)) + (true (turn ?player fire)) + (true (justMoved ?x1 ?y1)) + (dir ?dir) + (openPath ?x1 ?y1 ?x2 ?y2 ?dir)) + +(<= (openPath ?x1 ?y1 ?x2 ?y2 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (not (occupied ?x2 ?y2))) +; Ideal recursive call would probably look like this, but hard for provers to handle right... +;(<= (openPath ?x1 ?y1 ?x3 ?y3 ?dir) +; (openPath ?x1 ?y1 ?x2 ?y2 ?dir) +; (oneInDir ?x2 ?y2 ?x3 ?y3 ?dir) +; (not (occupied ?x3 ?y3))) +; This is in a sense "quadratic", because we also need to compute versions of openPath +; that start with each intermediate coordinate +(<= (openPath ?x1 ?y1 ?x3 ?y3 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (not (occupied ?x2 ?y2)) + (openPath ?x2 ?y2 ?x3 ?y3 ?dir)) + +(<= (occupied ?x ?y) + (true (cell ?x ?y ?any))) + +; Game dynamics + +(<= (next (turn ?player fire)) + (true (turn ?player move))) +(<= (next (turn ?opponent move)) + (true (turn ?player fire)) + (opponent ?player ?opponent)) + +(<= (next (cell ?x2 ?y2 ?player)) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) +(<= (next (cell ?x ?y ?player)) + (true (cell ?x ?y ?player)) + (not (vacated ?x ?y))) +(<= (vacated ?x1 ?y1) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) +(<= (next (justMoved ?x2 ?y2)) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) + +(<= (next (cell ?x ?y arrow)) + (does ?player (fire ?x ?y))) + +; Game ending conditions +(<= terminal + (true (turn ?player ?any)) + (not (anyLegalMove ?player))) +(<= (anyLegalMove ?player) + (legal ?player ?move)) + +(<= (goal ?player 0) + (true (turn ?player ?any))) +(<= (goal ?player 100) + (true (turn ?opponent ?any)) + (opponent ?opponent ?player)) + +; Constants + +(index 1) +(index 2) +(index 3) +(index 4) +(index 5) +(index 6) +(index 7) +(index 8) +(index 9) +(index 10) +(nextIndex 1 2) +(nextIndex 2 3) +(nextIndex 3 4) +(nextIndex 4 5) +(nextIndex 5 6) +(nextIndex 6 7) +(nextIndex 7 8) +(nextIndex 8 9) +(nextIndex 9 10) + +(opponent white black) +(opponent black white) + +(dir n) +(dir ne) +(dir e) +(dir se) +(dir s) +(dir sw) +(dir w) +(dir nw) + +(<= (oneInDir ?x ?y1 ?x ?y2 n) + (index ?x) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x1 ?y1 ?x2 ?y2 ne) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x1 ?y ?x2 ?y e) + (nextIndex ?x1 ?x2) + (index ?y)) +(<= (oneInDir ?x1 ?y2 ?x2 ?y1 se) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x ?y2 ?x ?y1 s) + (index ?x) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x2 ?y2 ?x1 ?y1 sw) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x2 ?y ?x1 ?y w) + (nextIndex ?x1 ?x2) + (index ?y)) +(<= (oneInDir ?x2 ?y1 ?x1 ?y2 nw) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) + +(<= (queenMove ?x1 ?y1 ?x2 ?y2) + (dir ?dir) + (queenMoveDir ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (queenMoveDir ?x1 ?y1 ?x2 ?y2 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (queenMoveDir ?x1 ?y1 ?x3 ?y3 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (queenMoveDir ?x2 ?y2 ?x3 ?y3 ?dir)) diff --git a/war/root/games/amazons_10x10/amazons_10x10.xsl b/war/root/games/amazons_10x10/amazons_10x10.xsl new file mode 100644 index 0000000..2180b81 --- /dev/null +++ b/war/root/games/amazons_10x10/amazons_10x10.xsl @@ -0,0 +1,112 @@ + + + + + +
+ + + + + + + + +
+ + + + + + + + + + + + + + + background-color: #222 + + +
+ + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ + + \ No newline at end of file diff --git a/war/root/games/amazons_8x8/METADATA b/war/root/games/amazons_8x8/METADATA new file mode 100644 index 0000000..09e73a1 --- /dev/null +++ b/war/root/games/amazons_8x8/METADATA @@ -0,0 +1,6 @@ +{ + "gameName": "Amazons (8x8)", + + "rulesheet": "amazons_8x8.kif", + "stylesheet": "amazons_8x8.xsl" +} \ No newline at end of file diff --git a/war/root/games/amazons_8x8/amazons_8x8.kif b/war/root/games/amazons_8x8/amazons_8x8.kif new file mode 100644 index 0000000..c61a36f --- /dev/null +++ b/war/root/games/amazons_8x8/amazons_8x8.kif @@ -0,0 +1,185 @@ +; Amazons 8x8 +; +; In this version of Amazons, moving and firing an arrow occur on separate turns. + +(role white) +(role black) + +; Bases and inputs + +(base (turn white move)) +(base (turn white fire)) +(base (turn black move)) +(base (turn black fire)) + +(<= (base (cell ?x ?y white)) + (index ?x) + (index ?y)) +(<= (base (cell ?x ?y black)) + (index ?x) + (index ?y)) +(<= (base (cell ?x ?y arrow)) + (index ?x) + (index ?y)) +(<= (base (justMoved ?x ?y)) + (index ?x) + (index ?y)) + +(<= (input ?player noop) + (role ?player)) +(<= (input ?player (move ?x1 ?y1 ?x2 ?y2)) + (role ?player) + (queenMove ?x1 ?y1 ?x2 ?y2)) +(<= (input ?player (fire ?x ?y)) + (role ?player) + (index ?x) + (index ?y)) + +; Initial state + +(init (cell 1 3 white)) +(init (cell 3 1 white)) +(init (cell 6 1 white)) +(init (cell 8 3 white)) +(init (cell 1 6 black)) +(init (cell 3 8 black)) +(init (cell 6 8 black)) +(init (cell 8 6 black)) + +(init (turn white move)) + +; Legal moves + +(<= (legal white noop) + (true (turn black ?any))) +(<= (legal black noop) + (true (turn white ?any))) + +(<= (legal ?player ?move) + (legalMove ?player ?move)) +(<= (legalMove ?player (move ?x1 ?y1 ?x2 ?y2)) + (true (turn ?player move)) + (true (cell ?x1 ?y1 ?player)) + (dir ?dir) + (openPath ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (legalMove ?player (fire ?x2 ?y2)) + (true (turn ?player fire)) + (true (justMoved ?x1 ?y1)) + (dir ?dir) + (openPath ?x1 ?y1 ?x2 ?y2 ?dir)) + +(<= (openPath ?x1 ?y1 ?x2 ?y2 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (not (occupied ?x2 ?y2))) +; Ideal recursive call would probably look like this, but hard for provers to handle right... +;(<= (openPath ?x1 ?y1 ?x3 ?y3 ?dir) +; (openPath ?x1 ?y1 ?x2 ?y2 ?dir) +; (oneInDir ?x2 ?y2 ?x3 ?y3 ?dir) +; (not (occupied ?x3 ?y3))) +; This is in a sense "quadratic", because we also need to compute versions of openPath +; that start with each intermediate coordinate +(<= (openPath ?x1 ?y1 ?x3 ?y3 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (not (occupied ?x2 ?y2)) + (openPath ?x2 ?y2 ?x3 ?y3 ?dir)) + +(<= (occupied ?x ?y) + (true (cell ?x ?y ?any))) + +; Game dynamics + +(<= (next (turn ?player fire)) + (true (turn ?player move))) +(<= (next (turn ?opponent move)) + (true (turn ?player fire)) + (opponent ?player ?opponent)) + +(<= (next (cell ?x2 ?y2 ?player)) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) +(<= (next (cell ?x ?y ?player)) + (true (cell ?x ?y ?player)) + (not (vacated ?x ?y))) +(<= (vacated ?x1 ?y1) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) +(<= (next (justMoved ?x2 ?y2)) + (does ?player (move ?x1 ?y1 ?x2 ?y2))) + +(<= (next (cell ?x ?y arrow)) + (does ?player (fire ?x ?y))) + +; Game ending conditions +(<= terminal + (true (turn ?player ?any)) + (not (anyLegalMove ?player))) +(<= (anyLegalMove ?player) + (legal ?player ?move)) + +(<= (goal ?player 0) + (true (turn ?player ?any))) +(<= (goal ?player 100) + (true (turn ?opponent ?any)) + (opponent ?opponent ?player)) + +; Constants + +(index 1) +(index 2) +(index 3) +(index 4) +(index 5) +(index 6) +(index 7) +(index 8) +(nextIndex 1 2) +(nextIndex 2 3) +(nextIndex 3 4) +(nextIndex 4 5) +(nextIndex 5 6) +(nextIndex 6 7) +(nextIndex 7 8) + +(opponent white black) +(opponent black white) + +(dir n) +(dir ne) +(dir e) +(dir se) +(dir s) +(dir sw) +(dir w) +(dir nw) + +(<= (oneInDir ?x ?y1 ?x ?y2 n) + (index ?x) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x1 ?y1 ?x2 ?y2 ne) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x1 ?y ?x2 ?y e) + (nextIndex ?x1 ?x2) + (index ?y)) +(<= (oneInDir ?x1 ?y2 ?x2 ?y1 se) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x ?y2 ?x ?y1 s) + (index ?x) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x2 ?y2 ?x1 ?y1 sw) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) +(<= (oneInDir ?x2 ?y ?x1 ?y w) + (nextIndex ?x1 ?x2) + (index ?y)) +(<= (oneInDir ?x2 ?y1 ?x1 ?y2 nw) + (nextIndex ?x1 ?x2) + (nextIndex ?y1 ?y2)) + +(<= (queenMove ?x1 ?y1 ?x2 ?y2) + (dir ?dir) + (queenMoveDir ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (queenMoveDir ?x1 ?y1 ?x2 ?y2 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir)) +(<= (queenMoveDir ?x1 ?y1 ?x3 ?y3 ?dir) + (oneInDir ?x1 ?y1 ?x2 ?y2 ?dir) + (queenMoveDir ?x2 ?y2 ?x3 ?y3 ?dir)) diff --git a/war/root/games/amazons_8x8/amazons_8x8.xsl b/war/root/games/amazons_8x8/amazons_8x8.xsl new file mode 100644 index 0000000..5ec0a74 --- /dev/null +++ b/war/root/games/amazons_8x8/amazons_8x8.xsl @@ -0,0 +1,112 @@ + + + + + +
+ + + + + + + + +
+ + + + + + + + + + + + + + + background-color: #222 + + +
+ + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ + + \ No newline at end of file diff --git a/war/root/games/cubicup/cubicup.kif b/war/root/games/cubicup/cubicup.kif index e69a6e3..7c4a05e 100644 --- a/war/root/games/cubicup/cubicup.kif +++ b/war/root/games/cubicup/cubicup.kif @@ -8,34 +8,34 @@ (init (cubes yellow 28)) (init (cubes red 28)) -(init (cube 0 0 0 base)) -(init (cube 1 0 0 base)) -(init (cube 1 1 0 base)) -(init (cube 2 0 0 base)) -(init (cube 2 1 0 base)) -(init (cube 2 2 0 base)) -(init (cube 3 0 0 base)) -(init (cube 3 1 0 base)) -(init (cube 3 2 0 base)) -(init (cube 3 3 0 base)) -(init (cube 4 0 0 base)) -(init (cube 4 1 0 base)) -(init (cube 4 2 0 base)) -(init (cube 4 3 0 base)) -(init (cube 4 4 0 base)) -(init (cube 5 0 0 base)) -(init (cube 5 1 0 base)) -(init (cube 5 2 0 base)) -(init (cube 5 3 0 base)) -(init (cube 5 4 0 base)) -(init (cube 5 5 0 base)) -(init (cube 6 0 0 base)) -(init (cube 6 1 0 base)) -(init (cube 6 2 0 base)) -(init (cube 6 3 0 base)) -(init (cube 6 4 0 base)) -(init (cube 6 5 0 base)) -(init (cube 6 6 0 base)) +(init (cube 0 0 0 ground)) +(init (cube 1 0 0 ground)) +(init (cube 1 1 0 ground)) +(init (cube 2 0 0 ground)) +(init (cube 2 1 0 ground)) +(init (cube 2 2 0 ground)) +(init (cube 3 0 0 ground)) +(init (cube 3 1 0 ground)) +(init (cube 3 2 0 ground)) +(init (cube 3 3 0 ground)) +(init (cube 4 0 0 ground)) +(init (cube 4 1 0 ground)) +(init (cube 4 2 0 ground)) +(init (cube 4 3 0 ground)) +(init (cube 4 4 0 ground)) +(init (cube 5 0 0 ground)) +(init (cube 5 1 0 ground)) +(init (cube 5 2 0 ground)) +(init (cube 5 3 0 ground)) +(init (cube 5 4 0 ground)) +(init (cube 5 5 0 ground)) +(init (cube 6 0 0 ground)) +(init (cube 6 1 0 ground)) +(init (cube 6 2 0 ground)) +(init (cube 6 3 0 ground)) +(init (cube 6 4 0 ground)) +(init (cube 6 5 0 ground)) +(init (cube 6 6 0 ground)) (lastcube 6 6 6) diff --git a/war/root/games/cubicup_3player/cubicup_3player.kif b/war/root/games/cubicup_3player/cubicup_3player.kif index 460c3e1..ccd9cdc 100644 --- a/war/root/games/cubicup_3player/cubicup_3player.kif +++ b/war/root/games/cubicup_3player/cubicup_3player.kif @@ -14,42 +14,42 @@ (init (cubes red 28)) (init (cubes green 28)) -(init (cube 0 0 0 base)) -(init (cube 1 0 0 base)) -(init (cube 1 1 0 base)) -(init (cube 2 0 0 base)) -(init (cube 2 1 0 base)) -(init (cube 2 2 0 base)) -(init (cube 3 0 0 base)) -(init (cube 3 1 0 base)) -(init (cube 3 2 0 base)) -(init (cube 3 3 0 base)) -(init (cube 4 0 0 base)) -(init (cube 4 1 0 base)) -(init (cube 4 2 0 base)) -(init (cube 4 3 0 base)) -(init (cube 4 4 0 base)) -(init (cube 5 0 0 base)) -(init (cube 5 1 0 base)) -(init (cube 5 2 0 base)) -(init (cube 5 3 0 base)) -(init (cube 5 4 0 base)) -(init (cube 5 5 0 base)) -(init (cube 6 0 0 base)) -(init (cube 6 1 0 base)) -(init (cube 6 2 0 base)) -(init (cube 6 3 0 base)) -(init (cube 6 4 0 base)) -(init (cube 6 5 0 base)) -(init (cube 6 6 0 base)) -(init (cube 7 0 0 base)) -(init (cube 7 1 0 base)) -(init (cube 7 2 0 base)) -(init (cube 7 3 0 base)) -(init (cube 7 4 0 base)) -(init (cube 7 5 0 base)) -(init (cube 7 6 0 base)) -(init (cube 7 7 0 base)) +(init (cube 0 0 0 ground)) +(init (cube 1 0 0 ground)) +(init (cube 1 1 0 ground)) +(init (cube 2 0 0 ground)) +(init (cube 2 1 0 ground)) +(init (cube 2 2 0 ground)) +(init (cube 3 0 0 ground)) +(init (cube 3 1 0 ground)) +(init (cube 3 2 0 ground)) +(init (cube 3 3 0 ground)) +(init (cube 4 0 0 ground)) +(init (cube 4 1 0 ground)) +(init (cube 4 2 0 ground)) +(init (cube 4 3 0 ground)) +(init (cube 4 4 0 ground)) +(init (cube 5 0 0 ground)) +(init (cube 5 1 0 ground)) +(init (cube 5 2 0 ground)) +(init (cube 5 3 0 ground)) +(init (cube 5 4 0 ground)) +(init (cube 5 5 0 ground)) +(init (cube 6 0 0 ground)) +(init (cube 6 1 0 ground)) +(init (cube 6 2 0 ground)) +(init (cube 6 3 0 ground)) +(init (cube 6 4 0 ground)) +(init (cube 6 5 0 ground)) +(init (cube 6 6 0 ground)) +(init (cube 7 0 0 ground)) +(init (cube 7 1 0 ground)) +(init (cube 7 2 0 ground)) +(init (cube 7 3 0 ground)) +(init (cube 7 4 0 ground)) +(init (cube 7 5 0 ground)) +(init (cube 7 6 0 ground)) +(init (cube 7 7 0 ground)) (lastcube 7 7 7)