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