models/489-object.smv

   1 MODULE ob(ix, iy)
   2 VAR
   3         x: 0..7;
   4         y: 0..7;
   5 INIT x=ix & y=iy
   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))
  13
  14 MODULE main
  15 VAR
  16         agent: ob(4, 3);
  17         b0: ob(2, 2);
  18         b1: ob(3, 2);
  19         b2: ob(3, 5);
  20         b3: ob(4, 5);
  21         movement: {left, up, right, down, finished};
  22 --Handy variable for deltas
  23 DEFINE dx := case
  24                 movement = left : -1;
  25                 movement = right: +1;
  26                 TRUE:              0;
  27         esac;
  28         dy := case
  29                 movement = up  : -1;
  30                 movement = down: +1;
  31                 TRUE:             0;
  32         esac;
  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);
  38 --Box not on box
  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) &
  42         TRUE;
  43 --Goal state
  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;
  68 --Agent movement
  69 TRANS next(agent.x) = agent.x + dx & next(agent.y) = agent.y + dy;
  70 --Box movement
  71 TRANS next(b0.x) = case
  72                 next(agent.x) = b0.x & next(agent.y) = b0.y: b0.x + dx;
  73                 TRUE: b0.x;
  74         esac;
  75 TRANS next(b0.y) = case
  76                 next(agent.x) = b0.x & next(agent.y) = b0.y: b0.y + dy;
  77                 TRUE: b0.y;
  78         esac;
  79 TRANS next(b1.x) = case
  80                 next(agent.x) = b1.x & next(agent.y) = b1.y: b1.x + dx;
  81                 TRUE: b1.x;
  82         esac;
  83 TRANS next(b1.y) = case
  84                 next(agent.x) = b1.x & next(agent.y) = b1.y: b1.y + dy;
  85                 TRUE: b1.y;
  86         esac;
  87 TRANS next(b2.x) = case
  88                 next(agent.x) = b2.x & next(agent.y) = b2.y: b2.x + dx;
  89                 TRUE: b2.x;
  90         esac;
  91 TRANS next(b2.y) = case
  92                 next(agent.x) = b2.x & next(agent.y) = b2.y: b2.y + dy;
  93                 TRUE: b2.y;
  94         esac;
  95 TRANS next(b3.x) = case
  96                 next(agent.x) = b3.x & next(agent.y) = b3.y: b3.x + dx;
  97                 TRUE: b3.x;
  98         esac;
  99 TRANS next(b3.y) = case
 100                 next(agent.x) = b3.x & next(agent.y) = b3.y: b3.y + dy;
 101                 TRUE: b3.y;
 102         esac;
 103 CTLSPEC ! EF (movement = finished);
 104