TLA+ - WIP : Modularization of functional aspects and temporal properties

TLAplus/TDMv2/RT_TDMv2.tla

+------------------------------ 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

TLAplus/TDMv2/TDMv2.tla

@@ -28,15 +28,18 @@ TypeOK ==
     /\ slotCounter \in 1..Len(tBANKS)
     /\ lastCmd \in [BANKS -> {"NOP","PRE","ACT","RD","WR"}]
     /\ bus_dir \in BusDir
-    /\ bus_status \in BusStatus
-    
+    /\ 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                                                       *)
 (***************************************************************************)
@@ -56,7 +59,7 @@ UseBus(b) ==
 ReleaseBus(b) ==
 
 SchChange ==
------------------------------------------------------------------------------
+
 Next == 
     \/ \E b \in BANKS : \/ IssueACT(b)
                         \/ IssueRD(b)
@@ -65,7 +68,11 @@ Next ==
                         \/ 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:25:06 CET 2021 by felipe
+\* Last modified Fri Feb 12 15:42:19 CET 2021 by felipe
 \* Created Fri Feb 12 11:43:19 CET 2021 by felipe