-module SocobanCoord
+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
-inputfile :== "screen.1"
-outputfile :== "solver.smv"
+inpath :== "screen.1001"
+outpath :== "solver.smv"
-:: SokobanPuzzle :== [[SokobanTile]]
-:: SokobanTile = Wall | Free | Box | Target | Agent
+checkX :: [[SokobanTile]] Int -> Int
+checkX p x = if (x > (length p - 1)) (-1) x
-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]]
+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" +++ toString x +++ "_" +++ toString y +++ ") := " +++ fromTile ((p !! x) !! y) +++ ";\n"
+
+genVars :: Int Int -> String
+genVars x y = " x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n"
-checkX :: Int -> Int
-checkX x = if (x > length (hd puzzle)) (-1) x
-
-checkY :: Int -> Int
-checkY y = if (y > length puzzle) (-1) y
-
-genVars :: Int Int -> [String]
-genVars x y = genVars` x y 0 0 []
-where
- genVars` :: Int Int Int Int [String] -> [String]
- genVars` a b x y res
- | (a+1) == x = res
- | b == y = genVars` a b (x+1) 0 [" x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n":res]
- | otherwise = genVars` a b x (y+1) [" x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n":res]
-
-genCoord :: Int Int -> [String]
-genCoord x y = [" next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n",
+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 (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",
+ " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent | x"
+ +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = AgentOnTarget) & move = Left: Agent;\n",
+ " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (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) +++ " = AgentOnTarget) & move = Up: Agent;\n",
+ " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x"
+ +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & move = Right : Agent;\n",
+ " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (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) +++ " = AgentOnTarget) & 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+1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Agent | x"
+ +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = AgentOnTarget) & 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+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent | x"
+ +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = AgentOnTarget) & 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-1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent | x"
+ +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = AgentOnTarget) & 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-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent | x"
+ +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = AgentOnTarget) & 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+1)) +++ " = BoxOnTarget) & (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+1)) +++ "_" +++ toString (checkY p x y) +++ " = BoxOnTarget) & (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-1)) +++ " = BoxOnTarget) & (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-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (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)) +++ " = 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: 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) +++ " = AgentOnTarget) & (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)) +++ " = 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 : 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) +++ " = AgentOnTarget) & (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 | x"
+ +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = AgentOnTarget) & move = Left: AgentOnTarget;\n",
+ " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (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) +++ " = AgentOnTarget) & move = Up: AgentOnTarget;\n",
+ " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x"
+ +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & move = Right : AgentOnTarget;\n",
+ " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (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) +++ " = AgentOnTarget) & 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+1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Agent | x"
+ +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = AgentOnTarget) & 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+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent | x"
+ +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = AgentOnTarget) & 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-1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent | x"
+ +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = AgentOnTarget) & 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-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent | x"
+ +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = AgentOnTarget) & 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)) +++ " = 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: 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) +++ " = 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: 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)) +++ " = AgentOnTarget) & (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) +++ " = 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 : AgentOnTarget;\n",
+
" TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
" esac;\n"
]
-genAll :: [String]
-genAll = [
+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
+
+fromTile :: SokobanTile -> String
+fromTile Wall = "Wall"
+fromTile Free = "Free"
+fromTile Box = "Box"
+fromTile Target = "Target"
+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
+ [
"MODULE main\n",
"VAR\n"
]
- ++ genVars ((length puzzle) - 1) ((length (hd puzzle)) - 1)
+ ++ [genVars x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
+ ++ [" move : {Up, Down, Left, Right};\n"]
++ [
- "ASSIGN",
- "init(x0_0) := Wall;", //currently just a stub
- "init(x0_1) := Wall;",
- "init(x0_2) := Wall;",
- "init(x0_3) := Wall;",
- "init(x0_4) := Wall;",
- "init(x0_5) := Wall;",
- "init(x1_0) := Wall;",
- "init(x1_1) := Free;",
- "init(x1_2) := Free;",
- "init(x1_3) := Free;",
- "init(x1_4) := Free;",
- "init(x1_5) := Wall;",
- "init(x2_0) := Wall;",
- "init(x2_1) := Agent;",
- "init(x2_2) := Free;",
- "init(x2_3) := Box;",
- "init(x2_4) := Free;",
- "init(x2_5) := Wall;",
- "init(x3_0) := Wall;",
- "init(x3_1) := Free;",
- "init(x3_2) := Free;",
- "init(x3_3) := Free;",
- "init(x3_4) := Target;",
- "init(x3_5) := Wall;",
- "init(x4_0) := Wall;",
- "init(x4_1) := Wall;",
- "init(x4_2) := Wall;",
- "init(x4_3) := Wall;",
- "init(x4_4) := Wall;",
- "init(x4_5) := Wall;",
- "init(move) := {Up, Down, Left, Right};"
+ " ASSIGN\n",
+ " init(move) := {Up, Down, Left, Right};\n"
]
- ++ flatten [filter (\x -> not (contains '-' x)) (genCoord x y) \\ x <- [0..4], y <- [0..5]]
+ ++ [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])
# world = fclose file world
= world
-Start = genAll
+Start :: *World -> *World
+Start w
+ # (p, w) = parse inpath w
+ # s = genAll p
+ # (f, w) = openOutFile w outpath
+ # f = writeLines s f
+ # (ok, w) = closeFile w f
+ = w
\ No newline at end of file