diff --git a/TLAplus/TDMv5/TDMv5.tla b/TLAplus/TDMv5/TDMv5.tla
index 5644eaed32228eaac115a80c62ed022f5acdf0ec..f74d19b3074f61286ad3207edb24250efe2690b4 100644
--- a/TLAplus/TDMv5/TDMv5.tla
+++ b/TLAplus/TDMv5/TDMv5.tla
@@ -1,10 +1,13 @@
------------------------------- MODULE TDMv5 -------------------------------
-EXTENDS Reals, Integers
+EXTENDS Integers, FiniteSets, Sequences, SequencesExt
-Max(a,b) == IF a >= b THEN a ELSE b
+\* Utility predicates
+Max2Numbers(a,b) == IF a >= b THEN a ELSE b
+Max(S) == CHOOSE x \in S : \A y \in S : x >= y
+Min(S) == CHOOSE x \in S : \A y \in S : x =< y
+ModuloSum(a,b,max) == IF a + b =< max THEN a + b ELSE max - ((a+b)%max)
CONSTANTS
- Banks,
\* Intra-bank constraints
t_RCD,
t_RP,
@@ -21,30 +24,75 @@ CONSTANTS
t_WRtoRD,
t_CCD,
t_WTR,
- t_BURST
+ t_BURST,
+ \* Other constants
+ Banks,
+ CrRq,
+ NCrRq,
+ Mapping,
+ Queue_Capacity
+
+\* This creates a function that maps each requestor to a bank
+Requestors == CrRq \cup NCrRq
+tMapping == SetToSeq(Mapping)
+BankMapping == [req \in Requestors |-> tMapping[req]]
+\* Length of the TDM slot. Worst case is a write miss
+TDM_Slot == t_RCD + t_WL + t_BURST + t_WR + t_RP + 1
+\* Peridiocity of the TDM
+TDM_Period == Cardinality(CrRq)
+
+ASSUME
+ /\ Cardinality(Requestors) = Cardinality(Mapping)
VARIABLES
- state,
- lbtimer,
- now,
- req_under_treatment
+ cmds_lbtimer, \* Lower bound timers, used for expressing timing constraints. There is one per bank per command type.
+ arvl_lbtimer, \* Upper bound timers, used for modelling arrival of requests. There is one per requestor. Could be any type of timer. SF required.
+ chsl_lbtimer, \* Lower bound timer, used for modelling the change in slot_owner. Coulbe be any type of timer. SF required.
+ now, \* Current time
+ bank_state, \* Used to control the issue of commands to each bank
+ queue, \* A sequence of records containing the requests that have arrived in the system
+ req_under_treatment, \* A record representing the request currently under treatment
+ request_count, \* Counts how many requests per requestor have arrived
+ slot_count, \* Counts how many TDM slots have elapsed at total
+ slot_owner, \* The requestor who currently owns the TDM slot
+ row_buffer, \* A function that maps banks to a row buffer situation, i.e open or closed
+ slack, \* A function that maps each critical request to a value of slack
+ control \* A variable that controls the general advance of the system
-vars == <<state,lbtimer,now,req_under_treatment>>
+vars == <<cmds_lbtimer,arvl_lbtimer,chsl_lbtimer,now,
+ bank_state,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack,control>>
+\* Auxiliary sets
CMDS == {"IDLE","USEBUS","RLSBUS","ACT","RD","WR","PRE"}
-
-\* How to express the type predicate for lbtimer ?
+CONTROL == {"INIT","ARRIVAL","TREATMENT","COMPLETED"}
+-----------------------------------------------------------------------------
+\* What is the rule for changing the slot owner ? Have to make an action for that ?
+\* How to express the type predicate for cmds_lbtimer ?
\* Bounding time for now
maxtime == 100
+-----------------------------------------------------------------------------
+TimeTypeOK ==
+ \* /\ cmds_lbtimer \in [Banks \X {CMDS \{"IDLE"}} -> Int]
+ /\ arvl_lbtimer \in [Requestors -> Int]
+ /\ chsl_lbtimer \in Int
+ /\ now \in 0..maxtime
+\* No type invariance for now : req_under_treatment, queue
TypeOK ==
- /\ state \in [Banks -> CMDS]
- /\ now \in 0..maxtime
+ /\ bank_state \in [Banks -> CMDS]
+ /\ request_count \in [Requestors -> Nat]
+ /\ slot_count \in Nat
+ /\ slot_owner \in 1..Cardinality(CrRq)
+ /\ row_buffer \in [Banks -> {"OPEN","CLOSED"}]
+ /\ slack \in [CrRq -> Nat]
+ /\ control \in CONTROL
Init ==
- /\ state = [b \in Banks |-> "IDLE"]
- /\ lbtimer = [b \in Banks, c \in CMDS |-> 0]
+ /\ cmds_lbtimer = [b \in Banks, c \in CMDS\{"IDLE"} |-> 0]
+ /\ arvl_lbtimer = [req \in Requestors |-> 0]
+ /\ chsl_lbtimer = 0
/\ now = 0
+ /\ bank_state = [b \in Banks |-> "IDLE"]
/\ req_under_treatment = [type |-> "NONE",
deadline |-> 0,
target |-> "NONE",
@@ -53,104 +101,195 @@ Init ==
issue_date |-> 0,
delayed_issue_date |-> 0,
hit_miss |-> "NONE"]
-
-\* QUESTION : How could I model the request arrival and treatment with this new model ?
-\* Opt 1. By bounds as well.
+ /\ queue = <<>>
+ /\ request_count = [r \in Requestors |-> 0]
+ /\ slot_count = 1
+ /\ slot_owner = 1
+ /\ row_buffer = [b \in Banks |-> "CLOSED"]
+ /\ slack = [req \in CrRq |-> 0]
+ /\ control = "INIT"
-----------------------------------------------------------------------------
-SetTimer(a,b,timer,value) == timer' = [timer EXCEPT ![a,b] = value]
-TimedOut(a,b,timer) == timer[a,b] = 0
+Set2dimTimer(a,b,timer,value) == timer' = [timer EXCEPT ![a,b] = value]
+Set1dimTimer(a,timer,value) == timer' = [timer EXCEPT ![a] = value]
+TimedOut_2dim(a,b,timer) == timer[a,b] = 0
+TimedOut_1dim(a,timer) == timer[a] = 0
-----------------------------------------------------------------------------
IssueACT(this_bank) ==
- /\ state[this_bank] = "ACT"
- \* Checks if command is both intra and inter-ready
- /\ \A bank \in Banks : TimedOut(bank,"ACT",lbtimer)
- \* Sets intra bank timers
- /\ SetTimer(this_bank,"RD",lbtimer,t_RCD)
- /\ SetTimer(this_bank,"WR",lbtimer,t_RCD)
- /\ SetTimer(this_bank,"ACT",lbtimer,t_RC)
- /\ SetTimer(this_bank,"PRE",lbtimer,t_RAS)
- \* Sets inter bank timers
- /\ \A other_bank \in Banks \ {this_bank} : SetTimer(other_bank,"ACT",lbtimer,t_RRD)
- \* Decide the next command to be issued
- /\ state' = IF req_under_treatment.type = "RD"
- THEN [state EXCEPT ![this_bank] = "RD"]
- ELSE [state EXCEPT ![this_bank] = "WR"]
- /\ UNCHANGED<<now,req_under_treatment>>
+ /\ bank_state[this_bank] = "ACT"
+ /\ control = "TREATMENT"
+ /\ bank_state' = [bank_state EXCEPT ![this_bank] = "RD"]
+ /\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack,control>>
IssueRD(this_bank) ==
- /\ state[this_bank] = "RD"
+ /\ bank_state[this_bank] = "RD"
+ /\ control = "TREATMENT"
\* Checks if command is both intra and inter-ready
- /\ \A bank \in Banks : TimedOut(bank,"RD",lbtimer)
+ /\ \A bank \in Banks : TimedOut_2dim(bank,"RD",cmds_lbtimer)
\* Sets intra bank timers
- /\ SetTimer(this_bank,"USEBUS",lbtimer,t_RL)
- /\ SetTimer(this_bank,"PRE",lbtimer,t_RTP)
+ /\ Set2dimTimer(this_bank,"USEBUS",cmds_lbtimer,t_RL)
+ /\ Set2dimTimer(this_bank,"PRE",cmds_lbtimer,t_RTP)
\* Sets inter and inter bank timers
- /\ \A bank \in Banks : /\ SetTimer(bank,"WR",lbtimer,t_RTW)
- /\ SetTimer(bank,"RD",lbtimer,t_CCD)
- /\ state' = [state EXCEPT ![this_bank] = "USEBUS"]
- /\ UNCHANGED<<now,req_under_treatment>>
+ /\ \A bank \in Banks : /\ Set2dimTimer(bank,"WR",cmds_lbtimer,t_RTW)
+ /\ Set2dimTimer(bank,"RD",cmds_lbtimer,t_CCD)
+ /\ bank_state' = [bank_state EXCEPT ![this_bank] = "USEBUS"]
+ /\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,
+ slot_count,slot_owner,row_buffer,slack,control>>
IssueWR(this_bank) ==
- /\ state[this_bank] = "WR"
+ /\ bank_state[this_bank] = "WR"
+ /\ control = "TREATMENT"
\* Checks if command is both intra and inter-ready
- /\ \A bank \in Banks : TimedOut(bank,"RD",lbtimer)
+ /\ \A bank \in Banks : TimedOut_2dim(bank,"RD",cmds_lbtimer)
\* Sets intra bank timers
- /\ SetTimer(this_bank,"USEBUS",lbtimer,t_WL)
- /\ SetTimer(this_bank,"PRE",lbtimer,t_RTP)
+ /\ Set2dimTimer(this_bank,"USEBUS",cmds_lbtimer,t_WL)
+ /\ Set2dimTimer(this_bank,"PRE",cmds_lbtimer,t_RTP)
\* Sets inter bank timers
- /\ \A other_bank \in Banks \ {this_bank} : SetTimer(other_bank,"RD",lbtimer,t_WRtoRD)
- /\ state' = [state EXCEPT ![this_bank] = "USEBUS"]
- /\ UNCHANGED<<now,req_under_treatment>>
+ /\ \A other_bank \in Banks \ {this_bank} : Set2dimTimer(other_bank,"RD",cmds_lbtimer,t_WRtoRD)
+ /\ bank_state' = [bank_state EXCEPT ![this_bank] = "USEBUS"]
+ /\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,
+ slot_count,slot_owner,row_buffer,slack,control>>
UseBus(this_bank) ==
- /\ state[this_bank] = "USEBUS"
- /\ \A bank \in Banks : TimedOut(bank,"USEBUS",lbtimer)
- /\ \A bank \in Banks : SetTimer(bank,"RLSBUS",lbtimer,t_BURST)
- /\ state' = [state EXCEPT ![this_bank] = "RLSBUS"]
- /\ UNCHANGED<<now,req_under_treatment>>
+ /\ bank_state[this_bank] = "USEBUS"
+ /\ control = "TREATMENT"
+ /\ \A bank \in Banks : TimedOut_2dim(bank,"USEBUS",cmds_lbtimer)
+ /\ \A bank \in Banks : Set2dimTimer(bank,"RLSBUS",cmds_lbtimer,t_BURST)
+ /\ bank_state' = [bank_state EXCEPT ![this_bank] = "RLSBUS"]
+ /\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,
+ slot_count,slot_owner,row_buffer,slack,control>>
ReleaseBus(this_bank) ==
- /\ state[this_bank] = "RLSBUS"
- /\ \A bank \in Banks : TimedOut(bank,"RLSBUS",lbtimer)
+ /\ bank_state[this_bank] = "RLSBUS"
+ /\ control = "TREATMENT"
+ /\ \A bank \in Banks : TimedOut_2dim(bank,"RLSBUS",cmds_lbtimer)
/\ IF req_under_treatment.type = "WR"
- THEN SetTimer(this_bank,"PRE",lbtimer,t_WR)
+ THEN Set2dimTimer(this_bank,"PRE",cmds_lbtimer,t_WR)
ELSE TRUE
/\ \A bank \in Banks : IF req_under_treatment.type = "WR"
- THEN SetTimer(bank,"RD",lbtimer,t_WTR)
+ THEN Set2dimTimer(bank,"RD",cmds_lbtimer,t_WTR)
ELSE TRUE
- /\ state' = [state EXCEPT ![this_bank] = "PRE"]
- /\ UNCHANGED<<now,req_under_treatment>>
+ /\ bank_state' = [bank_state EXCEPT ![this_bank] = "PRE"]
+ /\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,
+ slot_count,slot_owner,row_buffer,slack,control>>
IssuePRE(this_bank) ==
- /\ state[this_bank] = "PRE"
- /\ \A bank \in Banks : TimedOut(bank,"PRE",lbtimer)
+ /\ bank_state[this_bank] = "PRE"
+ /\ control = "TREATMENT"
+ /\ \A bank \in Banks : TimedOut_2dim(bank,"PRE",cmds_lbtimer)
\* Intra-bank : PRE to ACT
- /\ SetTimer(this_bank,"ACT",lbtimer,t_RP)
+ /\ Set2dimTimer(this_bank,"ACT",cmds_lbtimer,t_RP)
\* Complection : bank becomes idle again
- /\ state' = [state EXCEPT ![this_bank] = "IDLE"]
- /\ UNCHANGED<<now,req_under_treatment>>
+ /\ bank_state' = [bank_state EXCEPT ![this_bank] = "IDLE"]
+ /\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,
+ slot_count,slot_owner,row_buffer,slack,control>>
+-----------------------------------------------------------------------------
+treat_request ==
+LET deadlines == {queue[n].deadline : n \in 1..Len(queue)}
+ min_deadline == Min(deadlines)
+ selected_req == SelectSeq(queue, LAMBDA elem: elem.deadline = min_deadline)[1]
+ StartTreatment == /\ queue' = Remove(queue,selected_req)
+ /\ req_under_treatment' = selected_req
+ /\ bank_state' = [bank_state EXCEPT ![selected_req.target] = "ACT"]
+ ResumeTreatment == UNCHANGED<<queue,req_under_treatment,bank_state>>
+IN /\ (control = "ARRIVAL") \/ (control = "COMPLETE" /\ queue /= <<>>)
+ /\ control' = "TREATMENT"
+ /\ IF req_under_treatment.owner = 0
+ THEN StartTreatment
+ ELSE ResumeTreatment
+ /\ UNCHANGED<<arvl_lbtimer,cmds_lbtimer,chsl_lbtimer,now,request_count,slot_count,slot_owner,
+ row_buffer,slack>>
+-----------------------------------------------------------------------------
+\* so_did : slot owner considering the delayed issue date
+\* dist : distance to the next slot owned by the requestor
+request_arrival(req,ty,hm,arrival_rate) ==
+LET so_did == IF slack[req] >= (slot_count*TDM_Slot - now)
+ THEN ModuloSum((slack[req]%TDM_Slot)+1,slot_owner,TDM_Period)
+ ELSE slot_owner
+ dist == IF (now = TDM_Slot*(slot_count - 1)) /\ (req = slot_owner)
+ THEN 0
+ ELSE IF req = so_did
+ THEN TDM_Period
+ ELSE IF req - so_did >= 0
+ THEN req - so_did
+ ELSE so_did - req
+ calc_deadline == IF req \in CrRq
+ THEN TDM_Slot*(slot_count + dist)
+ ELSE TDM_Slot*(slot_count + 1)
+ request_instance == [number |-> request_count[req] + 1,
+ owner |-> req,
+ target |-> BankMapping[req],
+ issue_date |-> now,
+ delayed_issue_date |-> now + slack[req],
+ deadline |-> calc_deadline,
+ type |-> ty,
+ hit_miss |-> hm,
+ period |-> arrival_rate]
+IN \* Only one request per requestor in the queue
+ /\ req \notin {queue[n].owner : n \in 1..Len(queue)}
+ \* No consecutive arrivals
+ /\ control \in CONTROL \{"ARRIVAL"}
+ \* Sets up the timer for the next TDM slot
+ /\ IF control = "INIT" THEN chsl_lbtimer' = TDM_Slot ELSE UNCHANGED<<chsl_lbtimer>>
+ \* The next arrival should happen at max arrival_rate cycles after this
+ /\ TimedOut_1dim(req,arvl_lbtimer)
+ /\ Set1dimTimer(req,arvl_lbtimer,arrival_rate)
+ /\ control' = "ARRIVAL"
+ /\ request_count' = [request_count EXCEPT ![req] = request_count[req] + 1]
+ /\ queue' = Append(queue,request_instance)
+ /\ UNCHANGED<<cmds_lbtimer,now,bank_state,req_under_treatment,
+ slot_count,slot_owner,row_buffer,slack>>
+-----------------------------------------------------------------------------
+SlotChange ==
+ /\ control /= "INIT"
+ \* Checks if the timer has timed_out
+ /\ chsl_lbtimer = 0
+ \* Sets it aggain
+ /\ chsl_lbtimer' = TDM_Slot
+ /\ slot_count' = slot_count + 1
+ /\ slot_owner' = ModuloSum(slot_owner,1,TDM_Period)
+ /\ UNCHANGED<<cmds_lbtimer,arvl_lbtimer,now,bank_state,queue,req_under_treatment,request_count,row_buffer,slack,control>>
-----------------------------------------------------------------------------
-Tick ==
- \E d \in {r \in Real: r > 0}:
- /\ now' = now + d
- /\ lbtimer' = [b \in Banks, c \in CMDS |-> Max(0,lbtimer[b,c]-d)]
- /\ UNCHANGED<<state,req_under_treatment>>
-
TNext(bank) == \/ IssueACT(bank)
\/ IssueRD(bank)
\/ IssueWR(bank)
\/ UseBus(bank)
\/ ReleaseBus(bank)
\/ IssuePRE(bank)
-
-Next == Tick \/ (\E bank \in Banks : TNext(bank))
+
+Tick == LET d == 1 IN
+ /\ ~\E bank \in Banks : TNext(bank)
+ /\ \neg ENABLED (treat_request \/ request_arrival(1,"RD","HIT",10) \/ request_arrival(2,"WR","MISS",15) \/ SlotChange)
+ /\ now' = now + d
+ /\ arvl_lbtimer' = [req \in Requestors |-> Max2Numbers(0,arvl_lbtimer[req]-d)]
+ /\ cmds_lbtimer' = [b \in Banks, c \in CMDS \{"IDLE"} |-> Max2Numbers(0,cmds_lbtimer[b,c]-d)]
+ /\ chsl_lbtimer' = Max2Numbers(0,chsl_lbtimer-d)
+ /\ UNCHANGED<<bank_state,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack,control>>
+-----------------------------------------------------------------------------
+Next == \/ Tick
+ \/ \E bank \in Banks : TNext(bank)
+ \/ treat_request
+ \/ SlotChange
+ \/ request_arrival(1,"RD","HIT",10)
+ \/ request_arrival(2,"WR","MISS",15)
-----------------------------------------------------------------------------
SafetySpec == Init /\ [][Next]_vars
+FullQueue == Len(queue) =< Queue_Capacity
+THEOREM SafetySpec => FullQueue
-----------------------------------------------------------------------------
-Liveness == /\ \A bank \in Banks : WF_vars(TNext(bank))
- /\ \A r \in Real : <>(now > r)
-Spec == SafetySpec /\ Liveness
+Fairness == /\ \A b \in Banks :
+ /\ SF_vars(IssueACT(b))
+ /\ SF_vars(IssueRD(b))
+ /\ SF_vars(IssueWR(b))
+ /\ SF_vars(IssuePRE(b))
+ /\ SF_vars(UseBus(b))
+ /\ SF_vars(ReleaseBus(b))
+ /\ WF_vars(SlotChange)
+ /\ WF_vars(treat_request)
+ /\ WF_vars(request_arrival(1,"RD","HIT",10))
+ /\ WF_vars(request_arrival(2,"WR","MISS",15))
+
+Spec == SafetySpec /\ Fairness
=============================================================================
\* Modification History
-\* Last modified Wed Mar 03 23:08:30 CET 2021 by felipe
+\* Last modified Fri Mar 05 10:32:19 CET 2021 by felipe
\* Created Wed Mar 03 20:37:54 CET 2021 by felipe
diff --git a/TLAplus/TDMv6/TDMv6.tla b/TLAplus/TDMv6/TDMv6.tla
new file mode 100644
index 0000000000000000000000000000000000000000..20064c3daaa5cee866d357df887e41053ce3459b
--- /dev/null
+++ b/TLAplus/TDMv6/TDMv6.tla
@@ -0,0 +1,225 @@
+------------------------------- MODULE TDMv6 -------------------------------
+EXTENDS Integers, FiniteSets, Sequences, SequencesExt
+
+-----------------------------------------------------------------------------
+Max2Numbers(a,b) == IF a >= b THEN a ELSE b
+Max(S) == CHOOSE x \in S : \A y \in S : x >= y
+Min(S) == CHOOSE x \in S : \A y \in S : x =< y
+ModuloSum(a,b,max) == IF a + b =< max THEN a + b ELSE max - ((a+b)%max)
+-----------------------------------------------------------------------------
+Infinity == 1000
+Real == 0..100 \cup Infinity
+-----------------------------------------------------------------------------
+
+CONSTANTS
+ \* Intra-bank constraints
+ t_RCD,
+ t_RP,
+ t_RC,
+ t_RAS,
+ t_RL,
+ t_WL,
+ t_RTP,
+ t_WR,
+ \* Inter-bank constraints
+ t_RRD,
+ \* Inter- and intra-bank constraints
+ t_RTW,
+ t_WRtoRD,
+ t_CCD,
+ t_WTR,
+ t_BURST,
+ \* Other constants
+ Banks,
+ CrRq,
+ NCrRq,
+ Mapping,
+ Queue_Capacity
+
+\* This creates a function that maps each requestor to a bank
+Requestors == CrRq \cup NCrRq
+tMapping == SetToSeq(Mapping)
+BankMapping == [req \in Requestors |-> tMapping[req]]
+\* Length of the TDM slot. Worst case is a write miss
+TDM_Slot == t_RCD + t_WL + t_BURST + t_WR + t_RP + 1
+\* Peridiocity of the TDM
+TDM_Period == Cardinality(CrRq)
+
+ASSUME
+ /\ Cardinality(Requestors) = Cardinality(Mapping)
+
+VARIABLES
+ now,
+ ACT_lbtimer,
+ RD_lbtimer,
+ WR_lbtimer,
+ PRE_lbtimer,
+ USEBUS_lbtimer,
+ RLSBUS_lbtimer,
+ ARV_lbtimer,
+ SLOT_lbtimer,
+ bank_state,
+ queue,
+ req_under_treatment,
+ request_count,
+ slot_count,
+ slot_owner,
+ row_buffer,
+ slack,
+ control
+
+vars == <<now,ACT_lbtimer,RD_lbtimer,WR_lbtimer,PRE_lbtimer,USEBUS_lbtimer,RLSBUS_lbtimer,ARV_lbtimer,SLOT_lbtimer,
+ bank_state,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack,control>>
+-----------------------------------------------------------------------------
+CMDS == {"ACT","RD","WR","PRE","IDLE","USEBUS","RLSBUS"}
+CONTROL == {"INIT","ARRIVAL","TREATMENT","COMPLETED"}
+-----------------------------------------------------------------------------
+TimeTypeOK ==
+ /\ now \in Real
+ /\ ACT_lbtimer \in [Banks -> Real]
+ /\ RD_lbtimer \in [Banks -> Real]
+ /\ WR_lbtimer \in [Banks -> Real]
+ /\ PRE_lbtimer \in [Banks -> Real]
+ /\ USEBUS_lbtimer \in [Banks -> Real]
+ /\ RLSBUS_lbtimer \in [Banks -> Real]
+ /\ ARV_lbtimer \in [Requestors -> Real]
+ /\ SLOT_lbtimer \in Real
+
+\* No type invariance for now : req_under_treatment, queue
+TypeOK ==
+ /\ bank_state \in [Banks -> CMDS]
+ /\ request_count \in [Requestors -> Nat]
+ /\ slot_count \in Nat
+ /\ slot_owner \in 1..Cardinality(CrRq)
+ /\ row_buffer \in [Banks -> {"OPEN","CLOSED"}]
+ /\ slack \in [CrRq -> Nat]
+ /\ control \in CONTROL
+
+Init ==
+ /\ now = 0
+ /\ ACT_lbtimer = [b \in Banks |-> 0]
+ /\ RD_lbtimer = [b \in Banks |-> 0]
+ /\ WR_lbtimer = [b \in Banks |-> 0]
+ /\ PRE_lbtimer = [b \in Banks |-> 0]
+ /\ USEBUS_lbtimer = [b \in Banks |-> 0]
+ /\ RLSBUS_lbtimer = [b \in Banks |-> 0]
+ /\ ARV_lbtimer = [req \in Requestors |-> 0]
+ /\ SLOT_lbtimer = 0
+ /\ bank_state = [b \in Banks |-> "IDLE"]
+ /\ queue = <<>>
+ /\ req_under_treatment = [type |-> "NONE",deadline |-> 0,target |-> "NONE",number |-> 0,owner |-> 0,
+ issue_date |-> 0,delayed_issue_date |-> 0,hit_miss |-> "NONE"]
+ /\ request_count = [r \in Requestors |-> 0]
+ /\ slot_count = 1
+ /\ slot_owner = 1
+ /\ row_buffer = [b \in Banks |-> "CLOSED"]
+ /\ slack = [req \in CrRq |-> 0]
+ /\ control = "INIT"
+-----------------------------------------------------------------------------
+TimedOut(timer,index) == timer[index] = 0
+SetLBTimer(timer,index,value) == timer' = [timer EXCEPT ![index] = value]
+-----------------------------------------------------------------------------
+IssueACT(bank) ==
+ /\ control = "TREATMENT"
+ /\ bank_state[bank] = "ACT"
+ /\ ACT_lbtimer["N1"] = 0
+ /\ ACT_lbtimer["N2"] = 0
+ /\ control' = "INIT"
+ /\ UNCHANGED<<now,ACT_lbtimer,RD_lbtimer,WR_lbtimer,PRE_lbtimer,USEBUS_lbtimer,RLSBUS_lbtimer,ARV_lbtimer,SLOT_lbtimer,
+ bank_state,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack>>
+-----------------------------------------------------------------------------
+treat_request ==
+LET deadlines == {queue[n].deadline : n \in 1..Len(queue)}
+ min_deadline == Min(deadlines)
+ selected_req == SelectSeq(queue, LAMBDA elem: elem.deadline = min_deadline)[1]
+IN /\ (control = "ARRIVAL") \/ (control = "COMPLETE" /\ queue /= <<>>)
+ /\ control' = "TREATMENT"
+ /\ queue' = IF req_under_treatment.owner = 0 THEN Remove(queue,selected_req) ELSE queue
+ /\ req_under_treatment' = IF req_under_treatment.owner = 0 THEN selected_req ELSE req_under_treatment
+ /\ bank_state' = IF req_under_treatment.owner = 0 THEN [bank_state EXCEPT ![selected_req.target] = "ACT"] ELSE bank_state
+ /\ UNCHANGED<<now,ACT_lbtimer,RD_lbtimer,WR_lbtimer,PRE_lbtimer,USEBUS_lbtimer,RLSBUS_lbtimer,ARV_lbtimer,SLOT_lbtimer,
+ request_count,slot_count,slot_owner,row_buffer,slack>>
+-----------------------------------------------------------------------------
+request_arrival(req,ty,hm,arrival_rate) ==
+LET so_did == IF slack[req] >= (slot_count*TDM_Slot - now)
+ THEN ModuloSum((slack[req]%TDM_Slot)+1,slot_owner,TDM_Period)
+ ELSE slot_owner
+ dist == IF (now = TDM_Slot*(slot_count - 1)) /\ (req = slot_owner)
+ THEN 0
+ ELSE IF req = so_did
+ THEN TDM_Period
+ ELSE IF req - so_did >= 0
+ THEN req - so_did
+ ELSE so_did - req
+ calc_deadline == IF req \in CrRq
+ THEN TDM_Slot*(slot_count + dist)
+ ELSE TDM_Slot*(slot_count + 1)
+ request_instance == [number |-> request_count[req] + 1,
+ owner |-> req,
+ target |-> BankMapping[req],
+ issue_date |-> now,
+ delayed_issue_date |-> now + slack[req],
+ deadline |-> calc_deadline,
+ type |-> ty,
+ hit_miss |-> hm,
+ period |-> arrival_rate]
+IN /\ req \notin {queue[n].owner : n \in 1..Len(queue)}
+ /\ control \in CONTROL \{"ARRIVAL"}
+ /\ TimedOut(ARV_lbtimer,req)
+ \* Primed
+ /\ SLOT_lbtimer' = IF control = "INIT" THEN TDM_Slot ELSE SLOT_lbtimer
+ /\ SetLBTimer(ARV_lbtimer,req,arrival_rate)
+ /\ control' = "ARRIVAL"
+ /\ request_count' = [request_count EXCEPT ![req] = request_count[req] + 1]
+ /\ queue' = Append(queue,request_instance)
+ /\ UNCHANGED<<now,ACT_lbtimer,RD_lbtimer,WR_lbtimer,PRE_lbtimer,USEBUS_lbtimer,RLSBUS_lbtimer,
+ bank_state,req_under_treatment,slot_count,slot_owner,row_buffer,slack>>
+-----------------------------------------------------------------------------
+SlotChange ==
+ /\ control /= "INIT"
+ /\ SLOT_lbtimer = 0
+ /\ SLOT_lbtimer' = TDM_Slot
+ /\ slot_count' = slot_count + 1
+ /\ slot_owner' = ModuloSum(slot_owner,1,TDM_Period)
+ /\ UNCHANGED<<now,ACT_lbtimer,RD_lbtimer,WR_lbtimer,PRE_lbtimer,USEBUS_lbtimer,RLSBUS_lbtimer,ARV_lbtimer,
+ bank_state,queue,req_under_treatment,request_count,row_buffer,slack,control>>
+-----------------------------------------------------------------------------
+\*TNext(bank) == IssueACT(bank)
+-----------------------------------------------------------------------------
+\*Tick == \E d \in 0..100:
+\* \* The Tick action is only allowed to happen when other decision actions are not possible
+\* /\ ~\E bank \in Banks : IssueACT(bank)
+\* /\ \neg ENABLED (treat_request \/ request_arrival(1,"RD","HIT",10) \/ request_arrival(2,"WR","MISS",15) \/ SlotChange)
+\* /\ now' = now + d
+\* /\ ACT_lbtimer' = [b \in Banks |-> Max2Numbers(0,ACT_lbtimer[b]-d)]
+\* /\ RD_lbtimer' = [b \in Banks |-> Max2Numbers(0,RD_lbtimer[b]-d)]
+\* /\ WR_lbtimer' = [b \in Banks |-> Max2Numbers(0,WR_lbtimer[b]-d)]
+\* /\ PRE_lbtimer' = [b \in Banks |-> Max2Numbers(0,PRE_lbtimer[b]-d)]
+\* /\ USEBUS_lbtimer' = [b \in Banks |-> Max2Numbers(0,USEBUS_lbtimer[b]-d)]
+\* /\ RLSBUS_lbtimer' = [b \in Banks |-> Max2Numbers(0,RLSBUS_lbtimer[b]-d)]
+\* /\ ARV_lbtimer' = [b \in Banks |-> Max2Numbers(0,ARV_lbtimer[b]-d)]
+\* /\ SLOT_lbtimer' = Max2Numbers(0,SLOT_lbtimer-d)
+\* /\ UNCHANGED<<bank_state,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack,control>>
+-----------------------------------------------------------------------------
+Next == \/ request_arrival(1,"RD","HIT",10)
+ \/ request_arrival(2,"WR","MISS",15)
+ \*\/ Tick
+ \/ treat_request
+ \/ SlotChange
+ \/ \E bank \in Banks : IssueACT(bank)
+-----------------------------------------------------------------------------
+SafetySpec == Init /\ [][Next]_vars
+FullQueue == Len(queue) =< Queue_Capacity
+THEOREM SafetySpec => FullQueue
+-----------------------------------------------------------------------------
+Fairness == /\ SF_vars(SlotChange)
+ /\ SF_vars(treat_request)
+ /\ SF_vars(request_arrival(1,"RD","HIT",10))
+ /\ SF_vars(request_arrival(2,"WR","MISS",15))
+ /\ \A b \in Banks : SF_vars(IssueACT(b))
+
+Spec == SafetySpec /\ Fairness
+=============================================================================
+\* Modification History
+\* Last modified Fri Mar 05 14:21:57 CET 2021 by felipe
+\* Created Wed Mar 03 20:37:54 CET 2021 by felipe
\ No newline at end of file