report1/mart.tex

   1 \section{Object centered approach}
   2 We define:
   3 All boxes $B=\{b^0, b^1, \ldots, b^k\}$ and all targets $T=\{t^0, t^1, \ldots,
   4 t^k\}$.
   5 \subsection{Objects}
   6 We define the set $lex$ as being the set containing all legal $x$ values and
   7 the function $ley(x)$ that for a given $x$ returns the set of all legal $y$
   8 values for that $x$.
   9
  10 To reduce size of the encoding we introduce a module called \texttt{ob}
  11 representing an object in the screen. The module contains two integer variables
  12 $x$ and $y$ that contains the position of the object in the field. The $x$ and
  13 $y$ values are bounded by the level size through their domain and restricted to
  14 the non-wall positions with the following invariant:
  15 $$\bigvee_{i\in lex}\left(x=i\wedge\bigvee_{j\in ley(x)}y=j\right)$$
  16
  17 The initial values are determined by the values passed to it in the
  18 \texttt{main} module.
  19
  20 In the \texttt{main} module we define for all boxes and the agent such an
  21 \texttt{ob} that stores the position of that object in that particular state.
  22
  23 \subsection{Movement}
  24 We define a variable $movement=\{left,up,right,down,finished\}$ which describes
  25 the move in that state. From the movement variable new positions of objects are
  26 calculated using delta variables.
  27 $$\Delta_x=\left\{\begin{array}{ll}
  28         -1 & movement=left\\
  29         1 & movement=right\\
  30         0 & \text{otherwise}
  31 \end{array}\right.
  32 \Delta_y=\left\{\begin{array}{ll}
  33         -1 & movement=up\\
  34         1 & movement=down\\
  35         0 & \text{otherwise}
  36 \end{array}\right.$$
  37
  38 The next position of the agent is defined by the following invariant:
  39 $$next(agent_x)=agent_x+\Delta_x\wedge
  40 next(agent_y)=agent_y+\Delta_x$$
  41
  42 Determining the next position of the boxes depends on the position of the
  43 agent. This is described for the $x$ coordinate and analogous for the $y$
  44 value.
  45 $$next(b^i_x)=\left\{\begin{array}{ll}
  46         b^i_x+\Delta_x & next(agent_x)=b^i_x \wedge next(agent_y)=b^i_y\\
  47         b^i_x & \text{otherwise}
  48 \end{array}\right.$$
  49
  50 To restrict the boxes to being on top of each other we define the following
  51 invariant:
  52 $$\bigwedge_{i=0}^{k-1}\bigwedge_{j=i+1}^k\neg(b^i_x=b^j_x \wedge b^i_y=b^j_y)
  53 $$
  54
  55 \subsection{Goal}
  56 When the goal state is reached the $movement$ variable should be set to
  57 $finished$ to be able to specify the CTL specification more easily. Via the
  58 following invariant the goal state is tied to the $movement$ variable:
  59 $$\left(\bigvee_{B`\in perms(B)}
  60         \bigwedge_{b\in B`, i\in 0\ldots k}\left(
  61                 b_x=t^i_x \wedge b_y=t^i_y
  62 \right)\right)\leftrightarrow movement=finished$$
  63
  64 And a counterexample for the following CTL specification can then be seen as an
  65 example solution:
  66 $$\nexists\lozenge(movement=finished)$$