puzzleNew: 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 INV(xold:NATURAL, xnew:NATURAL, limit:NATURAL): BOOLEAN = (xold >= 0 AND xold <= limit AND xnew >= 0 AND xnew <= limit) ; INVALL(xold:NATURAL, yold:NATURAL, zold: NATURAL, xnew: NATURAL, ynew: NATURAL, znew: NATURAL): BOOLEAN = (INV(xold, xnew, 8) AND INV(yold,ynew,5) AND INV(zold,znew,3) AND xnew + ynew + znew = 8 AND ( (xnew = xold AND (ynew = 0 OR ynew = 5 OR znew = 0 OR znew = 3)) OR (ynew = yold AND (xnew = 0 OR xnew = 8 OR znew = 0 OR znew = 3)) OR (znew = zold AND (xnew = 0 OR xnew = 8 OR ynew = 0 OR ynew = 5)) ) ); puzzle: MODULE = BEGIN LOCAL x,y,z:NATURAL INITIALIZATION x=8; y=0; z=0; TRANSITION [ INVALL(x, y, z, x', y', z') --> x' IN { u: NATURAL | TRUE }; y' IN { u: NATURAL | TRUE }; z' IN { u: NATURAL | TRUE }; ] END ; % sal-inf-bmc collatz wrong check1 : THEOREM puzzle |- G( NOT(x=1) ) ; check4 : THEOREM puzzle |- G( NOT(x=4) ) ; END