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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/Graphs.tla
---
-------------------------------- MODULE Graphs ---------------------------------
LOCAL INSTANCE Naturals
LOCAL INSTANCE Sequences

IsDirectedGraph(G) ==
    /\ G = [node |-> G.node, edge |-> G.edge]
    /\ G.edge \subseteq (G.node \X G.node)

DirectedSubgraph(G) ==
{H \in [node: SUBSET G.node, edge: SUBSET (G.node \X G.node)]:
    IsDirectedGraph(H) /\ H.edge \subseteq G.edge}
--------------------------------------------------------------------------------
IsUndirectedGraph(G) ==
    /\ IsDirectedGraph(G)
    /\ \A e \in G.edge: << e[2], e[1] >> \in G.edge

UndirectedSubgraph(G) == {H \in DirectedSubgraph(G): IsUndirectedGraph(H)}
--------------------------------------------------------------------------------
Path(G) == {p \in Seq(G.node):
    /\ p /= <<>>
    /\ \A i \in 1..(Len(p) - 1): << p[i], p[i + 1] >> \in G.edge}

AreConnectedIn(m, n, G) ==
    \E p \in Path(G): (p[1] = m) /\ (p[Len(p)] = n)

IsStronglyConnected(G) ==
    \A m, n \in G.node: AreConnectedIn(m, n, G)
--------------------------------------------------------------------------------
IsTreeWithRoot(G, r) ==
    /\ IsDirectedGraph(G)
    /\ \A e \in G.edge:
        /\ e[1] /= r
        /\ \A f \in G.edge: (e[1] = f[1]) => (e = f)
    /\ \A n \in G.node: AreConnectedIn(n, r, G)
================================================================================