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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/Channel.tla
---
-------------------------------- MODULE Channel --------------------------------
EXTENDS Naturals
CONSTANT Data
VARIABLE chan

TypeInvariant == chan \in [val: Data, rdy: {0, 1}, ack: {0, 1}]
--------------------------------------------------------------------------------
Init ==
    /\ TypeInvariant
    /\ chan.ack = chan.rdy

Send(d) ==
    /\ chan.rdy = chan.ack
    /\ chan' = [chan EXCEPT !.val = d, !.rdy = 1 - @]

Rcv ==
    /\ chan.rdy /= chan.ack
    /\ chan' = [chan EXCEPT !.ack = 1 - @]

Next == (\E d \in Data: Send(d)) \/ Rcv

Spec == Init /\ [][Next]_chan
--------------------------------------------------------------------------------
THEOREM Spec => []TypeInvariant
================================================================================