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