[Toss-devel-svn] SF.net SVN: toss:[1450] trunk/Toss/www/reference/reference.tex

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

Revision: 1450
          http://toss.svn.sourceforge.net/toss/?rev=1450&view=rev
Author:   lukstafi
Date:     2011-05-21 22:28:01 +0000 (Sat, 21 May 2011)

Log Message:
-----------
Reference specification of GDL translation: minor correction.

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

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-05-21 14:32:28 UTC (rev 1449)
+++ trunk/Toss/www/reference/reference.tex	2011-05-21 22:28:01 UTC (rev 1450)
@@ -1315,15 +1315,13 @@
 of all GDL state terms which are true at some game state reachable
 from the initial state of $G$.
 
-For us, it is enough to approximate $\calS$ from above. To approximate $\calS$
-and determine the location structure of the Toss game, we currently perform
-an \emph{aggregate playout}, \ie a symbolic play in where all players take
-all their legal moves in a state. Since an approximation is sufficient,
-we check only the positive part of the legality condition of each move.
+For us, it is enough to approximate $\calS$ from above. To approximate
+$\calS$, we currently perform an \emph{aggregate playout}, \ie a
+symbolic play in where all players take all their legal moves in a
+state. Since an approximation is sufficient, we check only the
+positive part of the legality condition of each move.
 
-%The \emph{noop move} of a player in a
-%location is the only move available to her, determining them gives the
-%player of a turn. In the future, instead of an aggregate playout we
+%In the future, instead of an aggregate playout we
 %might use a form of type inference to approximate $\calS$.
 
 To construct the elements of the structure from state terms, 
@@ -1886,8 +1884,7 @@
 equality relations $Eq_{p,q}$.
 
 The result of translation is the disjunction of translations of each
-$\Phi_i$. Let $\mathtt{BL}(t)$
-be the term $t$ with fluent paths replaced with \texttt{BLANK}. A single $\Phi_i = G_i \wedge ST^{+}_i \wedge ST^{-}_i$
+$\Phi_i$. Let $\mathtt{BL}(t)=t\big[\calP_f \ot \mathtt{BLANK}\big]$. A single $\Phi_i = G_i \wedge ST^{+}_i \wedge ST^{-}_i$
 is translated as:
 
 \begin{align*}
@@ -1947,7 +1944,7 @@
 \ldots, \mathtt{(<= (R \ t^k_1 \ldots t^k_n) \ b_k)}$. For $i$th
 argument of $R$ ($i \in \{1,\ldots,n\}$) we will find
 $\mathtt{ArgType}(R,i)$ with possible values
-$(\mathtt{DefSide},\calS_i,p_i)$ and $(\mathtt{CallSide},\calS_i,p_i)$, with a mapping $\calS_i$ into state terms
+$(\mathtt{DefSide},\calS_i,p_i)$ and $(\mathtt{CallSide},p_i)$, with a mapping $\calS_i$ into state terms
 corresponding to the argument in a given context and a path $p_i \in
 \calP_m$ corresponding to the subterm position selected to
 ``transfer'' the argument.


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