puzzle: CONTEXT =
BEGIN
% I have 3 containers with capacity 8,5,3 gallons;
% Initially, the 8-gallon container is full; rest are empty
% Can I get into a state where one container has exactly 1 gallon?
% I can pour liquid from one container to the other, say A to B,
% s.t. either A becomes empty, or B becomes full
puzzle: MODULE =
BEGIN
LOCAL x,y,z:NATURAL
INITIALIZATION
x=8; y=0; z=0;
TRANSITION
[
y < 5 AND x' >= 0 -->
y' = 5; x' = x - (5-y);
[]
y < 5 AND z' >= 0 -->
y' = 5; z' = z - (5-y);
[]
y < 5 AND y' <= 5 -->
y' = y + x; x' = 0;
[]
y < 5 AND z <= (5-y) -->
y' = y + z; z' = 0;
[]
z < 3 AND x' >= 0 -->
z' = 3; x' = x - (3-z);
[]
z < 3 AND y' >= 0 -->
z' = 3; y' = y - (3-z);
[]
z < 3 AND z' <= 3 -->
z' = z + x; x' = 0;
[]
z < 3 AND z' <= 3 -->
z' = z + y; y' = 0;
[]
x < 8 AND z' >= 0 -->
x' = 8; z' = z - (8-x);
[]
x < 8 AND y' >= 0 -->
x' = 8; y' = y - (8-x);
[]
x < 8 AND x' <= 8 -->
x' = x + y; y' = 0;
[]
x < 8 AND x' <= 8 -->
x' = x + z; z' = 0;
]
END ;
% sal-inf-bmc collatz wrong
check1 : THEOREM
puzzle |- G( NOT(x=1) ) ;
check4 : THEOREM
puzzle |- G( NOT(x=4) ) ;
END