Start work on the generic namer

7 files changed, 282 insertions, 54 deletions

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index 766768e2..6418bc7a 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -111,7 +111,7 @@ namespace Microsoft.Boogie.ModelViewer.Base
         sb.Length -= 2;

         sb.Append(")");

       }

-      name = sb.ToString();

+      name = new EdgeName(sb.ToString());

     }

   }

 

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index 0c470bcf..de0121e9 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -18,12 +18,21 @@ namespace Microsoft.Boogie.ModelViewer
     Changed = 1

   }

 

+  public interface IEdgeName

+  {

+    int CompareTo(IEdgeName other);

+    string FullName();

+    string ShortName();

+    IEnumerable<Model.Element> Dependencies { get; }

+    int Score { get; }

+  }

+

   public interface IDisplayNode

   {

     /// <summary>

     ///  Used for indexing the state tree.

     /// </summary>

-    string EdgeName { get; }

+    IEdgeName Name { get; }

 

     /// <summary>

     /// Used to determine aliasing. Can be null.

@@ -34,7 +43,6 @@ namespace Microsoft.Boogie.ModelViewer
     IEnumerable<IDisplayNode> Expand();

 

     // Things displayed to the user.

-    string Name { get; }

     NodeState State { get; }

     IEnumerable<string> Values { get; }

     string ToolTip { get; }

@@ -70,16 +78,19 @@ namespace Microsoft.Boogie.ModelViewer
       get { return children; }

     }

   }

-

+  

   public abstract class DisplayNode : IDisplayNode

   {

-    protected string name;

+    protected IEdgeName name;

 

-    public DisplayNode(string n) { name = n; }

+    public DisplayNode(string n)

+    { 

+      name = new EdgeName(n);

+    }

 

-    public virtual string Name

+    public DisplayNode(IEdgeName n)

     {

-      get { return name; }

+      name = n;

     }

 

     public virtual IEnumerable<string> Values

@@ -106,7 +117,7 @@ namespace Microsoft.Boogie.ModelViewer
 

     public object ViewSync { get; set; }

 

-    public virtual string EdgeName

+    public virtual IEdgeName Name

     {

       get { return name; }

     }

@@ -122,12 +133,17 @@ namespace Microsoft.Boogie.ModelViewer
     protected Func<T, IDisplayNode> convert;

     protected IEnumerable<T> data;

 

-    public ContainerNode(string name, Func<T, IDisplayNode> convert, IEnumerable<T> data) : base(name)

+    public ContainerNode(IEdgeName name, Func<T, IDisplayNode> convert, IEnumerable<T> data) : base(name)

     {

       this.convert = convert;

       this.data = data;

     }

 

+    public ContainerNode(string name, Func<T, IDisplayNode> convert, IEnumerable<T> data)

+      : this(new EdgeName(name), convert, data)

+    {

+    }

+

     public override bool Expandable { get { return true; } }

     public override IEnumerable<IDisplayNode> Expand()

     {

@@ -149,6 +165,8 @@ namespace Microsoft.Boogie.ModelViewer
 

     public static IEnumerable<T> Empty<T>() { yield break; }

 

+    public static IEnumerable<T> Singleton<T>(T e) { yield return e; }

+

     public static IEnumerable<T> Map<S, T>(this IEnumerable<S> inp, Func<S, T> conv)

     {

       foreach (var s in inp) yield return conv(s);

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 7e45a558..e538e8b3 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -136,12 +136,12 @@ namespace Microsoft.Boogie.ModelViewer
       if (!item.active)

         textBrush = grayedOut;

 

-      var sz = e.Graphics.MeasureString(item.dispNode.Name, font);

+      var sz = e.Graphics.MeasureString(item.dispNode.Name.FullName(), font);

       nameRect.Width = currentStateView.Columns[0].Width - 1 - off;

       if (nameRect.Width < sz.Width + 2)

         nameRect.Width = (int)sz.Width + 20;

       nameRect.X += off;

-      e.Graphics.DrawString(item.dispNode.Name, font, textBrush, nameRect);

+      e.Graphics.DrawString(item.dispNode.Name.FullName(), font, textBrush, nameRect);

 

       var valRect = rect;

       valRect.X = nameRect.X + nameRect.Width + 4;

@@ -269,7 +269,7 @@ namespace Microsoft.Boogie.ModelViewer
         this.ToolTipText = values;

       }

 

-      this.SubItems[0].Text = dispNode.Name;

+      this.SubItems[0].Text = dispNode.Name.FullName();

       this.SubItems[1].Text = values;

     }

 

diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index 8acb4760..413abd67 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -75,6 +75,7 @@
     <Compile Include="Main.Designer.cs">

       <DependentUpon>Main.cs</DependentUpon>

     </Compile>

+    <Compile Include="Namer.cs" />

     <Compile Include="Program.cs" />

     <Compile Include="Properties\AssemblyInfo.cs" />

     <Compile Include="SearchBox.cs">

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
new file mode 100644
index 00000000..772c3c78
--- /dev/null
+++ b/Source/ModelViewer/Namer.cs
@@ -0,0 +1,203 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+namespace Microsoft.Boogie.ModelViewer

+{

+  class EltName

+  {

+    internal Model.Element elt;

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

+    internal IEdgeName minName;

+    internal int score = 10000;

+    internal string theName;

+

+    internal EltName(Model.Element e)

+    {

+      elt = e;

+      theName = e.ToString();

+    }

+  }

+

+  public class Namer

+  {

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

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

+

+    EltName GetName(Model.Element elt)

+    {

+      EltName res;

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

+        return res;

+      res = new EltName(elt);

+      eltNames.Add(res);

+      unfoldings.Add(elt, res);

+      return res;

+    }

+

+    int EdgeNameScore(IEdgeName name)

+    {

+      return name.Dependencies.Select(e => GetName(e).score).Max() + name.Score;

+    }

+

+    void ComputeBestName()

+    {

+      while (true) {

+        var changes = 0;

+        foreach (var elt in eltNames) {

+          foreach (var edge in elt.nodes) {

+            var newScore = EdgeNameScore(edge);

+            if (newScore < elt.score) {

+              elt.score = newScore;

+              elt.minName = edge;

+              changes++;

+            }

+          }

+        }

+        if (changes == 0)

+          break;

+      }

+      eltNames.Sort((x,y) => x.score - y.score);

+      foreach (var elt in eltNames) {

+        if (elt.minName == null)

+          elt.minName = elt.nodes[0];

+        elt.theName = elt.minName.FullName();

+      }

+    }

+

+    void Unfold(IDisplayNode n)

+    {

+      if (n.Element != null) {

+        var prev = GetName(n.Element);

+        prev.nodes.Add(n.Name);

+        if (prev.nodes.Count > 1) // we've already been here

+          return;

+      }

+

+      if (!n.Expandable) return;

+

+      foreach (var c in n.Expand()) {

+        Unfold(c);

+      }

+    }

+

+    public void ComputeNames(IEnumerable<IDisplayNode> n)

+    {

+      n.Iter(Unfold);

+      ComputeBestName();

+    }

+

+    public virtual string ElementName(Model.Element elt)

+    {

+      return GetName(elt).theName;

+    }

+  }

+

+  public class EdgeName : IEdgeName

+  {

+    static readonly Model.Element[] emptyArgs = new Model.Element[0];

+

+    string formatFull, formatShort;

+    Model.Element[] args;

+    Namer namer;

+

+    public EdgeName(Namer n, string formatFull, string formatShort, params Model.Element[] args)

+    {

+      this.namer = n;

+      this.formatFull = formatFull;

+      this.formatShort = formatShort;

+      this.args = args;

+      Score = args.Length * 10;

+    }

+

+    public EdgeName(Namer n, string formatMixed, params Model.Element[] args)

+      : this(n, formatMixed, formatMixed, args)

+    {

+      var beg = formatMixed.IndexOf("%(");

+      var end = formatMixed.IndexOf("%)");

+      if (beg >= 0 && end > beg)

+        this.formatShort = formatMixed.Substring(0, beg) + formatMixed.Substring(end + 2);

+    }

+

+    public EdgeName(string name) : this(null, name, emptyArgs) { }

+

+    public virtual int CompareTo(IEdgeName other)

+    {

+      return string.CompareOrdinal(this.FullName(), other.FullName());

+    }

+

+    public override string ToString()

+    {

+      return FullName();

+    }

+

+    public override int GetHashCode()

+    {

+      int res = formatFull.GetHashCode() + formatShort.GetHashCode() * 17;

+      foreach (var c in args) {

+        res += c.GetHashCode();

+        res *= 13;

+      }

+      return res;

+    }

+

+    public override bool Equals(object obj)

+    {

+      EdgeName e = obj as EdgeName;

+      if (e == null) return false;

+      if (e == this) return true;

+      if (e.formatFull != this.formatFull || e.formatShort != this.formatShort || e.args.Length != this.args.Length)

+        return false;

+      for (int i = 0; i < this.args.Length; ++i)

+        if (this.args[i] != e.args[i])

+          return false;

+      return true;

+    }

+

+    protected virtual string Format(string format)

+    {

+      if (args.Length == 0)

+        return format;

+

+      var res = new StringBuilder(format.Length);

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

+        var c = format[i];

+        if (c == '%' && i < format.Length - 1) {

+          var j = i + 1;

+          while (j < format.Length && char.IsDigit(format[j]))

+            j++;

+          var len = j - i - 1;

+          if (len > 0) {

+            var idx = int.Parse(format.Substring(i + 1, len));

+            res.Append(namer.ElementName(args[idx]));

+            i = j - 1;

+            continue;

+          }

+        }

+

+        res.Append(c);

+      }

+

+      return res.ToString();

+    }

+

+    public virtual string FullName()

+    {

+      return Format(formatFull);

+    }

+

+    public virtual string ShortName()

+    {

+      return Format(formatShort);

+    }

+

+    public virtual IEnumerable<Model.Element> Dependencies

+    {

+      get { return args; }

+    }

+

+    public virtual int Score { get; set; }

+  }

+

+}

diff --git a/Source/ModelViewer/TreeSkeleton.cs b/Source/ModelViewer/TreeSkeleton.cs
index 47f65e5d..3d7384ad 100644
--- a/Source/ModelViewer/TreeSkeleton.cs
+++ b/Source/ModelViewer/TreeSkeleton.cs
@@ -7,7 +7,7 @@ namespace Microsoft.Boogie.ModelViewer
 {

   internal class SkeletonItem

   {

-    readonly string name;

+    readonly IEdgeName name;

     readonly List<SkeletonItem> children = new List<SkeletonItem>();

     internal readonly IDisplayNode[] displayNodes;

     readonly SkeletonItem parent;

@@ -18,7 +18,7 @@ namespace Microsoft.Boogie.ModelViewer
     public void Iter(Action<SkeletonItem> handler)

     {

       handler(this);

-      children.Iter(u => u.Iter(handler));

+      children.ForEach(u => u.Iter(handler));

     }

 

     public IEnumerable<SkeletonItem> RecChildren

@@ -45,12 +45,12 @@ namespace Microsoft.Boogie.ModelViewer
 

     public SkeletonItem(Main m, int stateCount)

     {

-      name = "<root>";

+      name = new EdgeName("<root>");

       main = m;

       displayNodes = new IDisplayNode[stateCount];

     }

 

-    internal SkeletonItem(string n, SkeletonItem par)

+    internal SkeletonItem(IEdgeName n, SkeletonItem par)

       : this(par.main, par.displayNodes.Length)

     {

       parent = par;

@@ -76,15 +76,15 @@ namespace Microsoft.Boogie.ModelViewer
           if (wasExpanded) return;

           wasExpanded = true;

 

-          var created = new Dictionary<string, SkeletonItem>();

+          var created = new Dictionary<IEdgeName, SkeletonItem>();

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

             var dn = displayNodes[i];

             if (dn == null || !dn.Expandable) continue;

             foreach (var child in dn.Expand()) {

               SkeletonItem skelChild;

-              if (!created.TryGetValue(child.EdgeName, out skelChild)) {

-                skelChild = new SkeletonItem(child.EdgeName, this);

-                created.Add(child.EdgeName, skelChild);

+              if (!created.TryGetValue(child.Name, out skelChild)) {

+                skelChild = new SkeletonItem(child.Name, this);

+                created.Add(child.Name, skelChild);

                 children.Add(skelChild);

               }

               skelChild.displayNodes[i] = child;

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index ea0544bf..30ec3def 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -65,8 +65,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

     public void ComputeNames()

     {

-      var namer = new Namer(this);

-      allNames = namer.ComputeNames();

+      //var namer = new Namer(this);

+      //allNames = namer.ComputeNames();

       foreach (var e in allNames)

         primaryName[e.Key] = e.Value[0];

     }

@@ -141,21 +141,25 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       return res;

     }

 

-    public string FieldName(Model.Element elt)

+    public string ConstantFieldName(Model.Element elt)

     {

-      return primaryName[elt];

-    }

+      var bestScore = int.MaxValue;

+      string bestName = null;

 

-    public int CompareFields(ElementNode f1, ElementNode f2)

-    {

-      var n1 = f1.Name;

-      var n2 = f2.Name;

-      int s1 = n1.Contains('<') ? 1 : 0;

-      int s2 = n2.Contains('<') ? 1 : 0;

-      if (s1 == s2)

-        return string.CompareOrdinal(n1, n2);

-      else

-        return s2 - s1;

+      foreach (var t in elt.Names) {

+        if (t.Args.Length == 0) {

+          var name = t.Func.Name;

+          var score = 0;

+          if (name.Contains('.')) score += 10;

+          if (name.Contains('#')) score -= 1;

+          if (score < bestScore) {

+            bestScore = score;

+            bestName = name;

+          }

+        }

+      }

+

+      return bestName;    

     }

 

     public DataKind GetKind(Model.Element tp, out Model.FuncTuple tpl)

@@ -235,10 +239,12 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
             if (val != null) {

               var ftp = f_field_type.TryEval(fld.Args[1]);

               val = WrapForUse(val, ftp);

-              result.Add(new FieldNode(state, FieldName(fld.Args[1]), val, ftp));

+              var nm = ConstantFieldName(fld.Args[1]);

+              var edgname = nm == null ? new EdgeName(fld.Args[1].ToString()) { Score = 100 } : new EdgeName(state.namer, "%(%0->%)" + nm, elt) { Score = 10 };

+              result.Add(new FieldNode(state, edgname, val, ftp));

             }

           }

-          result.Sort(CompareFields);

+          //result.Sort(CompareFields);

         }

       } else if (kind == DataKind.Map) {

         var elTp = tpl.Args[1];

@@ -246,7 +252,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           if (sel.Arity == 2 && sel.Name.StartsWith("$select.$map_t")) {

             foreach (var app in sel.AppsWithArg(0, elt)) {

               var val = WrapForUse(app.Result, elTp);

-              result.Add(new MapletNode(state, "[" + ElementNames(app.Args[1])[0] + "]", val, elTp));

+              var edgname = new EdgeName(state.namer, "%(%0%)[%1]", elt, app.Args[1]) { Score = 20 };

+              result.Add(new MapletNode(state, edgname, val, elTp));

             }

           }

       }

@@ -264,6 +271,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

   }

 

+#if false

   class Namer

   {

     VccModel vm;

@@ -447,6 +455,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     }

 

   }

+#endif

   

   class StateNode : IState

   {

@@ -454,9 +463,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     string name;

     internal VccModel vm;

     internal List<VariableNode> vars;

+    internal Namer namer;

     

     public StateNode(VccModel parent, Model.CapturedState s)

     {

+      this.namer = new Namer();

       this.vm = parent;

       state = s;

 

@@ -487,7 +498,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

       if (vm.states.Count > 0) {

         var prev = vm.states.Last();

-        names = prev.vars.Map(v => v.EdgeName);

+        names = prev.vars.Map(v => v.Name.FullName());

       }

 

       names = names.Concat(state.Variables).Distinct();

@@ -503,6 +514,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           vars.Add(vn);

         }

       }

+

+      namer.ComputeNames(vars);

     }

 

     public string Name

@@ -523,19 +536,20 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
   {

     protected StateNode stateNode;

     protected Model.Element elt, tp;

-    protected string realName;

     protected VccModel vm { get { return stateNode.vm; } }

     protected List<ElementNode> children;

 

-    public ElementNode(StateNode st, string name, Model.Element elt, Model.Element tp)

+    public ElementNode(StateNode st, IEdgeName name, Model.Element elt, Model.Element tp)

       : base(name)

     {

       this.stateNode = st;

-      this.realName = name;

       this.tp = tp;

       this.elt = elt;

     }

 

+    public ElementNode(StateNode st, string name, Model.Element elt, Model.Element tp)

+      : this(st, new EdgeName(name), elt, tp) { }

+

     public override Model.Element Element

     {

       get

@@ -557,14 +571,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       }

     }

 

-    public override string EdgeName

-    {

-      get

-      {

-        return this.realName;

-      }

-    }

-

     public override IEnumerable<string> Values

     {

       get

@@ -609,7 +615,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

   class FieldNode : ElementNode

   {

-    public FieldNode(StateNode par, string realName, Model.Element elt, Model.Element tp)

+    public FieldNode(StateNode par, IEdgeName realName, Model.Element elt, Model.Element tp)

       : base(par, realName, elt, tp)

     {

       /*

@@ -622,7 +628,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

   class MapletNode : ElementNode

   {

-    public MapletNode(StateNode par, string realName, Model.Element elt, Model.Element tp)

+    public MapletNode(StateNode par, IEdgeName realName, Model.Element elt, Model.Element tp)

       : base(par, realName, elt, tp)

     {

     }

@@ -635,7 +641,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     public VariableNode(StateNode par, string realName, Model.Element elt, Model.Element tp)

       : base(par, realName, elt, tp)

     {

-      name = vm.GetUserVariableName(realName);

+      name = new EdgeName(vm.GetUserVariableName(realName));

     }

 

     public override NodeState State