+ "--Handy variable for deltas",
+ deltaDefine,
+ "--Initial values",
+ "INIT",
+ encodeObInit "agent" agent <+ " &",
+ join " &\n" [encodeObInit ("b" <+ i) p\\p<-boxes & i<-[0..]],
+ "--Agent not on the box",
+ "INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
+ "--Allowed box positions on the field",
+ join "\n" ["INVAR "<+encodeObPosition ("b"<+b) legalPos<+";"\\b<-boxnums],
+ "--Box not on box",
+ encodeBoxOnBoxes (indexList boxes),
+ "--Allowed agent positions",
+ "INVAR " <+ encodeObPosition "agent" legalPos,
+ "--Goal state",
+ "INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
+ "",
+ encodeObMovement "agent",
+ 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
+
+deltaDefine :: String
+deltaDefine = join "\n" [
+ "DEFINE dx := case",