added model

diff --git a/Models/489-coord.smv b/models/489-coord.smv
similarity index 100%
rename from Models/489-coord.smv
rename to models/489-coord.smv

diff --git a/models/489-object.smv b/models/489-object.smv
new file mode 100644 (file)
index 0000000..2acc7fc
--- /dev/null
+++ b/models/489-object.smv
@@ -0,0 +1,104 @@
+MODULE ob(ix, iy)
+VAR
+       x: 0..7;
+       y: 0..7;
+INIT x=ix & y=iy
+INVAR (x=0 & (y=0 | y=5 | y=6 | y=7)) |
+       (x=1 & (y=0 | y=2 | y=3 | y=7)) |
+       (x=3 & (y=1 | y=2 | y=3 | y=5)) |
+       (x=4 & (y=1 | y=2 | y=3 | y=4 | y=5 | y=6)) |
+       (x=5 & (y=1 | y=2 | y=4 | y=5 | y=6)) |
+       (x=2 & (y=2 | y=3 | y=4 | y=5 | y=7)) |
+       (x=6 & (y=2 | y=3 | y=4))
+
+MODULE main
+VAR
+       agent: ob(4, 3);
+       b0: ob(2, 2);
+       b1: ob(3, 2);
+       b2: ob(3, 5);
+       b3: ob(4, 5);
+       movement: {left, up, right, down, finished};
+--Handy variable for deltas
+DEFINE dx := case
+               movement = left : -1;
+               movement = right: +1;
+               TRUE:              0;
+       esac;
+       dy := case
+               movement = up  : -1;
+               movement = down: +1;
+               TRUE:             0;
+       esac;
+--Agent not on the box
+INVAR !(b0.x = agent.x & b0.y = agent.y) &
+       !(b1.x = agent.x & b1.y = agent.y) &
+       !(b2.x = agent.x & b2.y = agent.y) &
+       !(b3.x = agent.x & b3.y = agent.y);
+--Box not on box
+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) &
+       !(b1.x=b2.x &b1.y=b2.y) & !(b1.x=b3.x &b1.y=b3.y) &
+       !(b2.x=b3.x &b2.y=b3.y) &
+       TRUE;
+--Goal state
+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) |
+       (b1.x = 4 & b1.y = 2 & b0.x = 5 & b0.y = 2 & b2.x = 3 & b2.y = 3 & b3.x = 4 & b3.y = 5) |
+       (b2.x = 4 & b2.y = 2 & b1.x = 5 & b1.y = 2 & b0.x = 3 & b0.y = 3 & b3.x = 4 & b3.y = 5) |
+       (b1.x = 4 & b1.y = 2 & b2.x = 5 & b2.y = 2 & b0.x = 3 & b0.y = 3 & b3.x = 4 & b3.y = 5) |
+       (b2.x = 4 & b2.y = 2 & b0.x = 5 & b0.y = 2 & b1.x = 3 & b1.y = 3 & b3.x = 4 & b3.y = 5) |
+       (b0.x = 4 & b0.y = 2 & b2.x = 5 & b2.y = 2 & b1.x = 3 & b1.y = 3 & b3.x = 4 & b3.y = 5) |
+       (b3.x = 4 & b3.y = 2 & b2.x = 5 & b2.y = 2 & b1.x = 3 & b1.y = 3 & b0.x = 4 & b0.y = 5) |
+       (b2.x = 4 & b2.y = 2 & b3.x = 5 & b3.y = 2 & b1.x = 3 & b1.y = 3 & b0.x = 4 & b0.y = 5) |
+       (b2.x = 4 & b2.y = 2 & b1.x = 5 & b1.y = 2 & b3.x = 3 & b3.y = 3 & b0.x = 4 & b0.y = 5) |
+       (b3.x = 4 & b3.y = 2 & b1.x = 5 & b1.y = 2 & b2.x = 3 & b2.y = 3 & b0.x = 4 & b0.y = 5) |
+       (b1.x = 4 & b1.y = 2 & b3.x = 5 & b3.y = 2 & b2.x = 3 & b2.y = 3 & b0.x = 4 & b0.y = 5) |
+       (b1.x = 4 & b1.y = 2 & b2.x = 5 & b2.y = 2 & b3.x = 3 & b3.y = 3 & b0.x = 4 & b0.y = 5) |
+       (b3.x = 4 & b3.y = 2 & b0.x = 5 & b0.y = 2 & b1.x = 3 & b1.y = 3 & b2.x = 4 & b2.y = 5) |
+       (b0.x = 4 & b0.y = 2 & b3.x = 5 & b3.y = 2 & b1.x = 3 & b1.y = 3 & b2.x = 4 & b2.y = 5) |
+       (b0.x = 4 & b0.y = 2 & b1.x = 5 & b1.y = 2 & b3.x = 3 & b3.y = 3 & b2.x = 4 & b2.y = 5) |
+       (b3.x = 4 & b3.y = 2 & b1.x = 5 & b1.y = 2 & b0.x = 3 & b0.y = 3 & b2.x = 4 & b2.y = 5) |
+       (b1.x = 4 & b1.y = 2 & b3.x = 5 & b3.y = 2 & b0.x = 3 & b0.y = 3 & b2.x = 4 & b2.y = 5) |
+       (b1.x = 4 & b1.y = 2 & b0.x = 5 & b0.y = 2 & b3.x = 3 & b3.y = 3 & b2.x = 4 & b2.y = 5) |
+       (b3.x = 4 & b3.y = 2 & b0.x = 5 & b0.y = 2 & b2.x = 3 & b2.y = 3 & b1.x = 4 & b1.y = 5) |
+       (b0.x = 4 & b0.y = 2 & b3.x = 5 & b3.y = 2 & b2.x = 3 & b2.y = 3 & b1.x = 4 & b1.y = 5) |
+       (b0.x = 4 & b0.y = 2 & b2.x = 5 & b2.y = 2 & b3.x = 3 & b3.y = 3 & b1.x = 4 & b1.y = 5) |
+       (b3.x = 4 & b3.y = 2 & b2.x = 5 & b2.y = 2 & b0.x = 3 & b0.y = 3 & b1.x = 4 & b1.y = 5) |
+       (b2.x = 4 & b2.y = 2 & b3.x = 5 & b3.y = 2 & b0.x = 3 & b0.y = 3 & b1.x = 4 & b1.y = 5) |
+       (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;
+--Agent movement
+TRANS next(agent.x) = agent.x + dx & next(agent.y) = agent.y + dy;
+--Box movement
+TRANS next(b0.x) = case
+               next(agent.x) = b0.x & next(agent.y) = b0.y: b0.x + dx;
+               TRUE: b0.x;
+       esac;
+TRANS next(b0.y) = case
+               next(agent.x) = b0.x & next(agent.y) = b0.y: b0.y + dy;
+               TRUE: b0.y;
+       esac;
+TRANS next(b1.x) = case
+               next(agent.x) = b1.x & next(agent.y) = b1.y: b1.x + dx;
+               TRUE: b1.x;
+       esac;
+TRANS next(b1.y) = case
+               next(agent.x) = b1.x & next(agent.y) = b1.y: b1.y + dy;
+               TRUE: b1.y;
+       esac;
+TRANS next(b2.x) = case
+               next(agent.x) = b2.x & next(agent.y) = b2.y: b2.x + dx;
+               TRUE: b2.x;
+       esac;
+TRANS next(b2.y) = case
+               next(agent.x) = b2.x & next(agent.y) = b2.y: b2.y + dy;
+               TRUE: b2.y;
+       esac;
+TRANS next(b3.x) = case
+               next(agent.x) = b3.x & next(agent.y) = b3.y: b3.x + dx;
+               TRUE: b3.x;
+       esac;
+TRANS next(b3.y) = case
+               next(agent.x) = b3.x & next(agent.y) = b3.y: b3.y + dy;
+               TRUE: b3.y;
+       esac;
+CTLSPEC ! EF (movement = finished);
+