diff options
author | 2010-12-15 01:16:29 +0000 | |
---|---|---|
committer | 2010-12-15 01:16:29 +0000 | |
commit | e6f64bf4fb00f1bde7b73b8db3761be27ac8c6b9 (patch) | |
tree | 8afc1ff63d4e6fd824e00168b73efb63f71875b9 /Source/ModelViewer/Main.cs | |
parent | 801701bd08f75c4e61c9d3d7004426a4821a25bf (diff) |
Add reload-model option. Bugfixes when switching models
Diffstat (limited to 'Source/ModelViewer/Main.cs')
-rw-r--r-- | Source/ModelViewer/Main.cs | 55 |
1 files changed, 47 insertions, 8 deletions
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
|