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