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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/InternalMemory.tla
---
---------------------------- MODULE InternalMemory -----------------------------
EXTENDS MemoryInterface
VARIABLES mem, ctl, buf
--------------------------------------------------------------------------------
IInit ==
    /\ mem \in [Adr -> Val]
    /\ ctl = [p \in Proc |-> "rdy"]
    /\ buf = [p \in Proc |-> NoVal]
    /\ memInt \in InitMemInt

TypeInvariant ==
    /\ mem \in [Adr -> Val]
    /\ ctl \in [Proc -> {"rdy", "busy", "done"}]
    /\ buf \in [Proc -> MReq \union Val \union {NoVal}]

Req(p) ==
    /\ ctl[p] = "rdy"
    /\ \E req \in MReq:
        /\ Send(p, req, memInt, memInt')
        /\ buf' = [buf EXCEPT ![p] = req]
        /\ ctl' = [ctl EXCEPT ![p] = "busy"]
    /\ UNCHANGED mem

Do(p) ==
    /\ ctl[p] = "busy"
    /\ mem' = IF buf[p].op = "Wr"
        THEN [mem EXCEPT ![buf[p].adr] = buf[p].val]
        ELSE mem
    /\ buf' = [buf EXCEPT ![p] = IF buf[p].op = "Wr"
        THEN NoVal
        ELSE mem[buf[p].adr]]
    /\ ctl' = [ctl EXCEPT ![p] = "done"]
    /\ UNCHANGED memInt

Rsp(p) ==
    /\ ctl[p] = "done"
    /\ Reply(p, buf[p], memInt, memInt')
    /\ ctl' = [ctl EXCEPT ![p] = "rdy"]
    /\ UNCHANGED << mem, buf >>

INext == \E p \in Proc: Req(p) \/ Do(p) \/ Rsp(p)

ISpec == IInit /\ [][INext]_<< memInt, mem, ctl, buf >>
--------------------------------------------------------------------------------
THEOREM ISpec => []TypeInvariant
================================================================================