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",
+ encodeObVar "agent" maxX maxY,
+ join "\n" [encodeObVar ("b" <+ i) maxX maxY\\i<-boxnums],
"\tmovement: {left, up, right, down, finished};",
- "\tagent: " <+ encodeAgent annot,
- encodeBoxes boxes,
-
- "DEFINE",
- "\tdx := case",
+ "--Handy variable for deltas",
+ deltaDefine,
+ "--Initial values",
+ "INIT",
+ encodeObInit "agent" agent <+ " &",
+ join " &\n" [encodeObInit ("b" <+ i) p\\p<-boxes & i<-[0..]],
+ "--Agent not on the box",
+ "INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
+ "--Allowed box positions on the field",
+ join "\n" ["INVAR "<+encodeObPosition ("b"<+b) legalPos<+";"\\b<-boxnums],
+ "--Box not on box",
+ encodeBoxOnBoxes (indexList boxes),
+ "--Allowed agent positions",
+ "INVAR " <+ encodeObPosition "agent" legalPos,
+ "--Goal state",
+ "INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
+ "",
+ encodeObMovement "agent",
+ encodeBoxMovement boxnums,
+ "CTLSPEC ! EF (movement = finished);",
+
+ ""]
+ where
+ targetPos = getTargets annot
+ boxes = getBoxes annot
+ boxnums = indexList boxes
+ agent = hd $ getAgents annot
+ legalPos = legalPositions annot
+ annot = annotate p
+ (maxX, maxY) = getMetrics annot
+
+deltaDefine :: String
+deltaDefine = join "\n" [
+ "DEFINE dx := case",
"\t\tmovement = left : -1;",
"\t\tmovement = right: +1;",
"\t\tTRUE: 0;",
"\t\tmovement = up : -1;",
"\t\tmovement = down: +1;",
"\t\tTRUE: 0;",
- "\tesac;",
-
- "INVAR (" <+ encodeGoalState (indexList boxes) targetPos <+
- ") <-> movement = finished;",
- "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)"
- ]
- where
- targetPos = getTargets annot
- boxes = getBoxes annot
- legalPos = legalPositions annot
- annot = annotate p
- (maxX, maxY) = getMetrics annot
+ "\tesac;"]
//THIS IS NAIVE AND SHOULD BE IMPROVED
legalPositions :: AnnotatedSokoban -> [(Int, Int)]
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]
(<+) 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)
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]
+
+encodeObMovement :: String -> String
+encodeObMovement s = "TRANS next(" <+ s <+ "x) = " <+ s <+ "x + dx;\n" <+
+ "TRANS next(" <+ s <+ "y) = " <+ s <+ "y + dy;"
+
+encodeObPosition :: String [(Int, Int)] -> String
+encodeObPosition b p = join " |\n\t" [forThisX b x p\\x<-removeDup $ map fst p]
+ where
+ forThisX :: String Int [(Int, Int)] -> String
+ forThisX s cx p = "(" <+ s <+ "x=" <+ cx <+ " & (" <+
+ join " | " [s <+ "y=" <+ y \\(x, y)<-p | x == cx] <+ "))"
-encodeObjectPositions :: [(Int, Int)] -> String
-encodeObjectPositions p = join " | " ["x="<+x<+" & "<+"y="<+y\\(x, y)<-p]
+encodeObInit :: String (Int, Int) -> String
+encodeObInit s (x, y) = "\t" <+ s <+ "x=" <+ x <+ " & " <+ s <+ "y=" <+ y
-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
+encodeObVar :: String Int Int -> String
+encodeObVar s mx my = "\t" <+ s <+ "x: 0.." <+ mx <+ ";\n" <+
+ "\t" <+ s <+ "y: 0.." <+ my <+ ";\n"
-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;"
repositories / mc1516pa.git / blobdiff