diff --git a/TLAplus/SequencesExt.tla b/TLAplus/SequencesExt.tla
deleted file mode 100644
index 8777a477b02c111b9220d748e01cee05bfe8572d..0000000000000000000000000000000000000000
--- a/TLAplus/SequencesExt.tla
+++ /dev/null
@@ -1,145 +0,0 @@
----------------------------- MODULE SequencesExt ----------------------------
-
-LOCAL INSTANCE Sequences
-LOCAL INSTANCE Naturals
-LOCAL INSTANCE FiniteSets
-LOCAL INSTANCE Functions
- (*************************************************************************)
- (* Imports the definitions from the modules, but doesn't export them. *)
- (*************************************************************************)
-
------------------------------------------------------------------------------
-
-ToSet(s) ==
- (*************************************************************************)
- (* The image of the given sequence s. Cardinality(ToSet(s)) <= Len(s) *)
- (* see https://en.wikipedia.org/wiki/Image_(mathematics) *)
- (*************************************************************************)
- { s[i] : i \in DOMAIN s }
-
-IsInjective(s) ==
- (*************************************************************************)
- (* TRUE iff the sequence s contains no duplicates where two elements *)
- (* a, b of s are defined to be duplicates iff a = b. In other words, *)
- (* Cardinality(ToSet(s)) = Len(s) *)
- (* *)
- (* This definition is overridden by TLC in the Java class SequencesExt. *)
- (* The operator is overridden by the Java method with the same name. *)
- (* *)
- (* Also see Functions!Injective operator. *)
- (*************************************************************************)
- \A i, j \in DOMAIN s: (s[i] = s[j]) => (i = j)
-
-SetToSeq(S) ==
- (**************************************************************************)
- (* Convert a set to some sequence that contains all the elements of the *)
- (* set exactly once, and contains no other elements. *)
- (**************************************************************************)
- CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f)
-
------------------------------------------------------------------------------
-
-Contains(s, e) ==
- (**************************************************************************)
- (* TRUE iff the element e \in ToSet(s). *)
- (**************************************************************************)
- \E i \in 1..Len(s) : s[i] = e
-
-Reverse(s) ==
- (**************************************************************************)
- (* Reverse the given sequence s: Let l be Len(s) (length of s). *)
- (* Equals a sequence s.t. << S[l], S[l-1], ..., S[1]>> *)
- (**************************************************************************)
- [ i \in 1..Len(s) |-> s[(Len(s) - i) + 1] ]
-
-Remove(s, e) ==
- (************************************************************************)
- (* The sequence s with e removed or s iff e \notin Range(s) *)
- (************************************************************************)
- SelectSeq(s, LAMBDA t: t # e)
-
-ReplaceAll(s, old, new) ==
- (*************************************************************************)
- (* Equals the sequence s except that all occurrences of element old are *)
- (* replaced with the element new. *)
- (*************************************************************************)
- LET F[i \in 0..Len(s)] ==
- IF i = 0 THEN << >>
- ELSE IF s[i] = old THEN Append(F[i-1], new)
- ELSE Append(F[i-1], s[i])
- IN F[Len(s)]
-
------------------------------------------------------------------------------
-
-\* The operators below have been extracted from the TLAPS module
-\* SequencesTheorems.tla as of 10/14/2019. The original comments have been
-\* partially rewritten.
-
-InsertAt(s, i, e) ==
- (**************************************************************************)
- (* Inserts element e at the position i moving the original element to i+1 *)
- (* and so on. In other words, a sequence t s.t.: *)
- (* /\ Len(t) = Len(s) + 1 *)
- (* /\ t[i] = e *)
- (* /\ \A j \in 1..(i - 1): t[j] = s[j] *)
- (* /\ \A k \in (i + 1)..Len(s): t[k + 1] = s[k] *)
- (**************************************************************************)
- SubSeq(s, 1, i-1) \o <<e>> \o SubSeq(s, i, Len(s))
-
-ReplaceAt(s, i, e) ==
- (**************************************************************************)
- (* Replaces the element at position i with the element e. *)
- (**************************************************************************)
- [s EXCEPT ![i] = e]
-
-RemoveAt(s, i) ==
- (**************************************************************************)
- (* Replaces the element at position i shortening the length of s by one. *)
- (**************************************************************************)
- SubSeq(s, 1, i-1) \o SubSeq(s, i+1, Len(s))
-
------------------------------------------------------------------------------
-
-Front(s) ==
- (**************************************************************************)
- (* The sequence formed by removing its last element. *)
- (**************************************************************************)
- SubSeq(s, 1, Len(s)-1)
-
-Last(s) ==
- (**************************************************************************)
- (* The last element of the sequence. *)
- (**************************************************************************)
- s[Len(s)]
-
------------------------------------------------------------------------------
-
-IsPrefix(s, t) ==
- (**************************************************************************)
- (* TRUE iff the sequence s is a prefix of the sequence t, s.t. *)
- (* \E u \in Seq(Range(t)) : t = s \o u. In other words, there exists *)
- (* a suffix u that with s prepended equals t. *)
- (**************************************************************************)
- DOMAIN s \subseteq DOMAIN t /\ \A i \in DOMAIN s: s[i] = t[i]
-
-IsStrictPrefix(s,t) ==
- (**************************************************************************)
- (* TRUE iff the sequence s is a prefix of the sequence t and s # t *)
- (**************************************************************************)
- IsPrefix(s, t) /\ s # t
-
-IsSuffix(s, t) ==
- (**************************************************************************)
- (* TRUE iff the sequence s is a suffix of the sequence t, s.t. *)
- (* \E u \in Seq(Range(t)) : t = u \o s. In other words, there exists a *)
- (* prefix that with s appended equals t. *)
- (**************************************************************************)
- IsPrefix(Reverse(s), Reverse(t))
-
-IsStrictSuffix(s, t) ==
- (**************************************************************************)
- (* TRUE iff the sequence s is a suffix of the sequence t and s # t *)
- (**************************************************************************)
- IsSuffix(s,t) /\ s # t
-
-=============================================================================
\ No newline at end of file
diff --git a/TLAplus/TDMv1/TDM.tla b/TLAplus/TDMv1/TDM.tla
deleted file mode 100644
index cc0d399ce12e95f6b766328c2bdc93b7c34135b4..0000000000000000000000000000000000000000
--- a/TLAplus/TDMv1/TDM.tla
+++ /dev/null
@@ -1,256 +0,0 @@
--------------------------------- MODULE TDM --------------------------------
-(***************************************************************************)
-(* This is a simple TDM arbitration between memory requests *)
-(* inside a DRAM controller *)
-(***************************************************************************)
-EXTENDS Integers, Reals, Sequences, SequencesExt
-
-CONSTANT
- BANKS,
- t_RCD, \* ACT to RD/WR
- t_RP, \* PRE to ACT
- t_RC, \* ACT to ACT
- t_RAS, \* ACT to PRE
- t_WL, \* WL to data bus
- t_RL, \* RD to data bus
- t_RTP, \* RD to PRE
- t_WR, \* Enf of a WR to PRE
- t_RRD, \* ACT to ACT
- t_FAW, \* Four ACT window
- t_RTW,
- t_WR_to_RD,
- t_WTR,
- t_BURST,
- t_CCD
-
-VARIABLES
- time,
- slotOwner,
- bankState, \* last command sent to the bank
- lastACT,
- lastRD,
- lastWR,
- lastPRE,
- lastBUS,
- bus,
- slotCounter
-
-BusDir == {"RD","WR"}
-BusSta == BANKS \cup {"IDLE"}
-tBANKS == SetToSeq(BANKS)
-
-TDMTypeOK ==
- /\ time \in Int
- /\ slotOwner \in BANKS
- /\ bankState \in [BANKS -> {"NOP","PRE","ACT","RD","WR"}]
- /\ lastPRE \in [BANKS -> Int]
- /\ lastACT \in [BANKS -> Int]
- /\ lastRD \in [BANKS -> Int]
- /\ lastWR \in [BANKS -> Int]
- /\ lastBUS \in Int
- /\ bus.ocup \in BusSta
- /\ bus.dir \in BusDir
- /\ slotCounter \in 1..Len(tBANKS)
-
-TDMInit ==
- /\ time = 0
- /\ slotOwner = CHOOSE b \in BANKS : TRUE
- /\ bankState = [b \in BANKS |-> "NOP"]
- /\ lastPRE = [b \in BANKS |-> 100]
- /\ lastACT = [b \in BANKS |-> 100]
- /\ lastRD = [b \in BANKS |-> 100]
- /\ lastWR = [b \in BANKS |-> 100]
- /\ lastBUS = 100
- /\ bus = [ocup |-> "IDLE", dir |-> CHOOSE dir \in {"RD","WR"} : TRUE]
- /\ slotCounter = 1
-
------------------------------------------------------------------------------
-(***************************************************************************)
-(* BUS ACTIONS *)
-(***************************************************************************)
-\* To use the bus, the demanding bank must respect the timing constraints and the bus has to be idle
-UseBus(b) == /\ IF bankState[b] = "RD" THEN lastRD[b] >= t_RL + 1
- ELSE IF bankState[b] = "WR" THEN lastWR[b] >= t_WL + 1
- ELSE FALSE
- \* Not optimal, since this restraints that bus can only be used once per slot
- /\ lastBUS >= t_BURST + t_WR - 1 + t_RP
- /\ bus.ocup = "IDLE"
- /\ bus' = [ocup |-> b, dir |-> IF bankState[b] = "RD" THEN "RD" ELSE "WR"]
- /\ lastBUS' = 0
- /\ UNCHANGED <<time,slotOwner,bankState,lastACT,lastPRE,lastRD,lastWR,slotCounter>>
-
-ReleaseBus(b) == /\ lastBUS >= t_BURST
- /\ bus.ocup /= "IDLE"
- /\ bus' = [bus EXCEPT !.ocup = "IDLE"]
- /\ UNCHANGED <<time,slotOwner,bankState,lastACT,lastPRE,lastRD,lastWR,lastBUS,slotCounter>>
------------------------------------------------------------------------------
-(***************************************************************************)
-(* THE SCHEDULER ACTIONS *)
-(***************************************************************************)
-ACTintraReady(b) ==
- /\ lastACT[b] >= t_RC
- /\ lastPRE[b] >= t_RP
-
-ACTinterReady(b) ==
- /\ \A m \in BANKS \ {b} : /\ lastACT[m] >= t_RRD
- /\ lastACT[m] >= t_FAW
-
-SchACT(b) == /\ bankState[b] = "PRE" \/ bankState[b] = "NOP"
- \* We consider for now that an ACT can only be scheduled at the beginning of a TDM slot
- /\ time = 0
- /\ slotOwner = b
- /\ ACTintraReady(b)
- /\ ACTinterReady(b)
- /\ bankState' = [bankState EXCEPT ![b] = "ACT"]
- /\ lastACT' = [lastACT EXCEPT ![b] = 0]
- /\ UNCHANGED <<time,slotOwner,lastPRE,lastRD,lastWR,bus,lastBUS,slotCounter>>
-
-RDintraReady(b) ==
- /\ lastACT[b] >= t_RCD
- /\ lastRD[b] >= t_CCD
- /\ lastWR[b] >= t_WR_to_RD
-
-RDinterReady(b) ==
- /\ \A m \in BANKS \ {b} : /\ lastRD[m] >= t_CCD
- /\ lastWR[m] >= t_WR_to_RD
- /\ IF bus.dir = "WR" THEN lastBUS >= t_WTR + t_BURST ELSE TRUE
-
-SchRD(b) == /\ bankState[b] = "ACT"
- /\ slotOwner = b
- /\ RDintraReady(b)
- /\ RDinterReady(b)
- /\ bankState' = [bankState EXCEPT ![b] = "RD"]
- /\ lastRD' = [lastRD EXCEPT ![b] = 0]
- /\ UNCHANGED <<time,slotOwner,lastACT,lastPRE,lastWR,bus,lastBUS,slotCounter>>
-
-WRintraReady(b) ==
- /\ lastACT[b] >= t_RCD
- /\ lastRD[b] >= t_RTW
- /\ lastWR[b] >= t_CCD
-
-WRinterReady(b) ==
- /\ \A m \in BANKS \ {b} : /\ lastRD[m] >= t_RTW
- /\ lastWR[m] >= t_CCD
-
-SchWR(b) == /\ bankState[b] = "ACT" /\ bankState[b] /= "PRE"
- /\ slotOwner = b
- /\ WRintraReady(b)
- /\ WRinterReady(b)
- /\ bankState' = [bankState EXCEPT ![b] = "WR"]
- /\ lastWR' = [lastWR EXCEPT ![b] = 0]
- /\ UNCHANGED <<time,slotOwner,lastACT,lastPRE,lastRD,bus,lastBUS,slotCounter>>
-
-PREintraReady(b) ==
- /\ lastACT[b] >= t_RAS
- /\ lastRD [b] >= t_RTP
- \* Not the best, this is considering there will be only one use of the BUS per slot
- /\ IF bus.dir = "WR" THEN lastBUS >= t_WR - 1 + t_BURST ELSE TRUE
-
-SchPRE(b) == /\ bankState[b] = "RD" \/ bankState[b] = "WR"
- /\ slotOwner = b
- /\ PREintraReady(b)
- /\ bankState' = [bankState EXCEPT ![b] = "PRE"]
- /\ lastPRE' = [lastPRE EXCEPT ![b] = 0]
- /\ UNCHANGED <<time,slotOwner,lastACT,lastRD,lastWR,bus,lastBUS,slotCounter>>
-
-UpdateSlotOwner ==
- /\ slotCounter' = IF slotCounter = Len(tBANKS) - 1
- THEN 1
- ELSE slotCounter + 1
- /\ slotOwner' = tBANKS[slotCounter+1]
-
-SlotLength == t_RCD + t_WL + t_BURST + t_WR + t_RP
-
-SchChange == /\ slotCounter =< 2
- /\ time >= SlotLength
- /\ UpdateSlotOwner
- /\ time' = 0
- /\ UNCHANGED <<bankState,lastACT,lastRD,lastWR,lastPRE,bus,lastBUS>>
------------------------------------------------------------------------------
-(***************************************************************************)
-(* TIME ACTIONS *)
-(***************************************************************************)
-UpdateDelays ==
- /\ lastACT' = [b \in BANKS |-> lastACT[b] + 1]
- /\ lastRD' = [b \in BANKS |-> lastRD[b] + 1]
- /\ lastWR' = [b \in BANKS |-> lastWR[b] + 1]
- /\ lastPRE' = [b \in BANKS |-> lastPRE[b] + 1]
- /\ lastBUS' = lastBUS + 1
-
-Step ==
- \* A step can only happen if scheduling / bus actions are not enabled
- /\ \A b \in BANKS : /\ \neg (ENABLED SchACT(b))
- /\ \neg (ENABLED SchRD(b))
- /\ \neg (ENABLED SchWR(b))
- /\ \neg (ENABLED SchPRE(b))
- /\ \neg (ENABLED UseBus(b))
- /\ \neg (ENABLED ReleaseBus(b))
- /\ \neg (ENABLED SchChange)
- /\ slotCounter =< 2
- /\ time' = time + 1
- /\ UpdateDelays
- /\ UNCHANGED<<slotOwner,bankState,bus,slotCounter>>
------------------------------------------------------------------------------
-TDMNext ==
- \/ Step
- \/ \E b \in BANKS : \/ SchACT(b)
- \/ SchPRE(b)
- \/ SchRD(b)
- \/ SchWR(b)
- \/ UseBus(b)
- \/ ReleaseBus(b)
- \/ SchChange
------------------------------------------------------------------------------
-vars == <<time,slotOwner,bankState,lastACT,lastPRE,lastRD,lastWR,lastBUS,bus,slotCounter>>
-(***************************************************************************)
-(* Stong fairness of TDMNext states that if there is a non stuttering *)
-(* action possible TDMNext it must happen *)
-(***************************************************************************)
-TDMSpec == /\ TDMInit
- /\ [][TDMNext]_vars
- /\ SF_vars(TDMNext)
------------------------------------------------------------------------------
-\* Temporal properties
-(***************************************************************************)
-(* TDMTemp1 states that if a RD or a WR has been scheduled to a certain *)
-(* bank, then the bus will eventually by occupied by the requestor *)
-(* TDMTemp2 states that if a requestor owns the slot that eventually a RD *)
-(* will be issued *)
-(***************************************************************************)
-\* How can I check that things happen in the same slot (time < 0) ?
-TDMTemp1 ==
- /\ \A b \in BANKS : bankState[b] \in {"RD","WR"} ~> bus.ocup = b
-
-TDMTemp2 ==
- /\ \A b \in BANKS : slotOwner = b ~> bankState[b] = "RD"
-
-\* Ensures that changing slots will happen
-TDMChange ==
- []<><<SchChange>>_vars
-
-TDMLimit ==
- <>(slotCounter = 3)
------------------------------------------------------------------------------
-\*Invariants
-(***************************************************************************)
-(* TDMValidity1 states that if a RD or a WR has been scheduled for a *)
-(* certain bank, than the requestor owner of that bank owns the TDM slot *)
-(* TDMValidity2 states that if a certain bank b doesn't own the slot, than *)
-(* the last command sent to it must have been a NOP or a PRE *)
-(***************************************************************************)
-TDMValidity1 ==
- /\ \A b \in BANKS : bankState[b] \in {"RD","WR"} => slotOwner = b
-
-TDMValidity2 ==
- /\ \A b \in BANKS : slotOwner /= b => bankState[b] \in {"NOP", "PRE"}
-
-IntraBankConstraints ==
- /\ \A b \in BANKS : CASE ENABLED SchRD(b) -> lastACT[b] >= t_RCD /\ lastRD[b] >= t_RTW /\ lastWR[b] >= t_WR_to_RD
- [] ENABLED SchWR(b) -> lastACT[b] >= t_RCD /\ lastRD[b] >= t_RTW /\ lastWR[b] >= t_CCD
- [] ENABLED SchACT(b) -> lastACT[b] >= t_RC /\ lastPRE[b] >= t_RP
- [] ENABLED SchPRE(b) -> lastACT[b] >= t_RAS /\ lastRD [b] >= t_RTP /\ IF bus.dir = "WR" THEN lastBUS >= t_WR - 1 + t_BURST ELSE TRUE
- [] OTHER -> TRUE
-=============================================================================
-\* Modification History
-\* Last modified Wed Feb 10 11:42:39 CET 2021 by felipe
-\* Created Mon Jan 18 10:05:32 CET 2021 by felipe
diff --git a/TLAplus/TDMv2/RT_TDMv2.tla b/TLAplus/TDMv2/RT_TDMv2.tla
deleted file mode 100644
index c4a4ac52d8fc1e1e82f7b1f877cc1e39d3385ea9..0000000000000000000000000000000000000000
--- a/TLAplus/TDMv2/RT_TDMv2.tla
+++ /dev/null
@@ -1,36 +0,0 @@
------------------------------- MODULE RT_TDMv2 ------------------------------
-EXTENDS TDMv2, RealTimeNew, Sequences
-
-CONSTANTS
- t_RCD
-
-VARIABLE
- t1,
- t2,
- t3,
- t4
-
-BigInit ==
- /\ Init
- /\ now = 0
- /\ t1 = 0
- /\ t2 = 0
- /\ t3 = 0
-
-\* The time constraints go here
-BigNext ==
- /\ (Next \/ UNCHANGED<<vars>>)
- /\ (NowNext(vars) \/ now' = now)
- \*Intra-bank constraints
- /\ \A b \in BANKS : /\ IntervalLB(t1,{},IssueRD(b),vars,t_RCD,TRUE)
- /\ IntervalLB(t2,{},IssueWR(b),vars,t_RCD,TRUE)
- /\ IntervalLB(t2,IssueRD(b),IssuePRE(b),vars,t_RAS,TRUE)
- /\ DurationValue(TRUE,t3,IssueACT(b),vars,t_RRD)
- \*Inter-bank constraints
- /\ \A tb \in BANKS : \A ob \in BANKS \ {b} : /\ IntervalLB(t4,{IssueRD(ob),IssuePRE(ob)},IssueACT(tb),vars,t_RRD,TRUE)
- /\
-
-=============================================================================
-\* Modification History
-\* Last modified Fri Feb 12 16:37:42 CET 2021 by felipe
-\* Created Fri Feb 12 15:42:50 CET 2021 by felipe
diff --git a/TLAplus/TDMv2/RealTimeNew.tla b/TLAplus/TDMv2/RealTimeNew.tla
deleted file mode 100644
index 8a052638f610ada057c5fda253e77dc059529c0a..0000000000000000000000000000000000000000
--- a/TLAplus/TDMv2/RealTimeNew.tla
+++ /dev/null
@@ -1,119 +0,0 @@
----------------------------- MODULE RealTimeNew ----------------------------
-EXTENDS Reals
-
-VARIABLE now
-
-----------------------------------------------------------------------------
-(***************************************************************************)
-(* 1. Time Passing *)
-(***************************************************************************)
-NowNext(v) ==
- /\ now' \in {r \in Real : r > now}
- /\ UNCHANGED v
-----------------------------------------------------------------------------
-(***************************************************************************)
-(* 2. Constraints on duration of actions *)
-(***************************************************************************)
-DurationBound(STRflag,t,A,v,min,lb,max,ub) ==
-LET TNext == t' = IF <<A>>_v \/ \neg(ENABLED <<A>>_v)'
- THEN 0
- ELSE t + (now' - now)
- UpperBound == IF STRflag = TRUE
- THEN IF ub THEN t' =< max ELSE t' < max
- ELSE A => IF ub THEN t =< max ELSE t < max
- LowerBound == A => IF lb THEN t >= min ELSE t > min
-IN /\ TNext
- /\ UpperBound
- /\ LowerBound
-
-DurationUB(STRflag,t,A,v,max,ub) ==
-LET TNext == t' = IF <<A>>_v \/ \neg(ENABLED <<A>>_v)'
- THEN 0
- ELSE t + (now' - now)
- UpperBound == IF STRflag = TRUE
- THEN IF ub THEN t' =< max ELSE t' < max
- ELSE A => IF ub THEN t =< max ELSE t < max
-IN /\ TNext
- /\ UpperBound
-
-DurationLB(t,A,v,min,lb) ==
-LET TNext == t' = IF <<A>>_v \/ \neg(ENABLED <<A>>_v)'
- THEN 0
- ELSE t + (now' - now)
- LowerBound == A => IF lb THEN t >= min ELSE t > min
-IN /\ TNext
- /\ LowerBound
-
-DurationValue(STRflag,t,A,vars,val) ==
-LET TNext == t' = IF <<A>>_vars \/ \neg(ENABLED <<A>>_vars)'
- THEN 0
- ELSE t + (now' - now)
- ValueBound == IF STRflag = TRUE THEN t' = val ELSE A => t = val
-IN /\ TNext
- /\ ValueBound
-----------------------------------------------------------------------------
-(***************************************************************************)
-(* 3. Constraints on time interval between actions *)
-(***************************************************************************)
-IntervalBound(STRflag,t,Acts,B,v,min,lb,max,ub) ==
-LET TNext == t' = IF <<B>>_v \/ \neg(ENABLED <<Acts \/ B>>_v)'
- THEN 0
- ELSE t + (now' - now)
- UpperBound == IF STRflag = TRUE
- THEN IF ub THEN t' =< max ELSE t' < max
- ELSE B => IF ub THEN t =< max ELSE t < max
- LowerBound == B => IF lb THEN t >= min ELSE t > min
-IN /\ TNext
- /\ UpperBound
- /\ LowerBound
-
-IntervalUB(STRflag,t,Acts,B,v,max,ub)==
-LET TNext == t' = IF <<B>>_v \/ \neg(ENABLED <<Acts \/ B>>_v)'
- THEN 0
- ELSE t + (now' - now)
- UpperBound == IF STRflag = TRUE
- THEN IF ub THEN t' =< max ELSE t' < max
- ELSE B => IF ub THEN t =< max ELSE t < max
-IN /\ TNext
- /\ UpperBound
-
-IntervalLB(t,Acts,B,v,min,lb) ==
-LET TNext == t' = IF <<B>>_v \/ \neg(ENABLED <<Acts \/ B>>_v)'
- THEN 0
- ELSE t + (now' - now)
- LowerBound == B => IF lb THEN t >= min ELSE t > min
-IN /\ TNext
- /\ LowerBound
-
-IntervalValue(STRflag,t,Acts,B,vars,val) ==
-LET TNext == t' = IF <<B>>_vars \/ \neg(ENABLED <<Acts \/ B>>_vars)'
- THEN 0
- ELSE t + (now' - now)
- ValueBound == IF STRflag = TRUE THEN t' = val ELSE B => t = val
-IN /\ TNext
- /\ ValueBound
-----------------------------------------------------------------------------
-(***************************************************************************)
-(* 4. Advanced Time Patterns *)
-(***************************************************************************)
-\* A execution is delayed by val time units
-Delay(A,val,t,vars) ==
- DurationValue(TRUE,t,A,vars,val)
-
-\* A must terminate at max at t
-Deadline(A,val,t,vars) ==
- DurationUB(TRUE,t,A,vars,val,TRUE)
-
-\* If A does not occur in val time units, then execute the action B
-Timeout(A,B,val,t1,t2,vars) ==
- /\ DurationUB(FALSE,t1,A,vars,val,TRUE)
- /\ DurationValue(TRUE,t2,B,vars,val)
-(***************************************************************************)
-(* Non-Zeno Condition *)
-(***************************************************************************)
-RTFairness(v) ==
- \A r \in Real : WF_now(NowNext(v) /\ (now' > r))
-=============================================================================
-\* Modification History
-\* Last modified Fri Feb 12 14:56:41 CET 2021 by felipe
-\* Created Fri Feb 12 13:13:32 CET 2021 by felipe
diff --git a/TLAplus/TDMv2/TDMv2.tla b/TLAplus/TDMv2/TDMv2.tla
deleted file mode 100644
index 506641985732848cc2462e2125565fb986157d7e..0000000000000000000000000000000000000000
--- a/TLAplus/TDMv2/TDMv2.tla
+++ /dev/null
@@ -1,78 +0,0 @@
-------------------------------- MODULE TDMv2 -------------------------------
-(***************************************************************************)
-(* This is the functional module explaining the working mechanisms of TDM, *)
-(* time related expressions are decribed in RealTimeNew *)
-(***************************************************************************)
-EXTENDS Integers, Reals, Sequences, SequencesExt, FiniteSets
-
-CONSTANTS BANKS, REQUESTORS
-
-\* On a private bank policy, each requestor is served in a different DRAM bank
-ASSUME Cardinality(BANKS) = Cardinality(REQUESTORS)
-
-\* This is the set of banks converted to a sequence (tuple)
-tBANKS == SetToSeq(BANKS)
-
-VARIABLES
- slotOwner,
- slotCounter,
- lastCmd,
- bus_dir,
- bus_status
-
-BusDir == {"RD","WR"}
-BusStatus == {"IDLE","BUSY"}
-
-TypeOK ==
- /\ slotOwner \in BANKS
- /\ slotCounter \in 1..Len(tBANKS)
- /\ lastCmd \in [BANKS -> {"NOP","PRE","ACT","RD","WR"}]
- /\ bus_dir \in BusDir
- /\ bus_status \in BusStatus
------------------------------------------------------------------------------
-(***************************************************************************)
-(* Initial Predicate *)
-(***************************************************************************)
-Init ==
- /\ slotOwner = CHOOSE b \in BANKS : TRUE
- /\ slotCounter = 0
- /\ lastCmd = [b \in BANKS |-> "NOP"]
- /\ bus_dir = CHOOSE v \in BusDir : TRUE
- /\ bus_status = CHOOSE v \in BusStatus : TRUE
-
-(***************************************************************************)
-(* Scheduler Actions *)
-(***************************************************************************)
-IssueACT(b) == /\ lastCmd[b] \in {"NOP","PRE"}
- /\ slotOwner = b
- /\ lastCmd' = [lastCmd EXCEPT ![b] = "ACT"]
- /\ UNCHANGED <<slotOwner,slotCounter,bus_dir,bus_status>>
-
-IssueRD(b) ==
-
-IssueWR(b) ==
-
-IssuePRE(b) ==
-
-UseBus(b) ==
-
-ReleaseBus(b) ==
-
-SchChange ==
-
-Next ==
- \/ \E b \in BANKS : \/ IssueACT(b)
- \/ IssueRD(b)
- \/ IssueWR(b)
- \/ IssuePRE(b)
- \/ UseBus(b)
- \/ ReleaseBus(b)
- \/ SchChange
------------------------------------------------------------------------------
-vars == <<slotOwner,SlotCounter,lastCmd,bus_dir,bus_status>>
-L == WF_vars(Next)
-Spec == Init /\ [][Next]_vars /\ L
-=============================================================================
-\* Modification History
-\* Last modified Fri Feb 12 15:42:19 CET 2021 by felipe
-\* Created Fri Feb 12 11:43:19 CET 2021 by felipe
diff --git a/TLAplus/TDMv3/TDMv3.tla b/TLAplus/TDMv3/TDMv3.tla
deleted file mode 100644
index e1fab612bf1c9ae19138d2fcfd5abc10cf9c00b9..0000000000000000000000000000000000000000
--- a/TLAplus/TDMv3/TDMv3.tla
+++ /dev/null
@@ -1,288 +0,0 @@
-------------------------------- MODULE TDMv3 -------------------------------
-EXTENDS Naturals, FiniteSets, Sequences, SequencesExt
-
-(***************************************************************************)
-(* Utility functions *)
-(***************************************************************************)
-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
- CrRq, \* The set of critical requestors
- NCrRq, \* The set of non-critical requestors
- AllBanks, \* The set of DRAM private banks
- Mapping, \* Bank Adress Maping
- TDM_Slot, \* The length of the TDM slot
- Queue_Capacity \* The capacity of the request queue
-
-\*This produces a function that maps requestors to banks
-Requestors == CrRq \cup NCrRq
-tMapping == SetToSeq(Mapping)
-BankMapping == [req \in Requestors |-> tMapping[req]]
-
-ASSUME
- /\ Cardinality(Requestors) = Cardinality(Mapping)
-
-NumberOfSlots == Cardinality(CrRq)
-
-(***************************************************************************)
-(* In TLA+ language, arrays are functions, and can be also seen as a hash *)
-(* map. A record is a analogue to a data structure, where which field is *)
-(* also a function. So, it can also be seen as a two variable function, *)
-(* or a matrix. And finally, in this module, we have a tuple (or *)
-(* sequence) of records, which is analogue to 3d function *)
-(***************************************************************************)
-
-VARIABLES
- time,
- control,
- req_under_treatment,
- queue,
- request_count,
- slot_count,
- slot_owner,
- row_buffer,
- slack,
- bank_state,
- timer
-
-vars == <<time,control,req_under_treatment,queue,request_count,
- slot_count,slot_owner,row_buffer,slack,bank_state,timer>>
-
-CMDS == {"NOP","ACT","RD","BUS","WR","PRE","REF"}
-Control == {"IDLE","ARRIVAL","TREATMENT","COMPLETED"}
-
-\*Limit the model checking
-max_time == 50
-max_slots == 10
-max_requests == 100
-
-\* For now there are no type constraints on : queue, req_under_treatment
-
-TypeOK ==
- /\ time \in 0..500
- /\ control \in Control
- /\ request_count \in [Requestors -> 0..max_requests]
- /\ slot_count \in 1..10
- /\ slot_owner \in 1..NumberOfSlots
- /\ row_buffer \in [AllBanks -> {"OPEN","CLOSED"}]
- /\ slack \in [CrRq -> Nat]
- /\ bank_state \in [AllBanks -> CMDS]
-
-(***************************************************************************)
-(* O problema de usar o modelo com contatdores e clocks (ideal e seguro) é *)
-(* a complexidade de checagem do modelo. Pode-se argumentar então que o *)
-(* modelo aqui representado não corresponde exatamente ao controlador. O *)
-(* controlador implementado em hardware seria correto por design (timing *)
-(* constraints usadas como contadores) ou baseado em um modelo tal que *)
-(* esse? O controlador desta especificação não representa o mesmo da outra *)
-(***************************************************************************)
------------------------------------------------------------------------------
-(***************************************************************************)
-(* Init state predicate *)
-(***************************************************************************)
-Init ==
- /\ time = 0
- /\ control = "IDLE"
- /\ req_under_treatment = [type |-> "NONE",
- deadline |-> 0,
- target |-> "NONE",
- number |-> 0,
- owner |-> 0,
- issue_date |-> 0,
- delayed_issue_date |-> 0,
- hit_miss |-> "NONE"]
- /\ queue = <<>>
- /\ request_count = [r \in Requestors |-> 0]
- /\ slot_count = 1
- /\ slot_owner = 1
- /\ row_buffer = [b \in AllBanks |-> "CLOSED"]
- /\ slack = [req \in CrRq |-> 0]
- /\ bank_state = [b \in AllBanks |-> "NOP"]
- /\ timer = 0
------------------------------------------------------------------------------
-(***************************************************************************)
-(* Actions that representing the issuing of DRAM commands, they are the *)
-(* only ones that enable time to elapse *)
-(***************************************************************************)
-IssueACT(bank) ==
- /\ control = "TREATMENT"
- /\ bank_state[bank] = "ACT"
- /\ time' = time + 1
- /\ bank_state' = IF req_under_treatment.type = "RD"
- THEN [bank_state EXCEPT ![bank] = "RD"]
- ELSE [bank_state EXCEPT ![bank] = "WR"]
- /\ UNCHANGED<<control,req_under_treatment,queue,request_count,
- slot_count,slot_owner,row_buffer,slack,timer>>
-
-IssueRD(bank) ==
-LET t_RCD == 6
-IN /\ control = "TREATMENT"
- /\ bank_state[bank] = "RD"
- /\ time' = time + t_RCD
- /\ bank_state' = [bank_state EXCEPT ![bank] = "BUS"]
- /\ UNCHANGED<<control,req_under_treatment,queue,request_count,
- slot_count,slot_owner,row_buffer,slack,timer>>
-
-IssueWR(bank) ==
-LET t_RCD == 6
-IN /\ control = "TREATMENT"
- /\ bank_state[bank] = "WR"
- /\ time' = time + t_RCD
- /\ bank_state' = [bank_state EXCEPT ![bank] = "BUS"]
- /\ UNCHANGED<<control,req_under_treatment,queue,request_count,
- slot_count,slot_owner,row_buffer,slack,timer>>
-
-\* For RD requests, the PRE command can be issued instanteneously, as for WR requests
-\* there is a WR to PRE timing constraint
-IssuePRE(bank) ==
-LET t_WR == 6
- t_RTP == 4
- t_RL == 6
- t_BURST == 4
-IN /\ control = "TREATMENT"
- /\ control' = "COMPLETED"
- /\ bank_state[bank] = "PRE"
- /\ time' = IF req_under_treatment.type = "WR"
- THEN time + t_WR
- ELSE IF t_RTP >= t_RL + t_BURST
- THEN time + t_RTP - (t_RL + t_BURST)
- ELSE time
- /\ bank_state' = [bank_state EXCEPT ![bank] = "NOP"]
- /\ req_under_treatment' = [req_under_treatment EXCEPT !.owner = 0]
- /\ UNCHANGED<<queue,request_count,
- slot_count,slot_owner,row_buffer,slack,timer>>
-
-UsingBus(bank) ==
-LET t_RL == 6
- t_WL == 5
- t_BURST == 4
-IN /\ control = "TREATMENT"
- /\ bank_state[bank] = "BUS"
- /\ time' = IF req_under_treatment.type = "RD"
- THEN time + t_RL + t_BURST
- ELSE time + t_WL + t_BURST
- /\ bank_state' = [bank_state EXCEPT ![bank] = "PRE"]
- /\ UNCHANGED<<control,req_under_treatment,queue,request_count,
- slot_count,slot_owner,row_buffer,slack,timer>>
------------------------------------------------------------------------------
-\* Have to create a completed action, which will say
-(***************************************************************************)
-(* This action has to do the following things 1. Decide which is the next *)
-(* request (on the request queue) is to be treated 2. Decide which *)
-(* is the order of commands that has to be issued for that request 3. *)
-(* Decide to leave the row buffer open or closed based on the amount of *)
-(* slack gained. *)
-(***************************************************************************)
-\* Slacks are already considered in the delayed issue date, so, among all requests
-\* in the queue, we choose from EDF.
-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<<time,request_count,slot_count,slot_owner,row_buffer,slack,timer>>
------------------------------------------------------------------------------
-(***************************************************************************)
-(* Actions that model the arrival of new tasks into the system. They are *)
-(* stored in the request queue. *)
-(***************************************************************************)
-\* so_did -> slot owner of 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 - time)
- THEN ModuloSum((slack[req]%TDM_Slot)+1,slot_owner,NumberOfSlots)
- ELSE slot_owner
- dist == IF (time = TDM_Slot*(slot_count - 1)) /\ (req = slot_owner)
- THEN 0
- ELSE IF req = so_did
- THEN NumberOfSlots
- 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 |-> time,
- delayed_issue_date |-> time + slack[req],
- deadline |-> calc_deadline,
- type |-> ty,
- hit_miss |-> hm]
-\* Requist arrival
-\* 1. Only one request per requestor in the queue
-\* 2. No consecutive arrivals
-\* 3. There are at least arrival_rate cycles between two requests of the same requestor
-IN /\ req \notin {queue[n].owner : n \in 1..Len(queue)}
- /\ control /= "ARRIVAL"
- /\ time - request_count[req]*arrival_rate >= 0
- /\ control' = "ARRIVAL"
- /\ request_count' = [request_count EXCEPT ![req] = request_count[req] + 1]
- /\ queue' = Append(queue,request_instance)
- /\ UNCHANGED<<time,req_under_treatment,slot_count,slot_owner,row_buffer,slack,bank_state,timer>>
------------------------------------------------------------------------------
-\* From RealTimeNew Module
-IntervalLB(t,Acts,B,v,min,lb) ==
-LET TNext == t' = IF <<B>>_v \/ \neg(ENABLED <<Acts \/ B>>_v)'
- THEN 0
- ELSE t + (time' - time)
- LowerBound == B => IF lb THEN t >= min ELSE t > min
-IN /\ TNext
- /\ LowerBound
------------------------------------------------------------------------------
-(***************************************************************************)
-(* Next Predicate *)
-(***************************************************************************)
-Next ==
- \/ request_arrival(1,"RD","HIT",10)
- \/ request_arrival(2,"WR","HIT",20)
- \/ treat_request
- \/ \E b \in AllBanks : \/ IssueACT(b)
- \/ IssueRD(b)
- \/ IssueWR(b)
- \/ IssuePRE(b)
- \/ UsingBus(b)
- /\ LET t_RCD == 6 IN \A b \in AllBanks: IntervalLB(timer,TRUE,IssueRD(b),vars,t_RCD,TRUE)
------------------------------------------------------------------------------
-(***************************************************************************)
-(* Fairness and Temporal Formula *)
-(***************************************************************************)
-L == /\ WF_vars(request_arrival(1,"RD","HIT",10))
- /\ WF_vars(request_arrival(2,"WR","HIT",12))
- /\ WF_vars(treat_request)
- /\ \A b \in AllBanks : /\ SF_vars(IssueACT(b))
- /\ SF_vars(IssueRD(b))
- /\ SF_vars(IssueWR(b))
- /\ SF_vars(UsingBus(b))
- /\ SF_vars(IssuePRE(b))
-
-Spec == Init /\ [][Next]_vars /\ L
------------------------------------------------------------------------------
-(***************************************************************************)
-(* Invariants *)
-(***************************************************************************)
-\* The queue never becomes full
-FullQueue == Len(queue) =< Queue_Capacity
-\* The queue never has two requests of the same requestor
-OneRequestInTheQueue ==
-LET Owners == {queue[n].owner : n \in 1..Len(queue)}
-IN \A requestor \in Requestors : Cardinality({owner \in Owners : owner = requestor}) =< 1
-
-(***************************************************************************)
-(* Temporal Properties *)
-(***************************************************************************)
-\* Requests are eventually served
-MaxTime == <>(time = max_time)
-=============================================================================
-\* Modification History
-\* Last modified Fri Feb 26 18:53:51 CET 2021 by felipe
-\* Created Fri Feb 19 10:11:16 CET 2021 by felipe
diff --git a/TLAplus/TDMv5/TDMv5.tla b/TLAplus/TDMv5/TDMv5.tla
deleted file mode 100644
index f74d19b3074f61286ad3207edb24250efe2690b4..0000000000000000000000000000000000000000
--- a/TLAplus/TDMv5/TDMv5.tla
+++ /dev/null
@@ -1,295 +0,0 @@
-------------------------------- MODULE TDMv5 -------------------------------
-EXTENDS Integers, FiniteSets, Sequences, SequencesExt
-
-\* 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
- \* 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
- 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 == <<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"}
-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 ==
- /\ 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 ==
- /\ 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",
- number |-> 0,
- owner |-> 0,
- issue_date |-> 0,
- delayed_issue_date |-> 0,
- hit_miss |-> "NONE"]
- /\ 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"
------------------------------------------------------------------------------
-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) ==
- /\ 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) ==
- /\ bank_state[this_bank] = "RD"
- /\ control = "TREATMENT"
- \* Checks if command is both intra and inter-ready
- /\ \A bank \in Banks : TimedOut_2dim(bank,"RD",cmds_lbtimer)
- \* Sets intra bank timers
- /\ 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 : /\ 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) ==
- /\ bank_state[this_bank] = "WR"
- /\ control = "TREATMENT"
- \* Checks if command is both intra and inter-ready
- /\ \A bank \in Banks : TimedOut_2dim(bank,"RD",cmds_lbtimer)
- \* Sets intra bank timers
- /\ 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} : 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) ==
- /\ 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) ==
- /\ bank_state[this_bank] = "RLSBUS"
- /\ control = "TREATMENT"
- /\ \A bank \in Banks : TimedOut_2dim(bank,"RLSBUS",cmds_lbtimer)
- /\ IF req_under_treatment.type = "WR"
- THEN Set2dimTimer(this_bank,"PRE",cmds_lbtimer,t_WR)
- ELSE TRUE
- /\ \A bank \in Banks : IF req_under_treatment.type = "WR"
- THEN Set2dimTimer(bank,"RD",cmds_lbtimer,t_WTR)
- ELSE TRUE
- /\ 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) ==
- /\ bank_state[this_bank] = "PRE"
- /\ control = "TREATMENT"
- /\ \A bank \in Banks : TimedOut_2dim(bank,"PRE",cmds_lbtimer)
- \* Intra-bank : PRE to ACT
- /\ Set2dimTimer(this_bank,"ACT",cmds_lbtimer,t_RP)
- \* Complection : bank becomes idle again
- /\ 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>>
------------------------------------------------------------------------------
-TNext(bank) == \/ IssueACT(bank)
- \/ IssueRD(bank)
- \/ IssueWR(bank)
- \/ UseBus(bank)
- \/ ReleaseBus(bank)
- \/ IssuePRE(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
------------------------------------------------------------------------------
-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 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
deleted file mode 100644
index 20064c3daaa5cee866d357df887e41053ce3459b..0000000000000000000000000000000000000000
--- a/TLAplus/TDMv6/TDMv6.tla
+++ /dev/null
@@ -1,225 +0,0 @@
-------------------------------- 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