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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/TestGraphs.tla
---
------------------------------ MODULE TestGraphs -------------------------------
EXTENDS Sequences, Integers
(***************************************************************************)
(* The definitions of some graphs, paths, etc.  used for testing the       *)
(* definitions and the algorithm with the TLC model checker.               *)
(***************************************************************************)

\* Graph 1.
G1 == [states |-> 1..4,
    initials |-> {1, 2},
    actions |-> << {1, 2}, {1, 3}, {4}, {3} >>
]
V1 == {4}

\* Graph 1a.
G1a == [states |-> 1..4,
    initials |-> {3},
    actions |-> << {1, 2}, {1, 3}, {4}, {3} >>]
\* Graph-wise it's impossible to reach state 1 from state 3
V1a == {1}

\* Graph 2. This graph is actually a forest of two graphs
\*    {1,2} /\ {3,4,5}. {1,2} are an SCC.
G2 == [states |-> 1..5,
    initials |-> {1, 3},
    actions |-> << {1, 2}, {1}, {4, 5}, {}, {} >>]
V2 == {2, 5}

\* Graph 3.       
G3 == [states |-> 1..4,
    initials |-> {2},
    actions |-> << {1, 2}, {2, 3}, {3, 4}, {1, 4} >>]
V3 == {1}

\* Graph 4.
G4 == [states |-> 1..9,
    initials |-> {1, 2, 3},
    actions |-> << {3}, {4}, {5}, {6}, {7}, {7}, {8, 9}, {}, {4} >>]
V4 == {8}

\* Graph 5.
G5 == [states |-> 1..9,
    initials |-> {9},
    actions |-> << {4, 2}, {3}, {4}, {5}, {6}, {7}, {8}, {9}, {2} >>]
V5 == {8}

\* Graph 6.
G6 == [states |-> 1..5,
    initials |-> {5},
    actions |-> << {2, 4, 5}, {2}, {1}, {4}, {3} >>]
V6 == {2}

\* Graph Medium (node 22 is a sink)
G7 == [states |-> 1..50,
    initials |-> {1},
    actions |-> << {8, 35}, {15, 46, 22, 23, 50}, {20, 26, 34}, {5, 18, 28, 37, 43}, {18, 28}, {44}, {14, 29}, {42, 45}, {20, 49}, {10, 12, 31, 47},
        {1, 8, 29, 30, 35, 42}, {22, 31}, {10, 12, 22, 27}, {23, 24, 48}, {9, 22, 49}, {9, 35, 50}, {10}, {21, 25, 39}, {7, 29, 33, 43}, {16, 41}, {},
        {4, 36, 39, 47}, {7}, {12, 22, 23}, {5, 6, 39, 44}, {3, 35}, {10, 13, 17}, {6, 25, 33, 32, 43}, {23, 30, 40, 45}, {23, 50}, {24, 38},
        {19, 33}, {6, 7, 14, 38, 48}, {3, 9, 20}, {3, 20, 41}, {10, 38, 47}, {21, 43}, {6, 10, 36, 48}, {36, 38, 39}, {19, 43}, {16},
        {29, 45}, {32}, {38, 39}, {40}, {9, 15, 16, 50}, {17}, {24, 31}, {13, 22, 34}, {35, 23, 50} >>]
V7 == {50}

\* Graph 8.
G8 == [states |-> 1..4,
    initials |-> {1},
    actions |-> << {1, 2}, {2, 3}, {3, 4}, {4} >>]
V8 == {}

\* Graph 9.
G9 == [states |-> {1},
    initials |-> {1},
    actions |-> << {1} >>]
V9 == {1}

\* Graph 10.
G10 == [states |-> {},
    initials |-> {},
    actions |-> << {} >>]
V10 == {}

\* Graph 11.
G11 == [states |-> 1..10,
    initials |-> {},
    actions |-> << {} >>]
V11 == {}

\* Graph 12.
G12 == [states |-> 1..3,
    initials |-> {1, 2, 3},
    actions |-> << {}, {}, {} >>]
V12 == {1}

\* Graph 13 (simple sequence.
G13 == [states |-> 1..3,
    initials |-> {1},
    actions |-> << {2}, {3}, {} >>]
V13 == {}

--------------------------------------------------------------------------------

CONSTANT null
VARIABLES S, C, state, successors, i, counterexample, T, pc

INSTANCE TLCMC WITH StateGraph <- G7 , ViolationStates <- V7

================================================================================