works, tested with 2000 and 642

diff --git a/code/SokobanObjectwise.icl b/code/SokobanObjectwise.icl
index 9dc09a1..7297c32 100644 (file)
--- a/code/SokobanObjectwise.icl
+++ b/code/SokobanObjectwise.icl
@@ -24,25 +24,13 @@ Start w
 
 encode :: SokobanPuzzle -> String
 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",
+       encodeAgentVars maxX maxY,
+       encodeBoxVars (indexList boxes) maxX maxY,
        "\tmovement: {left, up, right, down, finished};",
-       "\tagent: " <+ encodeAgent annot,
-       encodeBoxes boxes,
-       
-       "DEFINE",
-       "\tdx := case",
+       "",
+       "DEFINE dx := case",
        "\t\tmovement = left : -1;",
        "\t\tmovement = right: +1;",
        "\t\tTRUE:              0;",
@@ -52,20 +40,30 @@ encode p = join "\n" [
        "\t\tmovement = down: +1;",
        "\t\tTRUE:             0;",
        "\tesac;",
-
-       "INVAR (" <+ encodeGoalState (indexList boxes) targetPos <+ 
-               ") <-> movement = finished;",
+       "",
+       "INIT",
+       encodeAgentInit agent <+ " &",
+       encodeBoxInit boxes <+ ";",
+       "--Agent not on the box",
        "INVAR " <+ encodeAgentNotOnBox (indexList boxes) <+ ";",
-       "INVAR " <+ encodeBoxesNotOnBox (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)"
-       ]
+       "--Allowed box positions on the field",
+       encodeBoxPositions (indexList boxes) legalPos,
+       "--Box not on box",
+       encodeBoxOnBoxes (indexList boxes),
+       "--Allowed agent positions",
+       "INVAR " <+ encodeAgentPositions legalPos,
+       "--Goal state",
+       "INVAR " <+ encodeGoalState (indexList boxes) targetPos <+ ";",
+       "",
+       encodeAgentMovement,
+       encodeBoxMovement (indexList boxes),
+       "CTLSPEC ! EF (movement = finished);",
+
+       ""]
        where
                targetPos = getTargets annot
                boxes = getBoxes annot
+               agent = hd $ getAgents annot
                legalPos = legalPositions annot
                annot = annotate p
                (maxX, maxY) = getMetrics annot
@@ -84,6 +82,9 @@ getTargets p = [(x, y)\\(x, y, t)<-p |
 getMetrics :: AnnotatedSokoban -> (Int, Int)
 getMetrics p = (maximum (map fst3 p),maximum (map snd3 p))
 
+getAgents :: AnnotatedSokoban -> [(Int, Int)]
+getAgents p = [(x, y)\\(x, y, Agent)<-p] ++ [(x, y)\\(x, y, TargetAgent)<-p]
+
 getBoxes :: AnnotatedSokoban -> [(Int, Int)]
 getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]
 
@@ -91,7 +92,8 @@ getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]
 (<+) a b = toString a +++ toString b
 
 encodeGoalState :: [Int] [(Int, Int)] -> String
-encodeGoalState boxes targets = join " |\n\t" $ map encodeOneGoal boxtargets
+encodeGoalState boxes targets = "(" <+
+       join " |\n\t" (map encodeOneGoal boxtargets) <+ ")<->movement=finished"
        where
                boxtargets = map (zip2 targets) (permutations boxes)
                
@@ -101,44 +103,69 @@ encodeGoalState boxes targets = join " |\n\t" $ map encodeOneGoal boxtargets
                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
+                       "b" <+ b <+ "x = " <+ x <+ " & " <+
+                       "b" <+ b <+ "y = " <+ y:encodeOneGoal` xs]
+
+encodeBoxOnBoxes :: [Int] -> String
+encodeBoxOnBoxes [] = ""
+encodeBoxOnBoxes [b] = ""
+encodeBoxOnBoxes [b:bs] = "INVAR " <+ encodeBoxOnBox b bs <+ ";\n" <+
+       encodeBoxOnBoxes 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;"
-
-//TODO
-encodeBoxesNotOnBox :: [Int] -> String
-encodeBoxesNotOnBox _ = "TRUE;"
+               encodeBoxOnBox :: Int [Int] -> String
+               encodeBoxOnBox x bs = join " & " ["!(b" <+ x <+ "x=b" <+ b <+ "x &" <+ 
+                       "b" <+ x <+ "y=b" <+ b <+ "y)"\\b<-bs]
 
 encodeAgentNotOnBox :: [Int] -> String
 encodeAgentNotOnBox bs = join " &\n\t" [
-       "(b" <+ i <+ ".x != agent.x & b" <+ i <+ ".y != agent.y)"\\i<-bs]
+       "!(b" <+ i <+ "x = agentx & b" <+ i <+ "y = agenty)"\\i<-bs]
+
+encodeObPosition :: String [(Int, Int)] -> String
+encodeObPosition b p = join " | " [
+       "(" <+ b <+ "x=" <+ x <+ " & " <+
+       b <+ "y=" <+ y <+ ")"\\ (x, y)<-p]
+
+encodeAgentInit :: (Int, Int) -> String
+encodeAgentInit (x, y) = "\tagentx=" <+ x <+ " & " <+ "agenty=" <+ y
+
+encodeAgentVars :: Int Int -> String
+encodeAgentVars mx my = 
+       "\tagentx: 0.." <+ mx <+ ";\n\tagenty: 0.." <+ my <+ ";\n"
+
+encodeAgentPositions :: [(Int, Int)] -> String
+encodeAgentPositions p = encodeObPosition "agent" p
+
+encodeAgentMovement :: String
+encodeAgentMovement = "TRANS next(agentx) = agentx + dx;\n" <+
+       "TRANS next(agenty) = agenty + dy;"
 
-encodeObjectPositions :: [(Int, Int)] -> String
-encodeObjectPositions p = join " | " ["x="<+x<+" & "<+"y="<+y\\(x, y)<-p]
+encodeBoxInit :: [(Int,Int)] -> String
+encodeBoxInit bs = join " &\n" [
+       "\tb" <+ i <+ "x=" <+ x <+ " & " <+
+       "b" <+ i <+ "y=" <+ y
+       \\(x, y)<-bs & i<-[0..]]
 
-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
+encodeBoxVars :: [Int] Int Int -> String
+encodeBoxVars p mx my = join "\n" 
+       ["\tb" <+ i <+ "x: 0.." <+ mx <+ ";\n" <+
+       "\tb" <+ i <+ "y: 0.." <+ my <+ ";" \\ i<-p]
+       
+encodeBoxPositions :: [Int] [(Int, Int)] -> String
+encodeBoxPositions bs ps = join "\n" [
+       "INVAR " <+ encodeObPosition ("b" <+ b) ps <+ ";"\\b<-bs]
 
-encodeBoxes :: [(Int, Int)] -> String
-encodeBoxes p = join "\n" 
-       ["\tb" <+ i <+ ": ob(" <+ bx <+ ", " <+ by <+ ", movement);"
-       \\(bx, by)<-p & i<-[0..]]
+encodeBoxMovement :: [Int] -> String
+encodeBoxMovement bs = join "\n" $ map ebm bs
+       where
+               ebm :: Int -> String
+               ebm i =
+                       "TRANS next(b" <+ i <+ "x) = case\n" <+
+                       "\t\tnext(agentx) = b" <+ i <+ "x & " <+
+                       "next(agenty) = b" <+ i <+ "y: b" <+ i <+ "x + dx;\n" <+
+                       "\t\tTRUE: b" <+ i <+ "x;\n" <+
+                       "\tesac;\n" <+
+                       "TRANS next(b" <+ i <+ "y) = case\n" <+
+                       "\t\tnext(agentx) = b" <+ i <+ "x & " <+
+                       "next(agenty) = b" <+ i <+ "y: b" <+ i <+ "y + dy;\n" <+
+                       "\t\tTRUE: b" <+ i <+ "y;\n" <+
+                       "\tesac;"