L'hôtelier, le groom et les clients (où est passé l'euro, suite)

MACHINE
HCG
SETS
ENTITE ={hotel, client, groom}; TYPE ={input, output}
VARIABLES
solde, montant
INVARIANT
montant : ENTITE * TYPE --> INTEGER &
solde = %ee. (ee : ENTITE montant(ee|-> input) - montant (ee |-> output)) & (
solde(hotel) + solde(client) + solde (groom)) = 0
INITIALISATION
/* solde, montant := ENTITE * {0}, (ENTITE*TYPE) * {0}*/
solde := {(hotel |-> 0),( client |-> 0), (groom |-> 0)}
montant := {((hotel |-> input)|-> 0), ((client |-> input) |-> 0), ((groom |-> input) |-> 0), ((hotel |-> output)|-> 0), ((client |-> output) |-> 0), ((groom |-> output) |-> 0)}
OPERATIONS
transaction(emetteur, recepteur, mt) =
PRE recepteur : ENTITE &
mt : INTEGER &
((mt + montant(recepteur |->input)) <-->output)) > MININT) &
((solde(emetteur) - mt) > MININT)
THEN
solde := solde \/ {(emetteur |-> solde(emetteur) - mt), (recepteur |-> solde(recepteur) + mt)} - {(emetteur |-> solde(emetteur)), (recepteur |-> solde(recepteur))}
montant := montant <+ {((recepteur|-> input) |->(montant(recepteur |->input) + mt)), ((emetteur |->output) |-> (montant(emetteur |-> output)+ mt ))}
END

END
P.S. attention ! certaines fontes ne "prennent" pas le "pipe" (en conséquence, il se peut que le symbole de maplet soit tronqué)