From 82956f1150a25c826d278d3e23bbeda0425a6be2 Mon Sep 17 00:00:00 2001
From: Felipe <flisboa@telecom-paris.fr>
Date: Tue, 23 Feb 2021 14:08:57 +0100
Subject: [PATCH] TLA+ : Model works, but income of requests is too heavy, have
to model the system to be less charged
---
TLAplus/TDMv3/TDMv3.tla | 31 ++++++++++++++++++++-----------
1 file changed, 20 insertions(+), 11 deletions(-)
diff --git a/TLAplus/TDMv3/TDMv3.tla b/TLAplus/TDMv3/TDMv3.tla
index f1efbcd..df73f0f 100644
--- a/TLAplus/TDMv3/TDMv3.tla
+++ b/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
--
GitLab