"--Agent not on the box",
"INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
"--Box not on box",
- encodeBoxOnBoxes (indexList boxes),
+ "INVAR " <+ encodeBoxOnBoxes boxnums <+ ";",
"--Goal state",
"INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
- "",
+ "--Agent movement",
encodeObMovement "agent",
+ "--Box movement",
encodeBoxMovement boxnums,
"CTLSPEC ! EF (movement = finished);",
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
"!(b" <+ i <+ ".x = agent.x & b" <+ i <+ ".y = agent.y)"\\i<-bs]
encodeObMovement :: String -> String
-encodeObMovement s = "TRANS next(" <+ s <+ ".x) = " <+ s <+ ".x + dx;\n" <+
- "TRANS next(" <+ s <+ ".y) = " <+ s <+ ".y + dy;"
+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]