Allow for model selection if there are multiple in the file

2 files changed, 46 insertions, 5 deletions

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index 439c0875..94f2c341 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -55,6 +55,7 @@
       this.everythingToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.toolStripMenuItem1 = new System.Windows.Forms.ToolStripSeparator();

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

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

       this.stateViewMenu.SuspendLayout();

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

       this.splitContainer1.Panel1.SuspendLayout();

@@ -270,7 +271,8 @@
       // 

       this.menuStrip1.Items.AddRange(new System.Windows.Forms.ToolStripItem[] {

             this.fileToolStripMenuItem,

-            this.viewToolStripMenuItem});

+            this.viewToolStripMenuItem,

+            this.modelsToolStripMenuItem});

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

       this.menuStrip1.Name = "menuStrip1";

       this.menuStrip1.Size = new System.Drawing.Size(915, 24);

@@ -339,6 +341,12 @@
       this.debugToolStripMenuItem.Text = "Debug";

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

       // 

+      // modelsToolStripMenuItem

+      // 

+      this.modelsToolStripMenuItem.Name = "modelsToolStripMenuItem";

+      this.modelsToolStripMenuItem.Size = new System.Drawing.Size(58, 20);

+      this.modelsToolStripMenuItem.Text = "&Models";

+      // 

       // Main

       // 

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

@@ -394,6 +402,7 @@
     private System.Windows.Forms.ToolStripMenuItem everythingToolStripMenuItem;

     private System.Windows.Forms.ToolStripSeparator toolStripMenuItem1;

     private System.Windows.Forms.ToolStripMenuItem debugToolStripMenuItem;

+    private System.Windows.Forms.ToolStripMenuItem modelsToolStripMenuItem;

 

 

   }

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 3466cd25..28744ac8 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -24,6 +24,7 @@ namespace Microsoft.Boogie.ModelViewer
     internal ILanguageSpecificModel langModel;

     ToolStripMenuItem[] viewItems;

     Model currentModel;

+    Model[] allModels;

     internal ViewOptions viewOpts = new ViewOptions();

 

     // TODO this should be dynamically loaded

@@ -46,25 +47,36 @@ namespace Microsoft.Boogie.ModelViewer
 

       var debugBreak = false;

       string filename = null;

+

       var args = Environment.GetCommandLineArgs();

       for (int i = 1; i < args.Length; i++) {

         var arg = args[i];

-        if (arg == "/break")

+        if (arg == "/break" || arg == "-break")

           debugBreak = true;

         else

           filename = arg;

       }

+

       if (debugBreak) {

         System.Diagnostics.Debugger.Launch();

       }

       if (filename == null) {

-        throw new Exception("error: usage:  ModelViewer.exe MyProgram.model");  // (where does this exception go?)

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

+          modelId = int.Parse(filename.Substring(idx + 1));

+          filename = filename.Substring(0, idx);

+        }

       }

 

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

-        var models = Model.ParseModels(rd);

-        currentModel = models[0];

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

       }

+      currentModel = allModels[modelId];

 

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

 

@@ -76,9 +88,29 @@ namespace Microsoft.Boogie.ModelViewer
         }

       }

 

+      AddModelMenu();

+      LoadModel(modelId);

+    }

+

+    private void LoadModel(int idx)

+    {

+      var i = 0;

+      foreach (ToolStripMenuItem it in modelsToolStripMenuItem.DropDownItems) {

+        it.Checked = i++ == idx;

+      }

+      currentModel = allModels[idx];

       BuildModel();

     }

 

+    private void AddModelMenu()

+    {

+      var idx = 0;

+      foreach (var m in allModels) {

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

+        modelsToolStripMenuItem.DropDownItems.Add(string.Format("Model #{0}", currIdx), null, (s, a) => LoadModel(currIdx));

+      }

+    }

+

     private void BuildModel()

     {

       stateList.Items.Clear();