From: Alexander Fedotov Date: Mon, 14 Mar 2016 13:49:28 +0000 (+0100) Subject: coordinate based report added X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=d002324ed1426eb44114b851daedf27e0025f0b2;p=mc1516pa.git coordinate based report added --- diff --git a/report1/alex.tex b/report1/alex.tex index 802992c..25e7bcd 100644 --- 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 = *)$$