break.tla

---- MODULE break ----
EXTENDS Integers, Sequences, TLC, FiniteSets

Max(S) == CHOOSE x \in S : \A y \in S : x >= y

CONSTANTS
    C,
    Srv,
    DB,
    MaxID,
    SrvCap,
    ProcTime,
    ReqRate,
    SrvTO

VARIABLES
    cReq,
    cResp,
    lastReq,
    sQueue,
    sProc,
    progress,
    dta,
    pReq,
    age,
    timedout,
    t,
    mtrcs

v == <<cReq, cResp, lastReq, sQueue, sProc, progress, dta,
      pReq, age, timedout, t, mtrcs>>

TypeOK ==
    /\ cReq \subseteq [c: C, id: Nat]
    /\ cResp \subseteq [c: C, id: Nat, resp: STRING, rTime: Nat]
    /\ lastReq \in [C -> Nat]
    /\ sQueue \subseteq [c: C, id: Nat, s: Srv, arrTime: Nat]
    /\ sProc \subseteq [c: C, id: Nat, s: Srv, sTime: Nat]
    /\ progress \in [sProc -> 0..ProcTime]
    /\ dta \in [DB -> STRING]
    /\ pReq \subseteq [c: C, id: Nat, subTime: Nat]
    /\ age \in [pReq -> Nat]
    /\ timedout \subseteq [c: C, id: Nat, toTime: Nat]
    /\ t \in Nat
    /\ mtrcs \in [
          tReq: Nat,
          cReq: Nat,
          toutReq: Nat,
          avgTime: Nat,
          maxLoad: Nat
       ]

Init ==
    /\ cReq = {}
    /\ cResp = {}
    /\ lastReq = [c \in C |-> 0]
    /\ sQueue = {}
    /\ sProc = {}
    /\ progress = [r \in {} |-> 0]
    /\ dta = [d \in DB |-> "initial data"]
    /\ pReq = {}
    /\ age = [r \in {} |-> 0]
    /\ timedout = {}
    /\ t = 0
    /\ mtrcs = [
          tReq |-> 0,
          cReq |-> 0,
          toutReq |-> 0,
          avgTime |-> 0,
          maxLoad |-> 0
       ]

NewReq(c) ==
    /\ t >= lastReq[c] + ReqRate
    /\ Cardinality(pReq) < 10
    /\ LET
         nid == mtrcs.tReq + 1
         req == [c |-> c, id |-> nid, subTime |-> t]
       IN
       /\ cReq' = cReq \union {[c |-> c, id |-> nid]}
       /\ pReq' = pReq \union {req}
       /\ age' = age @@ (req :> 0)
       /\ lastReq' = [lastReq EXCEPT ![c] = t]
       /\ mtrcs' = [mtrcs EXCEPT !.tReq = nid]
    /\ UNCHANGED <<cResp, sQueue, sProc, progress, dta, timedout, t>>

Accept ==
    /\ cReq /= {}
    /\ \E s \in Srv :
        /\ Cardinality({r \in sProc : r.s = s}) < SrvCap
        /\ LET
             oReq == CHOOSE r \in cReq :
                     \A o \in cReq : r.id <= o.id
             sReq == [c |-> oReq.c, id |-> oReq.id, s |-> s,
                     arrTime |-> t]
           IN
           /\ sQueue' = sQueue \union {sReq}
           /\ cReq' = cReq \ {oReq}
    /\ UNCHANGED <<cResp, lastReq, sProc, progress, dta, pReq,
                  age, timedout, t, mtrcs>>

Start ==
    /\ sQueue /= {}
    /\ LET
         oReq == CHOOSE r \in sQueue :
                \A o \in sQueue : r.arrTime <= o.arrTime
         procReq == [c |-> oReq.c, id |-> oReq.id, s |-> oReq.s,
                    sTime |-> t]
       IN
       /\ sProc' = sProc \union {procReq}
       /\ progress' = progress @@ (procReq :> 0)
       /\ sQueue' = sQueue \ {oReq}
    /\ UNCHANGED <<cReq, cResp, lastReq, dta, pReq, age,
                  timedout, t, mtrcs>>

Proc ==
    /\ sProc /= {}
    /\ \E r \in sProc :
        /\ progress[r] < ProcTime
        /\ progress' = [progress EXCEPT ![r] = @ + 1]
    /\ UNCHANGED <<cReq, cResp, lastReq, sQueue, sProc, dta,
                 pReq, age, timedout, t, mtrcs>>

Finish ==
    /\ \E req \in sProc :
        /\ progress[req] >= ProcTime
        /\ LET
             pr == CHOOSE p \in pReq : p.c = req.c /\ p.id = req.id
             rt == t - pr.subTime
             resp == [c |-> req.c, id |-> req.id,
                     resp |-> dta[CHOOSE d \in DB : TRUE],
                     rTime |-> rt]
             oldAvg == mtrcs.avgTime
             cnt == mtrcs.cReq
             newAvg == IF cnt = 0
                       THEN rt
                       ELSE (oldAvg * cnt + rt) \div (cnt + 1)
           IN
           /\ cResp' = cResp \union {resp}
           /\ pReq' = pReq \ {pr}
           /\ age' = [x \in pReq' |-> age[x]]
           /\ sProc' = sProc \ {req}
           /\ progress' = [x \in sProc' |-> progress[x]]
           /\ mtrcs' = [mtrcs EXCEPT
                       !.cReq = @ + 1,
                       !.avgTime = newAvg]
    /\ UNCHANGED <<cReq, lastReq, sQueue, dta, timedout, t>>

Timeout ==
    /\ LET
         tout == {rq \in pReq : t - rq.subTime >= SrvTO}
       IN
       /\ tout /= {}
       /\ timedout' = timedout \union
                      {[c |-> rq.c, id |-> rq.id, toTime |-> t] :
                       rq \in tout}
       /\ pReq' = pReq \ tout
       /\ age' = [rq \in pReq' |-> age[rq]]
       /\ cReq' = {rq \in cReq :
                  ~\E to \in tout : to.c = rq.c /\ to.id = rq.id}
       /\ sQueue' = {rq \in sQueue :
                    ~\E to \in tout : to.c = rq.c /\ to.id = rq.id}
       /\ LET
           toProc == {rq \in sProc :
                     \E to \in tout : to.c = rq.c /\ to.id = rq.id}
         IN
         /\ sProc' = sProc \ toProc
         /\ progress' = [rq \in sProc' |-> progress[rq]]
         /\ mtrcs' = [mtrcs EXCEPT
                     !.toutReq = @ + Cardinality(tout)]
    /\ UNCHANGED <<cResp, lastReq, dta, t>>

Tick ==
    /\ t' = t + 1
    /\ age' = [rq \in pReq |-> age[rq] + 1]
    /\ LET
         loads == {Cardinality({rq \in sProc : rq.s = s}) : s \in Srv}
         mLoad == IF loads = {} THEN 0 ELSE Max(loads)
       IN
       /\ mtrcs' = [mtrcs EXCEPT
                   !.maxLoad = IF mLoad > @ THEN mLoad ELSE @]
    /\ UNCHANGED <<cReq, cResp, lastReq, sQueue, sProc, progress,
                 dta, pReq, timedout>>

Next ==
    \/ \E c \in C : NewReq(c)
    \/ Accept
    \/ Start
    \/ Proc
    \/ Finish
    \/ Timeout
    \/ Tick

Spec == Init /\ [][Next]_v
        /\ WF_v(Accept)
        /\ WF_v(Start)
        /\ WF_v(Proc)
        /\ WF_v(Finish)
        /\ WF_v(Timeout)
        /\ WF_v(Tick)

AllReqHandled ==
    [](mtrcs.tReq > 0 =>
       <>(mtrcs.cReq + mtrcs.toutReq = mtrcs.tReq))

SomeReqTO ==
    <>(mtrcs.toutReq > 0)

SrvsOverload ==
    <>(mtrcs.maxLoad = SrvCap * Cardinality(Srv))

Constr ==
    /\ t < 25
    /\ mtrcs.tReq < 10

TOThreshold ==
    mtrcs.toutReq <= 4

====