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

------------------ 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 \cup Val \cup {NoVal}]
  /\ cache \in [Proc -> [Adr -> Val \cup {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 
==============================================================