From 36c7bbee78dc35e2311cfe62ede14fa8c58debb6 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Sun, 13 Mar 2016 15:15:23 +0100 Subject: [PATCH] almost finished my bit --- code/SokobanObjectwise.icl | 10 +++--- report1/Makefile | 2 +- report1/mart.tex | 67 +++++++++++++++++++++++++++++++++++++- report1/pre.tex | 8 +++++ 4 files changed, 80 insertions(+), 7 deletions(-) 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)} -- 2.20.1