ModelViewer:

* map back values introduced by bool_2_U and int_2_U
* map back internal names for select/store to [n] and [n:=], where n is the arity of the map
* added /break switch to ModelViewer
* display more things (including sequences) in Dafny provider

1 files changed, 17 insertions, 2 deletions

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index dbb91390..08869c17 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -32,11 +32,26 @@ namespace Microsoft.Boogie.ModelViewer
     {

       InitializeComponent();

 

-

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

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

+      }

+

       Model m;

 

-      using (var rd = File.OpenText(args[1])) {

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

         var models = Model.ParseModels(rd);

         m = models[0];

       }