From: Alexander Fedotov Date: Mon, 7 Mar 2016 18:27:33 +0000 (+0100) Subject: coord solution (unfinished) X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=ac799d3f661e5440845954ec72b80a98ca26c511;p=mc1516pa.git coord solution (unfinished) --- diff --git a/code/SokobanCoord.icl b/code/SokobanCoord.icl new file mode 100644 index 0000000..0cce0c4 --- /dev/null +++ b/code/SokobanCoord.icl @@ -0,0 +1,153 @@ +module SokobanCoord + +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" + ] + +/* +genAll :: SokobanPuzzle -> [[String]] +genAll p = [\\] +genAll [x:xs] = [] +*/ + +contains :: Char String -> Bool +contains char str = not (isEmpty [c\\c<-:str | char == c]) + +readLines :: File -> [String] +readLines file + | sfend file = [] + # (line, file) = sfreadline file + | otherwise = [line: readLines file] + +writeLines :: [String] *File -> *File +writeLines [] file = file +writeLines [l:ls] file = writeLines ls (file <<< l) + +openInpFile :: *World String -> (File, *World) +openInpFile world path + # (ok, file, world) = sfopen path 0 world + | not ok = abort "Error reading the file." + = (file, world) + +openOutFile :: *World String -> (*File, *World) +openOutFile world path + # (ok, file, world) = fopen path 1 world + | not ok = abort "Can not write to a file." + = (file, world) + +closeFile :: *World *File -> (Bool, *World) +closeFile world file + # world = fclose file world + = world + + + +Start = flatten [filter (\x -> not (contains '-' x)) (genCoord x y) \\ x <- [0..4], y <- [0..5]]