"--Agent not on the box",
"INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
"--Box not on box",
- encodeBoxOnBoxes (indexList boxes),
+ encodeBoxOnBoxes boxnums,
"--Goal state",
"INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
- "",
+ "--Agent movement",
encodeObMovement "agent",
+ "--Box movement",
encodeBoxMovement boxnums,
"CTLSPEC ! EF (movement = finished);",