Improve the generic model viewer

5 files changed, 114 insertions, 41 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 3d1df65e..0fe86f81 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -5,6 +5,7 @@
 //-----------------------------------------------------------------------------

 

 using System;

+using System.Linq;

 using System.Collections.Generic;

 

 namespace Microsoft.Boogie

@@ -303,6 +304,14 @@ namespace Microsoft.Boogie
       public readonly string Name;

 

       public IEnumerable<string> Variables { get { return vars; } }

+      public IEnumerable<string> AllVariables { 

+        get {

+          if (previous != null)

+            return previous.AllVariables.Concat(Variables).Distinct();

+          else

+            return Variables;

+        } 

+      }

       public int VariableCount { get { return vars.Count; } }

       public bool HasBinding(string varname)

       {

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index cf5f9909..dddc8c30 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -23,44 +23,91 @@ namespace Microsoft.Boogie.ModelViewer.Base
 

   public class GenericModel : LanguageModel

   {

-    Model m;

+    internal Model m;

+    List<BaseState> states = new List<BaseState>();

 

     public GenericModel(Model m)

     {

       this.m = m;

+      foreach (var s in m.States)

+        states.Add(new BaseState(this, s) { Name = s.Name });

+      foreach (var s in states)

+        this.Flush(s.nodes);

     }

 

-    public IDisplayNode Function(Model.Func f)

+    public override IEnumerable<IState> States

     {

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

+      get { return states; }

     }

+  }

 

-    IEnumerable<IDisplayNode> GetStateNodes(Model.CapturedState st)

+  public class BaseState : IState

+  {

+    internal GenericModel m;

+    Model.CapturedState st;

+

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

+    internal Dictionary<Model.Element, string> niceName = new Dictionary<Model.Element, string>();

+

+    public BaseState(GenericModel m, Model.CapturedState st)

     {

-      foreach (var v in st.Variables)

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

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

+      this.st = st;

+      this.m = m;

+

+      foreach (var v in st.AllVariables) {

+        var e = st.TryGet(v);

+        m.RegisterLocalValue(v, e);

+        nodes.Add(new ElementNode(this, v, e));

+

+        niceName[e] = v;

+        foreach (var r in e.References) {

+          if (r.Args.Length == 1 && r.Args[0] == e) {

+            if (!niceName.ContainsKey(e))

+              niceName[e] = r.Func.Name + "(" + v + ")";

+          }

+        }

+      }

+

+      nodes.Add(new ContainerNode<Model.Func>("[Functions]", f => f.Arity == 0 ? null : Function(f), m.m.Functions));

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

     }

 

-    public override IEnumerable<IState> States

+    IDisplayNode Function(Model.Func f)

     {

-      get {

-        foreach (var s in m.States)

-          yield return new TopState(s.Name, GetStateNodes(s));

-      }

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

+    }

+

+    public virtual string Name { get; set; }

+

+    public virtual IEnumerable<IDisplayNode> Nodes

+    {

+      get { return nodes; }

     }

   }

+

   public class ElementNode : DisplayNode

   {

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

+    BaseState st;

+

+    public ElementNode(BaseState st, string name, Model.Element elt) : base(st.m, name, elt) { this.st = st; }

+

+    protected override void ComputeChildren()

+    {

+      children.Add(new ContainerNode<Model.FuncTuple>(" == ", e => new AppNode(st, e), Element.References.Where(t => t.Result == Element)));

+      foreach (var e in Element.References) {

+        if (e.Args.Contains(Element))

+          children.Add(new AppNode(st, e, x => x == Element ? "*" : st.niceName.GetWithDefault(x, null)));

+      }

+    }

   }

 

   public class AppNode : ElementNode

   {

     protected Model.FuncTuple tupl;

 

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

+    public AppNode(BaseState m, Model.FuncTuple t) : this(m, t, _ => null) { }

+

+    public AppNode(BaseState m, Model.FuncTuple t, Func<Model.Element, string> nameElement)

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

     {

       tupl = t;

@@ -68,12 +115,17 @@ namespace Microsoft.Boogie.ModelViewer.Base
       sb.Append(t.Func.Name);

       if (t.Args.Length > 0) {

         sb.Append("(");

-        foreach (var a in t.Args)

-          sb.Append(a.ToString()).Append(", ");

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

+          var n = nameElement(t.Args[i]);

+          if (n == null)

+            sb.AppendFormat("%{0}, ", i);

+          else

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

+        }

         sb.Length -= 2;

         sb.Append(")");

       }

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

+      name = new EdgeName(m.m, sb.ToString(), t.Args);

     }

   }

 

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index 33211ef3..d83dfdd5 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -223,6 +223,14 @@ namespace Microsoft.Boogie.ModelViewer
       if (a != null) return a;

       return b;

     }

+

+    public static S GetWithDefault<T, S>(this Dictionary<T, S> dict, T key, S defl)

+    {

+      S r;

+      if (dict.TryGetValue(key, out r))

+        return r;

+      return defl;

+    }

   }

 

 }

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index 4fe8662f..9932a550 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -31,7 +31,7 @@
       this.currentStateView = new System.Windows.Forms.ListView();

       this.name = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

       this.value = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

-      this.aliases = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

+      this.prevValue = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

       this.stateViewMenu = new System.Windows.Forms.ContextMenuStrip(this.components);

       this.dummyItemToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.splitContainer1 = new System.Windows.Forms.SplitContainer();

@@ -63,7 +63,7 @@
       this.currentStateView.Columns.AddRange(new System.Windows.Forms.ColumnHeader[] {

             this.name,

             this.value,

-            this.aliases});

+            this.prevValue});

       this.currentStateView.ContextMenuStrip = this.stateViewMenu;

       this.currentStateView.Dock = System.Windows.Forms.DockStyle.Fill;

       this.currentStateView.FullRowSelect = true;

@@ -74,7 +74,7 @@
       this.currentStateView.Name = "currentStateView";

       this.currentStateView.OwnerDraw = true;

       this.currentStateView.ShowItemToolTips = true;

-      this.currentStateView.Size = new System.Drawing.Size(761, 612);

+      this.currentStateView.Size = new System.Drawing.Size(677, 558);

       this.currentStateView.TabIndex = 0;

       this.currentStateView.UseCompatibleStateImageBehavior = false;

       this.currentStateView.View = System.Windows.Forms.View.Details;

@@ -95,10 +95,10 @@
       this.value.Text = "Value";

       this.value.Width = 99;

       // 

-      // aliases

+      // prevValue

       // 

-      this.aliases.Text = "Aliases";

-      this.aliases.Width = 325;

+      this.prevValue.Text = "Previous";

+      this.prevValue.Width = 147;

       // 

       // stateViewMenu

       // 

@@ -111,7 +111,7 @@
       // dummyItemToolStripMenuItem

       // 

       this.dummyItemToolStripMenuItem.Name = "dummyItemToolStripMenuItem";

-      this.dummyItemToolStripMenuItem.Size = new System.Drawing.Size(119, 22);

+      this.dummyItemToolStripMenuItem.Size = new System.Drawing.Size(144, 22);

       this.dummyItemToolStripMenuItem.Text = "Dummy item";

       // 

       // splitContainer1

@@ -127,8 +127,8 @@
       // splitContainer1.Panel2

       // 

       this.splitContainer1.Panel2.Controls.Add(this.stateList);

-      this.splitContainer1.Size = new System.Drawing.Size(1028, 796);

-      this.splitContainer1.SplitterDistance = 761;

+      this.splitContainer1.Size = new System.Drawing.Size(915, 726);

+      this.splitContainer1.SplitterDistance = 677;

       this.splitContainer1.TabIndex = 1;

       // 

       // splitContainer2

@@ -148,8 +148,8 @@
       this.splitContainer2.Panel2.Controls.Add(this.linkLabel1);

       this.splitContainer2.Panel2.Controls.Add(this.label1);

       this.splitContainer2.Panel2.Controls.Add(this.textBox1);

-      this.splitContainer2.Size = new System.Drawing.Size(761, 796);

-      this.splitContainer2.SplitterDistance = 612;

+      this.splitContainer2.Size = new System.Drawing.Size(677, 726);

+      this.splitContainer2.SplitterDistance = 558;

       this.splitContainer2.TabIndex = 1;

       // 

       // matchesList

@@ -168,7 +168,7 @@
       this.matchesList.Name = "matchesList";

       this.matchesList.OwnerDraw = true;

       this.matchesList.ShowItemToolTips = true;

-      this.matchesList.Size = new System.Drawing.Size(761, 151);

+      this.matchesList.Size = new System.Drawing.Size(677, 135);

       this.matchesList.TabIndex = 4;

       this.matchesList.UseCompatibleStateImageBehavior = false;

       this.matchesList.View = System.Windows.Forms.View.Details;

@@ -192,7 +192,7 @@
       // 

       this.linkLabel1.Anchor = ((System.Windows.Forms.AnchorStyles)((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Right)));

       this.linkLabel1.AutoSize = true;

-      this.linkLabel1.Location = new System.Drawing.Point(701, 5);

+      this.linkLabel1.Location = new System.Drawing.Point(617, 5);

       this.linkLabel1.Name = "linkLabel1";

       this.linkLabel1.Size = new System.Drawing.Size(57, 13);

       this.linkLabel1.TabIndex = 3;

@@ -217,7 +217,7 @@
                   | System.Windows.Forms.AnchorStyles.Right)));

       this.textBox1.Location = new System.Drawing.Point(53, 3);

       this.textBox1.Name = "textBox1";

-      this.textBox1.Size = new System.Drawing.Size(642, 20);

+      this.textBox1.Size = new System.Drawing.Size(558, 20);

       this.textBox1.TabIndex = 1;

       this.textBox1.TextChanged += new System.EventHandler(this.textBox1_TextChanged);

       // 

@@ -236,7 +236,7 @@
       this.stateList.MultiSelect = false;

       this.stateList.Name = "stateList";

       this.stateList.ShowItemToolTips = true;

-      this.stateList.Size = new System.Drawing.Size(263, 796);

+      this.stateList.Size = new System.Drawing.Size(234, 726);

       this.stateList.TabIndex = 0;

       this.stateList.UseCompatibleStateImageBehavior = false;

       this.stateList.View = System.Windows.Forms.View.Details;

@@ -261,7 +261,7 @@
       // 

       this.AutoScaleDimensions = new System.Drawing.SizeF(6F, 13F);

       this.AutoScaleMode = System.Windows.Forms.AutoScaleMode.Font;

-      this.ClientSize = new System.Drawing.Size(1028, 796);

+      this.ClientSize = new System.Drawing.Size(915, 726);

       this.Controls.Add(this.splitContainer1);

       this.Name = "Main";

       this.Text = "Boogie Verification Debugger";

@@ -289,7 +289,7 @@
     private System.Windows.Forms.ColumnHeader columnHeader1;

     private System.Windows.Forms.ColumnHeader columnHeader2;

     private System.Windows.Forms.ColumnHeader columnHeader3;

-    private System.Windows.Forms.ColumnHeader aliases;

+    private System.Windows.Forms.ColumnHeader prevValue;

     private System.Windows.Forms.SplitContainer splitContainer2;

     private System.Windows.Forms.ListView matchesList;

     private System.Windows.Forms.ColumnHeader columnHeader4;

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 8c36de3c..e77b0178 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -116,11 +116,15 @@ namespace Microsoft.Boogie.ModelViewer
       }

     }

     #region field name sorting

-    static bool HasAny(string s, string chrs)

+    static bool HasSpecialChars(string s)

     {

-      foreach (var c in s)

-        if (chrs.Contains(c))

-          return true;

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

+        switch (s[i]) {

+          case '[':

+          case '<':

+          case '>':

+          case ']': return true;

+        }

       return false;

     }

 

@@ -137,8 +141,8 @@ namespace Microsoft.Boogie.ModelViewer
 

     public virtual int CompareFields(string f1, string f2)

     {

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

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

+      bool s1 = HasSpecialChars(f1);

+      bool s2 = HasSpecialChars(f2);

       if (s1 && !s2)

         return 1;

       if (!s1 && s2)