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

----------------------- 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
=============================================================================