Created
April 7, 2025 20:59
-
-
Save cyang-el/c34272279623135dd6e36beb0826b493 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ---- 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 | |
| ==== |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment