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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/AlternatingBit.tla
---
---------------------------- MODULE AlternatingBit -----------------------------
EXTENDS Naturals, Sequences
CONSTANTS Data
VARIABLES msgQ,
    ackQ,
    sBit,
    sAck,
    rBit,
    sent,
    rcvd
--------------------------------------------------------------------------------
ABInit ==
    /\ msgQ = <<>>
    /\ ackQ = <<>>
    /\ sBit \in {0, 1}
    /\ sAck = sBit
    /\ rBit = sBit
    /\ sent \in Data
    /\ rcvd \in Data

ABTypeInv ==
    /\ msgQ \in Seq({0, 1} \X Data)
    /\ ackQ \in Seq({0, 1})
    /\ sBit \in {0, 1}
    /\ sAck \in {0, 1}
    /\ rBit \in {0, 1}
    /\ sent \in Data
    /\ rcvd \in Data
--------------------------------------------------------------------------------
SndNewValue(d) ==
    /\ sAck = sBit
    /\ sent' = d
    /\ sBit' = 1 - sBit
    /\ msgQ' = Append(msgQ, << sBit', d >>)
    /\ UNCHANGED << ackQ, sAck, rBit, rcvd >>

ReSndMsg ==
    /\ sAck /= sBit
    /\ msgQ' = Append(msgQ, << sBit, sent >>)
    /\ UNCHANGED << ackQ, sBit, sAck, rBit, sent, rcvd >>

RcvMsg ==
    /\ msgQ /= <<>>
    /\ msgQ' = Tail(msgQ)
    /\ rBit' = Head(msgQ)[1]
    /\ rcvd' = Head(msgQ)[2]
    /\ UNCHANGED << ackQ, sBit, sAck, sent >>

SndAck ==
    /\ ackQ' = Append(ackQ, rBit)
    /\ UNCHANGED << msgQ, sBit, sAck, rBit, sent, rcvd >>

RcvAck ==
    /\ ackQ /= <<>>
    /\ ackQ' = Tail(ackQ)
    /\ sAck' = Head(ackQ)
    /\ UNCHANGED << msgQ, sBit, rBit, sent, rcvd >>

Lose(q) ==
    /\ q /= <<>>
    /\ \E i \in 1..Len(q):
        q' = [j \in 1..(Len(q) - 1) |-> IF j < i THEN q[j]
            ELSE q[j + 1]]
    /\ UNCHANGED << sBit, sAck, rBit, sent, rcvd >>

LoseMsg == Lose(msgQ) /\ UNCHANGED ackQ

LoseAck == Lose(ackQ) /\ UNCHANGED msgQ

ABNext ==
    \/ \E d \in Data: SndNewValue(d)
    \/ ReSndMsg \/ RcvMsg \/ SndAck \/ RcvAck
    \/ LoseMsg \/ LoseAck
--------------------------------------------------------------------------------
abvars == << msgQ, ackQ, sBit, sAck, rBit, sent, rcvd >>

ABFairness ==
    /\ WF_abvars(ReSndMsg) /\ WF_abvars(SndAck)
    /\ SF_abvars(RcvMsg) /\ SF_abvars(RcvAck)
--------------------------------------------------------------------------------
ABSpec == ABInit /\ [][ABNext]_abvars /\ ABFairness
--------------------------------------------------------------------------------
THEOREM ABSpec => []ABTypeInv
================================================================================