multi_user_wire.tla

-------------------------- 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





=============================================================================