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/InnerFIFO.tla
---
------------------------------- MODULE InnerFIFO -------------------------------
EXTENDS Naturals, Sequences
CONSTANT Message
VARIABLES in, out, q
InChan  == INSTANCE Channel WITH Data <- Message, chan <- in
OutChan == INSTANCE Channel WITH Data <- Message, chan <- out
--------------------------------------------------------------------------------
Init ==
    /\ InChan!Init
    /\ OutChan!Init
    /\ q = <<>>

TypeInvariant ==
    /\ InChan!TypeInvariant
    /\ OutChan!TypeInvariant
    /\ q \in Seq(Message)

SSend(msg) ==
    /\ InChan!Send(msg) \* Send msg on channel `in'.
    /\ UNCHANGED << out, q >>

BufRcv ==
    /\ InChan!Rcv                    \* Receive message from channel `in'.
    /\ q' = Append(q, in.val)        \*   and append it to tail of q.
    /\ UNCHANGED out

BufSend ==
    /\ q /= <<>>                      \* Enabled only if q is nonempty.
    /\ OutChan!Send(Head(q))          \* Send Head(q) on channel `out'
    /\ q' = Tail(q)                   \*   and remove it from q.
    /\ UNCHANGED in

RRcv ==
    /\ OutChan!Rcv \* Receive message from channel `out'.
    /\ UNCHANGED << in, q >>

Next ==
    \/ \E msg \in Message: SSend(msg)
    \/ BufRcv
    \/ BufSend
    \/ RRcv

Spec == Init /\ [][Next]_<< in, out, q >>
--------------------------------------------------------------------------------
THEOREM Spec => []TypeInvariant
================================================================================