1 \section{Object centered approach
}
3 All boxes $B=\
{b^
0, b^
1,
\ldots, b^k\
}$ and all targets $T=\
{t^
0, t^
1,
\ldots,
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$
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)$$
17 The initial values are determined by the values passed to it in the
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.
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
}
32 \Delta_y=
\left\
{\begin{array
}{ll
}
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$$
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$
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
}
50 To restrict the boxes to being on top of each other we define the following
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)
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 perm(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$$
64 And a counterexample for the following CTL specification can then be seen as an
66 $$
\nexists\lozenge(movement=finished)$$