Make it possible to look up variables in the Dafny error models.

3 files changed, 36 insertions, 36 deletions

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index c233d272..c2d786fc 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -29,7 +29,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     }

   }

 

-  class DafnyModel : LanguageModel

+  public class DafnyModel : LanguageModel

   {

     public readonly Model.Func f_heap_select, f_set_select, f_seq_length, f_seq_index, f_box, f_dim, f_index_field, f_multi_index_field, f_dtype, f_null;

     public readonly Dictionary<Model.Element, Model.Element[]> ArrayLengths = new Dictionary<Model.Element, Model.Element[]>();

@@ -265,10 +265,10 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     }

   }

 

-  class StateNode : NamedState

+  public class StateNode : NamedState

   {

     internal readonly DafnyModel dm;

-    internal readonly List<VariableNode> vars = new List<VariableNode>();

+    public readonly List<VariableNode> Vars = new List<VariableNode>();

     internal readonly List<VariableNode> skolems;

     internal readonly int index;

     

@@ -289,7 +289,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
 

       if (dm.states.Count > 0) {

         var prev = dm.states.Last();

-        names = prev.vars.Map(v => v.realName);

+        names = prev.Vars.Map(v => v.realName);

       }

 

       names = names.Concat(state.Variables).Distinct();

@@ -302,7 +302,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
           vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v);

           if (curVars.ContainsKey(v))

             dm.RegisterLocalValue(vn.Name, val);

-          vars.Add(vn);

+          Vars.Add(vn);

         }

       }

 

@@ -323,12 +323,12 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     public override IEnumerable<IDisplayNode> Nodes

     {

       get {

-        return vars.Concat(skolems);

+        return Vars.Concat(skolems);

       }

     }

   }

 

-  class ElementNode : DisplayNode

+  public class ElementNode : DisplayNode

   {

     protected StateNode stateNode;

     protected Model.Element elt;

@@ -371,7 +371,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     }

   }

 

-  class VariableNode : ElementNode

+  public class VariableNode : ElementNode

   {

     public bool updatedHere;

     public string realName;

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 41f43621..fde1971b 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -18,10 +18,10 @@ namespace Microsoft.Boogie.ModelViewer
   {

     SkeletonItem unfoldingRoot;

     SkeletonItem[] allItems;

-    int currentState, previousState = -1;

+    public int CurrentState, PreviousState = -1;

     IState[] states;

     internal ILanguageProvider langProvider;

-    internal ILanguageSpecificModel langModel;

+    public ILanguageSpecificModel LangModel;

     ToolStripMenuItem[] viewItems;

     Model currentModel;

     Model[] allModels;

@@ -183,8 +183,8 @@ namespace Microsoft.Boogie.ModelViewer
       stateList.Items.Clear();

 

       var items = new List<ListViewItem>();

-      langModel = langProvider.GetLanguageSpecificModel(currentModel, viewOpts);

-      states = langModel.States.ToArray();

+      LangModel = langProvider.GetLanguageSpecificModel(currentModel, viewOpts);

+      states = LangModel.States.ToArray();

       var oldRoot = unfoldingRoot;

       SkeletonItem selectedSkel = null;

       if (oldRoot != null && SelectedNode() != null) {

@@ -215,10 +215,10 @@ 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 (CurrentState >= stateList.Items.Count)

+          CurrentState = 0;

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

+          PreviousState = -1;

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

         SyncStateListValues();

         UpdateMatches(true);

@@ -238,9 +238,9 @@ namespace Microsoft.Boogie.ModelViewer
         stateList.SelectedIndices.Clear();

         stateList.SelectedIndices.Add(id);

       }

-      if (currentState != id) {

-        previousState = currentState;

-        currentState = id;

+      if (CurrentState != id) {

+        PreviousState = CurrentState;

+        CurrentState = id;

       }

       UpdateMatches(true);

     }

@@ -308,7 +308,7 @@ namespace Microsoft.Boogie.ModelViewer
         textBrush = Brushes.White;

       } else {

         var bg = Brushes.White;

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

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

           bg = nonPrimary;

         if (item.skel.isMatch)

           bg = matchBg;

@@ -426,7 +426,7 @@ namespace Microsoft.Boogie.ModelViewer
       for (int i = 0; i < ch.Length; ++i) {

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

         cb(di, ch[i]);

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

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

       }

       listView.EndUpdate();

       listView.Invalidate();

@@ -448,8 +448,8 @@ namespace Microsoft.Boogie.ModelViewer
       if (stateList.SelectedItems.Count == 0) return;

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

 

-      if (previousState >= 0)

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

+      if (PreviousState >= 0)

+        stateList.Items[PreviousState].ForeColor = regularStateBrush.Color;

 

       SetState(sel);

     }

@@ -504,11 +504,11 @@ namespace Microsoft.Boogie.ModelViewer
         if (w.StartsWith("eq:")) {

           if (eltEq != null) bad = true;

           else {

-            eltEq = langModel.FindElement(w.Substring(3));

+            eltEq = LangModel.FindElement(w.Substring(3));

             if (eltEq == null) bad = true;

           }

         } else if (w.StartsWith("use:")) {

-          var e = langModel.FindElement(w.Substring(4));

+          var e = LangModel.FindElement(w.Substring(4));

           if (e == null) bad = true;

           else eltRef.Add(e);

         } else {

@@ -529,8 +529,8 @@ namespace Microsoft.Boogie.ModelViewer
 

       foreach (var s in allItems) {

         var newMatch = false;

-        if (s.isPrimary[currentState] && !bad) {

-          newMatch = s.MatchesWords(wordsA, refsA, eltEq, currentState);

+        if (s.isPrimary[CurrentState] && !bad) {

+          newMatch = s.MatchesWords(wordsA, refsA, eltEq, CurrentState);

         }

         if (newMatch)

           matches.Add(s);

@@ -540,9 +540,9 @@ namespace Microsoft.Boogie.ModelViewer
         }

       }

 

-      if (previousState >= 0)

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

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

+      if (PreviousState >= 0)

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

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

 

       if (changed) {

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

@@ -594,7 +594,7 @@ namespace Microsoft.Boogie.ModelViewer
       var elts = new Model.Element[0];

 

       foreach (var s in allItems) {

-        if (s.isPrimary[currentState] && s.MatchesWords(words, elts, elt, currentState)) {

+        if (s.isPrimary[CurrentState] && s.MatchesWords(words, elts, elt, CurrentState)) {

           yield return s;

         }

       }

@@ -606,7 +606,7 @@ namespace Microsoft.Boogie.ModelViewer
 

       foreach (var s in skelsM) {

         var tmp = s;

-        items.Add(pref + s.LongName(currentState), null, (x, _) => GotoNode(tmp));

+        items.Add(pref + s.LongName(CurrentState), null, (x, _) => GotoNode(tmp));

       }

 

       if (skelsM.Length == max)

@@ -631,13 +631,13 @@ namespace Microsoft.Boogie.ModelViewer
       }

 

       foreach (var x in sel.References.Where(q => q != sel.Element)) {

-        var t = new ToolStripMenuItem(langModel.CanonicalName(x));

+        var t = new ToolStripMenuItem(LangModel.CanonicalName(x));

         items.Add(t);

         AddMenuItems(NamesFor(x), t.DropDownItems, "= ", 20);

       }

 

       if (sel.Element != null) {

-        var selName = langModel.CanonicalName(sel.Element);

+        var selName = LangModel.CanonicalName(sel.Element);

         items.Add("Find uses...", null, (s, _) => SetSearch("use:" + selName));

 

         var aliases = NamesFor(sel.Element).Where(s => s != skel).ToArray();

diff --git a/Source/ModelViewer/TreeSkeleton.cs b/Source/ModelViewer/TreeSkeleton.cs
index e1bc678a..543788a8 100644
--- a/Source/ModelViewer/TreeSkeleton.cs
+++ b/Source/ModelViewer/TreeSkeleton.cs
@@ -149,7 +149,7 @@ namespace Microsoft.Boogie.ModelViewer
         }

       }

 

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

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

         children.Add(created[name]);

       }

     }

@@ -186,7 +186,7 @@ namespace Microsoft.Boogie.ModelViewer
           parents.Add(curr.displayNodes[stateId]);

       }

       parents.Reverse();

-      return main.langModel.PathName(parents);

+      return main.LangModel.PathName(parents);

     }

 

     public void SyncWith(Dictionary<SkeletonItem, SkeletonItem> mapping, SkeletonItem old)