a2/src/2b.smv

   1 MODULE main
   2 DEFINE
   3 max1:=144; max2:=80; max3:=16;
   4 VAR
   5 b1: 0..max1; b2: 0..max2; b3: 0..max3;
   6 INIT
   7 b1=3 & b2=0 & b3=0
   8 TRANS
   9 -- Empty bottle 1
  10 (next(b1)=0 & next(b2)=b2 & next(b3)=b3) |
  11 -- Empty bottle 2
  12 (next(b1)=b1 & next(b2)=0 & next(b3)=b3) |
  13 -- Empty bottle 3
  14 (next(b1)=b1 & next(b2)=b2 & next(b3)=0) |
  15 -- Fill bottle 1
  16 (next(b1)=max1 & next(b2)=b2 & next(b3)=b3) |
  17 -- Fill bottle 2
  18 (next(b1)=b1 & next(b2)=max2 & next(b3)=b3) |
  19 -- Fill bottle 3
  20 (next(b1)=b1 & next(b2)=b2 & next(b3)=max3) |
  21 -- Empty bottle 1 in 2
  22 (       next(b1)=b1 - min(max2 - b2, b1) &
  23         next(b2)=b2 + min(max2 - b2, b1) &
  24         next(b3)=b3) |
  25 -- Empty bottle 1 in 3
  26 (       next(b1)=b1 - min(max3 - b3, b1) &
  27         next(b2)=b2 &
  28         next(b3)=b3 + min(max3 - b3, b1)) |
  29 -- Empty bottle 2 in 1
  30 (       next(b1)=b1 + min(max1 - b1, b2) &
  31         next(b2)=b2 - min(max1 - b1, b2) &
  32         next(b3)=b3) |
  33 -- Empty bottle 2 in 3
  34 (       next(b1)=b1 &
  35         next(b2)=b2 - min(max3 - b3, b2) &
  36         next(b3)=b3 + min(max3 - b3, b2)) |
  37 -- Empty bottle 3 in 1
  38 (       next(b1)=b1 + min(max1 - b1, b3) &
  39         next(b2)=b2 &
  40         next(b3)=b3 - min(max1 - b1, b3))
  41 LTLSPEC G !(b1=8 & b2=11)