From 6aa09a12ee9d3722446390d1332f83402ca0bbdb Mon Sep 17 00:00:00 2001 From: tabarbe Date: Tue, 3 Aug 2010 23:45:43 +0000 Subject: Dafny: Renaming the DafnyPipeline source files in preparation for the commit of my port of that project. --- Source/Dafny/SccGraph.ssc | 336 ---------------------------------------------- 1 file changed, 336 deletions(-) delete mode 100644 Source/Dafny/SccGraph.ssc (limited to 'Source/Dafny/SccGraph.ssc') diff --git a/Source/Dafny/SccGraph.ssc b/Source/Dafny/SccGraph.ssc deleted file mode 100644 index 0498f55d..00000000 --- a/Source/Dafny/SccGraph.ssc +++ /dev/null @@ -1,336 +0,0 @@ -using System.Collections.Generic; - -namespace Microsoft.Dafny { - - public class Graph - { - enum VisitedStatus { Unvisited, OnStack, Visited } - class Vertex { - public readonly Node N; - public readonly List! Successors = new List(); - public Vertex SccRepresentative; // null if not computed - public List 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! vertices = new Dictionary(); - bool sccComputed = false; - List 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() - { - } - - /// - /// Idempotently adds a vertex 'n' to the graph. - /// - public void AddVertex(Node n) { - GetVertex(n); - } - - /// - /// Idempotently adds a vertex 'n' to the graph and then returns the Vertex for it. - /// - 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(); - v.SccMembers.Add(v); - v.SccId = topologicallySortedRepresentatives.Count; - topologicallySortedRepresentatives.Add(v); - } - } - return v; - } - - /// - /// Returns the vertex for 'n' if 'n' is in the graph. Otherwise, returns null. - /// - 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; - } - } - - /// - /// Idempotently adds verices 'from' and 'to' the graph, and then - /// adds an edge from 'from' to 'to'. - /// - 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 - } - - /// - /// Idempotently adds 'n' as a vertex and then returns a Node that is the representative element of the - /// strongly connected component containing 'n'. - /// - public Node GetSCCRepresentative(Node n) { - return GetSCCRepr(n).N; - } - - /// - /// Idempotently adds 'n' as a vertex. Then, returns the number of SCCs before the SCC of 'n' in the - /// topologically sorting of SCCs. - /// - 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; - } - - /// - /// Returns a list of the topologically sorted SCCs, each represented in the list by its representative node. - /// - public List! TopologicallySortedComponents() { - ComputeSCCs(); - assert topologicallySortedRepresentatives != null; // follows from object invariant - List nn = new List(); - foreach (Vertex v in topologicallySortedRepresentatives) { - nn.Add(v.N); - } - return nn; - } - - /// - /// Idempotently adds 'n' as a vertex and then returns the set of Node's in the strongly connected component - /// that contains 'n'. - /// - public List! GetSCC(Node n) { - Vertex v = GetVertex(n); - ComputeSCCs(); - Vertex repr = v.SccRepresentative; - assert repr != null && repr.SccMembers != null; // follows from postcondition of ComputeSCCs - List nn = new List(); - foreach (Vertex w in repr.SccMembers) { - nn.Add(w.N); - } - return nn; - } - - /// - /// Idempotently adds 'n' as a vertex and then returns the size of the set of Node's in the strongly connected component - /// that contains 'n'. - /// - public int GetSCCSize(Node n) - ensures 1 <= result; - { - Vertex v = GetVertex(n); - ComputeSCCs(); - Vertex repr = v.SccRepresentative; - assert repr != null && repr.SccMembers != null; // follows from postcondition of ComputeSCCs - return repr.SccMembers.Count; - } - - /// - /// 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. - /// - void ComputeSCCs() - ensures sccComputed; - { - if (sccComputed) { return; } // check if already computed - - // reset all SCC information - topologicallySortedRepresentatives = new List(); - foreach (Vertex v in vertices.Values) { - v.Visited = VisitedStatus.Unvisited; - v.SccMembers = null; - } - Stack stack = new Stack(); - 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; - } - - /// - /// This is the 'SearchC' procedure from the Aho, Hopcroft, and Ullman book 'The Design and Analysis of Computer Algorithms'. - /// - void SearchC(Vertex! v, Stack! 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(); - while (true) { - Vertex x = stack.Pop(); - x.Visited = VisitedStatus.Visited; - x.SccRepresentative = v; - v.SccMembers.Add(x); - if (x == v) { break; } - } - } - } - - /// - /// Returns null if the graph has no cycles. If the graph does contain some cycle, returns the list of - /// vertices on one such cycle. - /// - public List 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 cycle = CycleSearch(v); - if (cycle != null) { - List nodes = new List(); - foreach (Vertex v in cycle) { - nodes.Add(v.N); - } - return nodes; // a cycle is found - } - } - } - return null; // there are no cycles - } - - /// - /// 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. - /// - List 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 cycle = new List(); - cycle.Add(succ); - if (v == succ) { - // entire cycle has been found - v.Visited = VisitedStatus.Visited; - } - return cycle; - } else { - assert succ.Visited == VisitedStatus.Unvisited; - List 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; - } - - /// - /// 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. - /// - 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)}; - } - } - } -} -- cgit v1.2.3