-
-
Save claudiouzelac/af68b513714aed569d89f8b0862b3ef3 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-------------------------- MODULE multi_user_wire -------------------------- | |
EXTENDS Integers, Sequences | |
CONSTANTS Users, Servers, Accounts | |
MAX_MONEY == 20 | |
AtMostOneAdminPerOrg(users, orgs) == {roles \in [users -> {"user","admin"}]: | |
\A x,y \in users: (roles[x] = "admin" /\ roles[y] = "admin") => x = y} | |
(*--algorithm multi_user_wire | |
variables | |
balance \in [Accounts -> (0..MAX_MONEY)], | |
organizations \in [Users -> Accounts], | |
roles \in AtMostOneAdminPerOrg(Users, organizations), | |
is_idle = [u \in Users |-> TRUE]; | |
define | |
IdleUsers == {u \in Users: is_idle[u] } | |
NoOverdraft == \A a \in Accounts: balance[a] >= 0 | |
end define; | |
procedure SendWire(user, acc) | |
variables withdraw_amt | |
begin | |
CheckPerms: | |
if roles[user] /= "admin" \/ balance[organizations[user]] <= 0 then | |
return | |
else | |
SendMoney: | |
await is_idle[user]; | |
is_idle[user] := FALSE; | |
with amt \in (1..balance[organizations[user]]) do | |
withdraw_amt := amt; | |
end with; | |
DoWire: | |
balance[organizations[user]] := balance[organizations[user]] - withdraw_amt || | |
balance[acc] := balance[acc] + withdraw_amt; | |
is_idle[user] := TRUE; | |
return; | |
end if; | |
end procedure; | |
procedure ChangeAccountPermission(user, acc) begin | |
ChangePerm: | |
await is_idle[user]; | |
is_idle[user] := TRUE; | |
roles := [v \in Users |-> IF organizations[v] = acc THEN (IF user = v THEN "admin" ELSE "user") ELSE roles[v]]; | |
EndChangePerm: | |
is_idle[user] := TRUE; | |
return; | |
end procedure; | |
process server \in Servers | |
begin | |
Action: | |
\* BEGIN part shown in blog post. Some contortions have been done | |
\* to keep this part simple | |
while TRUE do | |
with u \in IdleUsers, a \in Accounts do | |
either | |
call SendWire(u, a); | |
or | |
call ChangeAccountPermission(u, a); | |
end either; | |
end with; | |
end while; | |
end process; | |
end algorithm;*) | |
\* BEGIN TRANSLATION | |
\* Parameter user of procedure SendWire at line 24 col 20 changed to user_ | |
\* Parameter acc of procedure SendWire at line 24 col 26 changed to acc_ | |
CONSTANT defaultInitValue | |
VARIABLES balance, organizations, roles, is_idle, pc, stack | |
(* define statement *) | |
IdleUsers == {u \in Users: is_idle[u] } | |
NoOverdraft == \A a \in Accounts: balance[a] >= 0 | |
VARIABLES user_, acc_, withdraw_amt, user, acc | |
vars == << balance, organizations, roles, is_idle, pc, stack, user_, acc_, | |
withdraw_amt, user, acc >> | |
ProcSet == (Servers) | |
Init == (* Global variables *) | |
/\ balance \in [Accounts -> (0..MAX_MONEY)] | |
/\ organizations \in [Users -> Accounts] | |
/\ roles \in AtMostOneAdminPerOrg(Users, organizations) | |
/\ is_idle = [u \in Users |-> TRUE] | |
(* Procedure SendWire *) | |
/\ user_ = [ self \in ProcSet |-> defaultInitValue] | |
/\ acc_ = [ self \in ProcSet |-> defaultInitValue] | |
/\ withdraw_amt = [ self \in ProcSet |-> defaultInitValue] | |
(* Procedure ChangeAccountPermission *) | |
/\ user = [ self \in ProcSet |-> defaultInitValue] | |
/\ acc = [ self \in ProcSet |-> defaultInitValue] | |
/\ stack = [self \in ProcSet |-> << >>] | |
/\ pc = [self \in ProcSet |-> "Action"] | |
CheckPerms(self) == /\ pc[self] = "CheckPerms" | |
/\ IF roles[user_[self]] /= "admin" \/ balance[organizations[user_[self]]] <= 0 | |
THEN /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] | |
/\ withdraw_amt' = [withdraw_amt EXCEPT ![self] = Head(stack[self]).withdraw_amt] | |
/\ user_' = [user_ EXCEPT ![self] = Head(stack[self]).user_] | |
/\ acc_' = [acc_ EXCEPT ![self] = Head(stack[self]).acc_] | |
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] | |
ELSE /\ pc' = [pc EXCEPT ![self] = "SendMoney"] | |
/\ UNCHANGED << stack, user_, acc_, | |
withdraw_amt >> | |
/\ UNCHANGED << balance, organizations, roles, is_idle, | |
user, acc >> | |
SendMoney(self) == /\ pc[self] = "SendMoney" | |
/\ is_idle[user_[self]] | |
/\ is_idle' = [is_idle EXCEPT ![user_[self]] = FALSE] | |
/\ \E amt \in (1..balance[organizations[user_[self]]]): | |
withdraw_amt' = [withdraw_amt EXCEPT ![self] = amt] | |
/\ pc' = [pc EXCEPT ![self] = "DoWire"] | |
/\ UNCHANGED << balance, organizations, roles, stack, user_, | |
acc_, user, acc >> | |
DoWire(self) == /\ pc[self] = "DoWire" | |
/\ balance' = [balance EXCEPT ![organizations[user_[self]]] = balance[organizations[user_[self]]] - withdraw_amt[self], | |
![acc_[self]] = balance[acc_[self]] + withdraw_amt[self]] | |
/\ is_idle' = [is_idle EXCEPT ![user_[self]] = TRUE] | |
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] | |
/\ withdraw_amt' = [withdraw_amt EXCEPT ![self] = Head(stack[self]).withdraw_amt] | |
/\ user_' = [user_ EXCEPT ![self] = Head(stack[self]).user_] | |
/\ acc_' = [acc_ EXCEPT ![self] = Head(stack[self]).acc_] | |
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] | |
/\ UNCHANGED << organizations, roles, user, acc >> | |
SendWire(self) == CheckPerms(self) \/ SendMoney(self) \/ DoWire(self) | |
ChangePerm(self) == /\ pc[self] = "ChangePerm" | |
/\ is_idle[user[self]] | |
/\ is_idle' = [is_idle EXCEPT ![user[self]] = TRUE] | |
/\ roles' = [v \in Users |-> IF organizations[v] = acc[self] THEN (IF user[self] = v THEN "admin" ELSE "user") ELSE roles[v]] | |
/\ pc' = [pc EXCEPT ![self] = "EndChangePerm"] | |
/\ UNCHANGED << balance, organizations, stack, user_, acc_, | |
withdraw_amt, user, acc >> | |
EndChangePerm(self) == /\ pc[self] = "EndChangePerm" | |
/\ is_idle' = [is_idle EXCEPT ![user[self]] = TRUE] | |
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] | |
/\ user' = [user EXCEPT ![self] = Head(stack[self]).user] | |
/\ acc' = [acc EXCEPT ![self] = Head(stack[self]).acc] | |
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] | |
/\ UNCHANGED << balance, organizations, roles, user_, | |
acc_, withdraw_amt >> | |
ChangeAccountPermission(self) == ChangePerm(self) \/ EndChangePerm(self) | |
Action(self) == /\ pc[self] = "Action" | |
/\ \E u \in IdleUsers: | |
\E a \in Accounts: | |
\/ /\ /\ acc_' = [acc_ EXCEPT ![self] = a] | |
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "SendWire", | |
pc |-> "Action", | |
withdraw_amt |-> withdraw_amt[self], | |
user_ |-> user_[self], | |
acc_ |-> acc_[self] ] >> | |
\o stack[self]] | |
/\ user_' = [user_ EXCEPT ![self] = u] | |
/\ withdraw_amt' = [withdraw_amt EXCEPT ![self] = defaultInitValue] | |
/\ pc' = [pc EXCEPT ![self] = "CheckPerms"] | |
/\ UNCHANGED <<user, acc>> | |
\/ /\ /\ acc' = [acc EXCEPT ![self] = a] | |
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "ChangeAccountPermission", | |
pc |-> "Action", | |
user |-> user[self], | |
acc |-> acc[self] ] >> | |
\o stack[self]] | |
/\ user' = [user EXCEPT ![self] = u] | |
/\ pc' = [pc EXCEPT ![self] = "ChangePerm"] | |
/\ UNCHANGED <<user_, acc_, withdraw_amt>> | |
/\ UNCHANGED << balance, organizations, roles, is_idle >> | |
server(self) == Action(self) | |
Next == (\E self \in ProcSet: \/ SendWire(self) | |
\/ ChangeAccountPermission(self)) | |
\/ (\E self \in Servers: server(self)) | |
Spec == Init /\ [][Next]_vars | |
\* END TRANSLATION | |
============================================================================= |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment