From: Mart Lubbers <mart@martlubbers.net>
Date: Sun, 13 Mar 2016 14:15:23 +0000 (+0100)
Subject: almost finished my bit
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=36c7bbee78dc35e2311cfe62ede14fa8c58debb6;hp=-c;p=mc1516pa.git

almost finished my bit
---

36c7bbee78dc35e2311cfe62ede14fa8c58debb6
diff --git a/code/SokobanObjectwise.icl b/code/SokobanObjectwise.icl
index 4b9542d..656fad8 100644
--- a/code/SokobanObjectwise.icl
+++ b/code/SokobanObjectwise.icl
@@ -41,7 +41,7 @@ encode p = join "\n" [
 	"--Agent not on the box",
 	"INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
 	"--Box not on box",
-	encodeBoxOnBoxes boxnums,
+	"INVAR " <+ encodeBoxOnBoxes boxnums <+ ";",
 	"--Goal state",
 	"INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
 	"--Agent movement",
@@ -116,8 +116,8 @@ encodeGoalState boxes targets = "(" <+
 
 encodeBoxOnBoxes :: [Int] -> String
 encodeBoxOnBoxes [] = ""
-encodeBoxOnBoxes [b] = ""
-encodeBoxOnBoxes [b:bs] = "INVAR " <+ encodeBoxOnBox b bs <+ ";\n" <+
+encodeBoxOnBoxes [b] = "TRUE"
+encodeBoxOnBoxes [b:bs] = encodeBoxOnBox b bs <+ " &\n\t" <+
 	encodeBoxOnBoxes bs
 	where
 		encodeBoxOnBox :: Int [Int] -> String
@@ -129,8 +129,8 @@ encodeAgentNotOnBox bs = join " &\n\t" [
 	"!(b" <+ i <+ ".x = agent.x & b" <+ i <+ ".y = agent.y)"\\i<-bs]
 
 encodeObMovement :: String -> String
-encodeObMovement s = "TRANS next(" <+ s <+ ".x) = " <+ s <+ ".x + dx;\n" <+
-	"TRANS next(" <+ s <+ ".y) = " <+ s <+ ".y + dy;"
+encodeObMovement s = "TRANS next(" <+ s <+ ".x) = " <+ s <+ ".x + dx & " <+
+	"next(" <+ s <+ ".y) = " <+ s <+ ".y + dy;"
 
 encodeObPosition :: [(Int, Int)] -> String
 encodeObPosition p = join " |\n\t" [forThisX x p\\x<-removeDup $ map fst p]
diff --git a/report1/Makefile b/report1/Makefile
index 5940ab1..0e1af92 100644
--- a/report1/Makefile
+++ b/report1/Makefile
@@ -6,7 +6,7 @@ DOCUMENT:=report1
 
 all: $(DOCUMENT).pdf
 
-%.pdf: %.tex %.fmt
+%.pdf: %.tex %.fmt mart.tex alex.tex
 	$(LATEX) $<
 	$(LATEX) $<
 
diff --git a/report1/mart.tex b/report1/mart.tex
index 802992c..ee1d9b5 100644
--- a/report1/mart.tex
+++ b/report1/mart.tex
@@ -1 +1,66 @@
-Hello world
+\section{Object centered approach}
+We define:
+All boxes $B=\{b^0, b^1, \ldots, b^k\}$ and all targets $T=\{t^0, t^1, \ldots,
+t^k\}$.
+\subsection{Objects}
+We define the set $lex$ as being the set containing all legal $x$ values and
+the function $ley(x)$ that for a given $x$ returns the set of all legal $y$
+values for that $x$.
+
+To reduce size of the encoding we introduce a module called \texttt{ob}
+representing an object in the screen. The module contains two integer variables
+$x$ and $y$ that contains the position of the object in the field. The $x$ and
+$y$ values are bounded by the level size through their domain and restricted to
+the non-wall positions with the following invariant:
+$$\bigvee_{i\in lex}\left(x=i\wedge\bigvee_{j\in ley(x)}y=j\right)$$
+
+The initial values are determined by the values passed to it in the
+\texttt{main} module.
+
+In the \texttt{main} module we define for all boxes and the agent such an
+\texttt{ob} that stores the position of that object in that particular state.
+
+\subsection{Movement}
+We define a variable $movement=\{left,up,right,down,finished\}$ which describes
+the move in that state. From the movement variable new positions of objects are
+calculated using delta variables.
+$$\Delta_x=\left\{\begin{array}{ll}
+	-1 & movement=left\\
+	1 & movement=right\\
+	0 & \text{otherwise}
+\end{array}\right.
+\Delta_y=\left\{\begin{array}{ll}
+	-1 & movement=up\\
+	1 & movement=down\\
+	0 & \text{otherwise}
+\end{array}\right.$$
+
+The next position of the agent is defined by the following invariant:
+$$next(agent_x)=agent_x+\Delta_x\wedge
+next(agent_y)=agent_y+\Delta_x$$
+
+Determining the next position of the boxes depends on the position of the
+agent. This is described for the $x$ coordinate and analogous for the $y$
+value.
+$$next(b^i_x)=\left\{\begin{array}{ll}
+	b^i_x+\Delta_x & next(agent_x)=b^i_x \wedge next(agent_y)=b^i_y\\
+	b^i_x & \text{otherwise}
+\end{array}\right.$$
+
+To restrict the boxes to being on top of each other we define the following
+invariant:
+$$\bigwedge_{i=0}^{k-1}\bigwedge_{j=i+1}^k\neg(b^i_x=b^j_x \wedge b^i_y=b^j_y)
+$$
+
+\subsection{Goal}
+When the goal state is reached the $movement$ variable should be set to
+$finished$ to be able to specify the CTL specification more easily. Via the
+following invariant the goal state is tied to the $movement$ variable:
+$$\left(\bigvee_{B`\in perm(B)}
+	\bigwedge_{b\in B`, i\in 0\ldots k}\left(
+		b_x=t^i_x \wedge b_y=t^i_y
+\right)\right)\leftrightarrow movement=finished$$
+
+And a counterexample for the following CTL specification can then be seen as an
+example solution:
+$$\nexists\lozenge(movement=finished)$$
diff --git a/report1/pre.tex b/report1/pre.tex
index 76bc837..09bb5f2 100644
--- a/report1/pre.tex
+++ b/report1/pre.tex
@@ -1,6 +1,14 @@
 \documentclass{article}
 
 \usepackage{a4wide}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{listings}
+
+\lstset{%
+	breaklines,
+	basicstyle=\scriptsize
+}
 
 \title{Solving Sokoban with NuSMV}
 \author{Alexander Fedotov(s4460952)\and Mart Lubbers(s4109503)}