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/ABCorrectness.tla
---
----------------------------- MODULE ABCorrectness -----------------------------
EXTENDS Naturals
CONSTANTS Data
VARIABLES sBit, sAck, rBit, sent, rcvd
--------------------------------------------------------------------------------
ABCInit ==
    /\ sBit \in {0, 1}
    /\ sAck = sBit
    /\ rBit = sBit
    /\ sent \in Data
    /\ rcvd \in Data

CSndNewValue(d) ==
    /\ sAck = sBit
    /\ sent' = d
    /\ sBit' = 1 - sBit
    /\ UNCHANGED << sAck, rBit, rcvd >>

CRcvMsg ==
    /\ rBit /= sBit
    /\ rBit' = sBit
    /\ rcvd' = sent
    /\ UNCHANGED << sBit, sAck, sent >>

CRcvAck ==
    /\ rBit /= sAck
    /\ sAck' = rBit
    /\ UNCHANGED << sBit, rBit, sent, rcvd >>

ABCNext ==
    \/ \E d \in Data: CSndNewValue(d)
    \/ CRcvMsg \/ CRcvAck
--------------------------------------------------------------------------------
cvars == << sBit, sAck, rBit, sent, rcvd >>

TypeInv ==
    /\ sBit \in {0, 1}
    /\ sAck \in {0, 1}
    /\ rBit \in {0, 1}
    /\ sent \in Data
    /\ rcvd \in Data

ABCFairness == WF_cvars(CRcvMsg) /\ WF_cvars(CRcvAck)

ABCSpec == ABCInit /\ [][ABCNext]_cvars /\ ABCFairness
================================================================================