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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
|
using System.Collections.Generic;
namespace Microsoft.Dafny {
public class Graph<Node>
{
enum VisitedStatus { Unvisited, OnStack, Visited }
class Vertex {
public readonly Node N;
public readonly List<Vertex!>! Successors = new List<Vertex!>();
public Vertex SccRepresentative; // null if not computed
public List<Vertex!> SccMembers; // non-null only for the representative of the SCC
public int SccId; // valid only for SCC representatives; indicates position of this representative vertex in the graph's topological sort
// the following field is used during the computation of SCCs and of reachability
public VisitedStatus Visited;
// the following fields are used during the computation of SCCs:
public int DfNumber;
public int LowLink;
// the following field is used during a Reaches computation
public int Gen; // generation <= Gen means this vertex has been visited in the current generation
public Vertex(Node n) {
N = n;
}
public void AddSuccessor(Vertex! v) {
Successors.Add(v);
}
}
Dictionary<Node, Vertex!>! vertices = new Dictionary<Node, Vertex!>();
bool sccComputed = false;
List<Vertex!> topologicallySortedRepresentatives; // computed by the SCC computation
invariant sccComputed ==> topologicallySortedRepresentatives != null;
public int SccCount {
get {
ComputeSCCs();
assert topologicallySortedRepresentatives != null; // follows from postcondition of ComputeSCCs and the object invariant
return topologicallySortedRepresentatives.Count;
}
}
int generation = 0;
public Graph()
{
}
/// <summary>
/// Idempotently adds a vertex 'n' to the graph.
/// </summary>
public void AddVertex(Node n) {
GetVertex(n);
}
/// <summary>
/// Idempotently adds a vertex 'n' to the graph and then returns the Vertex for it.
/// </summary>
Vertex! GetVertex(Node n) {
Vertex v = FindVertex(n);
if (v == null) {
v = new Vertex(n);
vertices.Add(n, v);
if (sccComputed) {
assert topologicallySortedRepresentatives != null; // follows from object invariant
v.SccRepresentative = v;
v.SccMembers = new List<Vertex!>();
v.SccMembers.Add(v);
v.SccId = topologicallySortedRepresentatives.Count;
topologicallySortedRepresentatives.Add(v);
}
}
return v;
}
/// <summary>
/// Returns the vertex for 'n' if 'n' is in the graph. Otherwise, returns null.
/// </summary>
Vertex FindVertex(Node n) {
Vertex v;
if (vertices.TryGetValue(n, out v)) {
assert v != null; // follows from postcondition of TryGetValue (since 'vertices' maps to the type Vertex!)
return v;
} else {
return null;
}
}
/// <summary>
/// Idempotently adds verices 'from' and 'to' the graph, and then
/// adds an edge from 'from' to 'to'.
/// </summary>
public void AddEdge(Node from, Node to) {
Vertex v0 = GetVertex(from);
Vertex v1 = GetVertex(to);
v0.AddSuccessor(v1);
sccComputed = false; // the addition of an edge may invalidate any previous computation of the graph's SCCs
}
/// <summary>
/// Idempotently adds 'n' as a vertex and then returns a Node that is the representative element of the
/// strongly connected component containing 'n'.
/// </summary>
public Node GetSCCRepresentative(Node n) {
return GetSCCRepr(n).N;
}
/// <summary>
/// Idempotently adds 'n' as a vertex. Then, returns the number of SCCs before the SCC of 'n' in the
/// topologically sorting of SCCs.
/// </summary>
public int GetSCCRepresentativeId(Node n) {
return GetSCCRepr(n).SccId;
}
Vertex! GetSCCRepr(Node n) {
Vertex v = GetVertex(n);
ComputeSCCs();
assert v.SccRepresentative != null; // follows from what ComputeSCCs does
return v.SccRepresentative;
}
/// <summary>
/// Returns a list of the topologically sorted SCCs, each represented in the list by its representative node.
/// </summary>
public List<Node>! TopologicallySortedComponents() {
ComputeSCCs();
assert topologicallySortedRepresentatives != null; // follows from object invariant
List<Node> nn = new List<Node>();
foreach (Vertex v in topologicallySortedRepresentatives) {
nn.Add(v.N);
}
return nn;
}
/// <summary>
/// Idempotently adds 'n' as a vertex and then returns the set of Node's in the strongly connected component
/// that contains 'n'.
/// </summary>
public List<Node>! GetSCC(Node n) {
Vertex v = GetVertex(n);
ComputeSCCs();
Vertex repr = v.SccRepresentative;
assert repr != null && repr.SccMembers != null; // follows from postcondition of ComputeSCCs
List<Node> nn = new List<Node>();
foreach (Vertex w in repr.SccMembers) {
nn.Add(w.N);
}
return nn;
}
/// <summary>
/// This method sets the SccRepresentative fields of the graph's vertices so that two
/// vertices have the same representative iff they are in the same strongly connected
/// component.
/// As a side effect, this method may change the Visited, DfNumber, and LowLink fields
/// of the vertices.
/// </summary>
void ComputeSCCs()
ensures sccComputed;
{
if (sccComputed) { return; } // check if already computed
// reset all SCC information
topologicallySortedRepresentatives = new List<Vertex!>();
foreach (Vertex v in vertices.Values) {
v.Visited = VisitedStatus.Unvisited;
v.SccMembers = null;
}
Stack<Vertex!> stack = new Stack<Vertex!>();
int cnt = 0;
foreach (Vertex v in vertices.Values) {
if (v.Visited == VisitedStatus.Unvisited) {
SearchC(v, stack, ref cnt);
}
}
assert cnt == vertices.Count; // sanity check that everything has been visited
sccComputed = true;
}
/// <summary>
/// This is the 'SearchC' procedure from the Aho, Hopcroft, and Ullman book 'The Design and Analysis of Computer Algorithms'.
/// </summary>
void SearchC(Vertex! v, Stack<Vertex!>! stack, ref int cnt)
requires v.Visited == VisitedStatus.Unvisited;
requires topologicallySortedRepresentatives != null;
ensures v.Visited != VisitedStatus.Unvisited;
{
v.DfNumber = cnt;
cnt++;
v.LowLink = v.DfNumber;
stack.Push(v);
v.Visited = VisitedStatus.OnStack;
foreach (Vertex w in v.Successors) {
if (w.Visited == VisitedStatus.Unvisited) {
SearchC(w, stack, ref cnt);
v.LowLink = min{v.LowLink, w.LowLink};
} else if (w.Visited == VisitedStatus.OnStack) {
assert w.DfNumber < v.DfNumber || v.LowLink <= w.DfNumber; // the book also has the guard 'w.DfNumber < v.DfNumber', but that seems unnecessary to me, so this assert is checking my understanding
v.LowLink = min{v.LowLink, w.DfNumber};
}
}
if (v.LowLink == v.DfNumber) {
// The SCC containing 'v' has now been computed.
v.SccId = topologicallySortedRepresentatives.Count;
topologicallySortedRepresentatives.Add(v);
v.SccMembers = new List<Vertex!>();
while (true) {
Vertex x = stack.Pop();
x.Visited = VisitedStatus.Visited;
x.SccRepresentative = v;
v.SccMembers.Add(x);
if (x == v) { break; }
}
}
}
/// <summary>
/// Returns null if the graph has no cycles. If the graph does contain some cycle, returns the list of
/// vertices on one such cycle.
/// </summary>
public List<Node> TryFindCycle() {
// reset all visited information
foreach (Vertex v in vertices.Values) {
v.Visited = VisitedStatus.Unvisited;
}
foreach (Vertex v in vertices.Values) {
assert v.Visited != VisitedStatus.OnStack;
if (v.Visited == VisitedStatus.Unvisited) {
List<Vertex!> cycle = CycleSearch(v);
if (cycle != null) {
List<Node> nodes = new List<Node>();
foreach (Vertex v in cycle) {
nodes.Add(v.N);
}
return nodes; // a cycle is found
}
}
}
return null; // there are no cycles
}
/// <summary>
/// A return of null means there are no cycles involving any vertex in the subtree rooted at v.
/// A non-null return means a cycle has been found. Then:
/// If v.Visited == Visited, then the entire cycle is described in the returned list.
/// If v.Visited == OnStack, then the cycle consists of the vertices strictly deeper than
/// w on the stack followed by the vertices (in reverse order) in the returned list, where
/// w is the first vertex in the list returned.
/// </summary>
List<Vertex!> CycleSearch(Vertex! v)
requires v.Visited == VisitedStatus.Unvisited;
ensures v.Visited != VisitedStatus.Unvisited;
ensures result == null ==> v.Visited == VisitedStatus.Visited;
ensures result != null ==> result.Count != 0;
{
v.Visited = VisitedStatus.OnStack;
foreach (Vertex succ in v.Successors) {
// todo: I would use a 'switch' statement, but there seems to be a bug in the Spec# compiler's type checking.
if (succ.Visited == VisitedStatus.Visited) {
// there is no cycle in the subtree rooted at succ, hence this path does not give rise to any cycles
} else if (succ.Visited == VisitedStatus.OnStack) {
// we found a cycle!
List<Vertex!> cycle = new List<Vertex!>();
cycle.Add(succ);
if (v == succ) {
// entire cycle has been found
v.Visited = VisitedStatus.Visited;
}
return cycle;
} else {
assert succ.Visited == VisitedStatus.Unvisited;
List<Vertex!> cycle = CycleSearch(succ);
if (cycle != null) {
if (succ.Visited == VisitedStatus.Visited) {
// the entire cycle has been collected
v.Visited = VisitedStatus.Visited;
return cycle;
} else {
cycle.Add(succ);
if (v == cycle[0]) {
// the entire cycle has been collected and we are the first to find out
v.Visited = VisitedStatus.Visited;
}
return cycle;
}
}
}
}
v.Visited = VisitedStatus.Visited; // there are no cycles from here on
return null;
}
/// <summary>
/// Returns whether or not 'source' reaches 'sink' in the graph.
/// 'source' and 'sink' need not be in the graph; if neither is, the return value
/// is source==sink.
/// </summary>
public bool Reaches(Node source, Node sink) {
Vertex a = FindVertex(source);
Vertex b = FindVertex(sink);
if (a == null || b == null) {
return source.Equals(sink);
}
generation++;
return ReachSearch(a, b);
}
bool ReachSearch(Vertex! source, Vertex! sink) {
if (source == sink) {
return true;
} else if (source.Gen == generation) {
// already visited
return false;
} else {
source.Gen = generation;
return exists{Vertex succ in source.Successors; ReachSearch(succ, sink)};
}
}
}
}
|