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