coord generator minor fixes

diff --git a/code/SokobanCoord.icl b/code/SokobanCoord.icl
index dfbc60f..c082875 100644 (file)
--- a/code/SokobanCoord.icl
+++ b/code/SokobanCoord.icl
@@ -1,9 +1,9 @@
 module SokobanCoord
 
-import StdList, StdInt, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void
+import StdList, StdInt, StdBool, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void
 import Sokoban
 
-inpath  :== "screen.2000"
+inpath  :== "screen.2001"
 outpath :== "solver.smv"
 
 /*
@@ -15,11 +15,24 @@ puzzle = Sokoban [[Wall, Wall, Wall, Wall, Wall,   Wall],
                   [Wall, Wall, Wall, Wall, Wall,   Wall]]
 */
 
+instance == SokobanTile
+where
+  (==) Wall Wall = True
+  (==) Free Free = True
+  (==) Box Box = True
+  (==) Agent Agent = True
+  (==) Target Target = True
+  (==) TargetBox TargetBox = True
+  (==) TargetAgent TargetAgent = True
+  (==) _ _ = False
+
 checkX :: [[SokobanTile]] Int -> Int
 checkX p x = if (x > (length p - 1)) (-1) x
 
 checkY :: [[SokobanTile]] Int Int -> Int
-checkY p x y = if (y > (length (p !! x) - 1)) (-1) y
+checkY p x y 
+  | ((x < 0) || (x > (length p - 1))) = -1 
+  | otherwise = if (y > (length (p !! x) - 1)) (-1) y
 
 genField :: [[SokobanTile]] Int Int -> String
 genField p x y = "    init(x" +++ toString x +++ "_" +++ toString y +++ ") := " +++ fromTile ((p !! x) !! y) +++ ";\n"
@@ -30,38 +43,50 @@ genVars x y = "    x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free,
 genCoord :: [[SokobanTile]] Int Int -> [String]
 genCoord p x y = ["  next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & move = Left: Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Box & x" +++ toString x +++ "_" +++ toString (checkY p x  (y+2)) +++ " = Agent & move = Left: Box;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p (x+2)) +++ "_" +++ toString x +++ " = Agent & move = Up: Box;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (x-2) +++ " = Agent & move = Right : Box;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : Box;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Target) & move = Right: Free;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down: Free;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Free;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ "= Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Free;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left: Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up: Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Target) & move = Right : Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down : Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Box & x" +++ toString x +++ "_" +++ toString (checkY p x  (y+2)) +++ " = Agent & move = Left: BoxOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p (x+2)) +++ "_" +++ toString y +++ " = Agent & move = Up: BoxOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (y-2) +++ " = Agent & move = Right : BoxOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : BoxOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Target) & move = Right: Target;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down: Target;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Target;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Target;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left: AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up: AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Target) & move = Right : AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down : AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & move = Left: Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent & move = Up: Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent & move = Right : Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent & move = Down : Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Box & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+2)) +++ " = Agent & move = Left: Box;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Box & x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent & move = Up: Box;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent & move = Right : Box;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box & x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent & move = Down : Box;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Target) & move = Right: Free;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Target) & move = Down: Free;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left : Free;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ "= Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up : Free;\n",
+                
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box & x" 
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Target) & move = Right: Free;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Box & x" 
+                        +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Free | x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Target) & move = Down: Free;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box & x" 
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Target) & move = Left: Free;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box & x" 
+                        +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Free | x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Target) & move = Up: Free;\n",                        
+                        
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left: Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up: Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Target) & move = Right : Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Target) & move = Down : Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent & move = Up: AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent & move = Right : AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent & move = Down : AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Box & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+2)) +++ " = Agent & move = Left: BoxOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Box & x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent & move = Up: BoxOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent & move = Right : BoxOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box & x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent & move = Down : BoxOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Target) & move = Right: Target;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Target) & move = Down: Target;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left : Target;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up : Target;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left: AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" 
+                        +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up: AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Target) & move = Right : AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" 
+                        +++ toString (checkY p (x+1) y) +++ " = Target) & move = Down : AgentOnTarget;\n",
                 "    TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
                 "  esac;\n"
                 ]
@@ -75,6 +100,18 @@ fromTile Agent = "Agent"
 fromTile TargetAgent = "AgentOnTarget"
 fromTile TargetBox = "BoxOnTarget"
 
+genCond :: [[SokobanTile]] Int Int -> String
+genCond p x y
+  | x < 0 || y < 0 || x > (length p) - 1 = ""
+  | otherwise
+    | y > (length (p !! x) - 1) = ""
+    | otherwise = if ((p !! x) !! y == Target) ("x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget") ""
+    
+addLogic :: [String] -> [String]
+addLogic [] = []
+addLogic [x] = [x]
+addLogic [x:xs] = [x +++ " & ": addLogic xs]
+
 genAll :: SokobanPuzzle -> [String]
 genAll puzzle = let (Sokoban p) = puzzle in
          [
@@ -90,6 +127,9 @@ genAll puzzle = let (Sokoban p) = puzzle in
       ++ [genField p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
       ++ flatten [filter (\x -> not (contains '-' x)) (genCoord p x y) \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
       ++ ["  next(move) := {Up, Down, Left, Right};\n"]
+      ++ ["INVARSPEC !("]
+      ++ addLogic (filter (\x -> x <> "" ) [genCond p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]])
+      ++ [")\n"]
 
 contains :: Char String -> Bool
 contains char str = not (isEmpty [c\\c<-:str | char == c])
@@ -121,7 +161,6 @@ closeFile world file
   # world = fclose file world
   = world
 
-
 Start :: *World -> *World
 Start w
   # (p, w) = parse inpath w
@@ -129,4 +168,4 @@ Start w
   # (f, w) = openOutFile w outpath
   # f = writeLines s f
   # (ok, w) = closeFile w f
-  = w
+  = w
\ No newline at end of file