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
29
30
31
32
33
34
35

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/LiveWriteThroughCache.tla
---
------------------------- 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)