-import StdList, StdInt, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void
-
-inputfile :== "screen.1"
-outputfile :== "solver.smv"
-
-:: SokobanPuzzle :== [[SokobanTile]]
-:: SokobanTile = Wall | Free | Box | Target | Agent
-
-puzzle :: SokobanPuzzle
-puzzle = [[Wall, Wall, Wall, Wall, Wall, Wall],
- [Wall, Free, Free, Free, Free, Wall],
- [Wall, Agent,Free, Box, Free, Wall],
- [Wall, Free, Free, Free, Target, Wall],
- [Wall, Wall, Wall, Wall, Wall, Wall]]
-
-size :: (Int, Int)
-size = (4,5)
-
-checkX :: Int -> Int
-checkX x = if (x > length (hd puzzle)) (-1) x
-
-checkY :: Int -> Int
-checkY y = if (y > length puzzle) (-1) y
-
-/*
- next(x2_2) := case
- x2_2 = Wall: Wall;
-
- x2_2 = Free & x2_3 = Agent & move = Left: Agent;
- x2_2 = Free & x3_2 = Agent & move = Up: Agent;
- x2_2 = Free & x2_1 = Agent & move = Right : Agent;
- x2_2 = Free & x1_2 = Agent & move = Down : Agent;
-
- x2_2 = Free & x2_3 = Box & x2_4 = Agent & move = Left: Box;
- x2_2 = Free & x3_2 = Box & x4_2 = Agent & move = Up: Box;
- x2_2 = Free & x2_1 = Box & x2_0 = Agent & move = Right : Box;
- x2_2 = Free & x1_2 = Box & x0_2 = Agent & move = Down : Box;
-
- x2_2 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right: Free;
- x2_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down: Free;
- x2_2 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left : Free;
- x2_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up : Free;
-
- x2_2 = Box & x2_3 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left: Agent;
- x2_2 = Box & x3_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up: Agent;
- x2_2 = Box & x2_1 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right : Agent;
- x2_2 = Box & x1_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down : Agent;
-
- x2_2 = Target & x2_3 = Agent & move = Left: AgentOnTarget;
- x2_2 = Target & x3_2 = Agent & move = Up: AgentOnTarget;
- x2_2 = Target & x2_1 = Agent & move = Right : AgentOnTarget;
- x2_2 = Target & x1_2 = Agent & move = Down : AgentOnTarget;
-
- x2_2 = Target & x2_3 = Box & x2_4 = Agent & move = Left: BoxOnTarget;
- x2_2 = Target & x3_2 = Box & x4_2 = Agent & move = Up: BoxOnTarget;
- x2_2 = Target & x2_1 = Box & x2_0 = Agent & move = Right : BoxOnTarget;
- x2_2 = Target & x1_2 = Box & x0_2 = Agent & move = Down : BoxOnTarget;
-
- x2_2 = AgentOnTarget & (x2_3 = Free | x2_3 = Target) & move = Right: Target;
- x2_2 = AgentOnTarget & (x3_2 = Free | x3_2 = Target) & move = Down: Target;
- x2_2 = AgentOnTarget & (x2_1 = Free | x2_1 = Target) & move = Left : Target;
- x2_2 = AgentOnTarget & (x1_2 = Free | x1_2 = Target) & move = Up : Target;
-
- x2_2 = BoxOnTarget & x2_3 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left: AgentOnTarget;
- x2_2 = BoxOnTarget & x3_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up: AgentOnTarget;
- x2_2 = BoxOnTarget & x2_1 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right : AgentOnTarget;
- x2_2 = BoxOnTarget & x1_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down : AgentOnTarget;
-
- TRUE : x2_2;
- esac;
-
-*/
-
-genCoord :: Int Int -> [String]
-genCoord 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 (y+1)) +++ " = Agent & move = Left: Agent;\n",
- " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX (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 (y+1)) +++ " = Box & x" +++ toString x +++ "_" +++ toString (checkY (y+2)) +++ " = Agent & move = Left: Box;\n",
- " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX (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 (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Target) & move = Right: Free;\n",
- " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX (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 (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 (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 (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Target) & move = Right : Agent;\n",
- " x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down : Agent;\n",
- " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n",
- " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX (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 (y+1)) +++ " = Box & x" +++ toString x +++ "_" +++ toString (checkY (y+2)) +++ " = Agent & move = Left: BoxOnTarget;\n",
- " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX (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 (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Target) & move = Right: Target;\n",
- " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX (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 (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 (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 (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Target) & move = Right : AgentOnTarget;\n",
- " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down : AgentOnTarget;\n",
- " TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
- " esac;\n"
+import StdList, StdInt, StdBool, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Data.Tuple, Data.Void
+from Text import class Text(concat,join), instance Text String
+import Sokoban
+
+inpath :== "screen.2001"
+outpath :== "solver.smv"
+
+(<+) infixr 5 :: a b -> String | toString a & toString b
+(<+) a b = toString a +++ toString b
+
+checkX :: [[SokobanTile]] Int -> Int
+checkX p x = if (x > (length p - 1)) (-1) x
+
+checkY :: [[SokobanTile]] Int Int -> Int
+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" <+ x <+ "_" <+ y <+ ") := " <+ fromTile ((p !! x) !! y) <+ ";"
+
+genVars :: Int Int -> String
+genVars x y = " x" <+ x <+ "_" <+ y <+ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};"
+
+genCoord :: [[SokobanTile]] Int Int -> [String]
+genCoord p x y = [" next(x" <+ x <+ "_" <+ y <+ ") := case",
+ " x" <+ x <+ "_" <+ y <+ " = Wall: Wall;",
+ " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & move = Left: Agent;",
+ " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
+ <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & move = Up: Agent;",
+ " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & move = Right : Agent;",
+ " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
+ <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & move = Down : Agent;",
+
+ " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Box | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = AgentOnTarget) & move = Left: Box;",
+ " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Box | x"
+ <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Agent | x"
+ <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = AgentOnTarget) & move = Up: Box;",
+ " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = AgentOnTarget) & move = Right : Box;",
+ " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x"
+ <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Agent | x"
+ <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = AgentOnTarget) & move = Down : Box;",
+
+ " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right: Free;",
+ " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Target) & move = Down: Free;",
+ " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left : Free;",
+ " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ "= Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up : Free;",
+
+ " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Box | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = BoxOnTarget) & (x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Target) & move = Right: Free;",
+ " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Box | x"
+ <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = BoxOnTarget) & (x"
+ <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Free | x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Target) & move = Down: Free;",
+ " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Target) & move = Left: Free;",
+ " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x"
+ <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x"
+ <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Free | x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Target) & move = Up: Free;",
+
+ " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left: Agent;",
+ " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
+ <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & (x" <+ (x-1) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up: Agent;",
+ " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right : Agent;",
+ " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
+ <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Target) & move = Down : Agent;",
+
+ " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & move = Left: AgentOnTarget;",
+ " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
+ <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & move = Up: AgentOnTarget;",
+ " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & move = Right : AgentOnTarget;",
+ " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
+ <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & move = Down : AgentOnTarget;",
+
+ " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Box | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = AgentOnTarget) & move = Left: BoxOnTarget;",
+ " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Box | x"
+ <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Agent | x"
+ <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = AgentOnTarget) & move = Up: BoxOnTarget;",
+ " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = AgentOnTarget) & move = Right : BoxOnTarget;",
+ " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x"
+ <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Agent | x"
+ <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = AgentOnTarget) & move = Down : BoxOnTarget;",
+
+ " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right: Target;",
+ " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Target) & move = Down: Target;",
+ " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left : Target;",
+ " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up : Target;",
+
+ " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left: AgentOnTarget;",
+ " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
+ <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_"
+ <+ (checkY p (x-1) y) <+ " = Target) & move = Up: AgentOnTarget;",
+ " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
+ <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ x <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right : AgentOnTarget;",
+ " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
+ <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_"
+ <+ (checkY p (x+1) y) <+ " = Target) & move = Down : AgentOnTarget;",
+
+ " TRUE : x" <+ x <+ "_" <+ y <+ ";",
+ " esac;"