3 max1:=144; max2:=72; max3:=16;
5 b1: 0..max1; b2: 0..max2; b3: 0..max3;
10 (next(b1)=0 & next(b2)=b2 & next(b3)=b3) |
12 (next(b1)=b1 & next(b2)=0 & next(b3)=b3) |
14 (next(b1)=b1 & next(b2)=b2 & next(b3)=0) |
16 (next(b1)=max1 & next(b2)=b2 & next(b3)=b3) |
18 (next(b1)=b1 & next(b2)=max2 & next(b3)=b3) |
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) &
25 -- Empty bottle 1 in 3
26 ( next(b1)=b1 - min(max3 - b3, b1) &
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) &
33 -- Empty bottle 2 in 3
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) &
40 next(b3)=b3 - min(max1 - b1, b3))
41 LTLSPEC G !(b1=8 & b2=11)