+ "--Handy variable for deltas",
+ deltaDefine,
+ "--Agent not on the box",
+ "INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
+ "--Box not on box",
+ "INVAR " <+ encodeBoxOnBoxes boxnums <+ ";",
+ "--Goal state",
+ "INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
+ "--Agent movement",
+ encodeObMovement "agent",
+ "--Box movement",
+ encodeBoxMovement boxnums,
+ "CTLSPEC ! EF (movement = finished);",
+
+ ""]
+ where
+ targetPos = getTargets annot
+ boxes = getBoxes annot
+ boxnums = indexList boxes
+ agent = hd $ getAgents annot
+ legalPos = legalPositions annot
+ annot = annotate p
+ (maxX, maxY) = getMetrics annot
+
+declareObject :: (Int, Int) -> String
+declareObject (x, y) = "ob(" <+ x <+ ", " <+ y <+ ");"
+
+deltaDefine :: String
+deltaDefine = join "\n" [
+ "DEFINE dx := case",