repositories
/
mc1516pa.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
screen shrinking done
[mc1516pa.git]
/
code
/
SokobanObjectwise.icl
diff --git
a/code/SokobanObjectwise.icl
b/code/SokobanObjectwise.icl
index
6c65c6d
..
656fad8
100644
(file)
--- a/
code/SokobanObjectwise.icl
+++ b/
code/SokobanObjectwise.icl
@@
-41,11
+41,12
@@
encode p = join "\n" [
"--Agent not on the box",
"INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
"--Box not on box",
"--Agent not on the box",
"INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
"--Box not on box",
-
encodeBoxOnBoxes (indexList boxes)
,
+
"INVAR " <+ encodeBoxOnBoxes boxnums <+ ";"
,
"--Goal state",
"INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
"--Goal state",
"INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
- "",
+ "
--Agent movement
",
encodeObMovement "agent",
encodeObMovement "agent",
+ "--Box movement",
encodeBoxMovement boxnums,
"CTLSPEC ! EF (movement = finished);",
encodeBoxMovement boxnums,
"CTLSPEC ! EF (movement = finished);",
@@
-115,8
+116,8
@@
encodeGoalState boxes targets = "(" <+
encodeBoxOnBoxes :: [Int] -> String
encodeBoxOnBoxes [] = ""
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
encodeBoxOnBoxes bs
where
encodeBoxOnBox :: Int [Int] -> String
@@
-128,8
+129,8
@@
encodeAgentNotOnBox bs = join " &\n\t" [
"!(b" <+ i <+ ".x = agent.x & b" <+ i <+ ".y = agent.y)"\\i<-bs]
encodeObMovement :: String -> 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]
encodeObPosition :: [(Int, Int)] -> String
encodeObPosition p = join " |\n\t" [forThisX x p\\x<-removeDup $ map fst p]