6 INVAR (x=0 & (y=0 | y=5 | y=6 | y=7)) |
7 (x=1 & (y=0 | y=2 | y=3 | y=7)) |
8 (x=3 & (y=1 | y=2 | y=3 | y=5)) |
9 (x=4 & (y=1 | y=2 | y=3 | y=4 | y=5 | y=6)) |
10 (x=5 & (y=1 | y=2 | y=4 | y=5 | y=6)) |
11 (x=2 & (y=2 | y=3 | y=4 | y=5 | y=7)) |
12 (x=6 & (y=2 | y=3 | y=4))
21 movement: {left, up, right, down, finished};
22 --Handy variable for deltas
33 --Agent not on the box
34 INVAR !(b0.x = agent.x & b0.y = agent.y) &
35 !(b1.x = agent.x & b1.y = agent.y) &
36 !(b2.x = agent.x & b2.y = agent.y) &
37 !(b3.x = agent.x & b3.y = agent.y);
39 INVAR !(b0.x=b1.x &b0.y=b1.y) & !(b0.x=b2.x &b0.y=b2.y) & !(b0.x=b3.x &b0.y=b3.y) &
40 !(b1.x=b2.x &b1.y=b2.y) & !(b1.x=b3.x &b1.y=b3.y) &
41 !(b2.x=b3.x &b2.y=b3.y) &
44 INVAR ((b0.x = 4 & b0.y = 2 & b1.x = 5 & b1.y = 2 & b2.x = 3 & b2.y = 3 & b3.x = 4 & b3.y = 5) |
45 (b1.x = 4 & b1.y = 2 & b0.x = 5 & b0.y = 2 & b2.x = 3 & b2.y = 3 & b3.x = 4 & b3.y = 5) |
46 (b2.x = 4 & b2.y = 2 & b1.x = 5 & b1.y = 2 & b0.x = 3 & b0.y = 3 & b3.x = 4 & b3.y = 5) |
47 (b1.x = 4 & b1.y = 2 & b2.x = 5 & b2.y = 2 & b0.x = 3 & b0.y = 3 & b3.x = 4 & b3.y = 5) |
48 (b2.x = 4 & b2.y = 2 & b0.x = 5 & b0.y = 2 & b1.x = 3 & b1.y = 3 & b3.x = 4 & b3.y = 5) |
49 (b0.x = 4 & b0.y = 2 & b2.x = 5 & b2.y = 2 & b1.x = 3 & b1.y = 3 & b3.x = 4 & b3.y = 5) |
50 (b3.x = 4 & b3.y = 2 & b2.x = 5 & b2.y = 2 & b1.x = 3 & b1.y = 3 & b0.x = 4 & b0.y = 5) |
51 (b2.x = 4 & b2.y = 2 & b3.x = 5 & b3.y = 2 & b1.x = 3 & b1.y = 3 & b0.x = 4 & b0.y = 5) |
52 (b2.x = 4 & b2.y = 2 & b1.x = 5 & b1.y = 2 & b3.x = 3 & b3.y = 3 & b0.x = 4 & b0.y = 5) |
53 (b3.x = 4 & b3.y = 2 & b1.x = 5 & b1.y = 2 & b2.x = 3 & b2.y = 3 & b0.x = 4 & b0.y = 5) |
54 (b1.x = 4 & b1.y = 2 & b3.x = 5 & b3.y = 2 & b2.x = 3 & b2.y = 3 & b0.x = 4 & b0.y = 5) |
55 (b1.x = 4 & b1.y = 2 & b2.x = 5 & b2.y = 2 & b3.x = 3 & b3.y = 3 & b0.x = 4 & b0.y = 5) |
56 (b3.x = 4 & b3.y = 2 & b0.x = 5 & b0.y = 2 & b1.x = 3 & b1.y = 3 & b2.x = 4 & b2.y = 5) |
57 (b0.x = 4 & b0.y = 2 & b3.x = 5 & b3.y = 2 & b1.x = 3 & b1.y = 3 & b2.x = 4 & b2.y = 5) |
58 (b0.x = 4 & b0.y = 2 & b1.x = 5 & b1.y = 2 & b3.x = 3 & b3.y = 3 & b2.x = 4 & b2.y = 5) |
59 (b3.x = 4 & b3.y = 2 & b1.x = 5 & b1.y = 2 & b0.x = 3 & b0.y = 3 & b2.x = 4 & b2.y = 5) |
60 (b1.x = 4 & b1.y = 2 & b3.x = 5 & b3.y = 2 & b0.x = 3 & b0.y = 3 & b2.x = 4 & b2.y = 5) |
61 (b1.x = 4 & b1.y = 2 & b0.x = 5 & b0.y = 2 & b3.x = 3 & b3.y = 3 & b2.x = 4 & b2.y = 5) |
62 (b3.x = 4 & b3.y = 2 & b0.x = 5 & b0.y = 2 & b2.x = 3 & b2.y = 3 & b1.x = 4 & b1.y = 5) |
63 (b0.x = 4 & b0.y = 2 & b3.x = 5 & b3.y = 2 & b2.x = 3 & b2.y = 3 & b1.x = 4 & b1.y = 5) |
64 (b0.x = 4 & b0.y = 2 & b2.x = 5 & b2.y = 2 & b3.x = 3 & b3.y = 3 & b1.x = 4 & b1.y = 5) |
65 (b3.x = 4 & b3.y = 2 & b2.x = 5 & b2.y = 2 & b0.x = 3 & b0.y = 3 & b1.x = 4 & b1.y = 5) |
66 (b2.x = 4 & b2.y = 2 & b3.x = 5 & b3.y = 2 & b0.x = 3 & b0.y = 3 & b1.x = 4 & b1.y = 5) |
67 (b2.x = 4 & b2.y = 2 & b0.x = 5 & b0.y = 2 & b3.x = 3 & b3.y = 3 & b1.x = 4 & b1.y = 5))<->movement=finished;
69 TRANS next(agent.x) = agent.x + dx & next(agent.y) = agent.y + dy;
71 TRANS next(b0.x) = case
72 next(agent.x) = b0.x & next(agent.y) = b0.y: b0.x + dx;
75 TRANS next(b0.y) = case
76 next(agent.x) = b0.x & next(agent.y) = b0.y: b0.y + dy;
79 TRANS next(b1.x) = case
80 next(agent.x) = b1.x & next(agent.y) = b1.y: b1.x + dx;
83 TRANS next(b1.y) = case
84 next(agent.x) = b1.x & next(agent.y) = b1.y: b1.y + dy;
87 TRANS next(b2.x) = case
88 next(agent.x) = b2.x & next(agent.y) = b2.y: b2.x + dx;
91 TRANS next(b2.y) = case
92 next(agent.x) = b2.x & next(agent.y) = b2.y: b2.y + dy;
95 TRANS next(b3.x) = case
96 next(agent.x) = b3.x & next(agent.y) = b3.y: b3.x + dx;
99 TRANS next(b3.y) = case
100 next(agent.x) = b3.x & next(agent.y) = b3.y: b3.y + dy;
103 CTLSPEC ! EF (movement = finished);