mirror of https://github.com/vacp2p/research.git
61 lines
1.5 KiB
Plaintext
61 lines
1.5 KiB
Plaintext
|
------------------------------- MODULE gossip -------------------------------
|
||
|
|
|
||
|
|
EXTENDS Integers
|
||
|
|
|
||
|
|
(*--algorithm gossip
|
||
|
|
variables
|
||
|
|
people = {"alice", "bob"},
|
||
|
|
acc = [p \in people |-> 5],
|
||
|
|
sender = "alice",
|
||
|
|
receiver = "bob",
|
||
|
|
amount = 3;
|
||
|
|
|
||
|
|
define
|
||
|
|
NoOverdrafts == \A p \in people: acc[p] >= 0
|
||
|
|
end define;
|
||
|
|
|
||
|
|
begin
|
||
|
|
Withdraw:
|
||
|
|
acc[sender] := acc[sender] - amount;
|
||
|
|
Deposit:
|
||
|
|
acc[receiver] := acc[receiver] + amount;
|
||
|
|
end algorithm;*)
|
||
|
|
\* BEGIN TRANSLATION
|
||
|
|
VARIABLES people, acc, sender, receiver, amount, pc
|
||
|
|
|
||
|
|
(* define statement *)
|
||
|
|
NoOverdrafts == \A p \in people: acc[p] >= 0
|
||
|
|
|
||
|
|
|
||
|
|
vars == << people, acc, sender, receiver, amount, pc >>
|
||
|
|
|
||
|
|
Init == (* Global variables *)
|
||
|
|
/\ people = {"alice", "bob"}
|
||
|
|
/\ acc = [p \in people |-> 5]
|
||
|
|
/\ sender = "alice"
|
||
|
|
/\ receiver = "bob"
|
||
|
|
/\ amount = 3
|
||
|
|
/\ pc = "Withdraw"
|
||
|
|
|
||
|
|
Withdraw == /\ pc = "Withdraw"
|
||
|
|
/\ acc' = [acc EXCEPT ![sender] = acc[sender] - amount]
|
||
|
|
/\ pc' = "Deposit"
|
||
|
|
/\ UNCHANGED << people, sender, receiver, amount >>
|
||
|
|
|
||
|
|
Deposit == /\ pc = "Deposit"
|
||
|
|
/\ acc' = [acc EXCEPT ![receiver] = acc[receiver] + amount]
|
||
|
|
/\ pc' = "Done"
|
||
|
|
/\ UNCHANGED << people, sender, receiver, amount >>
|
||
|
|
|
||
|
|
Next == Withdraw \/ Deposit
|
||
|
|
\/ (* Disjunct to prevent deadlock on termination *)
|
||
|
|
(pc = "Done" /\ UNCHANGED vars)
|
||
|
|
|
||
|
|
Spec == Init /\ [][Next]_vars
|
||
|
|
|
||
|
|
Termination == <>(pc = "Done")
|
||
|
|
|
||
|
|
\* END TRANSLATION
|
||
|
|
|
||
|
|
=============================================================================
|