almost finished code, strange error

diff --git a/code/.gitignore b/code/.gitignore
index dacd0be..6c83100 100644 (file)
--- a/code/.gitignore
+++ b/code/.gitignore
@@ -1,3 +1,4 @@
 Clean System Files
 a.out
 SokobanObjectwise
+*.prj

diff --git a/code/SokobanObjectwise.icl b/code/SokobanObjectwise.icl
index 558cc4f..d51ee55 100644 (file)
--- a/code/SokobanObjectwise.icl
+++ b/code/SokobanObjectwise.icl
@@ -6,8 +6,15 @@ import StdTuple
 import StdFunc
 import StdOrdList
 import StdList
+
+from Data.Func import $
+from Data.List import intercalate, maximum, permutations
+from Text import class Text(concat,join), instance Text String
+
 import Sokoban
 
+:: AnnotatedSokoban :== [(Int, Int, SokobanTile)]
+
 Start :: *World -> *World
 Start w
 # (io, w) = stdio w
@@ -16,36 +23,117 @@ Start w
 = snd (fclose io w)
 
 encode :: SokobanPuzzle -> String
-encode p = foldr ((+++) o (+++) "\n") "" ([
-       "MODULE", 
-       "main",
-       "VAR":encodeBoxes p maxX maxY])
+encode p = join "\n" [
+       "MODULE ob(ix, iy, movement)",
+       "VAR",
+       "\tx: 0 .. " <+ maxX <+ ";",
+       "\ty: 0 .. " <+ maxX <+ ";",
+
+       "INVAR " <+ encodeObjectPositions legalPos <+ ";",
+
+       "ASSIGN",
+       "\tinit(x):=ix;",
+       "\tinit(y):=iy;\n",
+
+       "MODULE main",
+       "VAR",
+       "\tmovement: {left, up, right, down, finished};",
+       "\tagent: " <+ encodeAgent annot,
+       encodeBoxes boxes,
+       
+       "DEFINE",
+       "\tdx := case",
+       "\t\tmovement = left : -1;",
+       "\t\tmovement = right: +1;",
+       "\t\tTRUE:              0;",
+       "\tesac;",
+       "\tdy := case",
+       "\t\tmovement = up  : -1;",
+       "\t\tmovement = down: +1;",
+       "\t\tTRUE:             0;",
+       "\tesac;",
+
+       "INVAR (" <+ encodeGoalState (indexList boxes) targetPos <+ 
+               ") <-> movement = finished;",
+       "INVAR " <+ encodeAgentNotOnBox (indexList boxes) <+ ";",
+       "TRANS next(agent.x) = agent.x + dx;",
+       "TRANS next(agent.y) = agent.y + dy;",
+       encodeBlockMovement (indexList boxes),
+       "CTLSPEC ! EF (movement = finished)",
+       "CTLSPEC EF (b0.x=3)"
+       ]
        where
+               targetPos = getTargets annot
+               boxes = getBoxes annot
+               legalPos = legalPositions annot
                annot = annotate p
                (maxX, maxY) = getMetrics annot
 
-:: AnnotatedSokoban :== [(Int, Int, SokobanTile)]
+//THIS IS NAIVE AND SHOULD BE IMPROVED
+legalPositions :: AnnotatedSokoban -> [(Int, Int)]
+legalPositions p = [(x, y)\\(x, y, t)<-p | case t of Wall=False; _=True]
 
 annotate :: SokobanPuzzle -> AnnotatedSokoban
 annotate (Sokoban p) = flatten [[(x, y, t)\\t<-r & x<-[0..]]\\r<-p & y<-[0..]]
 
+getTargets :: AnnotatedSokoban -> [(Int, Int)]
+getTargets p = [(x, y)\\(x, y, t)<-p | 
+       case t of Target=True;TargetBox=True;TargetAgent=True;_=False] 
+
 getMetrics :: AnnotatedSokoban -> (Int, Int)
-getMetrics p = (maxList (map fst3 p),maxList (map snd3 p))
+getMetrics p = (maximum (map fst3 p),maximum (map snd3 p))
 
 getBoxes :: AnnotatedSokoban -> [(Int, Int)]
-getBoxes p = [t\\t=:(_, _, Box)<-p] ++ 
-
-       where
-               getBox` _ [] = []
-               getBox` x [b:bs] = let r = getBox` (x+1) bs in case b of
-                               Box = [x:r]
-                               TargetBox = [x:r]
-                               _ = r
+getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]
 
 (<+) infixr 5 :: a b -> String | toString a & toString b
 (<+) a b = toString a +++ toString b
 
-encodeBoxes :: SokobanPuzzle Int Int -> [String]
-encodeBoxes p mx my = [
-       "\tbox" <+ i <+ "x: " <+ "0 .. " <+ mx <+ ";\n\tbox" <+
-       i <+ "y: " <+ "0 .. " <+ my <+ ";"\\(bx, by)<-getBoxes p & i<-[0..]]
+encodeGoalState :: [Int] [(Int, Int)] -> String
+encodeGoalState boxes targets = join " |\n\t" $ map encodeOneGoal boxtargets
+       where
+               boxtargets = map (zip2 targets) (permutations boxes)
+               
+               encodeOneGoal :: [((Int, Int), Int)] -> String
+               encodeOneGoal p = "(" <+ join " & " (encodeOneGoal` p) <+ ")"
+
+               encodeOneGoal` :: [((Int, Int), Int)] -> [String]
+               encodeOneGoal` [] = []
+               encodeOneGoal` [((x, y), b):xs] = [
+                       "b" <+ b <+ ".x = " <+ x <+ " & " <+
+                       "b" <+ b <+ ".y = " <+ y:encodeOneGoal` xs]
+               
+
+encodeBlockMovement :: [Int] -> String
+encodeBlockMovement bs = join "\n" $ map ebm bs
+       where
+               ebm :: Int -> String
+               ebm i =
+                       "TRANS next(b" <+ i <+ ".x) = case\n" <+
+                       "\t\tnext(agent.x) != b" <+ i <+ ".x | " <+
+                       "next(agent.y) != b" <+ i <+ ".y: b" <+ i <+ ".x;\n" <+
+                       "\t\tTRUE: b" <+ i <+ ".x + dx;\n" <+
+                       "\tesac;\n" <+
+                       "TRANS next(b" <+ i <+ ".y) = case\n" <+
+                       "\t\tnext(agent.x) != b" <+ i <+ ".x | " <+
+                       "next(agent.y) != b" <+ i <+ ".y: b" <+ i <+ ".x;\n" <+
+                       "\t\tTRUE: b" <+ i <+ ".y + dy;\n" <+
+                       "\tesac;"
+
+encodeAgentNotOnBox :: [Int] -> String
+encodeAgentNotOnBox bs = join " &\n\t" [
+       "(b" <+ i <+ ".x != agent.x & b" <+ i <+ ".y != agent.y)"\\i<-bs]
+
+encodeObjectPositions :: [(Int, Int)] -> String
+encodeObjectPositions p = join " | " ["x="<+x<+" & "<+"y="<+y\\(x, y)<-p]
+
+encodeAgent :: AnnotatedSokoban -> String
+encodeAgent [x:xs] = case x of
+       (x, y, Agent) = "ob(" <+ x <+ "," <+ y <+ ", movement);"
+       (x, y, TargetAgent) = "ob(" <+ x <+ "," <+ y <+ ", movement);"
+       _ = encodeAgent xs
+
+encodeBoxes :: [(Int, Int)] -> String
+encodeBoxes p = join "\n" 
+       ["\tb" <+ i <+ ": ob(" <+ bx <+ ", " <+ by <+ ", movement);"
+       \\(bx, by)<-p & i<-[0..]]