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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/SpanTreeTest.tla
---
----------------------------- MODULE SpanTreeTest ------------------------------
(***************************************************************************)
(* The specification in this module is a modified version of the one in    *)
(* module SpanTree obtained by replacing the declared constant Edges with  *)
(* a variable of the same name that is set initially to any possible set   *)
(* of edges with nodes in Nodes.  Thus, it can be used to test the         *)
(* algorithm of SpanTree on all possible graphs having a particular number *)
(* of nodes.                                                               *)
(***************************************************************************)
EXTENDS Integers, FiniteSets, Randomization

CONSTANTS Nodes, Root, MaxCardinality

ASSUME /\ Root \in Nodes
       /\ MaxCardinality \in Nat
       /\ MaxCardinality >= Cardinality(Nodes)
       
VARIABLES mom, dist, Edges
vars == << mom, dist, Edges >>

Nbrs(n) == {m \in Nodes: {m, n} \in Edges}

TypeOK ==
    /\ mom \in [Nodes -> Nodes]
    /\ dist \in [Nodes -> Nat]
    /\ \A e \in Edges: (e \subseteq Nodes) /\ (Cardinality(e) = 2)

Init ==
    /\ mom = [n \in Nodes |-> n]
    /\ dist = [n \in Nodes |-> IF n = Root THEN 0 ELSE MaxCardinality]
    /\ Edges \in {E \in SUBSET (SUBSET Nodes): \A e \in E: Cardinality(e) = 2}
    (****************************************************************)
           (* SUBSET S is the set of all subsets of a set S.  Thus, this   *)
           (* allows Edges to have as its initial value any set of sets of *)
           (* nodes containing exactly two nodes.                          *)
           (****************************************************************)

Next == \E n \in Nodes:
    \E m \in Nbrs(n):
        /\ dist[m] < 1 + dist[n]
        /\ \E d \in (dist[m] + 1)..(dist[n] - 1):
            /\ dist' = [dist EXCEPT ![n] = d]
            /\ mom' = [mom EXCEPT ![n] = m]
            /\ Edges' = Edges

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
--------------------------------------------------------------------------------
PostCondition ==
    \A n \in Nodes:
        \/
            /\ n = Root
            /\ dist[n] = 0
            /\ mom[n] = n
        \/
            /\ dist[n] = MaxCardinality
            /\ mom[n] = n
            /\ \A m \in Nbrs(n): dist[m] = MaxCardinality
        \/
            /\ dist[n] \in 1..(MaxCardinality - 1)
            /\ mom[n] \in Nbrs(n)
            /\ dist[n] = dist[mom[n]] + 1

Safety == []((~ENABLED Next) => PostCondition)

Liveness == <>PostCondition
(***************************************************************************)
(* This took a few seconds to check for 4 nodes, and about 25 minutes for  *)
(* 5 nodes on my laptop.  To compute the initial value of Edges, TLC has   *)
(* to compute all the elements of SUBSET (SUBSET Nodes) (the set of all    *)
(* subsets of the set of all sets of nodes) and then throw away all the    *)
(* elements of that set that don't consist entirely of sets having         *)
(* cardinality 2.  For N nodes, SUBSET(SUBSET Nodes) contains 2^(2^N)      *)
(* elements.                                                               *)
(***************************************************************************)
================================================================================
\* Modification History
\* Last modified Mon Jun 17 05:43:38 PDT 2019 by lamport
\* Created Fri Jun 14 03:07:58 PDT 2019 by lamport