+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 = 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;"
+
+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(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(agent.x) = b" <+ i <+ ".x & " <+
+ "next(agent.y) = b" <+ i <+ ".y: b" <+ i <+ ".y + dy;\n" <+
+ "\t\tTRUE: b" <+ i <+ ".y;\n" <+
+ "\tesac;"