coordinate based report added

diff --git a/report1/alex.tex b/report1/alex.tex
index 802992c..25e7bcd 100644 (file)
--- a/report1/alex.tex
+++ b/report1/alex.tex
@@ -1 +1,84 @@
-Hello world
+\section{Coordinate based approach}
+Let $T = \{\_,@,.,\#,\$,*,+\}$. We model a sokoban field as a set $F = \{x_{i,j} | x_{i,j} \in T, \forall i,j \ni x_{i,j} \neq \perp \}$.\\
+We introduce a variable $m \in \{\text{up}, \text{down}, \text{left}, \text{right}\}$ which is picked up non-deterministically for each next step. The value of $m$ denotes the intended direction of movement of the actor. The values $x_{i,j} \in F$ are updated each step according the values of $m$ and the rules described in the subsection.
+\subsection{Changing the state}
+Let\\
+$\delta_{x}(x,m) =
+  \begin{cases}
+    (x+1) & \quad \text{if } m = left\\
+    (x-1) & \quad \text{if } m = right\\
+    x & \quad \text{otherwise}
+  \end{cases}$\quad
+$\delta'_{x}(x,m) =
+  \begin{cases}
+    (x-1) & \quad \text{if } m = left\\
+    (x+1) & \quad \text{if } m = right\\
+    x & \quad \text{otherwise}
+  \end{cases}$\\
+$\delta_{y}(y,m) =
+  \begin{cases}
+    (y+1) & \quad \text{if } m = up\\
+    (y-1) & \quad \text{if } m = down\\
+    y & \quad \text{otherwise}
+  \end{cases}$\quad
+$\delta'_{y}(y,m) =
+  \begin{cases}
+    (y-1) & \quad \text{if } m = up\\
+    (y+1) & \quad \text{if } m = down\\
+    y & \quad \text{otherwise}
+  \end{cases}$\\
+  $\gamma_{x}(x,m) =
+    \begin{cases}
+      (x+2) & \quad \text{if } m = left\\
+      (x-2) & \quad \text{if } m = right\\
+      x & \quad \text{otherwise}
+    \end{cases}$\quad
+  $\gamma_{y}(y,m) =
+    \begin{cases}
+      (y+2) & \quad \text{if } m = up\\
+      (y-2) & \quad \text{if } m = down\\
+      y & \quad \text{otherwise}
+    \end{cases}$
+
+%    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Agent | x"
+%                            <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left: AgentOnTarget;",
+%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
+%                            <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_"
+%                            <+ (checkY p (x-1) y) <+ " = Target) & move = Up: AgentOnTarget;",
+%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
+%                            <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Free | x" <+ x <+ "_" <+ (checkY p x  (y+1)) <+ " = Target) & move = Right : AgentOnTarget;",
+%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
+%                            <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_"
+%                            <+ (checkY p (x+1) y) <+ " = Target) & move = Down : AgentOnTarget;",
+
+
+
+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 = *)$$