simple 3 tier web app in TLA+

3_tier_1.tla

---- MODULE 3_tier_1 ----
EXTENDS Integers, Sequences, TLC, FiniteSets
CONSTANTS Clients, Srvrs, DBs, MaxID
VARIABLES
    clReqs,     \* Client requests
    clResps,    \* Client responses
    srvQueue,   \* Server queue
    srvProc,    \* Server processing
    dbQ,        \* Database queries
    dbDat,      \* Database data
    pendReqs,   \* Pending requests
    nxtID       \* Next ID
vars == <<clReqs, clResps, srvQueue, srvProc, dbQ, dbDat, pendReqs, nxtID>>

TypeOK ==
    /\ clReqs \subseteq [client: Clients, id: 0..MaxID]
    /\ clResps \subseteq [client: Clients, id: 0..MaxID, response: STRING]
    /\ srvQueue \subseteq [client: Clients, id: 0..MaxID, server: Srvrs]
    /\ srvProc \subseteq [client: Clients, id: 0..MaxID, server: Srvrs]
    /\ dbQ \subseteq [query: STRING, server: Srvrs, 
                      client: Clients, id: 0..MaxID]
    /\ dbDat \in [DBs -> STRING]
    /\ pendReqs \subseteq [client: Clients, id: 0..MaxID]
    /\ nxtID \in Nat

Init ==
    /\ clReqs = {}
    /\ clResps = {}
    /\ srvQueue = {}
    /\ srvProc = {}
    /\ dbQ = {}
    /\ dbDat = [d \in DBs |-> "initial"]
    /\ pendReqs = {}
    /\ nxtID = 0

StateConstraint ==
    Cardinality(pendReqs) <= 10

TraceLengthConstraint ==
    TLCGet("level") < 25

CombinedConstraint ==
    /\ StateConstraint
    /\ TraceLengthConstraint

ClientReq(c) ==
    /\ ~\E req \in pendReqs : req.client = c
    /\ Cardinality(pendReqs) < 10
    /\ clReqs' = clReqs \union {[client |-> c, id |-> nxtID]}
    /\ pendReqs' = pendReqs \union {[client |-> c, id |-> nxtID]}
    /\ nxtID' = nxtID + 1
    /\ UNCHANGED <<clResps, srvQueue, srvProc, dbQ, dbDat>>

SrvrAcceptReq ==
    /\ clReqs /= {}
    /\ LET oldR == CHOOSE req \in clReqs :
                     \A other \in clReqs : req.id <= other.id
           s == CHOOSE srv \in Srvrs : TRUE
       IN
        /\ srvQueue' = srvQueue \union 
                      {[client |-> oldR.client, 
                        id |-> oldR.id, 
                        server |-> s]}
        /\ clReqs' = clReqs \ {oldR}
    /\ UNCHANGED <<clResps, srvProc, dbQ, dbDat, pendReqs, nxtID>>

SrvrProcess ==
    /\ srvQueue /= {}
    /\ LET oldR == CHOOSE req \in srvQueue :
                     \A other \in srvQueue : req.id <= other.id
       IN
        /\ srvProc' = srvProc \union {oldR}
        /\ dbQ' = dbQ \union {[query |-> "READ", 
                              server |-> oldR.server,
                              client |-> oldR.client, 
                              id |-> oldR.id]}
        /\ srvQueue' = srvQueue \ {oldR}
    /\ UNCHANGED <<clReqs, clResps, dbDat, pendReqs, nxtID>>

DBProcess ==
    /\ dbQ /= {}
    /\ LET oldQ == CHOOSE q \in dbQ :
                     \A other \in dbQ : q.id <= other.id
       IN
        /\ \E req \in srvProc :
            /\ req.client = oldQ.client
            /\ req.id = oldQ.id
            /\ req.server = oldQ.server
            /\ LET respRec == [client |-> req.client, 
                              id |-> req.id,
                              response |-> dbDat[CHOOSE d \in DBs : TRUE]]
                   pendRec == [client |-> req.client, 
                              id |-> req.id]
               IN
                  /\ clResps' = clResps \union {respRec}
                  /\ pendReqs' = pendReqs \ {pendRec}
                  /\ srvProc' = srvProc \ {req}
                  /\ dbQ' = dbQ \ {oldQ}
    /\ UNCHANGED <<clReqs, srvQueue, dbDat, nxtID>>

SysTerminate ==
    /\ clReqs = {}
    /\ srvQueue = {}
    /\ srvProc = {}
    /\ dbQ = {}
    /\ pendReqs = {}
    /\ UNCHANGED vars

Next ==
    \/ \E c \in Clients : ClientReq(c)
    \/ SrvrAcceptReq
    \/ SrvrProcess
    \/ DBProcess
    \/ SysTerminate

Spec == Init /\ [][Next]_vars
        /\ WF_vars(SrvrAcceptReq)
        /\ WF_vars(SrvrProcess)
        /\ SF_vars(DBProcess)
        /\ WF_vars(SysTerminate)

AllReqsGetResps == <>[](pendReqs = {})

NoReqStaysPendingForever ==
    \A c \in Clients : \A id \in 0..MaxID :
        [](([client |-> c, id |-> id] \in pendReqs) => 
           <>([client |-> c, id |-> id] \notin pendReqs))
====