---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/WriteThroughCacheInstanced.tla
---
---------------------- MODULE WriteThroughCacheInstanced -----------------------
(***************************************************************************)
(* This module is a version of module WriteThroughCache with the INSTANCE *)
(* statements removed, because Version 1 of TLC cannot handle *)
(* instantiation. The one INSTANCE statement that we need to run TLC is *)
(* replaced by the equivalent definitions. Another INSTANCE statement, *)
(* not needed for running TLC, is just commented out. *)
(***************************************************************************)
EXTENDS Naturals, Sequences, MemoryInterface
VARIABLES wmem, ctl, buf, cache, memQ
CONSTANT QLen
ASSUME (QLen \in Nat) /\ (QLen > 0)
(***************************************************************************)
(* At this point, module WriteThroughCache contains the statement *)
(* *)
(* M == INSTANCE InternalMemory WITH mem <- wmem *)
(* *)
(* We perform the instantiations below "by hand". The text below is the *)
(* body of module InternalMemory (minus its EXTENDS and its declarations), *)
(* with wmem substituted everywhere for mem, and with the names of all *)
(* symbols it defines prefixed by "M_". (The actual INSTANCE statement *)
(* prefixes the names with "M!", but we use "_" instead of "!" because *)
(* TLA+ doesn't allow "!" to be used in a symbol name except when it is *)
(* added by instantiation.) *)
(***************************************************************************)
M_IInit ==
/\ wmem \in [Adr -> Val]
/\ ctl = [p \in Proc |-> "rdy"]
/\ buf = [p \in Proc |-> NoVal]
/\ memInt \in InitMemInt
M_TypeInvariant ==
/\ wmem \in [Adr -> Val]
/\ ctl \in [Proc -> {"rdy", "busy", "done"}]
/\ buf \in [Proc -> MReq \union Val \union {NoVal}]
M_Req(p) ==
/\ ctl[p] = "rdy"
/\ \E req \in MReq:
/\ Send(p, req, memInt, memInt')
/\ buf' = [buf EXCEPT ![p] = req]
/\ ctl' = [ctl EXCEPT ![p] = "busy"]
/\ UNCHANGED wmem
M_Do(p) ==
/\ ctl[p] = "busy"
/\ wmem' = IF buf[p].op = "Wr"
THEN [wmem EXCEPT ![buf[p].adr] = buf[p].val]
ELSE wmem
/\ buf' = [buf EXCEPT ![p] = IF buf[p].op = "Wr"
THEN NoVal
ELSE wmem[buf[p].adr]]
/\ ctl' = [ctl EXCEPT ![p] = "done"]
/\ UNCHANGED memInt
M_Rsp(p) ==
/\ ctl[p] = "done"
/\ Reply(p, buf[p], memInt, memInt')
/\ ctl' = [ctl EXCEPT ![p] = "rdy"]
/\ UNCHANGED << wmem, buf >>
M_INext == \E p \in Proc: M_Req(p) \/ M_Do(p) \/ M_Rsp(p)
M_ISpec == M_IInit /\ [][M_INext]_<< memInt, wmem, ctl, buf >>
--------------------------------------------------------------------------------
(***************************************************************************)
(* Below is the rest of module WriteThroughCache, except with each "!" *)
(* replaced by "_". *)
(***************************************************************************)
Init ==
/\ M_IInit
/\ cache = [p \in Proc |-> [a \in Adr |-> NoVal]]
/\ memQ = <<>>
TypeInvariant ==
/\ wmem \in [Adr -> Val]
/\ ctl \in [Proc -> {"rdy", "busy", "waiting", "done"}]
/\ buf \in [Proc -> MReq \union Val \union {NoVal}]
/\ cache \in [Proc -> [Adr -> Val \union {NoVal}]]
/\ memQ \in Seq(Proc \X MReq)
Coherence == \A p, q \in Proc, a \in Adr:
(NoVal \notin {cache[p][a], cache[q][a]})
=> (cache[p][a] = cache[q][a])
--------------------------------------------------------------------------------
Req(p) == M_Req(p) /\ UNCHANGED << cache, memQ >>
Rsp(p) == M_Rsp(p) /\ UNCHANGED << cache, memQ >>
RdMiss(p) ==
/\ (ctl[p] = "busy") /\ (buf[p].op = "Rd")
/\ cache[p][buf[p].adr] = NoVal
/\ Len(memQ) < QLen
/\ memQ' = Append(memQ, << p, buf[p] >>)
/\ ctl' = [ctl EXCEPT ![p] = "waiting"]
/\ UNCHANGED << memInt, wmem, buf, cache >>
DoRd(p) ==
/\ ctl[p] \in {"busy", "waiting"}
/\ buf[p].op = "Rd"
/\ cache[p][buf[p].adr] /= NoVal
/\ buf' = [buf EXCEPT ![p] = cache[p][buf[p].adr]]
/\ ctl' = [ctl EXCEPT ![p] = "done"]
/\ UNCHANGED << memInt, wmem, cache, memQ >>
DoWr(p) ==
LET r == buf[p]
IN
/\ (ctl[p] = "busy") /\ (r.op = "Wr")
/\ Len(memQ) < QLen
/\ cache' = [q \in Proc |->
IF (p = q) \/ (cache[q][r.adr] /= NoVal)
THEN [cache[q] EXCEPT ![r.adr] = r.val]
ELSE cache[q]]
/\ memQ' = Append(memQ, << p, r >>)
/\ buf' = [buf EXCEPT ![p] = NoVal]
/\ ctl' = [ctl EXCEPT ![p] = "done"]
/\ UNCHANGED << memInt, wmem >>
vmem ==
LET f[i \in 0..Len(memQ)] ==
IF i = 0 THEN wmem
ELSE IF memQ[i][2].op = "Rd"
THEN f[i - 1]
ELSE [f[i - 1] EXCEPT ![memQ[i][2].adr] =
memQ[i][2].val]
IN f[Len(memQ)]
MemQWr == LET r == Head(memQ)[2]
IN
/\ (memQ /= <<>>) /\ (r.op = "Wr")
/\ wmem' = [wmem EXCEPT ![r.adr] = r.val]
/\ memQ' = Tail(memQ)
/\ UNCHANGED << memInt, buf, ctl, cache >>
MemQRd ==
LET p == Head(memQ)[1]
r == Head(memQ)[2]
IN
/\ (memQ /= <<>>) /\ (r.op = "Rd")
/\ memQ' = Tail(memQ)
/\ cache' = [cache EXCEPT ![p][r.adr] = vmem[r.adr]]
/\ UNCHANGED << memInt, wmem, buf, ctl >>
Evict(p, a) ==
/\ (ctl[p] = "waiting") => (buf[p].adr /= a)
/\ cache' = [cache EXCEPT ![p][a] = NoVal]
/\ UNCHANGED << memInt, wmem, buf, ctl, memQ >>
Next ==
\/ \E p \in Proc:
\/ Req(p) \/ Rsp(p)
\/ RdMiss(p) \/ DoRd(p) \/ DoWr(p)
\/ \E a \in Adr: Evict(p, a)
\/ MemQWr \/ MemQRd
Spec ==
Init /\ [][Next]_<< memInt, wmem, buf, ctl, cache, memQ >>
--------------------------------------------------------------------------------
THEOREM Spec => [](TypeInvariant /\ Coherence)
--------------------------------------------------------------------------------
(***************************************************************************)
(* We comment out the following instantiation and theorem, since TLC can't *)
(* do anything with them anyway. *)
(***************************************************************************)
\* LM == INSTANCE Memory
\* THEOREM Spec => LM_Spec
================================================================================
THEOREM ISpec => []TypeInvariant
==============================================================