code/SokobanCoord.icl

   1 module SokobanCoord
   2
   3 import StdList, StdInt, StdBool, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void
   4 import Sokoban
   5
   6 inpath  :== "screen.2001"
   7 outpath :== "solver.smv"
   8
   9 /*
  10 puzzle :: SokobanPuzzle
  11 puzzle = Sokoban [[Wall, Wall, Wall, Wall, Wall,   Wall],
  12                   [Wall, Free, Free, Free, Free,   Wall],
  13                   [Wall, Agent,Free, Box,  Free,   Wall],
  14                   [Wall, Free, Free, Free, Target, Wall],
  15                   [Wall, Wall, Wall, Wall, Wall,   Wall]]
  16 */
  17
  18 instance == SokobanTile
  19 where
  20   (==) Wall Wall = True
  21   (==) Free Free = True
  22   (==) Box Box = True
  23   (==) Agent Agent = True
  24   (==) Target Target = True
  25   (==) TargetBox TargetBox = True
  26   (==) TargetAgent TargetAgent = True
  27   (==) _ _ = False
  28
  29 checkX :: [[SokobanTile]] Int -> Int
  30 checkX p x = if (x > (length p - 1)) (-1) x
  31
  32 checkY :: [[SokobanTile]] Int Int -> Int
  33 checkY p x y
  34   | ((x < 0) || (x > (length p - 1))) = -1
  35   | otherwise = if (y > (length (p !! x) - 1)) (-1) y
  36
  37 genField :: [[SokobanTile]] Int Int -> String
  38 genField p x y = "    init(x" +++ toString x +++ "_" +++ toString y +++ ") := " +++ fromTile ((p !! x) !! y) +++ ";\n"
  39
  40 genVars :: Int Int -> String
  41 genVars x y = "    x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n"
  42
  43 genCoord :: [[SokobanTile]] Int Int -> [String]
  44 genCoord p x y = ["  next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n",
  45                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",
  46                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & move = Left: Agent;\n",
  47                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent & move = Up: Agent;\n",
  48                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent & move = Right : Agent;\n",
  49                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent & move = Down : Agent;\n",
  50                 "    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",
  51                 "    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",
  52                 "    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",
  53                 "    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",
  54                 "    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",
  55                 "    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",
  56                 "    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",
  57                 "    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",
  58
  59                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box & x"
  60                         +++ 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",
  61                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Box & x"
  62                         +++ 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",
  63                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box & x"
  64                         +++ 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",
  65                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box & x"
  66                         +++ 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",
  67
  68                 "    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",
  69                 "    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",
  70                 "    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",
  71                 "    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",
  72                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n",
  73                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent & move = Up: AgentOnTarget;\n",
  74                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent & move = Right : AgentOnTarget;\n",
  75                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent & move = Down : AgentOnTarget;\n",
  76                 "    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",
  77                 "    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",
  78                 "    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",
  79                 "    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",
  80                 "    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",
  81                 "    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",
  82                 "    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",
  83                 "    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",
  84                 "    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",
  85                 "    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)) +++ "_"
  86                         +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up: AgentOnTarget;\n",
  87                 "    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",
  88                 "    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)) +++ "_"
  89                         +++ toString (checkY p (x+1) y) +++ " = Target) & move = Down : AgentOnTarget;\n",
  90                 "    TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
  91                 "  esac;\n"
  92                 ]
  93
  94 fromTile :: SokobanTile -> String
  95 fromTile Wall = "Wall"
  96 fromTile Free = "Free"
  97 fromTile Box = "Box"
  98 fromTile Target = "Target"
  99 fromTile Agent = "Agent"
 100 fromTile TargetAgent = "AgentOnTarget"
 101 fromTile TargetBox = "BoxOnTarget"
 102
 103 genCond :: [[SokobanTile]] Int Int -> String
 104 genCond p x y
 105   | x < 0 || y < 0 || x > (length p) - 1 = ""
 106   | otherwise
 107     | y > (length (p !! x) - 1) = ""
 108     | otherwise = if ((p !! x) !! y == Target) ("x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget") ""
 109
 110 addLogic :: [String] -> [String]
 111 addLogic [] = []
 112 addLogic [x] = [x]
 113 addLogic [x:xs] = [x +++ " & ": addLogic xs]
 114
 115 genAll :: SokobanPuzzle -> [String]
 116 genAll puzzle = let (Sokoban p) = puzzle in
 117          [
 118           "MODULE main\n",
 119           "VAR\n"
 120           ]
 121       ++ [genVars x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
 122       ++ ["    move : {Up, Down, Left, Right};\n"]
 123       ++ [
 124           "  ASSIGN\n",
 125           "    init(move) := {Up, Down, Left, Right};\n"
 126          ]
 127       ++ [genField p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
 128       ++ flatten [filter (\x -> not (contains '-' x)) (genCoord p x y) \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
 129       ++ ["  next(move) := {Up, Down, Left, Right};\n"]
 130       ++ ["INVARSPEC !("]
 131       ++ addLogic (filter (\x -> x <> "" ) [genCond p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]])
 132       ++ [")\n"]
 133
 134 contains :: Char String -> Bool
 135 contains char str = not (isEmpty [c\\c<-:str | char == c])
 136
 137 readLines :: File -> [String]
 138 readLines file
 139   | sfend file = []
 140   # (line, file) = sfreadline file
 141   | otherwise = [line: readLines file]
 142
 143 writeLines :: [String] *File -> *File
 144 writeLines [] file = file
 145 writeLines [l:ls] file = writeLines ls (file <<< l)
 146
 147 openInpFile :: *World String -> (File, *World)
 148 openInpFile world path
 149   # (ok, file, world) = sfopen path 0 world
 150   | not ok = abort "Error reading the file."
 151   = (file, world)
 152
 153 openOutFile :: *World String -> (*File, *World)
 154 openOutFile world path
 155   # (ok, file, world) = fopen path 1 world
 156   | not ok = abort "Can not write to a file."
 157   = (file, world)
 158
 159 closeFile :: *World *File -> (Bool, *World)
 160 closeFile world file
 161   # world = fclose file world
 162   = world
 163
 164 Start :: *World -> *World
 165 Start w
 166   # (p, w) = parse inpath w
 167   # s = genAll p
 168   # (f, w) = openOutFile w outpath
 169   # f = writeLines s f
 170   # (ok, w) = closeFile w f
 171   = w