[Toss-devel-svn] SF.net SVN: toss:[1456] trunk/Toss

[<luk...@us...>]

Revision: 1456
          http://toss.svn.sourceforge.net/toss/?rev=1456&view=rev
Author:   lukstafi
Date:     2011-05-23 12:02:27 +0000 (Mon, 23 May 2011)

Log Message:
-----------
Reference specification of GDL translation: {Concurrent Moves and Toss Locations} complete draft, work in progress.

Modified Paths:
--------------
    trunk/Toss/www/reference/reference.tex

Added Paths:
-----------
    trunk/Toss/GGP/examples/pacman3p.gdl

Added: trunk/Toss/GGP/examples/pacman3p.gdl
===================================================================
--- trunk/Toss/GGP/examples/pacman3p.gdl	                        (rev 0)
+++ trunk/Toss/GGP/examples/pacman3p.gdl	2011-05-23 12:02:27 UTC (rev 1456)
@@ -0,0 +1,456 @@
+; pacman3p
+(role pacman)
+(role blinky)
+(role inky)
+(init (control pacman))
+(init (location pacman 5 3))
+(init (location blinky 4 6))
+(init (location inky 5 6))
+(init (location pellet 3 1))
+(init (location pellet 4 1))
+(init (location pellet 5 1))
+(init (location pellet 6 1))
+(init (location pellet 3 2))
+(init (location pellet 6 2))
+(init (location pellet 1 3))
+(init (location pellet 2 3))
+(init (location pellet 3 3))
+(init (location pellet 4 3))
+(init (location pellet 6 3))
+(init (location pellet 7 3))
+(init (location pellet 8 3))
+(init (location pellet 1 4))
+(init (location pellet 3 4))
+(init (location pellet 6 4))
+(init (location pellet 8 4))
+(init (location pellet 1 5))
+(init (location pellet 3 5))
+(init (location pellet 6 5))
+(init (location pellet 8 5))
+(init (location pellet 1 6))
+(init (location pellet 2 6))
+(init (location pellet 3 6))
+(init (location pellet 6 6))
+(init (location pellet 7 6))
+(init (location pellet 8 6))
+(init (location pellet 3 7))
+(init (location pellet 6 7))
+(init (location pellet 3 8))
+(init (location pellet 4 8))
+(init (location pellet 5 8))
+(init (location pellet 6 8))
+(init (blockednorth 4 1))
+(init (blockednorth 5 1))
+(init (blockednorth 1 2))
+(init (blockednorth 2 2))
+(init (blockednorth 4 2))
+(init (blockednorth 5 2))
+(init (blockednorth 7 2))
+(init (blockednorth 8 2))
+(init (blockednorth 2 3))
+(init (blockednorth 4 3))
+(init (blockednorth 5 3))
+(init (blockednorth 7 3))
+(init (blockednorth 2 5))
+(init (blockednorth 4 5))
+(init (blockednorth 5 5))
+(init (blockednorth 7 5))
+(init (blockednorth 1 6))
+(init (blockednorth 2 6))
+(init (blockednorth 4 6))
+(init (blockednorth 5 6))
+(init (blockednorth 7 6))
+(init (blockednorth 8 6))
+(init (blockednorth 4 7))
+(init (blockednorth 5 7))
+(init (blockedeast 1 4))
+(init (blockedeast 1 5))
+(init (blockedeast 2 1))
+(init (blockedeast 2 2))
+(init (blockedeast 2 4))
+(init (blockedeast 2 5))
+(init (blockedeast 2 7))
+(init (blockedeast 2 8))
+(init (blockedeast 3 2))
+(init (blockedeast 3 4))
+(init (blockedeast 3 5))
+(init (blockedeast 3 7))
+(init (blockedeast 5 2))
+(init (blockedeast 5 4))
+(init (blockedeast 5 5))
+(init (blockedeast 5 7))
+(init (blockedeast 6 1))
+(init (blockedeast 6 2))
+(init (blockedeast 6 4))
+(init (blockedeast 6 5))
+(init (blockedeast 6 7))
+(init (blockedeast 6 8))
+(init (blockedeast 7 4))
+(init (blockedeast 7 5))
+(init (collected 0))
+(init (step 1))
+(<= (legal pacman (move ?dir))
+    (true (control pacman))
+    (true (location pacman ?x ?y))
+    (legalstep ?dir ?x ?y)
+    (distinct ?dir nowhere))
+(<= (legal pacman (move nowhere))
+    (not (true (control pacman))))
+(<= (legal ?ghost (move ?dir))
+    (ghost ?ghost)
+    (true (control ghosts))
+    (true (location ?ghost ?x ?y))
+    (legalstep ?dir ?x ?y)
+    (distinct ?dir nowhere))
+(<= (legal ?ghost (move nowhere))
+    (ghost ?ghost)
+    (not (true (control ghosts))))
+(<= (next (control pacman))
+    (true (control ghosts)))
+(<= (next (control ghosts))
+    (true (control pacman)))
+(<= (next (location pellet ?xp ?yp))
+    (true (location pellet ?xp ?yp))
+    (true (location pacman ?xpm1 ?ypm1))
+    (does pacman (move ?dir))
+    (nextcell ?dir ?xpm1 ?ypm1 ?xpm2 ?ypm2)
+    (distinctcell ?xp ?yp ?xpm2 ?ypm2))
+(<= (next (collected ?n++))
+    (true (location pacman ?x1 ?y1))
+    (does pacman (move ?dir))
+    (nextcell ?dir ?x1 ?y1 ?x2 ?y2)
+    (true (location pellet ?x2 ?y2))
+    (true (collected ?n))
+    (succ ?n ?n++))
+(<= (next (collected ?n))
+    (true (location pacman ?x1 ?y1))
+    (does pacman (move ?dir))
+    (nextcell ?dir ?x1 ?y1 ?x2 ?y2)
+    (not (true (location pellet ?x2 ?y2)))
+    (true (collected ?n)))
+(<= (next (blockednorth ?x ?y))
+    (true (blockednorth ?x ?y)))
+(<= (next (blockedeast ?x ?y))
+    (true (blockedeast ?x ?y)))
+(<= (next (location ?char ?x2 ?y2))
+    (movable ?char)
+    (true (location ?char ?x1 ?y1))
+    (does ?char (move ?dir))
+    (nextcell ?dir ?x1 ?y1 ?x2 ?y2))
+(<= (next (step ?n++))
+    (true (step ?n))
+    (succ ?n ?n++))
+(<= terminal
+    captured)
+(<= terminal
+    nopellets)
+(<= terminal
+    timeout)
+(<= (goal pacman ?g)
+    (true (collected ?n))
+    (scoremap ?n ?g))
+(<= (goal blinky 0)
+    (true (location pacman ?xp ?yp))
+    (true (location blinky ?xb ?yb))
+    (distinctcell ?xp ?yp ?xb ?yb))
+(<= (goal blinky 100)
+    (true (location pacman ?x ?y))
+    (true (location blinky ?x ?y)))
+(<= (goal inky 0)
+    (true (location pacman ?xp ?yp))
+    (true (location inky ?xi ?yi))
+    (distinctcell ?xp ?yp ?xi ?yi))
+(<= (goal inky 100)
+    (true (location pacman ?x ?y))
+    (true (location inky ?x ?y)))
+(<= (legalstep north ?x ?y)
+    (++ ?y ?ynew)
+    (cell ?x ?ynew)
+    (not (blocked ?x ?y ?x ?ynew)))
+(<= (legalstep south ?x ?y)
+    (-- ?y ?ynew)
+    (cell ?x ?ynew)
+    (not (blocked ?x ?y ?x ?ynew)))
+(<= (legalstep east ?x ?y)
+    (++ ?x ?xnew)
+    (cell ?xnew ?y)
+    (not (blocked ?x ?y ?xnew ?y)))
+(<= (legalstep west ?x ?y)
+    (-- ?x ?xnew)
+    (cell ?xnew ?y)
+    (not (blocked ?x ?y ?xnew ?y)))
+(<= (legalstep nowhere ?x ?y)
+    (cell ?x ?y))
+(<= (nextcell north ?x ?y ?x ?ynew)
+    (index ?x)
+    (++ ?y ?ynew))
+(<= (nextcell south ?x ?y ?x ?ynew)
+    (index ?x)
+    (-- ?y ?ynew))
+(<= (nextcell east ?x ?y ?xnew ?y)
+    (index ?y)
+    (++ ?x ?xnew))
+(<= (nextcell west ?x ?y ?xnew ?y)
+    (index ?y)
+    (-- ?x ?xnew))
+(<= (nextcell nowhere ?x ?y ?x ?y)
+    (cell ?x ?y))
+(<= (blocked ?x ?y1 ?x ?y2)
+    (true (blockednorth ?x ?y1))
+    (++ ?y1 ?y2))
+(<= (blocked ?x ?y2 ?x ?y1)
+    (true (blockednorth ?x ?y1))
+    (++ ?y1 ?y2))
+(<= (blocked ?x1 ?y ?x2 ?y)
+    (true (blockedeast ?x1 ?y))
+    (++ ?x1 ?x2))
+(<= (blocked ?x2 ?y ?x1 ?y)
+    (true (blockedeast ?x1 ?y))
+    (++ ?x1 ?x2))
+(<= (distinctcell ?x1 ?y1 ?x2 ?y2)
+    (cell ?x1 ?y1)
+    (cell ?x2 ?y2)
+    (distinct ?x1 ?x2))
+(<= (distinctcell ?x1 ?y1 ?x2 ?y2)
+    (cell ?x1 ?y1)
+    (cell ?x2 ?y2)
+    (distinct ?y1 ?y2))
+(<= captured
+    (true (location pacman ?x ?y))
+    (true (location blinky ?x ?y)))
+(<= captured
+    (true (location pacman ?x ?y))
+    (true (location inky ?x ?y)))
+(<= nopellets
+    (true (collected 35)))
+(<= timeout
+    (true (step 100)))
+(movable pacman)
+(movable blinky)
+(movable inky)
+(ghost blinky)
+(ghost inky)
+(index 1)
+(index 2)
+(index 3)
+(index 4)
+(index 5)
+(index 6)
+(index 7)
+(index 8)
+(cell 1 8)
+(cell 2 8)
+(cell 3 8)
+(cell 4 8)
+(cell 5 8)
+(cell 6 8)
+(cell 7 8)
+(cell 8 8)
+(cell 1 7)
+(cell 2 7)
+(cell 3 7)
+(cell 4 7)
+(cell 5 7)
+(cell 6 7)
+(cell 7 7)
+(cell 8 7)
+(cell 1 6)
+(cell 2 6)
+(cell 3 6)
+(cell 4 6)
+(cell 5 6)
+(cell 6 6)
+(cell 7 6)
+(cell 8 6)
+(cell 1 5)
+(cell 2 5)
+(cell 3 5)
+(cell 4 5)
+(cell 5 5)
+(cell 6 5)
+(cell 7 5)
+(cell 8 5)
+(cell 1 4)
+(cell 2 4)
+(cell 3 4)
+(cell 4 4)
+(cell 5 4)
+(cell 6 4)
+(cell 7 4)
+(cell 8 4)
+(cell 1 3)
+(cell 2 3)
+(cell 3 3)
+(cell 4 3)
+(cell 5 3)
+(cell 6 3)
+(cell 7 3)
+(cell 8 3)
+(cell 1 2)
+(cell 2 2)
+(cell 3 2)
+(cell 4 2)
+(cell 5 2)
+(cell 6 2)
+(cell 7 2)
+(cell 8 2)
+(cell 1 1)
+(cell 2 1)
+(cell 3 1)
+(cell 4 1)
+(cell 5 1)
+(cell 6 1)
+(cell 7 1)
+(cell 8 1)
+(++ 1 2)
+(++ 2 3)
+(++ 3 4)
+(++ 4 5)
+(++ 5 6)
+(++ 6 7)
+(++ 7 8)
+(-- 8 7)
+(-- 7 6)
+(-- 6 5)
+(-- 5 4)
+(-- 4 3)
+(-- 3 2)
+(-- 2 1)
+(succ 0 1)
+(succ 1 2)
+(succ 2 3)
+(succ 3 4)
+(succ 4 5)
+(succ 5 6)
+(succ 6 7)
+(succ 7 8)
+(succ 8 9)
+(succ 9 10)
+(succ 10 11)
+(succ 11 12)
+(succ 12 13)
+(succ 13 14)
+(succ 14 15)
+(succ 15 16)
+(succ 16 17)
+(succ 17 18)
+(succ 18 19)
+(succ 19 20)
+(succ 20 21)
+(succ 21 22)
+(succ 22 23)
+(succ 23 24)
+(succ 24 25)
+(succ 25 26)
+(succ 26 27)
+(succ 27 28)
+(succ 28 29)
+(succ 29 30)
+(succ 30 31)
+(succ 31 32)
+(succ 32 33)
+(succ 33 34)
+(succ 34 35)
+(succ 35 36)
+(succ 36 37)
+(succ 37 38)
+(succ 38 39)
+(succ 39 40)
+(succ 40 41)
+(succ 41 42)
+(succ 42 43)
+(succ 43 44)
+(succ 44 45)
+(succ 45 46)
+(succ 46 47)
+(succ 47 48)
+(succ 48 49)
+(succ 49 50)
+(succ 50 51)
+(succ 51 52)
+(succ 52 53)
+(succ 53 54)
+(succ 54 55)
+(succ 55 56)
+(succ 56 57)
+(succ 57 58)
+(succ 58 59)
+(succ 59 60)
+(succ 60 61)
+(succ 61 62)
+(succ 62 63)
+(succ 63 64)
+(succ 64 65)
+(succ 65 66)
+(succ 66 67)
+(succ 67 68)
+(succ 68 69)
+(succ 69 70)
+(succ 70 71)
+(succ 71 72)
+(succ 72 73)
+(succ 73 74)
+(succ 74 75)
+(succ 75 76)
+(succ 76 77)
+(succ 77 78)
+(succ 78 79)
+(succ 79 80)
+(succ 80 81)
+(succ 81 82)
+(succ 82 83)
+(succ 83 84)
+(succ 84 85)
+(succ 85 86)
+(succ 86 87)
+(succ 87 88)
+(succ 88 89)
+(succ 89 90)
+(succ 90 91)
+(succ 91 92)
+(succ 92 93)
+(succ 93 94)
+(succ 94 95)
+(succ 95 96)
+(succ 96 97)
+(succ 97 98)
+(succ 98 99)
+(succ 99 100)
+(scoremap 0 0)
+(scoremap 1 2)
+(scoremap 2 4)
+(scoremap 3 6)
+(scoremap 4 8)
+(scoremap 5 10)
+(scoremap 6 12)
+(scoremap 7 14)
+(scoremap 8 16)
+(scoremap 9 18)
+(scoremap 10 20)
+(scoremap 11 23)
+(scoremap 12 26)
+(scoremap 13 29)
+(scoremap 14 32)
+(scoremap 15 35)
+(scoremap 16 38)
+(scoremap 17 41)
+(scoremap 18 44)
+(scoremap 19 47)
+(scoremap 20 50)
+(scoremap 21 53)
+(scoremap 22 56)
+(scoremap 23 59)
+(scoremap 24 62)
+(scoremap 25 65)
+(scoremap 26 68)
+(scoremap 27 71)
+(scoremap 28 74)
+(scoremap 29 77)
+(scoremap 30 80)
+(scoremap 31 83)
+(scoremap 32 86)
+(scoremap 33 89)
+(scoremap 34 95)
+(scoremap 35 100)
+
+

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-05-23 01:32:57 UTC (rev 1455)
+++ trunk/Toss/www/reference/reference.tex	2011-05-23 12:02:27 UTC (rev 1456)
@@ -1772,8 +1772,11 @@
 
 For each suitable tuple $\ol{\calC}, \ol{\calN}$ we have now created
 the unifier $\sigma_{\ol{\calC}, \ol{\calN}}$ and computed the erasure
-clauses $\calE_{\ol{\calC}, \ol{\calN}}$. To create the rules, we need
-to further partition the \emph{rule clauses} $\sigma_{\ol{\calC},
+clauses $\calE_{\ol{\calC}, \ol{\calN}}$. At this point, clauses
+$\ol{\calC}, \ol{\calN}$ are optionally divided according to the
+player of the \texttt{does} relation atom in them, see
+Section~\ref{subsec-concurrency}. To create the rules, we need to
+further partition the \emph{rule clauses} $\sigma_{\ol{\calC},
   \ol{\calN}}(\calC_i), \sigma_{\ol{\calC}, \ol{\calN}}(\calN_i)$ and
 $\calE_{\ol{\calC}, \ol{\calN}}$, and augment them with further
 conditions. The reason is that the prepared rule clauses may have
@@ -1816,12 +1819,10 @@
 are extracted to be relations tuples in $\frakL$.
 
 Having constructed and filtered the rewriting rule candidates, we have
-almost completed the definition of $T(G)$. The rules are assigned to
-locations based on who moves in which location, as we only translate
-turn-based games for now. Payoff formulas are derived by instantiating
-variables standing for the \texttt{goal} values. The formulas defining
-the \texttt{terminal} condition and specific \texttt{goal} value
-conditions are translated as described in
+almost completed the definition of $T(G)$. Payoff formulas are derived
+by instantiating variables standing for the \texttt{goal} values. The
+formulas defining the \texttt{terminal} condition and specific
+\texttt{goal} value conditions are translated as described in
 Section~\ref{subsec-translate}, from disjunctions of bodies of their
 respective clauses. Actually, instead of ``freshening'' the clauses
 and translating the disjunction of their bodies, we (equivalently)
@@ -1843,6 +1844,13 @@
 a game state term $t$ such that $t\tpos_p = v$, and the incoming move
 has term $s$ at path $q$, then we add $Anch^s_p(x)$ to the precondition.
 
+It is actually possible, that there is more than a single rule and/or
+multiple embeddings; the semantics of the original GDL game
+specification demands that all rules should be applied over all their
+non-overlapping embeddings. For the most part we do not worry about
+such exceptional situations, but we handle one natural case in
+Paragraph~\ref{par-concurrent-moves}.
+
 To translate the outgoing move, we recall the heads of the
 \texttt{legal} clauses of the rule that is selected, as we only need to
 substitute all their variables. To eliminate a variable $v$ contained in
@@ -1851,6 +1859,51 @@
 such that $t\tpos_p = v$, and $a\tpos^m_p = s$, then we substitute
 $v$ by $s$. The move translation function $\mu$ is thus constructed.
 
+\subsubsection{Concurrent Moves and Toss Locations} \label{subsec-concurrency}
+
+In Section~\ref{subsec-rules}, we described the creation of
+state-transition rewrite rules, \ie where a single Toss rule is
+responsible for the transition to the next game state. But we also
+remarked that the rule clauses can be divided by players to whose
+actions they refer (by the \texttt{does} relation). In this case the
+game state transition is jointly described by several Toss rules that
+apply independently, each rule ``enacted'' by a player; such is the
+default way of defining simultaneous moves in Toss. We now elaborate
+on three modes of building the game graph in the translated game.
+
+\paragraph{Turn-based Games} are games where in any game state there
+is at most a single player having genuine choice. Rather than
+attempting a complex analysis to detect as many turn-based games as
+possible, we recognize some cases where in all states, all players but
+one have a single legal move that is a constant (term of size
+one). Such move is conventionally called \texttt{noop}. We simply
+check what moves are available to players in the states of the
+aggregate playout. Due to the character of aggregate playout, we only
+handle the case where the alternation of control forms a cycle
+(players do not need to strictly alternate, for example a
+single-player game is also a turn-based game, as another example in a
+three-player game the first player may intersperse the moves of second
+and third player). We build a corresponding cyclic graph of Toss
+locations.
+
+\paragraph{Concurrent Moves Games} \label{par-concurrent-moves} When
+translation as a turn-based game fails, but all rule clauses have at
+most one atom of \texttt{does} relation, we divide the clauses among
+players as mentioned earlier. For the clauses wihout \texttt{does}
+atoms, a new player, ``environment'', is created. We designate the
+``environment'' player to have all its matching rules applied, over
+all embeddings, at each state transition. We translate using a
+single-location game graph. (TODO: less terse descr)
+
+\paragraph{General Interaction Games} When some rule clause has
+multiple \texttt{does} relations, we cannot use straightforward
+translation of the previous paragraph. Instead, we translate into a
+two-location graph, where game players declare their moves in one
+location, and the (now obligatory) ``environment'' player carries out
+state changes in the other location. In effect, large parts of the
+translation function $\mu$ are built into the game. (TODO: will
+specify soon)
+
 \subsection{Translating Formulas} \label{subsec-translate}
 
 First we describe translation in the case all GDL relations other than


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.