Compute canonical element names

2 files changed, 64 insertions, 30 deletions

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 30e0c65b..859b718a 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -9,9 +9,10 @@ namespace Microsoft.Boogie.ModelViewer
   {

     internal Model.Element elt;

     internal List<IEdgeName> nodes = new List<IEdgeName>();

-    internal int score = 10000;

+    internal int score = Namer.maxScore;

     internal string theName;

     internal bool unfolded;

+    internal int stateIdx;

 

     internal EltName(Model.Element e)

     {

@@ -22,8 +23,10 @@ namespace Microsoft.Boogie.ModelViewer
 

   public class Namer

   {

+    internal const int maxScore = 10000;

     List<EltName> eltNames = new List<EltName>();

     Dictionary<Model.Element, EltName> unfoldings = new Dictionary<Model.Element, EltName>();

+    Dictionary<Model.Element, string> canonicalNames;

 

     EltName GetName(Model.Element elt)

     {

@@ -43,6 +46,13 @@ namespace Microsoft.Boogie.ModelViewer
 

     void ComputeBestName()

     {

+      foreach (var n in eltNames) {

+        n.score = maxScore;

+        string s;

+        if (canonicalNames != null && canonicalNames.TryGetValue(n.elt, out s))

+          n.theName = s;

+      }

+

       while (true) {

         var changes = 0;

         var thisElts = eltNames.ToArray();

@@ -94,6 +104,53 @@ namespace Microsoft.Boogie.ModelViewer
       ComputeBestName();

     }

 

+    public static void ComputeCanonicalNames(IEnumerable<Namer> namers)

+    {

+      var names = new Dictionary<Model.Element, EltName>();

+      var namersArr = namers.ToArray();

+      for (int i = 0; i < namersArr.Length; ++i) {

+        foreach (var n in namersArr[i].eltNames) {

+          n.stateIdx = i;

+          if (n.nodes.Count == 0) continue;

+          EltName curr;

+          if (names.TryGetValue(n.elt, out curr) && curr.score <= n.score)

+            continue;

+          names[n.elt] = n;

+        }

+      }

+

+      var canonicals = new Dictionary<Model.Element, string>();      

+      foreach (var n in names.Values) {

+        if (n.elt is Model.Boolean || n.elt is Model.Number)

+          canonicals[n.elt] = n.nodes[0].FullName();

+        else

+          canonicals[n.elt] = n.nodes[0].FullName() + "." + n.stateIdx;

+      }

+

+      var unnamedIdx = 1;

+

+      for (int i = 0; i < namersArr.Length; ++i) {

+        namersArr[i].canonicalNames = canonicals;

+        foreach (var n in namersArr[i].eltNames) {

+          if (!canonicals.ContainsKey(n.elt)) {

+            canonicals[n.elt] = string.Format("${0}", unnamedIdx++);

+          }

+        }

+      }

+

+      for (int i = 0; i < namersArr.Length; ++i) {

+        namersArr[i].ComputeBestName();

+      }

+    }

+

+    public virtual string CanonicalName(Model.Element elt)

+    {

+      string res;

+      if (canonicalNames.TryGetValue(elt, out res))

+        return res;

+      return elt.ToString();

+    }

+

     public virtual string ElementName(Model.Element elt)

     {

       return GetName(elt).theName;

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 62957b79..271e7da0 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -22,12 +22,9 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         var sn = new StateNode(vm.states.Count, vm, s);

         vm.states.Add(sn);

       }

-      foreach (var s in vm.states) {

-        s.CopyNames();

-      }

-      foreach (var s in vm.states) {

-        s.ComputeNames();

-      }

+      foreach (var s in vm.states) s.ComputeNames();

+      Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer));

+      Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer));

       return vm.states;

     }

   }

@@ -531,25 +528,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         yield return vm.states[j];

     }

 

-    internal void CopyNames()

-    {

-      var named = new HashSet<Tuple<string,Model.Element>>();

-

-      foreach (var v in vars) {

-        named.Add(Tuple.Create(v.Name.ShortName(), v.Element));

-      }

-

-      foreach (var s in OtherStates()) {

-        foreach (var v in s.vars) {

-          var th = Tuple.Create(v.Name.ShortName(), v.Element);

-          if (!named.Contains(th)) {

-            named.Add(th);

-            namer.AddName(v.Element, new EdgeName(v.Name.ShortName() + "." + s.index) { Score = 30 });

-          }

-        }

-      }

-    }

-

     internal void ComputeNames()

     {

       namer.ComputeNames(vars);

@@ -612,11 +590,10 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     {

       get

       {

-        Model.Boolean b = this.Element as Model.Boolean;

-        if (b != null) {

-          yield return b.ToString();

-        } else {

+        if (Element is Model.Boolean) {

           yield return Element.ToString();

+        } else {

+          yield return stateNode.namer.CanonicalName(Element);

           foreach (var edge in stateNode.namer.Aliases(Element))

             if (edge != Name)

               yield return edge.FullName();