Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
-------------------------- 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
You can’t perform that action at this time.