diff --git a/TLAplus/TDMv5/TDMv5.tla b/TLAplus/TDMv5/TDMv5.tla
new file mode 100644
index 0000000000000000000000000000000000000000..5644eaed32228eaac115a80c62ed022f5acdf0ec
--- /dev/null
+++ b/TLAplus/TDMv5/TDMv5.tla
@@ -0,0 +1,156 @@
+------------------------------- MODULE TDMv5 -------------------------------
+EXTENDS Reals, Integers
+
+Max(a,b) == IF a >= b THEN a ELSE b
+
+CONSTANTS 
+    Banks,
+    \* 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
+
+VARIABLES
+    state,
+    lbtimer,
+    now,
+    req_under_treatment
+
+vars == <<state,lbtimer,now,req_under_treatment>>
+
+CMDS == {"IDLE","USEBUS","RLSBUS","ACT","RD","WR","PRE"}
+
+\* How to express the type predicate for lbtimer ? 
+\* Bounding time for now
+maxtime == 100
+
+TypeOK ==
+    /\ state \in [Banks -> CMDS]
+    /\ now \in 0..maxtime
+
+Init ==
+    /\ state = [b \in Banks |-> "IDLE"]
+    /\ lbtimer = [b \in Banks, c \in CMDS |-> 0]
+    /\ now = 0
+    /\ req_under_treatment = [type |-> "NONE",
+                              deadline |-> 0,
+                              target |-> "NONE",
+                              number |-> 0,
+                              owner |-> 0,
+                              issue_date |-> 0,
+                              delayed_issue_date |-> 0,
+                              hit_miss |-> "NONE"]
+
+\* QUESTION : How could I model the request arrival and treatment with this new model ?
+\* Opt 1. By bounds as well.
+-----------------------------------------------------------------------------
+SetTimer(a,b,timer,value) == timer' = [timer EXCEPT ![a,b] = value]
+TimedOut(a,b,timer) == timer[a,b] = 0    
+-----------------------------------------------------------------------------
+IssueACT(this_bank) ==
+    /\ state[this_bank] = "ACT"
+    \* Checks if command is both intra and inter-ready
+    /\ \A bank \in Banks : TimedOut(bank,"ACT",lbtimer)
+    \* Sets intra bank timers
+    /\ SetTimer(this_bank,"RD",lbtimer,t_RCD)
+    /\ SetTimer(this_bank,"WR",lbtimer,t_RCD)
+    /\ SetTimer(this_bank,"ACT",lbtimer,t_RC)
+    /\ SetTimer(this_bank,"PRE",lbtimer,t_RAS)
+    \* Sets inter bank timers
+    /\ \A other_bank \in Banks \ {this_bank} : SetTimer(other_bank,"ACT",lbtimer,t_RRD)
+    \* Decide the next command to be issued
+    /\ state' = IF req_under_treatment.type = "RD"
+                   THEN [state EXCEPT ![this_bank] = "RD"]
+                   ELSE [state EXCEPT ![this_bank] = "WR"]
+    /\ UNCHANGED<<now,req_under_treatment>>
+    
+IssueRD(this_bank) ==
+    /\ state[this_bank] = "RD"
+    \* Checks if command is both intra and inter-ready
+    /\ \A bank \in Banks : TimedOut(bank,"RD",lbtimer)
+    \* Sets intra bank timers
+    /\ SetTimer(this_bank,"USEBUS",lbtimer,t_RL)
+    /\ SetTimer(this_bank,"PRE",lbtimer,t_RTP)
+    \* Sets inter and inter bank timers
+    /\ \A bank \in Banks : /\ SetTimer(bank,"WR",lbtimer,t_RTW)
+                           /\ SetTimer(bank,"RD",lbtimer,t_CCD)
+    /\ state' = [state EXCEPT ![this_bank] = "USEBUS"]
+    /\ UNCHANGED<<now,req_under_treatment>>
+
+IssueWR(this_bank) ==
+    /\ state[this_bank] = "WR"
+    \* Checks if command is both intra and inter-ready
+    /\ \A bank \in Banks : TimedOut(bank,"RD",lbtimer)
+    \* Sets intra bank timers
+    /\ SetTimer(this_bank,"USEBUS",lbtimer,t_WL)
+    /\ SetTimer(this_bank,"PRE",lbtimer,t_RTP)
+    \* Sets inter bank timers
+    /\ \A other_bank \in Banks \ {this_bank} : SetTimer(other_bank,"RD",lbtimer,t_WRtoRD)
+    /\ state' = [state EXCEPT ![this_bank] = "USEBUS"]
+    /\ UNCHANGED<<now,req_under_treatment>>
+    
+UseBus(this_bank) ==
+    /\ state[this_bank] = "USEBUS"
+    /\ \A bank \in Banks : TimedOut(bank,"USEBUS",lbtimer)
+    /\ \A bank \in Banks : SetTimer(bank,"RLSBUS",lbtimer,t_BURST)
+    /\ state' = [state EXCEPT ![this_bank] = "RLSBUS"]
+    /\ UNCHANGED<<now,req_under_treatment>>
+    
+ReleaseBus(this_bank) ==
+    /\ state[this_bank] = "RLSBUS"
+    /\ \A bank \in Banks : TimedOut(bank,"RLSBUS",lbtimer)
+    /\ IF req_under_treatment.type = "WR"
+          THEN SetTimer(this_bank,"PRE",lbtimer,t_WR)
+          ELSE TRUE
+    /\ \A bank \in Banks : IF req_under_treatment.type = "WR"
+                              THEN SetTimer(bank,"RD",lbtimer,t_WTR)
+                              ELSE TRUE
+    /\ state' = [state EXCEPT ![this_bank] = "PRE"]
+    /\ UNCHANGED<<now,req_under_treatment>> 
+
+IssuePRE(this_bank) ==
+    /\ state[this_bank] = "PRE"
+    /\ \A bank \in Banks : TimedOut(bank,"PRE",lbtimer)
+    \* Intra-bank : PRE to ACT
+    /\ SetTimer(this_bank,"ACT",lbtimer,t_RP)
+    \* Complection : bank becomes idle again
+    /\ state' = [state EXCEPT ![this_bank] = "IDLE"]
+    /\ UNCHANGED<<now,req_under_treatment>>
+-----------------------------------------------------------------------------
+Tick ==
+    \E d \in {r \in Real: r > 0}:
+        /\ now' = now + d
+        /\ lbtimer' = [b \in Banks, c \in CMDS |-> Max(0,lbtimer[b,c]-d)]
+        /\ UNCHANGED<<state,req_under_treatment>>
+        
+TNext(bank) == \/ IssueACT(bank)
+               \/ IssueRD(bank)
+               \/ IssueWR(bank)
+               \/ UseBus(bank)
+               \/ ReleaseBus(bank)
+               \/ IssuePRE(bank)
+       
+Next == Tick \/ (\E bank \in Banks : TNext(bank))
+-----------------------------------------------------------------------------
+SafetySpec == Init /\ [][Next]_vars
+-----------------------------------------------------------------------------
+Liveness == /\ \A bank \in Banks : WF_vars(TNext(bank))
+            /\ \A r \in Real : <>(now > r)
+Spec == SafetySpec /\ Liveness
+=============================================================================
+\* Modification History
+\* Last modified Wed Mar 03 23:08:30 CET 2021 by felipe
+\* Created Wed Mar 03 20:37:54 CET 2021 by felipe