Add search facility

4 files changed, 351 insertions, 86 deletions

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index 46125e74..0bbf51c6 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -36,14 +36,26 @@
       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.splitContainer2 = new System.Windows.Forms.SplitContainer();

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

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

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

+      this.linkLabel1 = new System.Windows.Forms.LinkLabel();

+      this.label1 = new System.Windows.Forms.Label();

+      this.textBox1 = new System.Windows.Forms.TextBox();

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

       this.splitContainer1.Panel1.SuspendLayout();

       this.splitContainer1.Panel2.SuspendLayout();

       this.splitContainer1.SuspendLayout();

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

+      this.splitContainer2.Panel1.SuspendLayout();

+      this.splitContainer2.Panel2.SuspendLayout();

+      this.splitContainer2.SuspendLayout();

       this.SuspendLayout();

       // 

       // currentStateView

       // 

+      this.currentStateView.BackColor = System.Drawing.SystemColors.Window;

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

             this.name,

             this.value,

@@ -57,16 +69,14 @@
       this.currentStateView.Name = "currentStateView";

       this.currentStateView.OwnerDraw = true;

       this.currentStateView.ShowItemToolTips = true;

-      this.currentStateView.Size = new System.Drawing.Size(614, 706);

+      this.currentStateView.Size = new System.Drawing.Size(721, 612);

       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.SelectedIndexChanged += new System.EventHandler(this.currentStateView_SelectedIndexChanged);

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

       // 

@@ -98,8 +108,8 @@
       // splitContainer1.Panel2

       // 

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

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

-      this.splitContainer1.SplitterDistance = 614;

+      this.splitContainer1.Size = new System.Drawing.Size(1028, 612);

+      this.splitContainer1.SplitterDistance = 721;

       this.splitContainer1.TabIndex = 1;

       // 

       // stateList

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

       this.stateList.Name = "stateList";

       this.stateList.ShowItemToolTips = true;

-      this.stateList.Size = new System.Drawing.Size(257, 706);

+      this.stateList.Size = new System.Drawing.Size(303, 612);

       this.stateList.TabIndex = 0;

       this.stateList.UseCompatibleStateImageBehavior = false;

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

@@ -138,18 +148,113 @@
       this.columnHeader2.Text = "Value";

       this.columnHeader2.Width = 116;

       // 

+      // splitContainer2

+      // 

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

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

+      this.splitContainer2.Name = "splitContainer2";

+      this.splitContainer2.Orientation = System.Windows.Forms.Orientation.Horizontal;

+      // 

+      // splitContainer2.Panel1

+      // 

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

+      // 

+      // splitContainer2.Panel2

+      // 

+      this.splitContainer2.Panel2.Controls.Add(this.matchesList);

+      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(1028, 796);

+      this.splitContainer2.SplitterDistance = 612;

+      this.splitContainer2.TabIndex = 1;

+      // 

+      // matchesList

+      // 

+      this.matchesList.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom)

+                  | System.Windows.Forms.AnchorStyles.Left)

+                  | System.Windows.Forms.AnchorStyles.Right)));

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

+            this.columnHeader4,

+            this.columnHeader5});

+      this.matchesList.FullRowSelect = true;

+      this.matchesList.GridLines = true;

+      this.matchesList.HeaderStyle = System.Windows.Forms.ColumnHeaderStyle.None;

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

+      this.matchesList.MultiSelect = false;

+      this.matchesList.Name = "matchesList";

+      this.matchesList.OwnerDraw = true;

+      this.matchesList.ShowItemToolTips = true;

+      this.matchesList.Size = new System.Drawing.Size(1028, 151);

+      this.matchesList.TabIndex = 4;

+      this.matchesList.UseCompatibleStateImageBehavior = false;

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

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

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

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

+      this.matchesList.DoubleClick += new System.EventHandler(this.matchesList_DoubleClick);

+      this.matchesList.Resize += new System.EventHandler(this.matchesList_Resize);

+      // 

+      // columnHeader4

+      // 

+      this.columnHeader4.Text = "Name";

+      this.columnHeader4.Width = 300;

+      // 

+      // columnHeader5

+      // 

+      this.columnHeader5.Text = "Value";

+      this.columnHeader5.Width = 500;

+      // 

+      // linkLabel1

+      // 

+      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(968, 5);

+      this.linkLabel1.Name = "linkLabel1";

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

+      this.linkLabel1.TabIndex = 3;

+      this.linkLabel1.TabStop = true;

+      this.linkLabel1.Text = "Show All...";

+      this.linkLabel1.VisitedLinkColor = System.Drawing.Color.Blue;

+      this.linkLabel1.LinkClicked += new System.Windows.Forms.LinkLabelLinkClickedEventHandler(this.linkLabel1_LinkClicked);

+      // 

+      // label1

+      // 

+      this.label1.AutoSize = true;

+      this.label1.Location = new System.Drawing.Point(3, 5);

+      this.label1.Name = "label1";

+      this.label1.Size = new System.Drawing.Size(44, 13);

+      this.label1.TabIndex = 2;

+      this.label1.Text = "Search:";

+      // 

+      // textBox1

+      // 

+      this.textBox1.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom)

+                  | System.Windows.Forms.AnchorStyles.Left)

+                  | 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(909, 20);

+      this.textBox1.TabIndex = 1;

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

+      // 

       // Main

       // 

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

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

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

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

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

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

       this.Name = "Main";

-      this.Text = "Boogie Model Viewer";

+      this.Text = "Boogie Verification Debugger";

       this.splitContainer1.Panel1.ResumeLayout(false);

       this.splitContainer1.Panel2.ResumeLayout(false);

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

       this.splitContainer1.ResumeLayout(false);

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

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

+      this.splitContainer2.Panel2.PerformLayout();

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

+      this.splitContainer2.ResumeLayout(false);

       this.ResumeLayout(false);

 

     }

@@ -165,6 +270,13 @@
     private System.Windows.Forms.ColumnHeader columnHeader2;

     private System.Windows.Forms.ColumnHeader columnHeader3;

     private System.Windows.Forms.ColumnHeader aliases;

+    private System.Windows.Forms.SplitContainer splitContainer2;

+    private System.Windows.Forms.ListView matchesList;

+    private System.Windows.Forms.ColumnHeader columnHeader4;

+    private System.Windows.Forms.ColumnHeader columnHeader5;

+    private System.Windows.Forms.LinkLabel linkLabel1;

+    private System.Windows.Forms.Label label1;

+    private System.Windows.Forms.TextBox textBox1;

 

 

   }

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 79a1d63c..4e20c6ef 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -17,6 +17,7 @@ namespace Microsoft.Boogie.ModelViewer
   {

     public string SearchText;

     SkeletonItem unfoldingRoot;

+    SkeletonItem[] allItems;

     int currentState;

     IState[] states;

     internal ILanguageProvider langProvider;

@@ -57,7 +58,7 @@ namespace Microsoft.Boogie.ModelViewer
         m = models[0];

       }

 

-      this.Text = Path.GetFileName(filename) + " - Boogie Model Viewer";

+      this.Text = Path.GetFileName(filename) + " - Boogie Verification Debugger";

 

       langProvider = null;

       foreach (var p in Providers()) {

@@ -70,7 +71,7 @@ namespace Microsoft.Boogie.ModelViewer
       var items = new List<ListViewItem>();

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

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

-      unfoldingRoot.PopulateRoot(states);

+      allItems = unfoldingRoot.PopulateRoot(states);

 

       var idx = 0;

       foreach (var i in states) {

@@ -90,7 +91,7 @@ namespace Microsoft.Boogie.ModelViewer
     void SetState(int id)

     {

       currentState = id;

-      SyncListView();

+      SyncCurrentStateView();

     }

 

     internal void Activate(TreeNode treeNode)

@@ -106,27 +107,42 @@ namespace Microsoft.Boogie.ModelViewer
     const int levelMult = 16;

     const int plusWidth = 16;

 

+    static Color Col(int c)

+    {

+      return Color.FromArgb(c >> 16, (c >> 8) & 0xff, c & 0xff);

+    }

+

     static StringFormat center = new StringFormat() { Alignment = StringAlignment.Center };

-    static Pen plusPen = new Pen(Color.FromArgb(0xaa, 0xaa, 0xaa));

-    static Brush grayedOut = new SolidBrush(Color.FromArgb(0xaa, 0xaa, 0xaa));

+    static Pen plusPen = new Pen(Col(0xaaaaaa));

+    static Brush grayedOut = new SolidBrush(Col(0xaaaaaa));

+    static Brush nonPrimary = new SolidBrush(Col(0xeeeeee));

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

     

     private void listView1_DrawItem(object sender, DrawListViewItemEventArgs e)

     {

       var item = (DisplayItem)e.Item;

       var skel = item.skel;

       var rect = e.Bounds;

+      var listView = (ListView)sender;

       rect.Y += 1;

       rect.Height -= 2;

 

       var textBrush = Brushes.Black;

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

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

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

         textBrush = Brushes.White;

       } else {

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

+        var bg = Brushes.White;

+        if (item.active && !skel.isPrimary[currentState])

+          bg = nonPrimary;

+        if (item.skel.isMatch)

+          bg = matchBg;

+        e.Graphics.FillRectangle(bg, rect);

       }

 

       var off = levelMult * item.skel.level;

+      if (item.IsMatchListItem)

+        off = 0;

 

       {

         var plusRect = rect;

@@ -149,23 +165,23 @@ namespace Microsoft.Boogie.ModelViewer
 

       off += plusWidth + 3;

       var nameRect = rect;

-      var font = currentStateView.Font;

+      var font = listView.Font;

 

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

         textBrush = Brushes.Red;

       if (!item.active)

         textBrush = grayedOut;

 

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

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

       nameRect.X += off;

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

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

 

       nameRect.X += width + 4;

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

+      nameRect.Width = listView.Columns[0].Width + listView.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;

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

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

     }

 

@@ -179,20 +195,12 @@ namespace Microsoft.Boogie.ModelViewer
       return minRect.Width;

     }

 

-    private void listView1_DrawSubItem(object sender, DrawListViewSubItemEventArgs e)

-    {

-    }

-

     private void listView1_DrawColumnHeader(object sender, DrawListViewColumnHeaderEventArgs e)

     {

       e.DrawBackground();

       e.DrawText();

     }

 

-    private void listView1_MouseMove(object sender, MouseEventArgs e)

-    {

-    }

-

     private void listView1_MouseUp(object sender, MouseEventArgs e)

     {

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

@@ -204,31 +212,39 @@ namespace Microsoft.Boogie.ModelViewer
         int plusLoc = skel.level * levelMult;

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

           skel.Expanded = !skel.Expanded;

-          SyncListView();

+          SyncCurrentStateView();

         }

       }

     }

 

-    private void SyncListView()

+    private void SyncCurrentStateView()

+    {

+      SyncListView(unfoldingRoot.RecChildren, currentStateView, (x, y) => { });

+    }

+

+    private void SyncListView(IEnumerable<SkeletonItem> items, ListView listView, Action<DisplayItem, SkeletonItem> cb)

     {

-      var ch = unfoldingRoot.RecChildren.ToArray();

-      var missing = ch.Length - currentStateView.Items.Count;

 

-      currentStateView.BeginUpdate();

+      var ch = items.ToArray();

+      var missing = ch.Length - listView.Items.Count;

+      listView.BeginUpdate();

       if (missing < 0) {

         missing = -missing;

         while (missing-- > 0) {

-          currentStateView.Items.RemoveAt(currentStateView.Items.Count - 1);

+          listView.Items.RemoveAt(listView.Items.Count - 1);

         }

       } else {

         while (missing-- > 0) {

-          currentStateView.Items.Add(new DisplayItem());

+          listView.Items.Add(new DisplayItem());

         }

       }

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

-        ((DisplayItem)currentStateView.Items[i]).Set(ch[i], currentState);

-      currentStateView.EndUpdate();

-      currentStateView.Invalidate();

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

+        var di = (DisplayItem)listView.Items[i];

+        di.Set(ch[i], currentState);

+        cb(di, ch[i]);

+      }

+      listView.EndUpdate();

+      listView.Invalidate();

     }

 

     private void listView1_ColumnWidthChanged(object sender, ColumnWidthChangedEventArgs e)

@@ -268,6 +284,70 @@ namespace Microsoft.Boogie.ModelViewer
       stateList.EndUpdate();

     }

 

+    private void ExpandParents(SkeletonItem item)

+    {

+      item = item.parent;

+      while (item != null && !item.Expanded) {

+        item.Expanded = true;

+        item = item.parent;

+      }

+    }

+

+    private void textBox1_TextChanged(object sender, EventArgs e)

+    {

+      UpdateMatches(false);

+    }

+

+    private void UpdateMatches(bool force)

+    {

+      var words = textBox1.Text.Split(' ').Where(s => s != "").Select(s => s.ToLower()).ToArray();

+      var changed = force;

+      var matches = new List<SkeletonItem>();

+      foreach (var s in allItems) {

+        var newMatch = false;

+        if (s.isPrimary[currentState] && words.Length > 0) {

+          newMatch = s.MatchesWords(words, currentState);

+        }

+        if (newMatch)

+          matches.Add(s);

+        if (s.isMatch != newMatch) {

+          changed = true;

+          s.isMatch = newMatch;

+        }

+      }

+

+      if (changed) {

+        SyncListView(matches, matchesList, (di, _) => { di.IsMatchListItem = true; });

+      }

+    }

+

+    private void matchesList_Resize(object sender, EventArgs e)

+    {

+      matchesList.Invalidate();

+    }

+

+    private void matchesList_DoubleClick(object sender, EventArgs e)

+    {

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

+      var sel = (DisplayItem) matchesList.SelectedItems[0];

+      ExpandParents(sel.skel);

+      SyncCurrentStateView();

+      foreach (DisplayItem it in currentStateView.Items) {

+        if (it.skel == sel.skel) {

+          it.Selected = true;

+          currentStateView.EnsureVisible(it.Index);

+          break;

+        }

+      }

+    }

+

+    private void linkLabel1_LinkClicked(object sender, LinkLabelLinkClickedEventArgs e)

+    {

+      foreach (DisplayItem it in matchesList.Items) {

+        ExpandParents(it.skel);

+      }

+      SyncCurrentStateView();

+    }

   }

 

   internal class DisplayItem : ListViewItem

@@ -277,6 +357,8 @@ namespace Microsoft.Boogie.ModelViewer
     internal bool active;

     internal IDisplayNode dispNode;

 

+    public bool IsMatchListItem { get; set; }

+

     internal void Set(SkeletonItem s, int id)

     {

       if (skel == s && stateId == id)

@@ -300,16 +382,17 @@ namespace Microsoft.Boogie.ModelViewer
 

       var tooltip = dispNode.ToolTip;

       var aliases = AliasesAsString(dispNode);

+      if (IsMatchListItem)

+        aliases = "";

       if (tooltip != null) {

         this.ToolTipText = tooltip;

       } else {

         this.ToolTipText = aliases;

       }

 

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

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

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

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

-      

     }

 

     internal DisplayItem()

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 7ac24500..e1fb2bad 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -81,20 +81,25 @@ namespace Microsoft.Boogie.ModelViewer
       }

     }

 

-    void Unfold(IDisplayNode n)

+    void Unfold(IEnumerable<IDisplayNode> ns)

     {

-      if (n.Element != null) {

-        var prev = GetName(n.Element);

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

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

-          return;

-        prev.unfolded = true;

-      }

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

+        if (!n.Expandable) return;

 

-      foreach (var c in n.Expand()) {

-        Unfold(c);

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

       }

     }

 

@@ -106,7 +111,7 @@ namespace Microsoft.Boogie.ModelViewer
 

     public void ComputeNames(IEnumerable<IDisplayNode> n)

     {

-      n.Iter(Unfold);

+      Unfold(n);

       ComputeBestName();

     }

 

@@ -131,7 +136,10 @@ namespace Microsoft.Boogie.ModelViewer
       var end = beg;

       while (end < s.Length && char.IsDigit(s[end]))

         end++;

-      return ulong.Parse(s.Substring(beg, end - beg)); 

+      ulong res;

+      if (!ulong.TryParse(s.Substring(beg, end - beg), out res))

+        return 0;

+      return res;

     }

 

     public static int CompareFields(string f1, string f2)

@@ -139,9 +147,9 @@ namespace Microsoft.Boogie.ModelViewer
       bool s1 = HasAny(f1, "[<>]");

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

       if (s1 && !s2)

-        return -1;

-      if (!s1 && s2)

         return 1;

+      if (!s1 && s2)

+        return -1;

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

       var numberPos = -1;

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

diff --git a/Source/ModelViewer/TreeSkeleton.cs b/Source/ModelViewer/TreeSkeleton.cs
index 08f2b3f0..3663f926 100644
--- a/Source/ModelViewer/TreeSkeleton.cs
+++ b/Source/ModelViewer/TreeSkeleton.cs
@@ -10,10 +10,12 @@ namespace Microsoft.Boogie.ModelViewer
     readonly IEdgeName name;

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

     internal readonly IDisplayNode[] displayNodes;

-    readonly SkeletonItem parent;

+    internal bool[] isPrimary;

+    internal readonly SkeletonItem parent;

     readonly Main main;

     internal readonly int level;

     internal bool expanded, wasExpanded;

+    internal bool isMatch;

 

     public void Iter(Action<SkeletonItem> handler)

     {

@@ -35,12 +37,14 @@ namespace Microsoft.Boogie.ModelViewer
       }

     }

 

-    public void PopulateRoot(IEnumerable<IState> states)

+    public SkeletonItem[] PopulateRoot(IEnumerable<IState> states)

     {

       var i = 0;

       foreach (var s in states) {

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

       }

+

+      return BfsExpand(this);

     }

 

     public SkeletonItem(Main m, int stateCount)

@@ -48,6 +52,7 @@ namespace Microsoft.Boogie.ModelViewer
       name = new EdgeName("<root>");

       main = m;

       displayNodes = new IDisplayNode[stateCount];

+      isPrimary = new bool[stateCount];

     }

 

     internal SkeletonItem(IEdgeName n, SkeletonItem par)

@@ -68,37 +73,94 @@ namespace Microsoft.Boogie.ModelViewer
       get { return expanded; }

       set

       {

-        if (!value) {

-          expanded = false;

-        } else {

-          if (expanded) return;

-          expanded = true;

-          if (wasExpanded) return;

-          wasExpanded = true;

-

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

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

-              SkeletonItem skelChild;

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

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

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

-                created.Add(name, skelChild);

-                names.Add(name);

-                

-              }

-              skelChild.displayNodes[i] = child;

-            }

-          }

+        expanded = value;

+        if (expanded)

+          ComputeChildren();

+      }

+    }

+

+    static SkeletonItem[] BfsExpand(SkeletonItem skel)

+    {

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

+        BfsExpandCore(skel, i);

+

+      var workItems = new Stack<SkeletonItem>();

+      var allNodes = new List<SkeletonItem>();

+      workItems.Push(skel);

+

+      while (workItems.Count > 0) {

+        var s = workItems.Pop();

+        if (!s.isPrimary.Any())

+          continue;

+        allNodes.Add(s);

+        s.children.Iter(workItems.Push);

+      }

+

+      return allNodes.ToArray();

+    }

+

+    static void BfsExpandCore(SkeletonItem skel, int idx)

+    {

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

+      var workItems = new Queue<SkeletonItem>();

+

+      workItems.Enqueue(skel);

+      while (workItems.Count > 0) {

+        var s = workItems.Dequeue();

+        if (s.displayNodes[idx] == null)

+          continue;

+        var e = s.displayNodes[idx].Element;

+        s.isPrimary[idx] = true;

+        if (e != null) {

+          if (visited.Contains(e))

+            continue;

+          visited.Add(e);

+        }

+        s.ComputeChildren();

+        s.children.Iter(workItems.Enqueue);

+      }

+    }

+

+    private void ComputeChildren()

+    {

+      if (wasExpanded) return;

+      wasExpanded = true;

+

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

+      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()) {

+          SkeletonItem skelChild;

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

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

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

+            created.Add(name, skelChild);

+            names.Add(name);

 

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

-            children.Add(created[name]);

           }

+          skelChild.displayNodes[i] = child;

         }

       }

+

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

+        children.Add(created[name]);

+      }

+    }

+

+    public bool MatchesWords(string[] words, int stateId)

+    {

+      var node = displayNodes[stateId];

+      if (node == null)

+        return false;

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

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

+      foreach (var w in words) {

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

+          return false;

+      }

+      return true;

     }

   }