Implementation of Coyote AccountManager example in TLA+

AccountManager.tla

--------------------------- MODULE AccountManager ---------------------------

EXTENDS Integers, TLC, FiniteSets, Sequences

CONSTANT NULL

(*--algorithm AccountManager 

variables
    accounts = {"anne", "bob"},
    \* TODO: Create Concurrent Database?
    database = << >>;

\* https://stackoverflow.com/questions/47115185/tla-how-to-delete-structure-key-value-pairings
 \* IF k \notin DOMAIN(database) THEN
define 
    CreateRow(k, v) ==  [x \in (DOMAIN database \cup {k}) |-> IF x = k THEN 
                                                                 v 
                                                              ELSE 
                                                                 database[x] ] 
    DoesRowExist(k) == k \in DOMAIN(database)
    GetRow(k) == IF k\in DOMAIN(database) THEN 
                        database[k] 
                 ELSE 
                    FALSE
    DeleteRow(k) == IF k \notin DOMAIN(database) THEN 
                        database 
                    ELSE 
                        [x \in DOMAIN(database) \ {k} |-> database[x] ]
end define;
 

\* Change this to 1..2 to be multithreaded
process Account \in 1..2
variable
    key \in accounts;
    returnval = TRUE;
begin
    WebRequest:
        while returnval do
            either CreateAccount:
                if DoesRowExist(key) then
                    returnval := FALSE;
                    goto WebRequest
                    end if;
                MakeAccount:
                    assert (key \notin DOMAIN database );
                    database := CreateRow(key, TRUE);
                    returnval := TRUE;
            or GetAccount:
                if ~DoesRowExist(key) then
                    returnval := FALSE;
                    goto WebRequest
                end if;
                GetValue:
                   returnval := GetRow(key);
            or DeleteAccount:
                if ~DoesRowExist(key) then
                    returnval := FALSE;
                    goto WebRequest                    
                end if;
                DeleteAccountRecord:
                    database := DeleteRow(key);
                    returnval := TRUE;
            end either;
        end while;
end process;
        
end algorithm;*)
\* BEGIN TRANSLATION (chksum(pcal) = "e5a735f9" /\ chksum(tla) = "f6bc8801")
VARIABLES accounts, database, pc

(* define statement *)
CreateRow(k, v) ==  [x \in (DOMAIN database \cup {k}) |-> IF x = k THEN
                                                             v
                                                          ELSE
                                                             database[x] ]
DoesRowExist(k) == k \in DOMAIN(database)
GetRow(k) == IF k\in DOMAIN(database) THEN
                    database[k]
             ELSE
                FALSE
DeleteRow(k) == IF k \notin DOMAIN(database) THEN
                    database
                ELSE
                    [x \in DOMAIN(database) \ {k} |-> database[x] ]

VARIABLES key, returnval

vars == << accounts, database, pc, key, returnval >>

ProcSet == (1..2)

Init == (* Global variables *)
        /\ accounts = {"anne", "bob"}
        /\ database = << >>
        (* Process Account *)
        /\ key \in [1..2 -> accounts]
        /\ returnval = [self \in 1..2 |-> TRUE]
        /\ pc = [self \in ProcSet |-> "WebRequest"]

WebRequest(self) == /\ pc[self] = "WebRequest"
                    /\ IF returnval[self]
                          THEN /\ \/ /\ pc' = [pc EXCEPT ![self] = "CreateAccount"]
                                  \/ /\ pc' = [pc EXCEPT ![self] = "GetAccount"]
                                  \/ /\ pc' = [pc EXCEPT ![self] = "DeleteAccount"]
                          ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
                    /\ UNCHANGED << accounts, database, key, returnval >>

CreateAccount(self) == /\ pc[self] = "CreateAccount"
                       /\ IF DoesRowExist(key[self])
                             THEN /\ returnval' = [returnval EXCEPT ![self] = FALSE]
                                  /\ pc' = [pc EXCEPT ![self] = "WebRequest"]
                             ELSE /\ pc' = [pc EXCEPT ![self] = "MakeAccount"]
                                  /\ UNCHANGED returnval
                       /\ UNCHANGED << accounts, database, key >>

MakeAccount(self) == /\ pc[self] = "MakeAccount"
                     /\ Assert((key[self] \notin DOMAIN database ), 
                               "Failure of assertion at line 47, column 21.")
                     /\ database' = CreateRow(key[self], TRUE)
                     /\ returnval' = [returnval EXCEPT ![self] = TRUE]
                     /\ pc' = [pc EXCEPT ![self] = "WebRequest"]
                     /\ UNCHANGED << accounts, key >>

GetAccount(self) == /\ pc[self] = "GetAccount"
                    /\ IF ~DoesRowExist(key[self])
                          THEN /\ returnval' = [returnval EXCEPT ![self] = FALSE]
                               /\ pc' = [pc EXCEPT ![self] = "WebRequest"]
                          ELSE /\ pc' = [pc EXCEPT ![self] = "GetValue"]
                               /\ UNCHANGED returnval
                    /\ UNCHANGED << accounts, database, key >>

GetValue(self) == /\ pc[self] = "GetValue"
                  /\ returnval' = [returnval EXCEPT ![self] = GetRow(key[self])]
                  /\ pc' = [pc EXCEPT ![self] = "WebRequest"]
                  /\ UNCHANGED << accounts, database, key >>

DeleteAccount(self) == /\ pc[self] = "DeleteAccount"
                       /\ IF ~DoesRowExist(key[self])
                             THEN /\ returnval' = [returnval EXCEPT ![self] = FALSE]
                                  /\ pc' = [pc EXCEPT ![self] = "WebRequest"]
                             ELSE /\ pc' = [pc EXCEPT ![self] = "DeleteAccountRecord"]
                                  /\ UNCHANGED returnval
                       /\ UNCHANGED << accounts, database, key >>

DeleteAccountRecord(self) == /\ pc[self] = "DeleteAccountRecord"
                             /\ database' = DeleteRow(key[self])
                             /\ returnval' = [returnval EXCEPT ![self] = TRUE]
                             /\ pc' = [pc EXCEPT ![self] = "WebRequest"]
                             /\ UNCHANGED << accounts, key >>

Account(self) == WebRequest(self) \/ CreateAccount(self)
                    \/ MakeAccount(self) \/ GetAccount(self)
                    \/ GetValue(self) \/ DeleteAccount(self)
                    \/ DeleteAccountRecord(self)

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == (\E self \in 1..2: Account(self))
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION 

\*Invariant == ~( "GetAccount" = pc[1] /\ "MakeAccount" = pc[2] /\ key[1] = key[2] /\ (database # <<>> ) /\ returnval = <<TRUE, TRUE>>)             


=============================================================================
\* Modification History
\* Last modified Tue Dec 13 21:36:46 EST 2022 by smiller
\* Created Tue Dec 06 23:06:33 EST 2022 by smiller