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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/AsynchInterface.tla
---
---------------------------- MODULE AsynchInterface ----------------------------
EXTENDS Naturals
CONSTANT Data
VARIABLES val, rdy, ack

TypeInvariant ==
    /\ val \in Data
    /\ rdy \in {0, 1}
    /\ ack \in {0, 1}
--------------------------------------------------------------------------------
Init ==
    /\ val \in Data
    /\ rdy \in {0, 1}
    /\ ack = rdy

Send ==
    /\ rdy = ack
    /\ val' \in Data
    /\ rdy' = 1 - rdy
    /\ UNCHANGED ack

Rcv ==
    /\ rdy /= ack
    /\ ack' = 1 - ack
    /\ UNCHANGED << val, rdy >>

Next == Send \/ Rcv

Spec == Init /\ [][Next]_<< val, rdy, ack >>
--------------------------------------------------------------------------------
THEOREM Spec => []TypeInvariant
================================================================================