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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/WriteThroughCache.tla
---
--------------------------- MODULE WriteThroughCache ---------------------------
EXTENDS Naturals, Sequences, MemoryInterface
VARIABLES wmem, ctl, buf, cache, memQ
CONSTANT QLen
ASSUME (QLen \in Nat) /\ (QLen > 0)
M == INSTANCE InternalMemory WITH mem <- wmem
--------------------------------------------------------------------------------
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)
--------------------------------------------------------------------------------
LM == INSTANCE Memory
THEOREM Spec => LM!Spec
================================================================================