Introduce node categories; sort fields based on that not special characters

8 files changed, 104 insertions, 62 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 0fe86f81..c04be448 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -162,6 +162,12 @@ namespace Microsoft.Boogie
         return null;

       }

 

+      public bool IsTrue(params Element[] args)

+      {

+        var r = TryEval(args) as Boolean;

+        return r != null && r.Value;

+      }

+

       public void AddApp(Element res, params Element[] args)

       {        

         if (Arity == 0)

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index 5759a657..ccec9f5e 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -364,13 +364,5 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       this.realName = realName;

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

     }

-

-    public override NodeState State

-    {

-      get

-      {

-        return base.State | (updatedHere ? NodeState.Changed : NodeState.Normal);

-      }

-    }

   }

 }

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index 1330640e..57729e4d 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -11,6 +11,17 @@ namespace Microsoft.Boogie.ModelViewer
     public bool DebugMode;

   }

 

+  // sync with Main.categoryBrushes!

+  public enum NodeCategory

+  {

+    Local,

+    PhysField,

+    SpecField,

+    MethodologyProperty,

+    UserFunction,

+    Maplet

+  }

+

   public interface ILanguageProvider

   {

     bool IsMyModel(Model m);

@@ -27,7 +38,8 @@ namespace Microsoft.Boogie.ModelViewer
 

     IEnumerable<IState> States { get; }

 

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

+    // This function is given IDisplayNode possibly from different states.

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

   }

 

   public interface IState

@@ -36,13 +48,6 @@ namespace Microsoft.Boogie.ModelViewer
     IEnumerable<IDisplayNode> Nodes { get; }

   }

 

-  [Flags]

-  public enum NodeState

-  {

-    Normal = 0,

-    Changed = 1

-  }

-

   public interface IDisplayNode

   {

     /// <summary>

@@ -50,7 +55,7 @@ namespace Microsoft.Boogie.ModelViewer
     /// </summary>

     string Name { get; }

 

-    NodeState State { get; }

+    NodeCategory Category { get; }

     string Value { get; }

     string ToolTip { get; }

 

@@ -113,10 +118,8 @@ namespace Microsoft.Boogie.ModelViewer
       get { return null; }

     }

 

-    public virtual int ViewLevel

-    {

-      get; set;

-    }

+    public virtual int ViewLevel { get; set; }

+    public virtual NodeCategory Category { get; set; }

 

     public virtual IEnumerable<IDisplayNode> Children

     {

@@ -134,8 +137,6 @@ namespace Microsoft.Boogie.ModelViewer
     {

     }

 

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

-

     public object ViewSync { get; set; }

 

     public virtual string Name

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index ae201690..439c0875 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -108,7 +108,7 @@
       // prevValue

       // 

       this.prevValue.Text = "Previous";

-      this.prevValue.Width = 62;

+      this.prevValue.Width = 100;

       // 

       // stateViewMenu

       // 

@@ -288,7 +288,7 @@
       // exitToolStripMenuItem

       // 

       this.exitToolStripMenuItem.Name = "exitToolStripMenuItem";

-      this.exitToolStripMenuItem.Size = new System.Drawing.Size(152, 22);

+      this.exitToolStripMenuItem.Size = new System.Drawing.Size(92, 22);

       this.exitToolStripMenuItem.Text = "&Exit";

       this.exitToolStripMenuItem.Click += new System.EventHandler(this.exitToolStripMenuItem_Click);

       // 

@@ -309,33 +309,33 @@
       this.normalToolStripMenuItem.Checked = true;

       this.normalToolStripMenuItem.CheckState = System.Windows.Forms.CheckState.Checked;

       this.normalToolStripMenuItem.Name = "normalToolStripMenuItem";

-      this.normalToolStripMenuItem.Size = new System.Drawing.Size(152, 22);

+      this.normalToolStripMenuItem.Size = new System.Drawing.Size(130, 22);

       this.normalToolStripMenuItem.Text = "&Normal";

       this.normalToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click);

       // 

       // expertToolStripMenuItem

       // 

       this.expertToolStripMenuItem.Name = "expertToolStripMenuItem";

-      this.expertToolStripMenuItem.Size = new System.Drawing.Size(152, 22);

+      this.expertToolStripMenuItem.Size = new System.Drawing.Size(130, 22);

       this.expertToolStripMenuItem.Text = "E&xpert";

       this.expertToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click);

       // 

       // everythingToolStripMenuItem

       // 

       this.everythingToolStripMenuItem.Name = "everythingToolStripMenuItem";

-      this.everythingToolStripMenuItem.Size = new System.Drawing.Size(152, 22);

+      this.everythingToolStripMenuItem.Size = new System.Drawing.Size(130, 22);

       this.everythingToolStripMenuItem.Text = "&Everything";

       this.everythingToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click);

       // 

       // toolStripMenuItem1

       // 

       this.toolStripMenuItem1.Name = "toolStripMenuItem1";

-      this.toolStripMenuItem1.Size = new System.Drawing.Size(149, 6);

+      this.toolStripMenuItem1.Size = new System.Drawing.Size(127, 6);

       // 

       // debugToolStripMenuItem

       // 

       this.debugToolStripMenuItem.Name = "debugToolStripMenuItem";

-      this.debugToolStripMenuItem.Size = new System.Drawing.Size(152, 22);

+      this.debugToolStripMenuItem.Size = new System.Drawing.Size(130, 22);

       this.debugToolStripMenuItem.Text = "Debug";

       this.debugToolStripMenuItem.Click += new System.EventHandler(this.debugToolStripMenuItem_Click);

       // 

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 5e1fc0ce..3466cd25 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -160,10 +160,19 @@ namespace Microsoft.Boogie.ModelViewer
     static Brush nonPrimary = new SolidBrush(Col(0xeeeeee));

     static Brush matchBg = new SolidBrush(Col(0xFFFA6F));

 

+    static SolidBrush currentStateBrush = new SolidBrush(Color.Red);

     static SolidBrush regularStateBrush = new SolidBrush(Color.Black);

     static SolidBrush previousStateBrush = new SolidBrush(Color.Blue);

-    static SolidBrush currentStateBrush = new SolidBrush(Color.Red);

-    

+

+    static SolidBrush[] categoryBrushes = new SolidBrush[] {

+      new SolidBrush(Color.Black), // Local

+      new SolidBrush(Color.Black), // PhysField

+      new SolidBrush(Color.Green), // SpecField

+      new SolidBrush(Color.Peru), // MethodologyProperty

+      new SolidBrush(Color.Green), // UserFunction

+      new SolidBrush(Color.Black), // Maplet

+    };

+

     private void listView1_DrawItem(object sender, DrawListViewItemEventArgs e)

     {

       var item = (DisplayItem)e.Item;

@@ -175,7 +184,7 @@ namespace Microsoft.Boogie.ModelViewer
 

       var textBrush = Brushes.Black;

       if (listView.SelectedIndices.Count > 0 && listView.SelectedIndices[0] == e.ItemIndex) {

-        e.Graphics.FillRectangle(Brushes.Navy, rect);

+        e.Graphics.FillRectangle(Brushes.Aquamarine, rect);

         textBrush = Brushes.White;

       } else {

         var bg = Brushes.White;

@@ -213,8 +222,8 @@ namespace Microsoft.Boogie.ModelViewer
       var nameRect = rect;

       var font = listView.Font;

 

-      if ((item.dispNode.State & NodeState.Changed) != 0)

-        textBrush = Brushes.Red;

+      textBrush = categoryBrushes[(int)item.dispNode.Category];

+

       if (!item.active)

         textBrush = grayedOut;

 

@@ -222,6 +231,7 @@ namespace Microsoft.Boogie.ModelViewer
       nameRect.X += off;

       var width = DrawString(e.Graphics, item.SubItems[0].Text, font, textBrush, nameRect);

 

+      textBrush = item.active ? Brushes.Black : grayedOut;

       nameRect.X += width + 4;

       nameRect.Width = listView.Columns[0].Width + listView.Columns[1].Width - nameRect.X;

       width = DrawString(e.Graphics, item.SubItems[1].Text, font, textBrush, nameRect);

@@ -229,7 +239,7 @@ namespace Microsoft.Boogie.ModelViewer
       nameRect.X += width + 4;

       nameRect.Width = listView.Width - nameRect.X;

       var t = item.SubItems[2].Text;

-      width = DrawString(e.Graphics, t, font, t == item.SubItems[1].Text ? grayedOut : previousStateBrush, nameRect);

+      width = DrawString(e.Graphics, t, font, t == item.SubItems[1].Text ? grayedOut : Brushes.Black, nameRect);

     }

 

     private int DrawString(Graphics g, string s, Font font, Brush textBrush, Rectangle minRect)

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index e77b0178..8998204b 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -33,7 +33,7 @@ namespace Microsoft.Boogie.ModelViewer
     public virtual void RegisterLocalValue(string name, Model.Element elt)

     {

       string curr;

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

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

         return;

       localValue[elt] = name;

     }

@@ -93,7 +93,7 @@ namespace Microsoft.Boogie.ModelViewer
       Action<IEnumerable<IDisplayNode>> addList = (IEnumerable<IDisplayNode> nodes) =>

       {

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

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

+        foreach (var k in SortFields(nodes))

           workList.Enqueue(ch[k]);

       };

 

@@ -116,6 +116,7 @@ namespace Microsoft.Boogie.ModelViewer
       }

     }

     #region field name sorting

+    /*

     static bool HasSpecialChars(string s)

     {

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

@@ -123,10 +124,16 @@ namespace Microsoft.Boogie.ModelViewer
           case '[':

           case '<':

           case '>':

-          case ']': return true;

+          case ']': 

+          case '#':

+          case '\\':

+          case '(':

+          case ')':

+            return true;

         }

       return false;

     }

+     */

 

     static ulong GetNumber(string s, int beg)

     {

@@ -139,14 +146,15 @@ namespace Microsoft.Boogie.ModelViewer
       return res;

     }

 

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

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

     {

+      /*

       bool s1 = HasSpecialChars(f1);

       bool s2 = HasSpecialChars(f2);

       if (s1 && !s2)

         return 1;

       if (!s1 && s2)

-        return -1;

+        return -1; */

       var len = Math.Min(f1.Length, f2.Length);

       var numberPos = -1;

       for (int i = 0; i < len; ++i) {

@@ -169,11 +177,18 @@ namespace Microsoft.Boogie.ModelViewer
       return string.CompareOrdinal(f1, f2);

     }

 

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

+    public virtual int CompareFields(IDisplayNode n1, IDisplayNode n2)

     {

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

+      var diff = (int)n1.Category - (int)n2.Category;

+      if (diff != 0) return diff;

+      else return CompareFieldNames(n1.Name, n2.Name);

+    }

+

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

+    {

+      var fields = new List<IDisplayNode>(fields_);

       fields.Sort(CompareFields);

-      return fields;

+      return fields.Select(f => f.Name);

     }

     #endregion

   }

diff --git a/Source/ModelViewer/TreeSkeleton.cs b/Source/ModelViewer/TreeSkeleton.cs
index 0c7e6607..fa758ea5 100644
--- a/Source/ModelViewer/TreeSkeleton.cs
+++ b/Source/ModelViewer/TreeSkeleton.cs
@@ -131,7 +131,7 @@ namespace Microsoft.Boogie.ModelViewer
       wasExpanded = true;

 

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

-      var names = new List<string>();

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

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

         var dn = displayNodes[i];

         if (dn == null) continue;

@@ -143,8 +143,7 @@ namespace Microsoft.Boogie.ModelViewer
           if (!created.TryGetValue(name, out skelChild)) {

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

             created.Add(name, skelChild);

-            names.Add(name);

-

+            names.Add(child);

           }

           skelChild.displayNodes[i] = child;

         }

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 1eabc9df..2d372326 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -38,7 +38,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     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, f_select_ptr,

                                f_owners, f_closed, f_roots, f_timestamps, f_select_bool, f_select_int, f_is_null, f_good_state,

-                               f_int_to_version, f_int_to_ptrset, f_set_in0;

+                               f_int_to_version, f_int_to_ptrset, f_set_in0, f_is_ghost_field, f_is_phys_field;

     public readonly Model.Element tp_object, tp_mathint, tp_bool, tp_state, tp_ptrset;

     public readonly Model.Element elt_me, elt_null;

     Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();

@@ -77,6 +77,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       f_int_to_version = m.MkFunc("$int_to_version", 1);

       f_int_to_ptrset = m.MkFunc("$int_to_ptrset", 1);

       f_set_in0 = m.MkFunc("$set_in0", 2);

+      f_is_ghost_field = m.MkFunc("$is_ghost_field", 1);

+      f_is_phys_field = m.MkFunc("$is_phys_field", 1);

 

       tp_bool = m.GetFunc("^^bool").GetConstant();

       tp_mathint = m.GetFunc("^^mathint").GetConstant();

@@ -450,7 +452,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           tp = tp_mathint;

         }

         if (val != null) {

-          res.Add(new FieldNode(state, new EdgeName(name), val, tp));

+          res.Add(new FieldNode(state, new EdgeName(name), val, tp) { Category = NodeCategory.MethodologyProperty });

         }

       }

     }

@@ -473,7 +475,13 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
               val = WrapForUse(val, ftp);

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

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

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

+

+              var cat = NodeCategory.PhysField;

+              if (f_is_ghost_field.IsTrue(fld.Args[1]))

+                cat = NodeCategory.SpecField;

+              if (nm != null && nm.Contains("<"))

+                cat = NodeCategory.MethodologyProperty;

+              result.Add(new FieldNode(state, edgname, val, ftp) { Category = cat });

             }

           }

 

@@ -491,13 +499,13 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
             foreach (var app in sel.AppsWithArg(0, elt)) {

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

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

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

+              result.Add(new MapletNode(state, edgname, val, elTp) { Category = NodeCategory.Maplet });

             }

           }

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

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

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

-          result.Add(new MapletNode(state, edgname, sel.Result, tp_bool));

+          result.Add(new MapletNode(state, edgname, sel.Result, tp_bool) { Category = NodeCategory.Maplet });

         }

       }

 

@@ -509,6 +517,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
             continue;          

           var argsFmt = new StringBuilder();

           var name = tupl.Func.Name;

+          var cat = NodeCategory.MethodologyProperty;

+          if (name.StartsWith("F#")) {

+            name = name.Substring(2);

+            cat = NodeCategory.UserFunction;

+          }

           argsFmt.Append(name).Append("(");

           var args = new List<Model.Element>();

           foreach (var a in tupl.Args) {

@@ -524,7 +537,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           argsFmt.Length -= 2;

           argsFmt.Append(")");

           var edgeName = new EdgeName(this, argsFmt.ToString(), args.ToArray());

-          result.Add(new MapletNode(state, edgeName, tupl.Result, GuessType(tupl.Result)) { ViewLevel = FunctionScore(tupl.Func.Name) });

+          result.Add(new MapletNode(state, edgeName, tupl.Result, GuessType(tupl.Result)) { ViewLevel = FunctionScore(tupl.Func.Name), Category = cat });

         }

       }

 

@@ -581,6 +594,20 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       else

         return "";

     }

+

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

+    {

+      var sb = new StringBuilder();

+      foreach (var d in path) {

+        var name = d.Name;

+        if (name == "") continue; // can that happen?

+        if (sb.Length > 0 && name[0] != '[')

+          sb.Append("->");

+        sb.Append(d.Name);

+      }

+

+      return sb.ToString();

+    }

   }

 

   class StateNode : IState

@@ -601,7 +628,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       var idx = name.LastIndexOfAny(new char[] { '\\', '/' });

       if (idx > 0)

         name = name.Substring(idx + 1);

-      var limit = 16;

+      var limit = 30;

       if (name.Length > limit) {

         idx = name.IndexOf('(');

         if (idx > 0) {

@@ -734,13 +761,5 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       this.realName = realName;

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

     }

-

-    public override NodeState State

-    {

-      get

-      {

-        return base.State | (updatedHere ? NodeState.Changed : NodeState.Normal);

-      }

-    }

   }

 }