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