MACHINE Mondex1 /* Michael Butler */ SETS PURSE = {P1,P2,P3} CONSTANTS total PROPERTIES total:NAT & total=5 VARIABLES purse, value INVARIANT purse : POW(PURSE) & value : purse --> (0..total) & SIGMA(p).( p:purse | value(p) ) = total INITIALISATION purse := {P1} || value := { P1 |-> total } OPERATIONS AddPurse = ANY p WHERE p : (PURSE-purse) THEN purse := purse\/{p} || value(p) := 0 END; TransferOk( p1, p2, a ) = PRE p1:PURSE & p2:PURSE & a:NATURAL THEN SELECT p1:purse & p2:purse & p1/=p2 & 0= a THEN value := value <+ { p1 |-> value(p1)-a, p2 |-> value(p2)+a } END END ; TransferLost( p1, p2, a ) = PRE p1:PURSE & p2:PURSE & a:NATURAL THEN SELECT p1:purse & p2:purse & p1/=p2 & 0= a THEN skip END END END