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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/ChannelRefinement.tla
---
--------------------------- MODULE ChannelRefinement ---------------------------
EXTENDS Naturals, Sequences
VARIABLES h, l

ErrorVal == CHOOSE v: v \notin [val: 1..12, rdy: {0, 1}, ack: {0, 1}]

    BitSeqToNat[s \in Seq({0, 1})] ==
        IF s = <<>> THEN 0 ELSE Head(s) + 2 * BitSeqToNat[Tail(s)]

H == INSTANCE Channel WITH chan <- h, Data <- 1..12
L == INSTANCE Channel WITH chan <- l, Data <- {0,1}
--------------------------------- MODULE Inner ---------------------------------
VARIABLE bitsSent

Init ==
    /\ bitsSent = <<>>
    /\ IF L!Init THEN H!Init
        ELSE h = ErrorVal

SendBit == \E b \in {0, 1}:
    /\ L!Send(b)
    /\ IF Len(bitsSent) < 3
        THEN
            /\ bitsSent' = << b >> \o bitsSent
            /\ UNCHANGED h
        ELSE
            /\ bitsSent' = <<>>
            /\ H!Send(BitSeqToNat[<<b>> \o bitsSent])

RcvBit ==
    /\ L!Rcv
    /\ IF bitsSent = <<>> THEN H!Rcv
        ELSE UNCHANGED h
    /\ UNCHANGED bitsSent

Error ==
    /\ l' /= l
    /\ ~((\E b \in {0, 1}: L!Send(b) ) \/ L!Rcv )
    /\ h' = ErrorVal

Next == SendBit \/ RcvBit \/ Error

InnerIR == Init /\ [][Next]_<< l, h, bitsSent >>
================================================================================
I(bitsSent) == INSTANCE Inner
IR == \EE bitsSent : I(bitsSent)!InnerIR
================================================================================