From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 19 Apr 2016 13:14:04 +0000 (+0200)
Subject: started with transitions in formal documentg
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=d8496404fca14bd5f221987df167930f482c622b;p=mc1516pa.git

started with transitions in formal documentg
---

diff --git a/report2/implementation.tex b/report2/implementation.tex
index 9657891..32a5bd7 100644
--- a/report2/implementation.tex
+++ b/report2/implementation.tex
@@ -6,11 +6,11 @@ spaces are removed.
 Let $T=\{free,box,target,agent,targetagent,targetbox\}$ be the set of possible
 states of a tile. Tiles are numbered and thus a sokoban screen is the set $F$
 containing a $x_i\in T$ for every tile. We introduce a function $ord(x, y)$
-that returns the tile number for a given $x$ and $y$ coordinate. To encode the
+that returns the tile number for a given $x$ and $y$ coordinate and a function
+$iord(i)$ that does the reverse. To encode the
 state we introduce an encoding function that encodes a state in three boolean
 variables:
 $$encode(t)=\begin{cases}
-	000 & \text{if }t=wall\\
 	001 & \text{if }t=free\\
 	010 & \text{if }t=box\\
 	011 & \text{if }t=target\\
@@ -26,8 +26,7 @@ We introduce a variable denoting the intended direction of movement $m \in
 \{\text{up}, \text{down}, \text{left}, \text{right}\}$. Per move we define a
 $\delta$ and $\gamma$ variable which represent the change in coordinate value
 respectively for the next position and the position next to the next postition.
-\\
-$\delta_{(x,y)}(m)=\begin{cases}
+$$\delta_{(x,y)}(m)=\begin{cases}
 	(x-1, y) & \text{if } m = left\\
 	(x+1, y) & \text{if } m = right\\
 	(x, y+1) & \text{if } m = down\\
@@ -38,34 +37,16 @@ $\delta_{(x,y)}(m)=\begin{cases}
 	(x+2, y) & \text{if } m = right\\
 	(x, y+2) & \text{if } m = down\\
 	(x, y-2) & \text{if } m = up\\
-\end{cases} $
+\end{cases}$$
 
-%We define the tile update function $next(x_{i,j}), x_{i,j} \in F, \forall i,j \text{ s.t.} x_{i,j} \neq \perp$ as\\
-%$
-%next(x_{i,j}) =
-%  \begin{cases}
-%    \# & \quad \text{if } x_{i,j} = \#\\
-%    @ & \quad \text{if } x_{i,j} = \_ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp\\
-%    @ & \quad \text{if } x_{i,j} = \$ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +)\\
-%    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
-%    & \quad \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} \neq \perp\\
-%    \$ & \quad \text{if } x_{i,j} = \_ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *)\\ & \quad \wedge (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = @ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = +) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
-%    \_ & \quad \text{if } x_{i,j} = @ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \_ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = .)\\
-%    & \quad \vee ((x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *) \wedge \\
-%    & \quad (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = \_ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = .)) \\
-%    & \quad x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
-%    + & \quad x_{i,j} = . \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp\\
-%    + & \quad x_{i,j} = * \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +)\\
-%    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
-%    & \quad \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} \neq \perp\\
-%    * & \quad \text{if } x_{i,j} = . \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *)\\
-%    & \quad \wedge (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = @ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = +)\\
-%    & \quad \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
-%    . & \quad x_{i,j} = + \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \_ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = .) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp\\
-%    x_{i,j} & \quad \text{otherwise}\\
-%  \end{cases}
-%$
-%\subsection{Goal}
-%Let $G = \{z_{i,j} | z_{i,j} \in F, \forall i,j \text{ s.t.} z_{i,j} \in \{.,*\}\}$ be a subset of $F$.
-%In order to check a sokoban field for a possible solution, we introduce the following invariant:\\
-%$$\neg \bigwedge_{x \in G} (x = *)$$
+We define the tile update function $next(i)$ for $i \in F$.
+$$next(i)=\left\{\begin{array}{lll}
+	free & \text{if } & i=agent \wedge \delta(i)=free\\
+		& \vee & i = agent \wedge \delta(i)=target\\
+	target & \text{if } & i=targetagent \wedge \delta(i)=free\\
+		& \vee & i = targetagent \wedge \delta(i)=target\\
+	agent & \text{if } & i=free \wedge \delta(i)=agent\\
+		& \vee & i = free \wedge \delta(i)=targetagent\\
+	targetagent & \text{if } & i=target \wedge \delta(i)=agent\\
+		& \vee & i = target \wedge \delta(i)=targetagent\\
+\end{array}\right.$$