encode :: SokobanPuzzle -> String
encode p = join "\n" [
+ "MODULE ob(ix, iy)",
+ "VAR",
+ "\tx: 0.." <+ maxX <+ ";",
+ "\ty: 0.." <+ maxY <+ ";",
+ "INIT x=ix & y=iy",
+ "INVAR " <+ encodeObPosition legalPos,
+ "",
"MODULE main",
"VAR",
- encodeAgentVars maxX maxY,
- encodeBoxVars (indexList boxes) maxX maxY,
+ "\tagent: " <+ declareObject agent,
+ join "\n" ["\tb" <+ i <+ ": " <+ declareObject b\\i<-boxnums & b<-boxes],
"\tmovement: {left, up, right, down, finished};",
- "",
- "DEFINE dx := 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;",
- "",
- "INIT",
- encodeAgentInit agent <+ " &",
- encodeBoxInit boxes <+ ";",
+ "--Handy variable for deltas",
+ deltaDefine,
"--Agent not on the box",
- "INVAR " <+ encodeAgentNotOnBox (indexList boxes) <+ ";",
- "--Allowed box positions on the field",
- encodeBoxPositions (indexList boxes) legalPos,
+ "INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
"--Box not on box",
- encodeBoxOnBoxes (indexList boxes),
- "--Allowed agent positions",
- "INVAR " <+ encodeAgentPositions legalPos,
+ "INVAR " <+ encodeBoxOnBoxes boxnums <+ ";",
"--Goal state",
- "INVAR " <+ encodeGoalState (indexList boxes) targetPos <+ ";",
- "",
- encodeAgentMovement,
- encodeBoxMovement (indexList boxes),
+ "INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
+ "--Agent movement",
+ encodeObMovement "agent",
+ "--Box movement",
+ 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
+declareObject :: (Int, Int) -> String
+declareObject (x, y) = "ob(" <+ x <+ ", " <+ y <+ ");"
+
+deltaDefine :: String
+deltaDefine = join "\n" [
+ "DEFINE dx := 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;"]
+
//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]
encodeOneGoal` :: [((Int, Int), Int)] -> [String]
encodeOneGoal` [] = []
encodeOneGoal` [((x, y), b):xs] = [
- "b" <+ b <+ "x = " <+ x <+ " & " <+
- "b" <+ b <+ "y = " <+ y:encodeOneGoal` xs]
+ "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 [b] = "TRUE"
+encodeBoxOnBoxes [b:bs] = encodeBoxOnBox b bs <+ " &\n\t" <+
encodeBoxOnBoxes bs
where
encodeBoxOnBox :: Int [Int] -> String
- encodeBoxOnBox x bs = join " & " ["!(b" <+ x <+ "x=b" <+ b <+ "x &" <+
- "b" <+ x <+ "y=b" <+ b <+ "y)"\\b<-bs]
+ 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 = 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;"
-
-encodeBoxInit :: [(Int,Int)] -> String
-encodeBoxInit bs = join " &\n" [
- "\tb" <+ i <+ "x=" <+ x <+ " & " <+
- "b" <+ i <+ "y=" <+ y
- \\(x, y)<-bs & i<-[0..]]
-
-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]
+ "!(b" <+ i <+ ".x = agent.x & b" <+ i <+ ".y = agent.y)"\\i<-bs]
+
+encodeObMovement :: String -> String
+encodeObMovement s = "TRANS next(" <+ s <+ ".x) = " <+ s <+ ".x + dx & " <+
+ "next(" <+ s <+ ".y) = " <+ s <+ ".y + dy;"
+
+encodeObPosition :: [(Int, Int)] -> String
+encodeObPosition p = join " |\n\t" [forThisX x p\\x<-removeDup $ map fst p]
+ where
+ forThisX :: Int [(Int, Int)] -> String
+ forThisX cx p = "(x=" <+ cx <+ " & (" <+
+ join " | " ["y=" <+ y \\(x, y)<-p | x == cx] <+ "))"
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" <+
+ 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 + 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" <+
+ "TRANS next(b" <+ i <+ ".y) = case\n" <+
+ "\t\tnext(agent.x) = b" <+ i <+ ".x & " <+
+ "next(agent.y) = b" <+ i <+ ".y: b" <+ i <+ ".y + dy;\n" <+
+ "\t\tTRUE: b" <+ i <+ ".y;\n" <+
"\tesac;"
repositories / mc1516pa.git / blobdiff