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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/spanning.tla
---
------------------------------- MODULE spanning --------------------------------
EXTENDS Integers
CONSTANTS Proc, NoPrnt, root, nbrs
ASSUME NoPrnt \notin Proc /\ nbrs \subseteq Proc \times Proc
VARIABLES prnt, rpt, msg
vars == << prnt, rpt, msg >>

Init ==
    /\ prnt = [i \in Proc |-> NoPrnt]
    /\ rpt = [i \in Proc |-> FALSE]
    /\ msg = {}

CanSend(i, j) == (<< i, j >> \in nbrs) /\ (i = root \/ prnt[i] /= NoPrnt)

Update(i, j) ==
    /\ prnt' = [prnt EXCEPT ![i] = j]
    /\ UNCHANGED << rpt, msg >>

Send(i) == \E k \in Proc:
    /\ CanSend(i, k) /\ (<< i, k >> \notin msg)
    /\ msg' = msg \union {<< i, k >>}
    /\ UNCHANGED << prnt, rpt >>

Parent(i) ==
    /\ prnt[i] /= NoPrnt /\ ~rpt[i]
    /\ rpt' = [rpt EXCEPT ![i] = TRUE]
    /\ UNCHANGED << msg, prnt >>

Next == \E i, j \in Proc: IF i /= root /\ prnt[i] = NoPrnt /\ << j, i >> \in msg
THEN Update(i, j)
ELSE
    \/ Send(i) \/ Parent(i)
    \/ UNCHANGED << prnt, msg, rpt >>

Spec ==
    /\ Init /\ [][Next]_vars
    /\ WF_vars(\E i, j \in Proc: IF i /= root /\ prnt[i] = NoPrnt /\ << j, i >> \in msg
        THEN Update(i, j)
        ELSE
            \/ Send(i) \/ Parent(i)
            \/ UNCHANGED << prnt, msg, rpt >>)

TypeOK ==
    /\ \A i \in Proc: prnt[i] = NoPrnt \/ << i, prnt[i] >> \in nbrs
    /\ rpt \in [Proc -> BOOLEAN ]
    /\ msg \subseteq Proc \times Proc

Termination == <>(\A i \in Proc: i = root \/ (prnt[i] /= NoPrnt /\ << i, prnt[i] >> \in nbrs))

OneParent == [][\A i \in Proc : prnt[i] # NoPrnt => prnt[i] = prnt'[i]]_vars

SntMsg == \A i \in Proc: (i /= root /\ prnt[i] = NoPrnt => \A j \in Proc: << i, j >> \notin msg)

================================================================================
\* Modification History
\* Last modified Mon Jul 09 13:30:26 CEST 2018 by tthai