diff options
author | 2010-11-09 01:31:30 +0000 | |
---|---|---|
committer | 2010-11-09 01:31:30 +0000 | |
commit | 48130b22b197754f03f27a1da1f1c70d47d65900 (patch) | |
tree | d2c570cac971014e6096ab51e14f2cde2d022cd2 /Source/ModelViewer/Main.cs | |
parent | ea1898f88e2edcecf3a58923fcd1a5d2b87219a8 (diff) |
Implement different levels of view (normal, expert, etc).
Display functions and pointer sets in VCC
Diffstat (limited to 'Source/ModelViewer/Main.cs')
-rw-r--r-- | Source/ModelViewer/Main.cs | 97 |
1 files changed, 81 insertions, 16 deletions
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 816043bd..5e1fc0ce 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -22,6 +22,9 @@ namespace Microsoft.Boogie.ModelViewer IState[] states;
internal ILanguageProvider langProvider;
internal ILanguageSpecificModel langModel;
+ ToolStripMenuItem[] viewItems;
+ Model currentModel;
+ internal ViewOptions viewOpts = new ViewOptions();
// TODO this should be dynamically loaded
IEnumerable<ILanguageProvider> Providers()
@@ -35,6 +38,12 @@ namespace Microsoft.Boogie.ModelViewer {
InitializeComponent();
+ viewItems = new ToolStripMenuItem[] {
+ normalToolStripMenuItem,
+ expertToolStripMenuItem,
+ everythingToolStripMenuItem
+ };
+
var debugBreak = false;
string filename = null;
var args = Environment.GetCommandLineArgs();
@@ -52,26 +61,36 @@ namespace Microsoft.Boogie.ModelViewer throw new Exception("error: usage: ModelViewer.exe MyProgram.model"); // (where does this exception go?)
}
- Model m;
-
using (var rd = File.OpenText(filename)) {
var models = Model.ParseModels(rd);
- m = models[0];
+ currentModel = models[0];
}
this.Text = Path.GetFileName(filename) + " - Boogie Verification Debugger";
langProvider = null;
foreach (var p in Providers()) {
- if (p.IsMyModel(m)) {
+ if (p.IsMyModel(currentModel)) {
langProvider = p;
break;
}
}
-
+
+ BuildModel();
+ }
+
+ private void BuildModel()
+ {
+ stateList.Items.Clear();
+
var items = new List<ListViewItem>();
- langModel = langProvider.GetLanguageSpecificModel(m);
+ langModel = langProvider.GetLanguageSpecificModel(currentModel, viewOpts);
states = langModel.States.ToArray();
+ var oldRoot = unfoldingRoot;
+ SkeletonItem selectedSkel = null;
+ if (oldRoot != null && SelectedNode() != null) {
+ selectedSkel = SelectedNode().skel;
+ }
unfoldingRoot = new SkeletonItem(this, states.Length);
allItems = unfoldingRoot.PopulateRoot(states);
@@ -84,9 +103,22 @@ namespace Microsoft.Boogie.ModelViewer }
stateList.Items.AddRange(items.ToArray());
unfoldingRoot.Expanded = true;
- SetState(0);
- stateList.Items[0].Selected = true;
- SetColumnSizes();
+
+ if (oldRoot == null) {
+ SetState(0);
+ stateList.Items[0].Selected = true;
+ SetColumnSizes();
+ } else {
+ var mapping = new Dictionary<SkeletonItem, SkeletonItem>();
+ unfoldingRoot.SyncWith(mapping, oldRoot);
+ SkeletonItem newIt = null;
+ while (selectedSkel != null) {
+ if (mapping.TryGetValue(selectedSkel, out newIt)) break;
+ selectedSkel = selectedSkel.parent;
+ }
+ if (newIt != null) GotoNode(newIt);
+ UpdateMatches(true);
+ }
}
private void SetColumnSizes()
@@ -283,7 +315,6 @@ namespace Microsoft.Boogie.ModelViewer private void stateList_SelectedIndexChanged(object sender, EventArgs e)
{
-
if (stateList.SelectedItems.Count == 0) return;
var sel = stateList.SelectedItems[0].Index;
@@ -295,10 +326,16 @@ namespace Microsoft.Boogie.ModelViewer SetState(sel);
}
+ DisplayItem SelectedNode()
+ {
+ if (currentStateView.SelectedItems.Count == 0) return null;
+ return (DisplayItem)currentStateView.SelectedItems[0];
+ }
+
private void currentStateView_SelectedIndexChanged(object sender, EventArgs e)
{
- if (currentStateView.SelectedItems.Count == 0) return;
- var sel = (DisplayItem) currentStateView.SelectedItems[0];
+ var sel = SelectedNode();
+ if (sel == null) return;
stateList.BeginUpdate();
for (int i = 0; i < sel.skel.displayNodes.Length; ++i) {
@@ -443,10 +480,9 @@ namespace Microsoft.Boogie.ModelViewer {
IDisplayNode sel = null;
SkeletonItem skel = null;
- if (currentStateView.SelectedItems.Count > 0) {
- var it = currentStateView.SelectedItems[0];
- sel = ((DisplayItem)it).dispNode;
- skel = ((DisplayItem)it).skel;
+ if (SelectedNode() != null) {
+ sel = SelectedNode().dispNode;
+ skel = SelectedNode().skel;
}
var items = stateViewMenu.Items;
@@ -472,6 +508,35 @@ namespace Microsoft.Boogie.ModelViewer AddMenuItems(aliases, items, " = ", 10);
}
}
+
+ private void normalToolStripMenuItem_Click(object sender, EventArgs e)
+ {
+ int viewLev = -1;
+ for (int i = 0; i < viewItems.Length; ++i) {
+ if (viewItems[i] == sender) {
+ viewLev = i;
+ viewItems[i].Checked = true;
+ } else {
+ viewItems[i].Checked = false;
+ }
+ }
+ if (viewLev != -1 && viewLev != viewOpts.ViewLevel) {
+ viewOpts.ViewLevel = viewLev;
+ BuildModel();
+ }
+ }
+
+ private void debugToolStripMenuItem_Click(object sender, EventArgs e)
+ {
+ debugToolStripMenuItem.Checked = !debugToolStripMenuItem.Checked;
+ viewOpts.DebugMode = debugToolStripMenuItem.Checked;
+ BuildModel();
+ }
+
+ private void exitToolStripMenuItem_Click(object sender, EventArgs e)
+ {
+ this.Close();
+ }
}
internal class DisplayItem : ListViewItem
|