libtlafmt 0.4.1

A formatter library for TLA+ specs, core of tlafmt
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

------------------------ MODULE LiveWriteThroughCache ----------------------- 
(***************************************************************************)
(* This module adds the liveness condition described in the section "The   *)
(* Write-Through Cache" to the specification Spec of module                *)
(* WriteThroughCache.  To allow us to check it with TLC, we actually use   *)
(* the equivalent definition of Spec from module                           *)
(* WriteThroughCacheInstanced.                                             *)
(***************************************************************************)

EXTENDS WriteThroughCacheInstanced

vars == <<memInt, wmem, buf, ctl, cache, memQ>>

QCond == \/ Len(memQ) = QLen
         \/ \E i \in 1 .. Len(memQ) : memQ[i][2].op = "Rd"

Liveness == /\ \A p \in Proc : /\ WF_vars(Rsp(p) \/ DoRd(p))
                               /\ SF_vars(RdMiss(p) \/ DoWr(p))
            /\ WF_vars((QCond /\ MemQWr) \/ MemQRd)

LSpec == Spec /\ Liveness

=============================================================================

Liveness == /\ \A p \in Proc : /\ WF_vars(Rsp(p) \/ DoRd(p))
                               /\ SF_vars(RdMiss(p) \/ DoWr(p))
            /\ WF_vars(MemQWr \/ MemQRd)