generation with model stub (still prototyping)

diff --git a/code/SokobanCoord.icl b/code/SokobanCoord.icl
index c23e282..a2379b7 100644 (file)
--- a/code/SokobanCoord.icl
+++ b/code/SokobanCoord.icl
@@ -1,7 +1,10 @@
-module SokobanCoord
+module SocobanCoord

 
 import StdList, StdInt, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void
 
 
 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
 
 :: SokobanPuzzle :== [[SokobanTile]]
 :: SokobanTile = Wall | Free | Box | Target | Agent
 


@@ -12,8 +15,6 @@ puzzle = [[Wall, Wall, Wall, Wall, Wall,   Wall],
           [Wall, Free, Free, Free, Target, Wall],
           [Wall, Wall, Wall, Wall, Wall,   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
 
 checkX :: Int -> Int
 checkX x = if (x > length (hd puzzle)) (-1) x


@@ -21,6 +22,15 @@ checkX x = if (x > length (hd puzzle)) (-1) x
 checkY :: Int -> Int
 checkY y = if (y > length puzzle) (-1) y
 
 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",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",
 genCoord :: Int Int -> [String]
 genCoord x y = ["  next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",


@@ -60,11 +70,47 @@ genCoord x y = ["  next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\
                 "  esac;\n"
                 ]
 
                 "  esac;\n"
                 ]
 

-/*
-genAll :: SokobanPuzzle -> [[String]]
-genAll p = [\\]
-genAll [x:xs] = []
-*/
+genAll :: [String]
+genAll = [
+          "MODULE main\n",
+          "VAR\n"
+          ]
+      ++ genVars ((length puzzle) - 1) ((length (hd puzzle)) - 1)
+      ++ [
+          "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};"
+         ]
+      ++ flatten [filter (\x -> not (contains '-' x)) (genCoord x y) \\ x <- [0..4], y <- [0..5]]

 
 contains :: Char String -> Bool
 contains char str = not (isEmpty [c\\c<-:str | char == c])
 
 contains :: Char String -> Bool
 contains char str = not (isEmpty [c\\c<-:str | char == c])


@@ -96,6 +142,4 @@ closeFile world file
   # world = fclose file world
   = world
 
   # world = fclose file world
   = world
 

-
-
-Start = flatten [filter (\x -> not (contains '-' x)) (genCoord x y) \\ x <- [0..4], y <- [0..5]]
+Start = genAll