TLA+ : Model works, but income of requests is too heavy, have to model the...

TLA+ : Model works, but income of requests is too heavy, have to model the system to be less charged

TLAplus/TDMv3/TDMv3.tla

@@ -76,7 +76,14 @@ TypeOK ==
 Init ==
     /\ time = 0
     /\ control = "IDLE"
-    /\ req_under_treatment = "NONE"
+    /\ 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
@@ -133,7 +140,7 @@ IN /\ control = "TREATMENT"
                          THEN time + t_RTP - (t_RL + t_BURST)
                          ELSE time
    /\ bank_state' = [bank_state EXCEPT ![bank] = "NOP"]
-   /\ req_under_treatment' = "NONE"
+   /\ req_under_treatment' = [req_under_treatment EXCEPT !.owner = "NONE"]
    /\ UNCHANGED<<queue,request_count,
                  slot_count,slot_owner,row_buffer,slack>>
    
@@ -160,9 +167,8 @@ IN  /\ control = "TREATMENT"
 \* Slacks are already considered in the delayed issue date, so, among all requests
 \* in the queue, we choose from EDF.
 treat_request ==
-LET deadlines == SelectSeq(queue, LAMBDA elem: elem.deadline)
-    set_deadlines == ToSet(deadlines)
-    min_deadline == Min(set_deadlines)
+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
@@ -170,7 +176,7 @@ LET deadlines == SelectSeq(queue, LAMBDA elem: elem.deadline)
     ResumeTreatment == UNCHANGED<<queue,req_under_treatment,bank_state>>
 IN  /\ (control = "ARRIVAL") \/ (control = "COMPLETE" \/ queue /= <<>>) 
     /\ control' = "TREATMENT"
-    /\ IF req_under_treatment = "NONE" 
+    /\ IF req_under_treatment.type = "NONE" 
           THEN StartTreatment
           ELSE ResumeTreatment
     /\ UNCHANGED<<time,request_count,slot_count,slot_owner,row_buffer,slack>>
@@ -187,7 +193,9 @@ LET so_did == IF slack[req] >= (slot_count*TDM_Slot - time)
                 ELSE slot_owner
     dist == IF (time = TDM_Slot*(slot_count - 1)) /\ (req = slot_owner)
                 THEN 0
-                ELSE NumberOfSlots - so_did + req
+                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)
@@ -199,9 +207,9 @@ LET so_did == IF slack[req] >= (slot_count*TDM_Slot - time)
                          deadline |-> calc_deadline,
                          type |-> ty,
                          hit_miss |-> hm]
-    
 IN /\ time - request_count[req]*arrival_rate >= 0
-   /\ control \in {"IDLE","COMPLETED"}
+   \*/\ control \in {"IDLE","COMPLETED"}
+   /\ control /= "ARRIVAL"
    /\ control' = "ARRIVAL"
    /\ request_count' = [request_count EXCEPT ![req] = request_count[req] + 1]
    /\ queue' = Append(queue,request_instance) 
@@ -224,6 +232,7 @@ Next ==
 (* Fairness and Temporal Formula                                           *)
 (***************************************************************************)
 L == /\ WF_vars(request_arrival(1,"RD","HIT",5))
+     /\ WF_vars(request_arrival(2,"WR","MISS",10))
      /\ WF_vars(treat_request)
      /\ \A b \in AllBanks : /\ SF_vars(IssueACT(b))
                             /\ SF_vars(IssueRD(b))
@@ -231,7 +240,7 @@ L == /\ WF_vars(request_arrival(1,"RD","HIT",5))
                             /\ SF_vars(UsingBus(b))
                             /\ SF_vars(IssuePRE(b))
 
-Spec == Init /\ [][Next]_vars /\ SF_vars(Next)
+Spec == Init /\ [][Next]_vars /\ L
 -----------------------------------------------------------------------------
 (***************************************************************************)
 (* Invariants                                                              *)
@@ -239,5 +248,5 @@ Spec == Init /\ [][Next]_vars /\ SF_vars(Next)
 FullQueue == Len(queue) =< Queue_Capacity
 =============================================================================
 \* Modification History
-\* Last modified Tue Feb 23 12:23:35 CET 2021 by felipe
+\* Last modified Tue Feb 23 13:59:40 CET 2021 by felipe
 \* Created Fri Feb 19 10:11:16 CET 2021 by felipe