From 5ced6412ed00204204ebd9351dab36e555f2e718 Mon Sep 17 00:00:00 2001
From: allydonaldson <unknown>
Date: Fri, 28 Jun 2013 13:31:38 +0100
Subject: Adapted method for computing dual of graph so that it copes with
 graphs that exhibit exit-free cycles

---
 Source/Graph/Graph.cs | 33 ++++++++++++++++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

(limited to 'Source/Graph')

diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs
index 4d81e741..b6fe8cfc 100644
--- a/Source/Graph/Graph.cs
+++ b/Source/Graph/Graph.cs
@@ -866,25 +866,56 @@ namespace Microsoft.Boogie.GraphUtil {
       s.AppendLine("}");
       return s.ToString();
     }
+
+    public ICollection<Node> ComputeReachable() {
+      ICollection<Node> result = new HashSet<Node>();
+      Stack<Node> stack = new Stack<Node>();
+      stack.Push(source);
+      while(!(stack.Count() == 0)) {
+        Node n = stack.Pop();
+        result.Add(n);
+        foreach(var m in Successors(n)) {
+          if(!result.Contains(m)) {
+            stack.Push(m);
+          }
+        }
+      }
+      return result;
+    }
+
   } // end: class Graph
 
   public static class GraphAlgorithms
   {
 
+
       public static Graph<Node> Dual<Node>(this Graph<Node> g, Node dummySource)
       {
           var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList();
+          Node source;
           if (exits.Count == 0)
-              return null;
+              exits.Add(dummySource);
           var dual = new Graph<Node>(new HashSet<Tuple<Node, Node>>(g.Edges.Select(e => new Tuple<Node, Node>(e.Item2, e.Item1))));
           if (exits.Count == 1)
+          {
               dual.AddSource(exits[0]);
+              source = exits[0];
+          }
           else
           {
               dual.AddSource(dummySource);
+              source = dummySource;
               foreach (var exit in exits)
                   dual.AddEdge(dummySource, exit);
           }
+
+          #region Dual graph may not be connected, so add an edge from the dual graph's soure node to any unreachable node
+          foreach (var n in dual.Nodes.Where(Item => !dual.ComputeReachable().Contains(Item)))
+          {
+              dual.AddEdge(source, n);
+          }
+          #endregion
+
           return dual;
       }
 
-- 
cgit v1.2.3