Simplify languague-specific interface

7 files changed, 301 insertions, 576 deletions

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index c4bae59e..8875cce6 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -15,22 +15,39 @@ namespace Microsoft.Boogie.ModelViewer.Base
       return true;

     }

 

-    IEnumerable<IDisplayNode> GetStateNodes(Model m)

+    public ILanguageSpecificModel GetLanguageSpecificModel(Model m)

     {

-      yield return GenericNodes.Functions(m);

-      yield return GenericNodes.Constants(m);

-      foreach (var s in m.States)

-        yield return new StateNode(s);

+      return new GenericModel(m);

+    }

+  }

+

+  public class GenericModel : LanguageModel

+  {

+    Model m;

+

+    public GenericModel(Model m)

+    {

+      this.m = m;

     }

 

-    public IEnumerable<IState> GetStates(Model m)

+    public IDisplayNode Function(Model.Func f)

     {

-      yield return new TopState("TOP", GetStateNodes(m));

+      return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(this, a), f.Apps);

     }

 

-    public IEnumerable<string> SortFields(IEnumerable<string> fields)

+    IEnumerable<IDisplayNode> GetStateNodes()

     {

-      return GlobalNamer.DefaultSortFields(fields);

+      yield return new ContainerNode<Model.Func>("Functions", f => f.Arity == 0 ? null : Function(f), m.Functions);

+      yield return new ContainerNode<Model.Func>("Constants", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.Functions);

+      foreach (var s in m.States)

+        yield return new StateNode(this, s);

+    }

+

+    public override IEnumerable<IState> States

+    {

+      get { 

+        yield return new TopState("TOP", GetStateNodes());

+      }

     }

   }

 

@@ -38,73 +55,41 @@ namespace Microsoft.Boogie.ModelViewer.Base
   {

     protected Model.CapturedState state;

 

-    public StateNode(Model.CapturedState s) : base(s.Name)

+    public StateNode(ILanguageSpecificModel p, Model.CapturedState s) : base(p, s.Name, null)

     {

       state = s;

     }

 

-    public override IEnumerable<string> Aliases

+    public override string Value

     {

-      get { foreach (var v in state.Variables) yield return v; }

+      get {

+        return state.Variables.Concat(", ");

+      }

     }

 

-    public override bool Expandable { get { return state.VariableCount != 0; } }

-

-    public override IEnumerable<IDisplayNode> Expand()

+    protected override void ComputeChildren()

     {

       foreach (var v in state.Variables) {

-        yield return new ElementNode(v, state.TryGet(v));

+        children.Add(new ElementNode(langModel, v, state.TryGet(v)));

       }

     }

   }

 

   public class ElementNode : DisplayNode

   {

-    protected Model.Element elt;

-

-    public ElementNode(string name, Model.Element elt) : base(name)

-    {

-      this.elt = elt;

-    }

-

-    public override IEnumerable<string> Aliases

-    {

-      get

-      {

-        if (!(elt is Model.Uninterpreted))

-          yield return elt.ToString();

-        foreach (var tupl in elt.Names) {

-          if (tupl.Func.Arity == 0)

-            yield return tupl.Func.Name;

-        }

-      }

-    }

+    public ElementNode(ILanguageSpecificModel p, string name, Model.Element elt) : base(p, name, elt) {}

   }

 

   public static class GenericNodes

   {

-    public static IDisplayNode Function(Model.Func f)

-    {

-      return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(a), f.Apps);

-    }

-

-    public static IDisplayNode Functions(Model m)

-    {

-      return new ContainerNode<Model.Func>("Functions", f => f.Arity == 0 ? null : Function(f), m.Functions);

-    }

-

-    public static IDisplayNode Constants(Model m)

-    {

-      return new ContainerNode<Model.Func>("Constants", f => f.Arity != 0 ? null : new AppNode(f.Apps.First()), m.Functions);

-    }

   }

 

   public class AppNode : ElementNode

   {

     protected Model.FuncTuple tupl;

 

-    public AppNode(Model.FuncTuple t)

-      : base(t.Func.Name, t.Result)

+    public AppNode(ILanguageSpecificModel m, Model.FuncTuple t)

+      : base(m, t.Func.Name, t.Result)

     {

       tupl = t;

       var sb = new StringBuilder();

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index 41d02a21..cbb4e424 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -17,27 +17,19 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       return m.TryGetFunc("$$Language$Dafny") != null;

     }

 

-    public IEnumerable<IState> GetStates(Model m)

+    public ILanguageSpecificModel GetLanguageSpecificModel(Model m)

     {

       var dm = new DafnyModel(m);

       foreach (var s in m.States) {

         var sn = new StateNode(dm.states.Count, dm, s);

         dm.states.Add(sn);

       }

-      foreach (var s in dm.states) s.ComputeNames();

-      dm.gn.ComputeCanonicalNames();

-      return dm.states;

-    }

-

-    public IEnumerable<string> SortFields(IEnumerable<string> fields)

-    {

-      return GlobalNamer.DefaultSortFields(fields);

+      return dm;

     }

   }

 

-  class DafnyModel : INamerCallbacks

+  class DafnyModel : LanguageModel

   {

-    public readonly GlobalNamer gn;

     public readonly Model model;

     public readonly Model.Func f_heap_select, f_set_select, f_seq_length, f_seq_index, f_box, f_dim, f_index_field, f_multi_index_field;

     public readonly Dictionary<Model.Element, Model.Element[]> ArrayLengths = new Dictionary<Model.Element, Model.Element[]>();

@@ -46,7 +38,6 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
 

     public DafnyModel(Model m)

     {

-      gn = new GlobalNamer(this);

       model = m;

       f_heap_select = m.MkFunc("[3]", 3);

       f_set_select = m.MkFunc("[2]", 2);

@@ -78,6 +69,11 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       }

     }

 

+    public override IEnumerable<IState> States

+    {

+      get { return states; }

+    }

+

     public string GetUserVariableName(string name)

     {

       if (name == "$Heap" || name == "$_Frame" || name == "#cev_pc")

@@ -104,11 +100,10 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
         var seqLen = f_seq_length.AppWithArg(0, elt);

         if (seqLen != null) {

           // elt is a sequence

-          var edgname = new EdgeName(state.namer, "|%0|", "|.|", elt);

+          var edgname = new EdgeName(this, "|.|", elt);

           result.Add(new FieldNode(state, edgname, seqLen.Result));

           foreach (var tpl in f_seq_index.AppsWithArg(0, elt)) {

-            var fieldName = string.Format("[{0}]", tpl.Args[1].ToString());

-            edgname = new EdgeName(state.namer, "%0" + fieldName, fieldName, elt);

+            edgname = new EdgeName(this, "[%0]", tpl.Args[1]);

             result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));

           }

 

@@ -119,7 +114,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
             int i = 0;

             foreach (var len in lengths) {

               var name = lengths.Length == 1 ? "Length" : "Length" + i;

-              var edgname = new EdgeName(state.namer, "%0." + name, name, elt);

+              var edgname = new EdgeName(this, name);

               result.Add(new FieldNode(state, edgname, len));

               i++;

             }

@@ -128,7 +123,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
           if (heap != null) {

             foreach (var tpl in f_heap_select.AppsWithArgs(0, heap, 1, elt)) {

               var field = new FieldName(tpl.Args[2], this);

-              var edgname = new EdgeName(state.namer, "%0" + (field.Dims == 0 ? "." : "") + field.Name, field.Name, elt);

+              var edgname = new EdgeName(this, field.Name, elt);

               result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));

             }

           }

@@ -193,11 +188,6 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       else

         return elt;

     }

-

-    public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

-    {

-      return GlobalNamer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);

-    }

   }

 

   class StateNode : IState

@@ -206,13 +196,11 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     readonly string name;

     internal readonly DafnyModel dm;

     internal readonly List<VariableNode> vars = new List<VariableNode>();

-    internal readonly StateNamer namer;

     internal readonly int index;

     

     public StateNode(int i, DafnyModel parent, Model.CapturedState s)

     {

       dm = parent;

-      namer = new StateNamer(dm.gn);

       state = s;

       index = i;

 

@@ -251,19 +239,13 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
           var val = state.TryGet(v);

           var vn = new VariableNode(this, v, val);

           vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v);

+          if (curVars.ContainsKey(v))

+            dm.RegisterLocalValue(vn.Name, val);

           vars.Add(vn);

         }

       }

 

-      foreach (var e in dm.model.Elements) {        

-        if (e is Model.Number || e is Model.Boolean)

-          namer.AddName(e, new EdgeName(e.ToString()));

-      }

-    }

-

-    internal void ComputeNames()

-    {

-      namer.ComputeNames(vars);

+      dm.Flush(vars);

     }

 

     public string Name

@@ -285,10 +267,9 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     protected StateNode stateNode;

     protected Model.Element elt;

     protected DafnyModel vm { get { return stateNode.dm; } }

-    protected List<ElementNode> children;

 

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

-      : base(name)

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

+      : base(st.dm, name, elt)

     {

       this.stateNode = st;

       this.elt = elt;

@@ -297,85 +278,15 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     public ElementNode(StateNode st, string name, Model.Element elt)

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

 

-    public override Model.Element Element

-    {

-      get

-      {

-        return elt;

-      }

-    }

-

-    protected virtual void DoInitChildren()

+    protected override void ComputeChildren()

     {

       children.AddRange(vm.GetExpansion(stateNode, elt));

     }

-

-    protected void InitChildren()

-    {

-      if (children == null) {

-        children = new List<ElementNode>();

-        DoInitChildren();

-      }

-    }

-

-    public override string CanonicalValue

-    {

-      get

-      {

-        return stateNode.namer.CanonicalName(Element);

-      }

-    }

-

-    public override IEnumerable<string> Aliases

-    {

-      get

-      {

-        if (Element is Model.Boolean) {

-          yield break;

-        } else {

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

-            if (!edge.Equals(Name))

-              yield return edge.FullName();

-        }

-      }

-    }

-

-    public override string ToolTip

-    {

-      get

-      {

-        var sb = new StringBuilder();

-        int limit = 30;

-        foreach (var n in Aliases){

-          sb.AppendFormat("   = {0}\n", n); 

-          if (limit-- < 0) {

-            sb.Append("...");

-            break;

-          }

-        }

-        return sb.ToString();

-      }

-    }

-

-    public override bool Expandable

-    {

-      get

-      {

-        InitChildren();

-        return children.Count > 0;

-      }

-    }

-

-    public override IEnumerable<IDisplayNode> Expand()

-    {

-      InitChildren();

-      return children;

-    }

   }

 

   class FieldNode : ElementNode

   {

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

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

       : base(par, realName, elt)

     {

       /*

@@ -388,7 +299,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
 

   class MapletNode : ElementNode

   {

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

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

       : base(par, realName, elt)

     {

     }

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index 05bc6168..5fedf732 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -8,24 +8,24 @@ namespace Microsoft.Boogie.ModelViewer
   public interface ILanguageProvider

   {

     bool IsMyModel(Model m);

-    IEnumerable<IState> GetStates(Model m);

+    ILanguageSpecificModel GetLanguageSpecificModel(Model m);

+  }

+

+  public interface ILanguageSpecificModel

+  {

+    string CanonicalName(Model.Element elt);

+

+    string PathName(IEnumerable<IDisplayNode> path);

+

+    IEnumerable<IState> States { get; }

+

     IEnumerable<string> SortFields(IEnumerable<string> fields);

   }

 

-  public interface INamerCallbacks

+  public interface IState

   {

-    // Elements (other than integers and Booleans) get canonical names of the form 

-    // "<base>'<idx>", where <base> is returned by this function, and <idx> is given 

-    // starting with 0, and incrementing when they are conflicts between bases.

-    //

-    // This function needs to return an appropriate base name for the element. It is given

-    // the element, and if possible an IEdgeName in a particular stat that seems to be the

-    // best bet to construct the canonical name from.

-    //

-    // A reasonable strategy is to check if it's a name of the local, and if so return it,

-    // and otherwise use the type of element (e.g., return "seq" for elements representing

-    // sequences). It is also possible to return "" in such cases.

-    string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx);

+    string Name { get; }

+    IEnumerable<IDisplayNode> Nodes { get; }

   }

 

   [Flags]

@@ -35,45 +35,29 @@ 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>

-    IEdgeName Name { get; }

+    string Name { get; }

+

+    NodeState State { get; }

+    string Value { get; }

+    string ToolTip { get; }

 

     /// <summary>

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

     /// </summary>

     Model.Element Element { get; }

 

-    bool Expandable { get; }

-    IEnumerable<IDisplayNode> Expand();

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

 

-    // Things displayed to the user.

-    NodeState State { get; }

-    string CanonicalValue { get; }

-    IEnumerable<string> Aliases { get; }

-    string ToolTip { get; }

+    IEnumerable<IDisplayNode> Children { get; }

 

     object ViewSync { get; set; }

   }

 

-  public interface IState

-  {

-    string Name { get; }

-    IEnumerable<IDisplayNode> Nodes { get; }

-  }

-

 

   public class TopState : IState

   {

@@ -99,26 +83,19 @@ namespace Microsoft.Boogie.ModelViewer
   

   public abstract class DisplayNode : IDisplayNode

   {

-    protected IEdgeName name;

+    protected EdgeName name;

+    protected Model.Element element;

+    protected ILanguageSpecificModel langModel;

+    protected List<IDisplayNode> children;

 

-    public DisplayNode(string n)

-    { 

-      name = new EdgeName(n);

-    }

+    public DisplayNode(ILanguageSpecificModel model, string n, Model.Element elt) 

+      : this(model, new EdgeName(n), elt) {}

 

-    public DisplayNode(IEdgeName n)

+    public DisplayNode(ILanguageSpecificModel model, EdgeName n, Model.Element elt)

     {

+      langModel = model;

       name = n;

-    }

-

-    public virtual string CanonicalValue

-    {

-      get { return name.FullName(); }

-    }

-

-    public virtual IEnumerable<string> Aliases

-    {

-      get { yield break; }

+      element = elt;

     }

 

     public virtual string ToolTip

@@ -126,28 +103,55 @@ namespace Microsoft.Boogie.ModelViewer
       get { return null; }

     }

 

-    public virtual bool Expandable

+    public virtual IEnumerable<IDisplayNode> Children

     {

-      get { return false; }

+      get

+      {

+        if (children == null) {

+          children = new List<IDisplayNode>();

+          ComputeChildren();

+        }

+        return children;

+      }

     }

 

-    public virtual IEnumerable<IDisplayNode> Expand()

+    protected virtual void ComputeChildren()

     {

-      yield break;

     }

 

     public virtual NodeState State { get { return NodeState.Normal; } }

 

     public object ViewSync { get; set; }

 

-    public virtual IEdgeName Name

+    public virtual string Name

     {

-      get { return name; }

+      get { return name.ToString(); }

     }

 

     public virtual Model.Element Element

     {

-      get { return null; }

+      get { return element; }

+    }

+

+    public virtual string Value

+    {

+      get

+      {

+        if (element == null)

+          return "";

+        return langModel.CanonicalName(element);

+      }

+    }

+

+    public IEnumerable<Model.Element> References

+    {

+      get

+      {

+        foreach (var r in name.Dependencies)

+          yield return r;

+        if (element != null)

+          yield return element;

+      }

     }

   }

 

@@ -156,7 +160,7 @@ namespace Microsoft.Boogie.ModelViewer
     protected Func<T, IDisplayNode> convert;

     protected IEnumerable<T> data;

 

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

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

     {

       this.convert = convert;

       this.data = data;

@@ -167,13 +171,12 @@ namespace Microsoft.Boogie.ModelViewer
     {

     }

 

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

-    public override IEnumerable<IDisplayNode> Expand()

+    protected override void ComputeChildren()

     {

       foreach (var f in data) {

         var res = convert(f);

         if (res != null)

-          yield return res;

+          children.Add(res);

       }

     }

   }

@@ -186,6 +189,16 @@ namespace Microsoft.Boogie.ModelViewer
       if (!cond) throw new System.Exception("assertion violation");

     }

 

+    public static string Concat(this IEnumerable<string> strs, string sep)

+    {

+      var res = new StringBuilder();

+      foreach (var e in strs)

+        res.Append(e).Append(sep);

+      if (res.Length > 0)

+        res.Length -= sep.Length;

+      return res.ToString();

+    }

+

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

 

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

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 37c7676b..e8a9df36 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -21,12 +21,13 @@ namespace Microsoft.Boogie.ModelViewer
     int currentState;

     IState[] states;

     internal ILanguageProvider langProvider;

+    internal ILanguageSpecificModel langModel;

 

     // TODO this should be dynamically loaded

     IEnumerable<ILanguageProvider> Providers()

     {

       yield return Vcc.Provider.Instance;

-      yield return Dafny.Provider.Instance;

+      //yield return Dafny.Provider.Instance;

       yield return Base.Provider.Instance;

     }

 

@@ -69,7 +70,8 @@ namespace Microsoft.Boogie.ModelViewer
       }

       

       var items = new List<ListViewItem>();

-      states = langProvider.GetStates(m).ToArray();

+      langModel = langProvider.GetLanguageSpecificModel(m);

+      states = langModel.States.ToArray();

       unfoldingRoot = new SkeletonItem(this, states.Length);

       allItems = unfoldingRoot.PopulateRoot(states);

 

@@ -279,7 +281,7 @@ namespace Microsoft.Boogie.ModelViewer
       stateList.BeginUpdate();

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

         var dn = sel.skel.displayNodes[i];

-        stateList.Items[i].SubItems[2].Text = dn == null ? "" : dn.CanonicalValue;

+        stateList.Items[i].SubItems[2].Text = dn == null ? "" : dn.Value;

       }

       stateList.EndUpdate();

     }

@@ -382,7 +384,7 @@ namespace Microsoft.Boogie.ModelViewer
       }

 

       var tooltip = dispNode.ToolTip;

-      var aliases = AliasesAsString(dispNode);

+      var aliases = ""; // AliasesAsString(dispNode);

       if (IsMatchListItem)

         aliases = "";

       if (tooltip != null) {

@@ -391,9 +393,22 @@ namespace Microsoft.Boogie.ModelViewer
         this.ToolTipText = aliases;

       }

 

-      this.SubItems[0].Text = IsMatchListItem ? dispNode.Name.FullName() : dispNode.Name.ShortName();

-      this.SubItems[1].Text = active ? dispNode.CanonicalValue : "";

-      this.SubItems[2].Text = active ? aliases : "";

+      var name = dispNode.Name;

+

+      if (IsMatchListItem) {

+        Util.Assert(active);

+        var parents = new List<IDisplayNode>();

+        for (var curr = skel; curr != null; curr = curr.parent) {

+          if (curr.parent != null) // skip the root

+            parents.Add(curr.displayNodes[stateId]);

+        }

+        parents.Reverse();

+        name = skel.main.langModel.PathName(parents);

+      }

+

+      this.SubItems[0].Text = name;

+      this.SubItems[1].Text = active ? dispNode.Value : "";

+      // this.SubItems[2].Text = active ? aliases : "";

     }

 

     internal DisplayItem()

@@ -401,6 +416,7 @@ namespace Microsoft.Boogie.ModelViewer
     {

     }

 

+    /*

     static internal string AliasesAsString(IDisplayNode dn)

     {

       if (dn == null) return "";

@@ -417,5 +433,6 @@ namespace Microsoft.Boogie.ModelViewer
       if (sb.Length > 2) sb.Length -= 2;

       return sb.ToString();

     }

+     */

   }

 }

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index fc22afef..afbcf4ee 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -5,42 +5,107 @@ using System.Text;
 

 namespace Microsoft.Boogie.ModelViewer

 {

-  class EltName

+  public abstract class LanguageModel : ILanguageSpecificModel

   {

-    internal Model.Element elt;

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

-    internal int score = StateNamer.maxScore;

-    internal string theName;

-    internal bool unfolded;

-    internal int stateIdx;

-

-    internal EltName(Model.Element e)

+    protected Dictionary<string, int> baseNameUse = new Dictionary<string, int>();

+    protected Dictionary<Model.Element, string> canonicalName = new Dictionary<Model.Element, string>();

+    protected Dictionary<Model.Element, string> localValue = new Dictionary<Model.Element, string>();

+

+    // Elements (other than integers and Booleans) get canonical names of the form 

+    // "<base>'<idx>", where <base> is returned by this function, and <idx> is given 

+    // starting with 0, and incrementing when there are conflicts between bases.

+    //

+    // This function needs to return an appropriate base name for the element. It is given

+    // the element.

+    //

+    // A reasonable strategy is to check if it's a name of the local, and if so return it,

+    // and otherwise use the type of element (e.g., return "seq" for elements representing

+    // sequences). It is also possible to return "" in such cases.

+    protected virtual string CanonicalBaseName(Model.Element elt)

     {

-      elt = e;

-      theName = e.ToString();

+      string res;

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

+        return res;

+      return "";

     }

-  }

 

-  public class GlobalNamer

-  {

-    internal Dictionary<Model.Element, string> canonicalNames;

-    INamerCallbacks cb;

-    internal List<StateNamer> stateNamers = new List<StateNamer>();

+    public virtual void RegisterLocalValue(string name, Model.Element elt)

+    {

+      string curr;

+      if (localValue.TryGetValue(elt, out curr) && CompareFields(name, curr) >= 0)

+        return;

+      localValue[elt] = name;

+    }

+

+    protected virtual string LiteralName(Model.Element elt)

+    {

+      if (elt is Model.Integer)

+        return elt.ToString();

+      if (elt is Model.Boolean)

+        return elt.ToString();

+      return null;

+    }

 

-    public GlobalNamer(INamerCallbacks cb)

+    public virtual string CanonicalName(Model.Element elt)

     {

-      this.cb = cb;

+      string res;

+      if (canonicalName.TryGetValue(elt, out res)) return res;

+      res = LiteralName(elt);

+      if (res == null) {

+        var baseName = CanonicalBaseName(elt);

+        int cnt;

+        if (!baseNameUse.TryGetValue(baseName, out cnt)) {

+          cnt = -1;

+        }

+        cnt++;

+        res = baseName + "'" + cnt;

+        baseNameUse[baseName] = cnt;

+      }

+      canonicalName.Add(elt, res);

+      return res;

     }

 

-    #region default namer callback implementations

-    public static string DefaultCanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

+    public virtual string PathName(IEnumerable<IDisplayNode> path)

     {

-      if (edgeName == null)

-        return "";

-      var name = edgeName.FullName();

-      return name;

+      return path.Select(n => n.Name).Concat(".");

     }

 

+    public abstract IEnumerable<IState> States { get; }

+

+    /// <summary>

+    /// Walks each input tree in BFS order, and force evaluation of Name and Value properties

+    /// (to get reasonable numbering of canonical values).

+    /// </summary>

+    public void Flush(IEnumerable<IDisplayNode> roots)

+    {

+      var workList = new Queue<IDisplayNode>();

+

+      Action<IEnumerable<IDisplayNode>> addList = (IEnumerable<IDisplayNode> nodes) =>

+      {

+        var ch = nodes.ToDictionary(x => x.Name);

+        foreach (var k in SortFields(ch.Keys))

+          workList.Enqueue(ch[k]);

+      };

+

+      addList(roots);

+

+      var visited = new HashSet<Model.Element>();

+      while (workList.Count > 0) {

+        var n = workList.Dequeue();

+        

+        var dummy1 = n.Name;

+        var dummy2 = n.Value;

+

+        if (n.Element != null) {

+          if (visited.Contains(n.Element))

+            continue;

+          visited.Add(n.Element);

+        }

+

+        addList(n.Children);

+      }

+    }

+    #region field name sorting

     static bool HasAny(string s, string chrs)

     {

       foreach (var c in s)

@@ -60,7 +125,7 @@ namespace Microsoft.Boogie.ModelViewer
       return res;

     }

 

-    public static int CompareFields(string f1, string f2)

+    public virtual int CompareFields(string f1, string f2)

     {

       bool s1 = HasAny(f1, "[<>]");

       bool s2 = HasAny(f2, "[<>]");

@@ -90,233 +155,40 @@ namespace Microsoft.Boogie.ModelViewer
       return string.CompareOrdinal(f1, f2);

     }

 

-    public static IEnumerable<string> DefaultSortFields(IEnumerable<string> fields_)

+    public virtual IEnumerable<string> SortFields(IEnumerable<string> fields_)

     {

       var fields = new List<string>(fields_);

       fields.Sort(CompareFields);

       return fields;

     }

     #endregion

-

-    public void ComputeCanonicalNames()

-    {

-      for (int i = 0; i < 2; i++)

-        ComputeCanonicalNamesCore();

-    }

-

-    void ComputeCanonicalNamesCore()

-    {

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

-      var namersArr = stateNamers.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>();

-      var usedNames = new Dictionary<string, int>();

-      Model model = null;

-      foreach (var n in names.Values) {

-        string name = "";

-        model = n.elt.Model;

-        if (n.nodes.Count == 0) {

-          name = cb.CanonicalBaseName(n.elt, null, 0);

-          name = AppendIndex(usedNames, name);

-        } else if (n.elt is Model.Boolean || n.elt is Model.Number)

-          name = n.nodes[0].FullName();

-        else {

-          name = cb.CanonicalBaseName(n.elt, n.nodes[0], n.stateIdx);

-          name = AppendIndex(usedNames, name);

-        }

-        canonicals[n.elt] = name;

-      }

-

-      canonicalNames = canonicals;

-

-      foreach (var e in model.Elements) {

-        if (!canonicals.ContainsKey(e)) {

-          var name = cb.CanonicalBaseName(e, null, 0);

-          canonicals[e] = AppendIndex(usedNames, name);

-        }

-      }

-

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

-        namersArr[i].ComputeBestName();

-      }

-    }

-

-    private static string AppendIndex(Dictionary<string, int> usedNames, string name)

-    {

-      var idx = 0;

-      if (!usedNames.TryGetValue(name, out idx))

-        idx = 0;

-      usedNames[name] = idx + 1;

-      name = name + "'" + idx;

-      return name;

-    }

-

-    public virtual string CanonicalName(Model.Element elt)

-    {

-      string res;

-      if (canonicalNames != null && canonicalNames.TryGetValue(elt, out res))

-        return res; // +" " + elt.ToString();

-      return elt.ToString();

-    }

   }

 

-  public class StateNamer

-  {

-    GlobalNamer globalNamer;

-    internal const int maxScore = 10000;

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

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

-

-    public StateNamer(GlobalNamer gn)

-    {

-      globalNamer = gn;

-      gn.stateNamers.Add(this);

-    }

-

-    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).Concat1(0).Max() + name.Score;

-    }

-

-    internal void ComputeBestName()

-    {

-      foreach (var n in eltNames) {

-        n.score = maxScore;

-        string s;

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

-          n.theName = s;

-      }

-

-      while (true) {

-        var changes = 0;

-        var thisElts = eltNames.ToArray();

-        foreach (var elt in thisElts) {

-          var newScore = elt.nodes.Select(EdgeNameScore).Concat1(int.MaxValue).Min();

-          if (newScore < elt.score) {

-            elt.score = newScore;

-            changes++;

-          }

-        }

-        if (changes == 0 && thisElts.Length == eltNames.Count)

-          break;

-      }

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

-      foreach (var elt in eltNames) {

-        if (elt.nodes.Count > 0) {

-          elt.nodes.Sort((x, y) => EdgeNameScore(x) - EdgeNameScore(y));

-          elt.theName = elt.nodes[0].FullName();

-        }

-      }

-    }

-

-    void Unfold(IEnumerable<IDisplayNode> ns)

-    {

-      var workList = new Queue<IDisplayNode>(); // do BFS

-      ns.Iter(workList.Enqueue);

-

-      while (workList.Count > 0) {

-        var n = workList.Dequeue();

-

-        if (n.Element != null) {

-          var prev = GetName(n.Element);

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

-          if (prev.unfolded) // we've already been here

-            continue;

-          prev.unfolded = true;

-        }

-

-        if (!n.Expandable) return;

-

-        n.Expand().Iter(workList.Enqueue);

-      }

-    }

-

-    public void AddName(Model.Element elt, IEdgeName name)

-    {

-      var e = GetName(elt);

-      e.nodes.Add(name);

-    }

-

-    public void ComputeNames(IEnumerable<IDisplayNode> n)

-    {

-      Unfold(n);

-      ComputeBestName();

-    }

-

-    public virtual string ElementName(Model.Element elt)

-    {

-      return GetName(elt).theName;

-    }

-

-    public virtual IEnumerable<IEdgeName> Aliases(Model.Element elt)

-    {

-      return GetName(elt).nodes;

-    }

-

-    public virtual string CanonicalName(Model.Element elt)

-    {

-      return globalNamer.CanonicalName(elt);

-    }

-  }

-

-  public class EdgeName : IEdgeName

+  public class EdgeName

   {

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

 

-    string formatFull, formatShort;

+    ILanguageSpecificModel langModel;

+    string format;

     Model.Element[] args;

-    StateNamer namer;

 

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

+    public EdgeName(ILanguageSpecificModel n, string format, params Model.Element[] args)

     {

-      this.namer = n;

-      this.formatFull = formatFull;

-      this.formatShort = formatShort;

+      this.langModel = n;

+      this.format = format;

       this.args = args;

-      Score = args.Length * 10;

-    }

-

-    public EdgeName(StateNamer n, string formatBoth, params Model.Element[] args)

-      : this(n, formatBoth, formatBoth, args)

-    {

     }

 

     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();

+      return Format();

     }

 

     public override int GetHashCode()

     {

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

+      int res = format.GetHashCode();

       foreach (var c in args) {

         res += c.GetHashCode();

         res *= 13;

@@ -329,7 +201,7 @@ namespace Microsoft.Boogie.ModelViewer
       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)

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

         return false;

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

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

@@ -337,7 +209,7 @@ namespace Microsoft.Boogie.ModelViewer
       return true;

     }

 

-    protected virtual string Format(string format)

+    protected virtual string Format()

     {

       if (args.Length == 0)

         return format;

@@ -345,14 +217,16 @@ namespace Microsoft.Boogie.ModelViewer
       var res = new StringBuilder(format.Length);

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

         var c = format[i];

-        var canonical = false;

 

+        /*

+        var canonical = false;

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

           if (format[i + 1] == 'c') {

             ++i;

             canonical = true;

           }

         }

+         */

 

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

           var j = i + 1;

@@ -361,7 +235,7 @@ namespace Microsoft.Boogie.ModelViewer
           var len = j - i - 1;

           if (len > 0) {

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

-            res.Append(canonical ? namer.CanonicalName(args[idx]) : namer.ElementName(args[idx]));

+            res.Append(langModel.CanonicalName(args[idx]));

             i = j - 1;

             continue;

           }

@@ -373,22 +247,10 @@ namespace Microsoft.Boogie.ModelViewer
       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 3663f926..b7a83dee 100644
--- a/Source/ModelViewer/TreeSkeleton.cs
+++ b/Source/ModelViewer/TreeSkeleton.cs
@@ -7,12 +7,12 @@ namespace Microsoft.Boogie.ModelViewer
 {

   internal class SkeletonItem

   {

-    readonly IEdgeName name;

+    readonly string name;

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

     internal readonly IDisplayNode[] displayNodes;

     internal bool[] isPrimary;

     internal readonly SkeletonItem parent;

-    readonly Main main;

+    internal readonly Main main;

     internal readonly int level;

     internal bool expanded, wasExpanded;

     internal bool isMatch;

@@ -49,13 +49,13 @@ namespace Microsoft.Boogie.ModelViewer
 

     public SkeletonItem(Main m, int stateCount)

     {

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

+      name = "<root>";

       main = m;

       displayNodes = new IDisplayNode[stateCount];

       isPrimary = new bool[stateCount];

     }

 

-    internal SkeletonItem(IEdgeName n, SkeletonItem par)

+    internal SkeletonItem(string n, SkeletonItem par)

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

     {

       parent = par;

@@ -65,7 +65,7 @@ namespace Microsoft.Boogie.ModelViewer
 

     public bool Expandable

     {

-      get { return displayNodes.Any(d => d != null && d.Expandable); }

+      get { return displayNodes.Any(d => d != null && d.Children.Count() > 0); }

     }

 

     public bool Expanded

@@ -130,10 +130,10 @@ namespace Microsoft.Boogie.ModelViewer
       var names = new List<string>();

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

         var dn = displayNodes[i];

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

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

+        if (dn == null) continue;

+        foreach (var child in dn.Children) {

           SkeletonItem skelChild;

-          var name = child.Name.ShortName();

+          var name = child.Name;

           if (!created.TryGetValue(name, out skelChild)) {

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

             created.Add(name, skelChild);

@@ -144,7 +144,7 @@ namespace Microsoft.Boogie.ModelViewer
         }

       }

 

-      foreach (var name in main.langProvider.SortFields(names)) {

+      foreach (var name in main.langModel.SortFields(names)) {

         children.Add(created[name]);

       }

     }

@@ -154,8 +154,8 @@ namespace Microsoft.Boogie.ModelViewer
       var node = displayNodes[stateId];

       if (node == null)

         return false;

-      var s1 = node.Name.FullName().ToLower();

-      var s2 = node.CanonicalValue.ToLower();

+      var s1 = node.Name.ToLower();

+      var s2 = node.Value.ToLower();

       foreach (var w in words) {

         if (!s1.Contains(w) && !s2.Contains(w))

           return false;

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 8eb9f331..b155f1a1 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -15,23 +15,15 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       return m.TryGetFunc("$is_ghost_field") != null && m.TryGetFunc("$fk_vol_version") != null;

     }

 

-    public IEnumerable<IState> GetStates(Model m)

+    public ILanguageSpecificModel GetLanguageSpecificModel(Model m)

     {

       var vm = new VccModel(m);

       foreach (var s in m.States) {

         var sn = new StateNode(vm.states.Count, vm, s);

         vm.states.Add(sn);

       }

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

-      vm.gn.ComputeCanonicalNames();

-      return vm.states;

+      return vm;

     }

-

-    public IEnumerable<string> SortFields(IEnumerable<string> fields)

-    {

-      return GlobalNamer.DefaultSortFields(fields);

-    }

-

   }

 

   enum DataKind

@@ -42,9 +34,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     Map

   }

 

-  class VccModel : INamerCallbacks

+  class VccModel : LanguageModel

   {

-    public readonly GlobalNamer gn;

     public readonly Model model;

     public readonly Model.Func f_ptr_to, f_phys_ptr_cast, f_spec_ptr_cast, f_mathint, f_local_value_is, f_spec_ptr_to, f_heap, f_select_field,

                                f_select_value, f_field, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t;

@@ -53,7 +44,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

     public VccModel(Model m)

     {

-      gn = new GlobalNamer(this);

       model = m;

       f_ptr_to = m.MkFunc("$ptr_to", 1);

       f_spec_ptr_to = m.MkFunc("$spec_ptr_to", 1);

@@ -252,7 +242,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
               var ftp = f_field_type.TryEval(fld.Args[1]);

               val = WrapForUse(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, nm, elt) { Score = 10 };

+              var edgname = nm == null ? new EdgeName(fld.Args[1].ToString()) : new EdgeName(this, nm);

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

             }

           }

@@ -264,7 +254,7 @@ 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);

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

+              var edgname = new EdgeName(this, "[%0]", app.Args[1]);

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

             }

           }

@@ -273,10 +263,18 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       return result;

     }

 

-    public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

+    public override IEnumerable<IState> States

+    {

+      get

+      {

+        return states;

+      }

+    }

+

+    protected override string CanonicalBaseName(Model.Element elt)

     {

       var vm = this;

-      var name = GlobalNamer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);

+      var name = base.CanonicalBaseName(elt);

 

       if (name.Contains("[") || name.Contains("'") || name.Contains("-"))

         name = "";

@@ -311,13 +309,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     string name;

     internal VccModel vm;

     internal List<VariableNode> vars;

-    internal StateNamer namer;

     internal int index;

     

     public StateNode(int i, VccModel parent, Model.CapturedState s)

     {

       this.vm = parent;

-      this.namer = new StateNamer(vm.gn);

       state = s;

       index = i;

 

@@ -361,21 +357,15 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           val = vm.WrapForUse(val, tp);

           var vn = new VariableNode(this, v, val, tp);

           vn.updatedHere = vm.states.Count > 0 && curVars.ContainsKey(v);

+          if (curVars.ContainsKey(v))

+            vm.RegisterLocalValue(vn.Name, val);

           vars.Add(vn);

         }

       }

 

-      foreach (var e in vm.model.Elements) {        

-        if (e is Model.Number || e is Model.Boolean)

-          namer.AddName(e, new EdgeName(e.ToString()));

-      }

+      vm.Flush(vars);

     } 

 

-    internal void ComputeNames()

-    {

-      namer.ComputeNames(vars);

-    }

-

     public string Name

     {

       get { return name; }

@@ -393,62 +383,22 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
   class ElementNode : DisplayNode

   {

     protected StateNode stateNode;

-    protected Model.Element elt, tp;

+    protected Model.Element tp;

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

-    protected List<ElementNode> children;

 

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

-      : base(name)

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

+      : base(st.vm, name, elt)

     {

       this.stateNode = st;

       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

-      {

-        return elt;

-      }

-    }

-

-    protected virtual void DoInitChildren()

+    protected override void ComputeChildren()

     {

-      children.AddRange(vm.GetExpansion(stateNode, elt, tp));

-    }

-

-    protected void InitChildren()

-    {

-      if (children == null) {

-        children = new List<ElementNode>();

-        DoInitChildren();

-      }

-    }

-

-    public override string CanonicalValue

-    {

-      get

-      {

-        return stateNode.namer.CanonicalName(Element);

-      }

-    }

-

-    public override IEnumerable<string> Aliases

-    {

-      get

-      {

-        if (Element is Model.Boolean) {

-          yield break;

-        } else {

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

-            if (!edge.Equals(Name))

-              yield return edge.FullName();

-        }

-      }

+      children.AddRange(vm.GetExpansion(stateNode, element, tp));

     }

 

     public override string ToolTip

@@ -457,6 +407,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       {

         var sb = new StringBuilder();

         sb.AppendFormat("Type: {0}\n", vm.TypeName(tp));

+        /*

         int limit = 30;

         foreach (var n in Aliases){

           sb.AppendFormat("   = {0}\n", n); 

@@ -465,29 +416,15 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
             break;

           }

         }

+         */

         return sb.ToString();

       }

     }

-

-    public override bool Expandable

-    {

-      get

-      {

-        InitChildren();

-        return children.Count > 0;

-      }

-    }

-

-    public override IEnumerable<IDisplayNode> Expand()

-    {

-      InitChildren();

-      return children;

-    }

   }

 

   class FieldNode : ElementNode

   {

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

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

       : base(par, realName, elt, tp)

     {

       /*

@@ -500,7 +437,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

   class MapletNode : ElementNode

   {

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

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

       : base(par, realName, elt, tp)

     {

     }