Add reload-model option. Bugfixes when switching models

2 files changed, 58 insertions, 9 deletions

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index 417527a9..0449e6b5 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -58,6 +58,7 @@
       this.toolStripMenuItem1 = new System.Windows.Forms.ToolStripSeparator();

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

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

+      this.reloadModelFileToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.stateViewMenu.SuspendLayout();

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

       this.splitContainer1.Panel1.SuspendLayout();

@@ -284,6 +285,7 @@
       // fileToolStripMenuItem

       // 

       this.fileToolStripMenuItem.DropDownItems.AddRange(new System.Windows.Forms.ToolStripItem[] {

+            this.reloadModelFileToolStripMenuItem,

             this.exitToolStripMenuItem});

       this.fileToolStripMenuItem.Name = "fileToolStripMenuItem";

       this.fileToolStripMenuItem.Size = new System.Drawing.Size(37, 20);

@@ -292,7 +294,7 @@
       // exitToolStripMenuItem

       // 

       this.exitToolStripMenuItem.Name = "exitToolStripMenuItem";

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

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

       this.exitToolStripMenuItem.Text = "&Exit";

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

       // 

@@ -357,6 +359,13 @@
       this.modelsToolStripMenuItem.Size = new System.Drawing.Size(58, 20);

       this.modelsToolStripMenuItem.Text = "&Models";

       // 

+      // reloadModelFileToolStripMenuItem

+      // 

+      this.reloadModelFileToolStripMenuItem.Name = "reloadModelFileToolStripMenuItem";

+      this.reloadModelFileToolStripMenuItem.Size = new System.Drawing.Size(166, 22);

+      this.reloadModelFileToolStripMenuItem.Text = "&Reload model file";

+      this.reloadModelFileToolStripMenuItem.Click += new System.EventHandler(this.reloadModelFileToolStripMenuItem_Click);

+      // 

       // Main

       // 

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

@@ -415,6 +424,7 @@
     private System.Windows.Forms.ToolStripMenuItem debugToolStripMenuItem;

     private System.Windows.Forms.ToolStripMenuItem modelsToolStripMenuItem;

     private System.Windows.Forms.ToolStripMenuItem includeTheKitchenSinkToolStripMenuItem;

+    private System.Windows.Forms.ToolStripMenuItem reloadModelFileToolStripMenuItem;

 

 

   }

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 0a67c9a9..4870c9be 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -25,6 +25,8 @@ namespace Microsoft.Boogie.ModelViewer
     ToolStripMenuItem[] viewItems;

     Model currentModel;

     Model[] allModels;

+    int modelId;

+    string modelFileName;

     internal ViewOptions viewOpts = new ViewOptions();

 

     // TODO this should be dynamically loaded

@@ -65,7 +67,6 @@ namespace Microsoft.Boogie.ModelViewer
         throw new Exception("error: usage:  ModelViewer.exe MyProgram.model[:N]");  // (where does this exception go?)

       }

 

-      var modelId = 0;

       {

         var idx = filename.IndexOf(':');

         if (idx > 0) {

@@ -74,10 +75,8 @@ namespace Microsoft.Boogie.ModelViewer
         }

       }

 

-      using (var rd = File.OpenText(filename)) {

-        allModels = Model.ParseModels(rd).ToArray();

-      }

-      currentModel = allModels[modelId];

+      modelFileName = filename;

+      ReadModels();

 

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

 

@@ -89,22 +88,44 @@ namespace Microsoft.Boogie.ModelViewer
         }

       }

 

-      AddModelMenu();

       LoadModel(modelId);

     }

 

+    private void ReadModels()

+    {

+      using (var rd = File.OpenText(modelFileName)) {

+        allModels = Model.ParseModels(rd).ToArray();

+      }

+      if (modelId >= allModels.Length)

+        modelId = 0;

+

+      currentModel = allModels[modelId];

+      AddModelMenu();      

+    }

+

     private void LoadModel(int idx)

     {

       var i = 0;

+      

+      //var stateIdx = stateList.SelectedIndices.Count == 0 ? 0 : stateList.SelectedIndices[0];

+

+      modelId = idx;

       foreach (ToolStripMenuItem it in modelsToolStripMenuItem.DropDownItems) {

         it.Checked = i++ == idx;

       }

       currentModel = allModels[idx];

       BuildModel();

+

+      /*

+      if (stateList.Items.Count <= stateIdx)

+        stateIdx = 0;

+      stateList.Items[stateIdx].Selected = true;      

+       */

     }

 

     private void AddModelMenu()

     {

+      modelsToolStripMenuItem.DropDownItems.Clear();

       var idx = 0;

       foreach (var m in allModels) {

         var currIdx = idx++; // this local needs to be in this block

@@ -149,7 +170,12 @@ namespace Microsoft.Boogie.ModelViewer
           if (mapping.TryGetValue(selectedSkel, out newIt)) break;

           selectedSkel = selectedSkel.parent;

         }

+        if (currentState >= stateList.Items.Count)

+          currentState = 0;

+        if (previousState >= stateList.Items.Count)

+          previousState = -1;

         if (newIt != null) GotoNode(newIt);

+        SyncStateListValues();

         UpdateMatches(true);

       }

     }

@@ -363,8 +389,6 @@ namespace Microsoft.Boogie.ModelViewer
 

       if (previousState >= 0)

         stateList.Items[previousState].ForeColor = regularStateBrush.Color;

-      stateList.Items[currentState].ForeColor = previousStateBrush.Color;

-      stateList.Items[sel].ForeColor = currentStateBrush.Color;

 

       SetState(sel);

     }

@@ -377,6 +401,11 @@ namespace Microsoft.Boogie.ModelViewer
 

     private void currentStateView_SelectedIndexChanged(object sender, EventArgs e)

     {

+      SyncStateListValues();

+    }

+

+    private void SyncStateListValues()

+    {

       var sel = SelectedNode();

       if (sel == null) return;

 

@@ -449,6 +478,10 @@ namespace Microsoft.Boogie.ModelViewer
           s.isMatch = newMatch;

         }

       }

+      

+      if (previousState >= 0)

+        stateList.Items[previousState].ForeColor = previousStateBrush.Color;

+      stateList.Items[currentState].ForeColor = currentStateBrush.Color;

 

       if (changed) {

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

@@ -582,6 +615,12 @@ namespace Microsoft.Boogie.ModelViewer
     {

       this.Close();

     }

+

+    private void reloadModelFileToolStripMenuItem_Click(object sender, EventArgs e)

+    {

+      ReadModels();

+      LoadModel(modelId);

+    }

   }

 

   internal class DisplayItem : ListViewItem