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
= snd (fclose io w)
encode :: SokobanPuzzle -> String
-encode p = foldr ((+++) o (+++) "\n") "" ([
- "MODULE",
- "main",
- "VAR":encodeBoxes p maxX maxY])
+encode p = join "\n" [
+ "MODULE main",
+ "VAR",
+ encodeAgentVars maxX maxY,
+ encodeBoxVars (indexList boxes) maxX maxY,
+ "\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 <+ ";",
+ "--Agent not on the box",
+ "INVAR " <+ encodeAgentNotOnBox (indexList boxes) <+ ";",
+ "--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
-:: 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] ++
+getAgents :: AnnotatedSokoban -> [(Int, Int)]
+getAgents p = [(x, y)\\(x, y, Agent)<-p] ++ [(x, y)\\(x, y, TargetAgent)<-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 :: AnnotatedSokoban -> [(Int, Int)]
+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) <+ ")<->movement=finished"
+ 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]
+
+encodeBoxOnBoxes :: [Int] -> String
+encodeBoxOnBoxes [] = ""
+encodeBoxOnBoxes [b] = ""
+encodeBoxOnBoxes [b:bs] = "INVAR " <+ encodeBoxOnBox b bs <+ ";\n" <+
+ 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]
+
+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]
+
+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