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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/RTWriteThroughCache.tla
---
-------------------------- MODULE RTWriteThroughCache --------------------------
EXTENDS WriteThroughCache, RealTime_SS

CONSTANT N
ASSUME (N \in Nat) /\ (Proc = 0 .. N-1)

CONSTANTS Delta, Epsilon, Rho

ASSUME /\ (Delta \in Real)   /\ (Delta > 0)
       /\ (Epsilon \in Real) /\ (Epsilon > 0)
       /\ (Rho \in Real)     /\ (Rho > 0)
       /\ 2*(N+1)*Epsilon + (N+QLen)*Delta \leq Rho
--------------------------------------------------------------------------------
VARIABLE lastP

RTInit == Init /\ (lastP \in Proc)

position(p) == CHOOSE i \in 1..N: p = (lastP + i) % N

canGoNext(p) ==
    \A q \in Proc: (position(q) < position(p))
    => ~ENABLED (RdMiss(q) \/ DoWr(q))

RTRdMiss(p) ==
    /\ canGoNext(p)
    /\ RdMiss(p)
    /\ lastP' = p

RTDoWr(p) ==
    /\ canGoNext(p)
    /\ DoWr(p)
    /\ lastP' = p

RTNext ==
    \/ \E p \in Proc: RTRdMiss(p) \/ RTDoWr(p)
    \/
        /\
            \/ \E p \in Proc:
                \/ Req(p) \/ Rsp(p) \/ DoRd(p)
                \/ \E a \in Adr: Evict(p, a)
            \/ MemQWr \/ MemQRd
        /\ UNCHANGED lastP

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

RTSpec ==
    /\ RTInit /\ [][RTNext]_vars
    /\ RTBound(MemQWr \/ MemQRd, vars, 0, Delta)
    /\ \A p \in Proc:
        /\ RTBound(RTDoWr(p) \/ DoRd(p) \/ Rsp(p),
            vars, 0, Epsilon)
        /\ RTBound(RTRdMiss(p), vars, 0, Epsilon)
    /\ RTnow(vars)
--------------------------------------------------------------------------------
RTM == INSTANCE RTMemory
THEOREM RTSpec => RTM!RTSpec
================================================================================