Introduce distinction between canonical element name and its aliases

5 files changed, 62 insertions, 41 deletions

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index 6418bc7a..247021a0 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -38,7 +38,7 @@ namespace Microsoft.Boogie.ModelViewer.Base
       state = s;

     }

 

-    public override IEnumerable<string> Values

+    public override IEnumerable<string> Aliases

     {

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

     }

@@ -62,7 +62,7 @@ namespace Microsoft.Boogie.ModelViewer.Base
       this.elt = elt;

     }

 

-    public override IEnumerable<string> Values

+    public override IEnumerable<string> Aliases

     {

       get

       {

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index c2ffdf4b..a640055f 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -44,7 +44,8 @@ namespace Microsoft.Boogie.ModelViewer
 

     // Things displayed to the user.

     NodeState State { get; }

-    IEnumerable<string> Values { get; }

+    string CanonicalValue { get; }

+    IEnumerable<string> Aliases { get; }

     string ToolTip { get; }

 

     object ViewSync { get; set; }

@@ -93,7 +94,12 @@ namespace Microsoft.Boogie.ModelViewer
       name = n;

     }

 

-    public virtual IEnumerable<string> Values

+    public virtual string CanonicalValue

+    {

+      get { return name.FullName(); }

+    }

+

+    public virtual IEnumerable<string> Aliases

     {

       get { yield break; }

     }

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index a8d7be4c..eae222aa 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -35,6 +35,7 @@
       this.columnHeader3 = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

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

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

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

       ((System.ComponentModel.ISupportInitialize)(this.splitContainer1)).BeginInit();

       this.splitContainer1.Panel1.SuspendLayout();

       this.splitContainer1.Panel2.SuspendLayout();

@@ -45,7 +46,8 @@
       // 

       this.currentStateView.Columns.AddRange(new System.Windows.Forms.ColumnHeader[] {

             this.name,

-            this.value});

+            this.value,

+            this.aliases});

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

       this.currentStateView.FullRowSelect = true;

       this.currentStateView.GridLines = true;

@@ -76,7 +78,7 @@
       // value

       // 

       this.value.Text = "Value";

-      this.value.Width = 394;

+      this.value.Width = 99;

       // 

       // splitContainer1

       // 

@@ -130,6 +132,11 @@
       this.columnHeader2.Text = "Value";

       this.columnHeader2.Width = 116;

       // 

+      // aliases

+      // 

+      this.aliases.Text = "Aliases";

+      this.aliases.Width = 325;

+      // 

       // Main

       // 

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

@@ -156,6 +163,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;

 

 

   }

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 8da0166f..800455f0 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -64,7 +64,7 @@ namespace Microsoft.Boogie.ModelViewer
       unfoldingRoot.Expanded = true;

       SetState(0);

 

-      currentStateView.Columns[1].Width = currentStateView.Width - currentStateView.Columns[0].Width - 5;

+      currentStateView.Columns[2].Width = currentStateView.Width - currentStateView.Columns[0].Width - currentStateView.Columns[1].Width - 5;

     }

 

     void SetState(int id)

@@ -136,18 +136,27 @@ namespace Microsoft.Boogie.ModelViewer
       if (!item.active)

         textBrush = grayedOut;

 

-      var dispName = item.dispNode.Name.ShortName();

-      var sz = e.Graphics.MeasureString(dispName, 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(dispName, font, textBrush, nameRect);

+      var width = DrawString(e.Graphics, item.dispNode.Name.ShortName(), font, textBrush, nameRect);

 

-      var valRect = rect;

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

-      valRect.Width = currentStateView.Width - valRect.X;

-      e.Graphics.DrawString(item.SubItems[1].Text, font, textBrush, valRect); // , StringFormat.GenericDefault);

+      nameRect.X += width + 4;

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

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

+

+      nameRect.X += width + 4;

+      nameRect.Width = currentStateView.Width - nameRect.X;

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

+    }

+

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

+    {

+      var sz = g.MeasureString(s, font).Width;

+      if (sz > minRect.Width - 2) {

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

+      }

+      g.DrawString(s, font, textBrush, minRect);

+      return minRect.Width;

     }

 

     private void listView1_DrawSubItem(object sender, DrawListViewSubItemEventArgs e)

@@ -227,7 +236,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 = DisplayItem.ValuesAsString(dn);

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

       }

       stateList.EndUpdate();

     }

@@ -263,28 +272,29 @@ namespace Microsoft.Boogie.ModelViewer
       }

 

       var tooltip = dispNode.ToolTip;

-      var values = ValuesAsString(dispNode);

+      var aliases = AliasesAsString(dispNode);

       if (tooltip != null) {

         this.ToolTipText = tooltip;

       } else {

-        this.ToolTipText = values;

+        this.ToolTipText = aliases;

       }

 

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

-      this.SubItems[1].Text = values;

+      this.SubItems[1].Text = dispNode.CanonicalValue;

+      this.SubItems[2].Text = aliases;

     }

 

     internal DisplayItem()

-       : base(new string[] { "", "" })

+       : base(new string[] { "", "", "" })

     {

     }

 

-    static internal string ValuesAsString(IDisplayNode dn)

+    static internal string AliasesAsString(IDisplayNode dn)

     {

       if (dn == null) return "";

 

       var sb = new StringBuilder();

-      foreach (var n in dn.Values) {

+      foreach (var n in dn.Aliases) {

         sb.Append(n).Append(", ");

         if (sb.Length > 300)

           break;

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 271e7da0..cabc6171 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -512,21 +512,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         }

       }

 

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

-        Model.Number n = e as Model.Number;

-        if (n != null)

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

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

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

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

       }

-    }

-

-    IEnumerable<StateNode> OtherStates()

-    {

-      var i = index;

-      for (var j = i - 1; j >= 0; j--)

-        yield return vm.states[j];

-      for (var j = i + 1; j < vm.states.Count; j++)

-        yield return vm.states[j];

-    }

+    } 

 

     internal void ComputeNames()

     {

@@ -586,14 +576,21 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       }

     }

 

-    public override IEnumerable<string> Values

+    public override string CanonicalValue

+    {

+      get

+      {

+        return stateNode.namer.CanonicalName(Element);

+      }

+    }

+

+    public override IEnumerable<string> Aliases

     {

       get

       {

         if (Element is Model.Boolean) {

-          yield return Element.ToString();

+          yield break;

         } else {

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

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

             if (edge != Name)

               yield return edge.FullName();

@@ -608,7 +605,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 Values){

+        foreach (var n in Aliases){

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

           if (limit-- < 0) {

             sb.Append("...");