small report add and test make add

diff --git a/modelchecker/test.sh b/modelchecker/test.sh
index e34ffae..368814a 100755 (executable)
--- a/modelchecker/test.sh
+++ b/modelchecker/test.sh
@@ -1,5 +1,7 @@
 #!/bin/bash
+set -e
 
+make
 TOTAL=0
 PASSED=0
 for testscreen in tests/*; do

diff --git a/report2/implementation.tex b/report2/implementation.tex
index 04893f7..bb00db8 100644 (file)
--- a/report2/implementation.tex
+++ b/report2/implementation.tex
@@ -3,10 +3,12 @@
 When parsed the sokoban screen is stripped of all walls and unreachable empty
 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. To encode the state we
-introduce an encoding function that encodes a state in three boolean variables:
+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
+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\\
@@ -21,7 +23,7 @@ This means that the encoding of a screen takes $3*|F|$ variables.
 
 \subsection{Transition encoding}
 We introduce a variable denoting the intended direction of movement $m \in
-\{\text{up}, \text{down}, \text{left}, \text{right}\}$. 
+\{\text{up}, \text{down}, \text{left}, \text{right}\}$. Tiles 
 %
 %Let\\
 %$\delta_{x}(x,m) =