diff --git a/TLAplus/FirstModels/TDMv1/TDM.tla b/TLAplus/FirstModels/TDMv1/TDM.tla
new file mode 100644
index 0000000000000000000000000000000000000000..cc0d399ce12e95f6b766328c2bdc93b7c34135b4
--- /dev/null
+++ b/TLAplus/FirstModels/TDMv1/TDM.tla
@@ -0,0 +1,256 @@
+-------------------------------- 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/FirstModels/TDMv2/TDMv2.tla b/TLAplus/FirstModels/TDMv2/TDMv2.tla
new file mode 100644
index 0000000000000000000000000000000000000000..506641985732848cc2462e2125565fb986157d7e
--- /dev/null
+++ b/TLAplus/FirstModels/TDMv2/TDMv2.tla
@@ -0,0 +1,78 @@
+------------------------------- 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/FirstModels/TDMv3/TDMv3.tla b/TLAplus/FirstModels/TDMv3/TDMv3.tla
new file mode 100644
index 0000000000000000000000000000000000000000..e1fab612bf1c9ae19138d2fcfd5abc10cf9c00b9
--- /dev/null
+++ b/TLAplus/FirstModels/TDMv3/TDMv3.tla
@@ -0,0 +1,288 @@
+------------------------------- 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/FirstModels/TDMv4/TDMv4.tla b/TLAplus/FirstModels/TDMv4/TDMv4.tla
new file mode 100644
index 0000000000000000000000000000000000000000..f78fba0cd0213c8203b859d42d3a3e4217c928c0
--- /dev/null
+++ b/TLAplus/FirstModels/TDMv4/TDMv4.tla
@@ -0,0 +1,147 @@
+------------------------------- MODULE TDMv4 -------------------------------
+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)
+
+\* Total : 15 variables. Is this too much ?
+VARIABLES
+ time,
+ lastACT,
+ lastRD,
+ lastWR,
+ lastPRE,
+ lastBUS,
+ control,
+ req_under_treatment,
+ req_queue,
+ req_count,
+ slot_count,
+ slot_owner,
+ bank_state,
+ row_buffer,
+ slack,
+ bus
+
+vars == <<time, lastACT, lastRD, lastWR, lastPRE, lastBUS,
+ control, req_under_treatment, req_queue, req_count, slot_count, slot_owner,
+ bank_state, row_buffer, slack, bus>>
+
+\* Auxiliary sets
+Control == {"IDLE","ARRIVAL","TREATMENT","COMPLETED"}
+CMDS == {"NOP","ACT","RD","BUS","WR","PRE","REF"}
+
+\* Simulation bounds
+max_time == 100
+max_requests == 10
+max_slots == 50
+
+\* Timing constraints
+t_RCD == 6
+t_RP == 6
+t_RC == 21
+t_RAS == 15
+t_WL == 5
+t_RL == 6
+t_RTP == 4
+t_WR == 6
+t_RRD == 4
+t_FAW == 5
+t_RTW == 7
+t_WRtoRD == 13
+t_WTR == 4
+t_BURST == 4
+t_CCD == 4
+
+\* Some variables (for now) don`t have type invariance.
+TypeOK ==
+ /\ time \in 0..max_time
+ /\ lastACT \in [AllBanks -> Nat]
+ /\ lastRD \in [AllBanks -> Nat]
+ /\ lastWR \in [AllBanks -> Nat]
+ /\ lastPRE \in [AllBanks -> Nat]
+ /\ lastBUS \in Nat
+ /\ control \in Control
+ /\ req_count \in [Requestors -> 0..max_requests]
+ /\ slot_count \in 1..max_slots
+ /\ slot_owner \in 1..NumberOfSlots
+ /\ bank_state \in [AllBanks -> CMDS]
+ /\ row_buffer \in [AllBanks -> {"OPEN","CLOSED"}]
+ /\ slack \in [CrRq -> Nat]
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* The Initial Predicate *)
+(***************************************************************************)
+Init ==
+ /\ time = 0
+ /\ lastACT = [b \in AllBanks |-> 100]
+ /\ lastRD = [b \in AllBanks |-> 100]
+ /\ lastWR = [b \in AllBanks |-> 100]
+ /\ lastPRE = [b \in AllBanks |-> 100]
+ /\ lastBUS = 100
+ /\ 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"]
+ /\ req_queue = <<>>
+ /\ req_count = [r \in Requestors |-> 0]
+ /\ slot_count = 1
+ /\ slot_owner = 1
+ /\ bank_state = [b \in AllBanks |-> "NOP"]
+ /\ row_buffer = [b \in AllBanks |-> "CLOSED"]
+ /\ slack = [req \in CrRq |-> 0]
+ /\ bus = [ocup |-> "IDLE", dir |-> CHOOSE dir \in {"RD","WR"} : TRUE]
+
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* DRAM commmands *)
+(***************************************************************************)
+\* Commands are only available when they are intra or inter ready. This ensures
+\* time correctness by design.
+IssueACT(b) ==
+LET
+ ACTintraReady == /\ lastACT[b] >= t_RC /\ lastPRE[b] >= t_RP
+ ACTinterReady == \A m \in AllBanks \ {b} : /\ lastACT[m] >= t_RRD /\ lastACT[m] >= t_FAW
+IN
+ /\ control = "TREATMENT"
+ /\ bank_state[b] = "ACT"
+ /\ ACTintraReady
+ /\ ACTinterReady
+ /\ bank_state' = IF req_under_treatment.type = "RD"
+ THEN [bank_state EXCEPT ![b] = "RD"]
+ ELSE [bank_state EXCEPT ![b] = "WR"]
+ /\ UNCHANGED SetToSeq({{vars[n] : n \in 1..Len(vars)} \ bank_state})
+
+
+=============================================================================
+\* Modification History
+\* Last modified Fri Feb 26 20:28:30 CET 2021 by felipe
+\* Created Fri Feb 26 18:57:44 CET 2021 by felipe
diff --git a/TLAplus/FirstModels/TDMv5/TDMv5.tla b/TLAplus/FirstModels/TDMv5/TDMv5.tla
new file mode 100644
index 0000000000000000000000000000000000000000..f74d19b3074f61286ad3207edb24250efe2690b4
--- /dev/null
+++ b/TLAplus/FirstModels/TDMv5/TDMv5.tla
@@ -0,0 +1,295 @@
+------------------------------- 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/FirstModels/TDMv6/TDMv6.tla b/TLAplus/FirstModels/TDMv6/TDMv6.tla
new file mode 100644
index 0000000000000000000000000000000000000000..7b398bead8b38c31aaab2c710d3ad7d21a905c19
--- /dev/null
+++ b/TLAplus/FirstModels/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
+-----------------------------------------------------------------------------
+Liveness == /\ 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 /\ Liveness
+=============================================================================
+\* Modification History
+\* Last modified Fri Mar 05 15:30:05 CET 2021 by felipe
+\* Created Wed Mar 03 20:37:54 CET 2021 by felipe
\ No newline at end of file
diff --git a/TLAplus/StandardModules/RealTimeNew.tla b/TLAplus/StandardModules/RealTimeNew.tla
new file mode 100644
index 0000000000000000000000000000000000000000..8a052638f610ada057c5fda253e77dc059529c0a
--- /dev/null
+++ b/TLAplus/StandardModules/RealTimeNew.tla
@@ -0,0 +1,119 @@
+---------------------------- 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/StandardModules/SequencesExt.tla b/TLAplus/StandardModules/SequencesExt.tla
new file mode 100644
index 0000000000000000000000000000000000000000..8777a477b02c111b9220d748e01cee05bfe8572d
--- /dev/null
+++ b/TLAplus/StandardModules/SequencesExt.tla
@@ -0,0 +1,145 @@
+---------------------------- 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