diff --git a/TLAplus/TDMv3/TDMv3.tla b/TLAplus/TDMv3/TDMv3.tla
index df73f0f78e4cf6abce887aa4e10f72569d87d9f3..e1fab612bf1c9ae19138d2fcfd5abc10cf9c00b9 100644
--- a/TLAplus/TDMv3/TDMv3.tla
+++ b/TLAplus/TDMv3/TDMv3.tla
@@ -44,10 +44,11 @@ VARIABLES
slot_owner,
row_buffer,
slack,
- bank_state
+ bank_state,
+ timer
vars == <<time,control,req_under_treatment,queue,request_count,
- slot_count,slot_owner,row_buffer,slack,bank_state>>
+ slot_count,slot_owner,row_buffer,slack,bank_state,timer>>
CMDS == {"NOP","ACT","RD","BUS","WR","PRE","REF"}
Control == {"IDLE","ARRIVAL","TREATMENT","COMPLETED"}
@@ -60,7 +61,7 @@ max_requests == 100
\* For now there are no type constraints on : queue, req_under_treatment
TypeOK ==
- /\ time \in 0..max_time
+ /\ time \in 0..500
/\ control \in Control
/\ request_count \in [Requestors -> 0..max_requests]
/\ slot_count \in 1..10
@@ -68,7 +69,15 @@ TypeOK ==
/\ 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 *)
@@ -91,6 +100,7 @@ Init ==
/\ 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 *)
@@ -104,7 +114,7 @@ IssueACT(bank) ==
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>>
+ slot_count,slot_owner,row_buffer,slack,timer>>
IssueRD(bank) ==
LET t_RCD == 6
@@ -113,7 +123,7 @@ IN /\ control = "TREATMENT"
/\ 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>>
+ slot_count,slot_owner,row_buffer,slack,timer>>
IssueWR(bank) ==
LET t_RCD == 6
@@ -122,7 +132,7 @@ IN /\ control = "TREATMENT"
/\ 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>>
+ 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
@@ -140,9 +150,9 @@ IN /\ control = "TREATMENT"
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 = "NONE"]
+ /\ req_under_treatment' = [req_under_treatment EXCEPT !.owner = 0]
/\ UNCHANGED<<queue,request_count,
- slot_count,slot_owner,row_buffer,slack>>
+ slot_count,slot_owner,row_buffer,slack,timer>>
UsingBus(bank) ==
LET t_RL == 6
@@ -155,8 +165,9 @@ IN /\ control = "TREATMENT"
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>>
+ 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 *)
@@ -176,10 +187,10 @@ LET deadlines == {queue[n].deadline : n \in 1..Len(queue)}
ResumeTreatment == UNCHANGED<<queue,req_under_treatment,bank_state>>
IN /\ (control = "ARRIVAL") \/ (control = "COMPLETE" \/ queue /= <<>>)
/\ control' = "TREATMENT"
- /\ IF req_under_treatment.type = "NONE"
+ /\ IF req_under_treatment.owner = 0
THEN StartTreatment
ELSE ResumeTreatment
- /\ UNCHANGED<<time,request_count,slot_count,slot_owner,row_buffer,slack>>
+ /\ 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 *)
@@ -207,32 +218,46 @@ 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"}
+\* 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>>
+ /\ 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",5)
- \/ request_arrival(2,"WR","MISS",10)
+ \/ 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",5))
- /\ WF_vars(request_arrival(2,"WR","MISS",10))
+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))
@@ -245,8 +270,19 @@ 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 Tue Feb 23 13:59:40 CET 2021 by felipe
+\* Last modified Fri Feb 26 18:53:51 CET 2021 by felipe
\* Created Fri Feb 19 10:11:16 CET 2021 by felipe