Work on keeping the unfolding skeleton when switching between states

5 files changed, 388 insertions, 106 deletions

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index a4c61589..766768e2 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -15,13 +15,18 @@ namespace Microsoft.Boogie.ModelViewer.Base
       return true;

     }

 

-    public IEnumerable<IDisplayNode> GetStates(Model m)

+    IEnumerable<IDisplayNode> GetStateNodes(Model m)

     {

       yield return GenericNodes.Functions(m);

       yield return GenericNodes.Constants(m);

       foreach (var s in m.States)

         yield return new StateNode(s);

     }

+

+    public IEnumerable<IState> GetStates(Model m)

+    {

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

+    }

   }

 

   public class StateNode : DisplayNode

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index bda154ca..f1b0b26f 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -5,6 +5,12 @@ using System.Text;
 

 namespace Microsoft.Boogie.ModelViewer

 {

+  public interface ILanguageProvider

+  {

+    bool IsMyModel(Model m);

+    IEnumerable<IState> GetStates(Model m);

+  }

+

   [Flags]

   public enum NodeState

   {

@@ -14,18 +20,54 @@ namespace Microsoft.Boogie.ModelViewer
 

   public interface IDisplayNode

   {

-    string Name { get; }

-    IEnumerable<string> Values { get; }

+    /// <summary>

+    ///  Used for indexing the state tree.

+    /// </summary>

+    string EdgeName { get; }

+

+    /// <summary>

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

+    /// </summary>

+    Model.Element Element { get; }

+

     bool Expandable { get; }

     IEnumerable<IDisplayNode> Expand();

-    object ViewSync { get; set; }

+

+    // Things displayed to the user.

+    string Name { get; }

     NodeState State { get; }

+    IEnumerable<string> Values { get; }

+

+    object ViewSync { get; set; }

   }

 

-  public interface ILanguageProvider

+  public interface IState

   {

-    bool IsMyModel(Model m);

-    IEnumerable<IDisplayNode> GetStates(Model m);

+    string Name { get; }

+    IEnumerable<IDisplayNode> Nodes { get; }

+  }

+

+

+  public class TopState : IState

+  {

+    protected IDisplayNode[] children;

+    protected string name;

+

+    public TopState(string name, IEnumerable<IDisplayNode> nodes)

+    {

+      this.name = name;

+      children = nodes.ToArray();

+    }

+

+    public string Name

+    {

+      get { return name; }

+    }

+

+    public IEnumerable<IDisplayNode> Nodes

+    {

+      get { return children; }

+    }

   }

 

   public abstract class DisplayNode : IDisplayNode

@@ -57,13 +99,15 @@ namespace Microsoft.Boogie.ModelViewer
     public virtual NodeState State { get { return NodeState.Normal; } }

 

     public object ViewSync { get; set; }

-  }

 

-  public static class SeqExtensions

-  {

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

+    public virtual string EdgeName

     {

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

+      get { return name; }

+    }

+

+    public virtual Model.Element Element

+    {

+      get { return null; }

     }

   }

 

@@ -90,4 +134,22 @@ namespace Microsoft.Boogie.ModelViewer
   }

 

 

+  public static class Util

+  {

+    public static void Assert(bool cond)

+    {

+      if (!cond) throw new System.Exception("assertion violation");

+    }

+

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

+    {

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

+    }

+

+    public static void Iter<T>(this IEnumerable<T> inp, Action<T> fn)

+    {

+      foreach (var s in inp) fn(s);

+    }

+  }

+

 }

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index 5441c627..64164f0e 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -27,64 +27,126 @@
     /// </summary>

     private void InitializeComponent()

     {

-      this.listView1 = new System.Windows.Forms.ListView();

+      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.splitContainer1 = new System.Windows.Forms.SplitContainer();

+      this.stateList = new System.Windows.Forms.ListView();

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

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

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

+      this.splitContainer1.Panel1.SuspendLayout();

+      this.splitContainer1.Panel2.SuspendLayout();

+      this.splitContainer1.SuspendLayout();

       this.SuspendLayout();

       // 

-      // listView1

+      // currentStateView

       // 

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

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

             this.name,

             this.value});

-      this.listView1.Dock = System.Windows.Forms.DockStyle.Fill;

-      this.listView1.FullRowSelect = true;

-      this.listView1.GridLines = true;

-      this.listView1.HeaderStyle = System.Windows.Forms.ColumnHeaderStyle.Nonclickable;

-      this.listView1.Location = new System.Drawing.Point(0, 0);

-      this.listView1.MultiSelect = false;

-      this.listView1.Name = "listView1";

-      this.listView1.OwnerDraw = true;

-      this.listView1.ShowItemToolTips = true;

-      this.listView1.Size = new System.Drawing.Size(851, 689);

-      this.listView1.TabIndex = 0;

-      this.listView1.UseCompatibleStateImageBehavior = false;

-      this.listView1.View = System.Windows.Forms.View.Details;

-      this.listView1.ColumnWidthChanged += new System.Windows.Forms.ColumnWidthChangedEventHandler(this.listView1_ColumnWidthChanged);

-      this.listView1.DrawColumnHeader += new System.Windows.Forms.DrawListViewColumnHeaderEventHandler(this.listView1_DrawColumnHeader);

-      this.listView1.DrawItem += new System.Windows.Forms.DrawListViewItemEventHandler(this.listView1_DrawItem);

-      this.listView1.DrawSubItem += new System.Windows.Forms.DrawListViewSubItemEventHandler(this.listView1_DrawSubItem);

-      this.listView1.MouseMove += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseMove);

-      this.listView1.MouseUp += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseUp);

-      this.listView1.Resize += new System.EventHandler(this.listView1_Resize);

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

+      this.currentStateView.FullRowSelect = true;

+      this.currentStateView.GridLines = true;

+      this.currentStateView.HeaderStyle = System.Windows.Forms.ColumnHeaderStyle.Nonclickable;

+      this.currentStateView.Location = new System.Drawing.Point(0, 0);

+      this.currentStateView.MultiSelect = false;

+      this.currentStateView.Name = "currentStateView";

+      this.currentStateView.OwnerDraw = true;

+      this.currentStateView.ShowItemToolTips = true;

+      this.currentStateView.Size = new System.Drawing.Size(654, 706);

+      this.currentStateView.TabIndex = 0;

+      this.currentStateView.UseCompatibleStateImageBehavior = false;

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

+      this.currentStateView.ColumnWidthChanged += new System.Windows.Forms.ColumnWidthChangedEventHandler(this.listView1_ColumnWidthChanged);

+      this.currentStateView.DrawColumnHeader += new System.Windows.Forms.DrawListViewColumnHeaderEventHandler(this.listView1_DrawColumnHeader);

+      this.currentStateView.DrawItem += new System.Windows.Forms.DrawListViewItemEventHandler(this.listView1_DrawItem);

+      this.currentStateView.DrawSubItem += new System.Windows.Forms.DrawListViewSubItemEventHandler(this.listView1_DrawSubItem);

+      this.currentStateView.MouseMove += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseMove);

+      this.currentStateView.MouseUp += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseUp);

+      this.currentStateView.Resize += new System.EventHandler(this.listView1_Resize);

       // 

       // name

       // 

       this.name.Text = "Name";

-      this.name.Width = 190;

+      this.name.Width = 174;

       // 

       // value

       // 

       this.value.Text = "Value";

-      this.value.Width = 500;

+      this.value.Width = 463;

+      // 

+      // splitContainer1

+      // 

+      this.splitContainer1.Dock = System.Windows.Forms.DockStyle.Fill;

+      this.splitContainer1.Location = new System.Drawing.Point(0, 0);

+      this.splitContainer1.Name = "splitContainer1";

+      // 

+      // splitContainer1.Panel1

+      // 

+      this.splitContainer1.Panel1.Controls.Add(this.currentStateView);

+      // 

+      // splitContainer1.Panel2

+      // 

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

+      this.splitContainer1.Size = new System.Drawing.Size(875, 706);

+      this.splitContainer1.SplitterDistance = 654;

+      this.splitContainer1.TabIndex = 1;

+      // 

+      // stateList

+      // 

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

+            this.columnHeader1,

+            this.columnHeader2});

+      this.stateList.Dock = System.Windows.Forms.DockStyle.Fill;

+      this.stateList.FullRowSelect = true;

+      this.stateList.GridLines = true;

+      this.stateList.HeaderStyle = System.Windows.Forms.ColumnHeaderStyle.Nonclickable;

+      this.stateList.Location = new System.Drawing.Point(0, 0);

+      this.stateList.MultiSelect = false;

+      this.stateList.Name = "stateList";

+      this.stateList.ShowItemToolTips = true;

+      this.stateList.Size = new System.Drawing.Size(217, 706);

+      this.stateList.TabIndex = 0;

+      this.stateList.UseCompatibleStateImageBehavior = false;

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

+      this.stateList.SelectedIndexChanged += new System.EventHandler(this.stateList_SelectedIndexChanged);

+      // 

+      // columnHeader1

+      // 

+      this.columnHeader1.Text = "State";

+      this.columnHeader1.Width = 82;

+      // 

+      // columnHeader2

+      // 

+      this.columnHeader2.Text = "Value";

+      this.columnHeader2.Width = 128;

       // 

       // Main

       // 

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

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

-      this.ClientSize = new System.Drawing.Size(851, 689);

-      this.Controls.Add(this.listView1);

+      this.ClientSize = new System.Drawing.Size(875, 706);

+      this.Controls.Add(this.splitContainer1);

       this.Name = "Main";

       this.Text = "Boogie Model Viewer";

+      this.splitContainer1.Panel1.ResumeLayout(false);

+      this.splitContainer1.Panel2.ResumeLayout(false);

+      ((System.ComponentModel.ISupportInitialize)(this.splitContainer1)).EndInit();

+      this.splitContainer1.ResumeLayout(false);

       this.ResumeLayout(false);

 

     }

 

     #endregion

 

-    private System.Windows.Forms.ListView listView1;

+    private System.Windows.Forms.ListView currentStateView;

     private System.Windows.Forms.ColumnHeader name;

     private System.Windows.Forms.ColumnHeader value;

+    private System.Windows.Forms.SplitContainer splitContainer1;

+    private System.Windows.Forms.ListView stateList;

+    private System.Windows.Forms.ColumnHeader columnHeader1;

+    private System.Windows.Forms.ColumnHeader columnHeader2;

 

 

   }

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 71fc7742..ee882c74 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -16,6 +16,9 @@ namespace Microsoft.Boogie.ModelViewer
   public partial class Main : Form

   {

     public string SearchText;

+    SkeletonItem unfoldingRoot;

+    int currentState;

+    IState[] states;

 

     // TODO this should be dynamically loaded

     IEnumerable<ILanguageProvider> Providers()

@@ -28,6 +31,7 @@ namespace Microsoft.Boogie.ModelViewer
     {

       InitializeComponent();

 

+

       var args = Environment.GetCommandLineArgs();

       Model m;

 

@@ -43,13 +47,41 @@ namespace Microsoft.Boogie.ModelViewer
           break;

         }

       }

-       

+      

       var items = new List<ListViewItem>();

-      foreach (var i in prov.GetStates(m))

-        items.Add(new DisplayItem(i));

-      listView1.Items.AddRange(items.ToArray());

+      states = prov.GetStates(m).ToArray();

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

+      unfoldingRoot.PopulateRoot(states);

+

+      foreach (var i in states) {

+        var it = new ListViewItem(new string[] { i.Name, "" });

+        it.Tag = i;

+        items.Add(it);

+      }

+      stateList.Items.AddRange(items.ToArray());

+      SetState(0);

 

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

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

+    }

+

+    void SetState(int id)

+    {

+      currentState = id;

+      unfoldingRoot.SetStateId(id);

+

+      SkeletonItem sel = null;

+      if (currentStateView.SelectedItems.Count > 0)

+        sel = ((DisplayItem)currentStateView.SelectedItems[0]).skel;

+

+      currentStateView.BeginUpdate();

+      currentStateView.Items.Clear();

+      currentStateView.Items.AddRange(unfoldingRoot.DisplayItems().Skip(1).ToArray());

+      if (sel != null && sel.DisplayItem != null) {

+        var it = sel.DisplayItem;

+        it.Selected = true;

+        currentStateView.EnsureVisible(it.Index);

+      }

+      currentStateView.EndUpdate();

     }

 

     internal void Activate(TreeNode treeNode)

@@ -76,7 +108,7 @@ namespace Microsoft.Boogie.ModelViewer
       rect.Height -= 2;

 

       var textBrush = Brushes.Black;

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

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

         // Draw the background and focus rectangle for a selected item.

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

         // e.DrawFocusRectangle();

@@ -85,7 +117,7 @@ namespace Microsoft.Boogie.ModelViewer
         e.Graphics.FillRectangle(Brushes.White, rect);

       }

 

-      var off = levelMult * item.level;

+      var off = levelMult * item.skel.level;

 

       {

         var plusRect = rect;

@@ -101,17 +133,17 @@ namespace Microsoft.Boogie.ModelViewer
           float midX = plusBorder.X + plusBorder.Width / 2;

           float midY = plusBorder.Y + plusBorder.Height / 2;

           e.Graphics.DrawLine(plusPen, plusBorder.X + 2, midY, plusBorder.Right - 2, midY);

-          if (!item.expanded)

+          if (!item.skel.expanded)

             e.Graphics.DrawLine(plusPen, midX, plusBorder.Y + 2, midX, plusBorder.Bottom - 2);

         }

       }

 

       off += plusWidth + 3;

       var nameRect = rect;

-      var font = listView1.Font;

+      var font = currentStateView.Font;

 

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

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

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

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

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

       nameRect.X += off;

@@ -119,7 +151,7 @@ namespace Microsoft.Boogie.ModelViewer
 

       var valRect = rect;

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

-      valRect.Width = listView1.Width - valRect.X;

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

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

     }

 

@@ -139,77 +171,197 @@ namespace Microsoft.Boogie.ModelViewer
 

     private void listView1_MouseUp(object sender, MouseEventArgs e)

     {

-      var clickedItem = (DisplayItem)listView1.GetItemAt(5, e.Y);

+      var clickedItem = (DisplayItem)currentStateView.GetItemAt(5, e.Y);

       if (clickedItem != null) {

         clickedItem.Selected = true;

         clickedItem.Focused = true;

 

-        int plusLoc = clickedItem.level * levelMult;

+        var skel = clickedItem.skel;

+        int plusLoc = skel.level * levelMult;

         if (clickedItem.displayNode.Expandable && e.X >= plusLoc && e.X <= plusLoc + plusWidth) {

-          clickedItem.expanded = !clickedItem.expanded;

-

-          if (clickedItem.expanded) {

-            if (clickedItem.collapsedChildren == null) {

-              var items = new List<DisplayItem>();

-              foreach (var ch in clickedItem.displayNode.Expand()) {

-                var it = new DisplayItem(ch);

-                it.level = clickedItem.level + 1;

-                items.Add(it);

-              }

-              clickedItem.collapsedChildren = items.ToArray();

-            }

-            var pos = clickedItem.Index + 1;

-            listView1.BeginUpdate();

-            foreach (var it in clickedItem.collapsedChildren) {

-              listView1.Items.Insert(pos, it);

-              pos++;

-            }

-            listView1.EndUpdate();

-          } else {

-            var collapsed = new List<DisplayItem>();

-            var beg = clickedItem.Index + 1;

-            for (int i = beg; i < listView1.Items.Count; ++i) {

-              var curr = (DisplayItem)listView1.Items[i];

-              if (curr.level <= clickedItem.level) break;

-              collapsed.Add(curr);

-            }

-            clickedItem.collapsedChildren = collapsed.ToArray();

-            listView1.BeginUpdate();

-            for (int i = 0; i < collapsed.Count; ++i)

-              listView1.Items.RemoveAt(beg);

-            listView1.EndUpdate();

-          }

-

-          listView1.Invalidate();

+          SetExpansion(clickedItem, !skel.expanded);

         }

       }

     }

 

+    private void SetExpansion(DisplayItem clickedItem, bool exp)

+    {

+      var pos = clickedItem.Index + 1;

+      var skel = clickedItem.skel;

+

+      if (skel.expanded == exp) return;

+

+      if (!skel.expanded) {

+        skel.Expand(currentState);

+

+        currentStateView.BeginUpdate();

+        foreach (var it in skel.DisplayItems()) {

+          currentStateView.Items.Insert(pos, it);

+          pos++;

+        }

+        currentStateView.EndUpdate();

+      } else {

+        var cnt = skel.DisplayItems().Count();

+

+        skel.Fold();

+

+        currentStateView.BeginUpdate();

+        for (int i = 0; i < cnt; ++i)

+          currentStateView.Items.RemoveAt(pos);

+        currentStateView.EndUpdate();

+      }

+

+      currentStateView.Invalidate();

+    }

+

     private void listView1_ColumnWidthChanged(object sender, ColumnWidthChangedEventArgs e)

     {

-      listView1.Invalidate();

+      currentStateView.Invalidate();

     }

 

     private void listView1_Resize(object sender, EventArgs e)

     {

-      listView1.Invalidate();

+      currentStateView.Invalidate();

     }

 

+    private void stateList_SelectedIndexChanged(object sender, EventArgs e)

+    {

+      if (stateList.SelectedItems.Count == 0) return;

+      var sel = stateList.SelectedItems[0].Index;

+      SetState(sel);

+    }

   }

 

-  internal class DisplayItem : ListViewItem

+  internal class SkeletonItem

   {

-    internal IDisplayNode displayNode;

+    readonly string name;

+    readonly List<SkeletonItem> inactiveChildren = new List<SkeletonItem>();

+    readonly List<SkeletonItem> activeChildren = new List<SkeletonItem>();

+    readonly IDisplayNode[] displayNodes;

+    readonly IDisplayNode[][] displayNodeExpansions;

+    readonly SkeletonItem parent;

+    readonly Main main;

+    internal readonly int level;

     internal bool expanded;

-    internal int level;

-    internal DisplayItem[] collapsedChildren;

+    DisplayItem currNode; // in the current view

+

+    public void Iter(Action<SkeletonItem> handler)

+    {

+      handler(this);

+      activeChildren.Iter(u => u.Iter(handler));

+      inactiveChildren.Iter(u => u.Iter(handler));

+    }

+

+    public void SetStateId(int id)

+    {

+      expanded = true;

+      Iter(u =>

+      {

+        u.currNode = null;

+        u.inactiveChildren.AddRange(activeChildren);

+        u.activeChildren.Clear();

+      });

+      CreateBacking(id);

+    }

+

+    public DisplayItem DisplayItem { get { return currNode; } }

+

+    public IEnumerable<DisplayItem> DisplayItems()

+    {

+      Util.Assert(currNode != null);

+      yield return currNode;

+      if (expanded) {

+        foreach (var ch in activeChildren)

+          foreach (var d in ch.DisplayItems())

+            yield return d;

+      }

+    }

 

-    internal DisplayItem(IDisplayNode d)

+    public void PopulateRoot(IEnumerable<IState> states)

+    {

+      var i = 0;

+      foreach(var s in states) {

+        displayNodes[i++] = new ContainerNode<IDisplayNode>(this.name, x => x, s.Nodes);

+      }

+    }

+

+    public SkeletonItem(Main m, int stateCount)

+    {

+      name = "<root>";

+      main = m;

+      displayNodes = new IDisplayNode[stateCount];

+      displayNodeExpansions = new IDisplayNode[stateCount][];

+    }

+

+    internal SkeletonItem(string n, SkeletonItem par)

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

+    {

+      parent = par;

+      name = n;

+      level = par.level + 1;

+    }

+

+    public void Fold()

+    {

+      expanded = false;

+    }

+

+    public void Expand(int stateId)

+    {

+      if(expanded) return;

+      expanded = true;

+      CreateBacking(stateId);

+    }

+

+    private void CreateBacking(int stateId)

+    {

+      var dn = displayNodes[stateId];

+      if (currNode == null)

+        currNode = new DisplayItem(dn, this);

+

+      if (!expanded || activeChildren.Count > 0)

+        return;

+

+      if (displayNodeExpansions[stateId] == null) {

+        if (dn.Expandable) {

+          displayNodeExpansions[stateId] = dn.Expand().ToArray();

+        } else {

+          displayNodeExpansions[stateId] = new DisplayNode[0];

+        }

+      }

+

+      if (activeChildren.Count == displayNodeExpansions[stateId].Length)

+        return;

+

+      var dict = inactiveChildren.ToDictionary(u => u.name);

+

+      foreach (var d in displayNodeExpansions[stateId]) {

+        SkeletonItem child;

+        if (dict.TryGetValue(d.EdgeName, out child)) {

+          dict.Remove(d.EdgeName);

+        } else {

+          child = new SkeletonItem(d.EdgeName, this);

+        }

+        activeChildren.Add(child);

+        child.displayNodes[stateId] = d;

+      }

+      inactiveChildren.Clear();

+      inactiveChildren.AddRange(dict.Values);

+

+      activeChildren.Iter(c => c.CreateBacking(stateId));

+    }

+  }

+

+  internal class DisplayItem : ListViewItem

+  {

+    internal readonly IDisplayNode displayNode;

+    internal readonly SkeletonItem skel;

+

+    internal DisplayItem(IDisplayNode d, SkeletonItem s)

        : base(d.Name)

     {

       displayNode = d;

-      displayNode.ViewSync = this;

-      expanded = false;

+      skel = s;

 

       var sb = new StringBuilder();

       foreach (var n in displayNode.Values) {

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

     }

 

-    public IEnumerable<IDisplayNode> GetStates(Model m)

+    public IEnumerable<IState> GetStates(Model m)

     {

       var vm = new VccModel();

       foreach (var s in m.States) {

@@ -37,22 +37,24 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     }

   }

 

-  class StateNode : DisplayNode

+  class StateNode : IState

   {

     Model.CapturedState state;

+    string name;

     VccModel parent;

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

 

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

+    public StateNode(VccModel parent, Model.CapturedState s)

     {

       this.parent = parent;

       state = s;

 

+      name = s.Name;

       var idx = name.LastIndexOfAny(new char[] { '\\', '/' });

       if (idx > 0)

         name = name.Substring(idx + 1);

 

-      var prev = parent.states.Last();

+      // var prev = parent.states.Last();

 

       foreach (var v in state.Variables) {

         var n = parent.GetUserVariableName(v);

@@ -64,15 +66,14 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       }

     }

 

-    public override IEnumerable<string> Values

+    public string Name

     {

-      get { return vars.Map(v => v.Name); }

+      get { return name; }

     }

 

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

-    public override IEnumerable<IDisplayNode> Expand()

+    public IEnumerable<IDisplayNode> Nodes

     {

-      foreach (var v in vars) yield return v;

+      get { return vars; }

     }

   }