diff options
author | 2010-11-06 01:21:28 +0000 | |
---|---|---|
committer | 2010-11-06 01:21:28 +0000 | |
commit | 67fc54f87988135c316f5d3b4ef2d90b59ba2374 (patch) | |
tree | 8192f94232602000ec4947fda35d3d1f67704add /Source | |
parent | 34e5dd6c2177a83159982aca6c025ef95474689c (diff) |
Improve the generic model viewer
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Model/Model.cs | 9 | ||||
-rw-r--r-- | Source/ModelViewer/BaseProvider.cs | 88 | ||||
-rw-r--r-- | Source/ModelViewer/DataModel.cs | 8 | ||||
-rw-r--r-- | Source/ModelViewer/Main.Designer.cs | 34 | ||||
-rw-r--r-- | Source/ModelViewer/Namer.cs | 16 |
5 files changed, 114 insertions, 41 deletions
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 3d1df65e..0fe86f81 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -5,6 +5,7 @@ //-----------------------------------------------------------------------------
using System;
+using System.Linq;
using System.Collections.Generic;
namespace Microsoft.Boogie
@@ -303,6 +304,14 @@ namespace Microsoft.Boogie public readonly string Name;
public IEnumerable<string> Variables { get { return vars; } }
+ public IEnumerable<string> AllVariables {
+ get {
+ if (previous != null)
+ return previous.AllVariables.Concat(Variables).Distinct();
+ else
+ return Variables;
+ }
+ }
public int VariableCount { get { return vars.Count; } }
public bool HasBinding(string varname)
{
diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs index cf5f9909..dddc8c30 100644 --- a/Source/ModelViewer/BaseProvider.cs +++ b/Source/ModelViewer/BaseProvider.cs @@ -23,44 +23,91 @@ namespace Microsoft.Boogie.ModelViewer.Base public class GenericModel : LanguageModel
{
- Model m;
+ internal Model m;
+ List<BaseState> states = new List<BaseState>();
public GenericModel(Model m)
{
this.m = m;
+ foreach (var s in m.States)
+ states.Add(new BaseState(this, s) { Name = s.Name });
+ foreach (var s in states)
+ this.Flush(s.nodes);
}
- public IDisplayNode Function(Model.Func f)
+ public override IEnumerable<IState> States
{
- return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(this, a), f.Apps);
+ get { return states; }
}
+ }
- IEnumerable<IDisplayNode> GetStateNodes(Model.CapturedState st)
+ public class BaseState : IState
+ {
+ internal GenericModel m;
+ Model.CapturedState st;
+
+ internal List<IDisplayNode> nodes = new List<IDisplayNode>();
+ internal Dictionary<Model.Element, string> niceName = new Dictionary<Model.Element, string>();
+
+ public BaseState(GenericModel m, Model.CapturedState st)
{
- foreach (var v in st.Variables)
- yield return new ElementNode(this, v, st.TryGet(v));
- yield return new ContainerNode<Model.Func>("[Functions]", f => f.Arity == 0 ? null : Function(f), m.Functions);
- yield return new ContainerNode<Model.Func>("[Constants]", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.Functions);
+ this.st = st;
+ this.m = m;
+
+ foreach (var v in st.AllVariables) {
+ var e = st.TryGet(v);
+ m.RegisterLocalValue(v, e);
+ nodes.Add(new ElementNode(this, v, e));
+
+ niceName[e] = v;
+ foreach (var r in e.References) {
+ if (r.Args.Length == 1 && r.Args[0] == e) {
+ if (!niceName.ContainsKey(e))
+ niceName[e] = r.Func.Name + "(" + v + ")";
+ }
+ }
+ }
+
+ nodes.Add(new ContainerNode<Model.Func>("[Functions]", f => f.Arity == 0 ? null : Function(f), m.m.Functions));
+ nodes.Add(new ContainerNode<Model.Func>("[Constants]", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.m.Functions));
}
- public override IEnumerable<IState> States
+ IDisplayNode Function(Model.Func f)
{
- get {
- foreach (var s in m.States)
- yield return new TopState(s.Name, GetStateNodes(s));
- }
+ return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(this, a), f.Apps);
+ }
+
+ public virtual string Name { get; set; }
+
+ public virtual IEnumerable<IDisplayNode> Nodes
+ {
+ get { return nodes; }
}
}
+
public class ElementNode : DisplayNode
{
- public ElementNode(ILanguageSpecificModel p, string name, Model.Element elt) : base(p, name, elt) {}
+ BaseState st;
+
+ public ElementNode(BaseState st, string name, Model.Element elt) : base(st.m, name, elt) { this.st = st; }
+
+ protected override void ComputeChildren()
+ {
+ children.Add(new ContainerNode<Model.FuncTuple>(" == ", e => new AppNode(st, e), Element.References.Where(t => t.Result == Element)));
+ foreach (var e in Element.References) {
+ if (e.Args.Contains(Element))
+ children.Add(new AppNode(st, e, x => x == Element ? "*" : st.niceName.GetWithDefault(x, null)));
+ }
+ }
}
public class AppNode : ElementNode
{
protected Model.FuncTuple tupl;
- public AppNode(ILanguageSpecificModel m, Model.FuncTuple t)
+ public AppNode(BaseState m, Model.FuncTuple t) : this(m, t, _ => null) { }
+
+ public AppNode(BaseState m, Model.FuncTuple t, Func<Model.Element, string> nameElement)
: base(m, t.Func.Name, t.Result)
{
tupl = t;
@@ -68,12 +115,17 @@ namespace Microsoft.Boogie.ModelViewer.Base sb.Append(t.Func.Name);
if (t.Args.Length > 0) {
sb.Append("(");
- foreach (var a in t.Args)
- sb.Append(a.ToString()).Append(", ");
+ for (int i = 0; i < t.Args.Length; ++i) {
+ var n = nameElement(t.Args[i]);
+ if (n == null)
+ sb.AppendFormat("%{0}, ", i);
+ else
+ sb.AppendFormat("{0}, ", n);
+ }
sb.Length -= 2;
sb.Append(")");
}
- name = new EdgeName(sb.ToString());
+ name = new EdgeName(m.m, sb.ToString(), t.Args);
}
}
diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs index 33211ef3..d83dfdd5 100644 --- a/Source/ModelViewer/DataModel.cs +++ b/Source/ModelViewer/DataModel.cs @@ -223,6 +223,14 @@ namespace Microsoft.Boogie.ModelViewer if (a != null) return a;
return b;
}
+
+ public static S GetWithDefault<T, S>(this Dictionary<T, S> dict, T key, S defl)
+ {
+ S r;
+ if (dict.TryGetValue(key, out r))
+ return r;
+ return defl;
+ }
}
}
diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs index 4fe8662f..9932a550 100644 --- a/Source/ModelViewer/Main.Designer.cs +++ b/Source/ModelViewer/Main.Designer.cs @@ -31,7 +31,7 @@ this.currentStateView = new System.Windows.Forms.ListView();
this.name = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));
this.value = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));
- this.aliases = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));
+ this.prevValue = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));
this.stateViewMenu = new System.Windows.Forms.ContextMenuStrip(this.components);
this.dummyItemToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();
this.splitContainer1 = new System.Windows.Forms.SplitContainer();
@@ -63,7 +63,7 @@ this.currentStateView.Columns.AddRange(new System.Windows.Forms.ColumnHeader[] {
this.name,
this.value,
- this.aliases});
+ this.prevValue});
this.currentStateView.ContextMenuStrip = this.stateViewMenu;
this.currentStateView.Dock = System.Windows.Forms.DockStyle.Fill;
this.currentStateView.FullRowSelect = true;
@@ -74,7 +74,7 @@ this.currentStateView.Name = "currentStateView";
this.currentStateView.OwnerDraw = true;
this.currentStateView.ShowItemToolTips = true;
- this.currentStateView.Size = new System.Drawing.Size(761, 612);
+ this.currentStateView.Size = new System.Drawing.Size(677, 558);
this.currentStateView.TabIndex = 0;
this.currentStateView.UseCompatibleStateImageBehavior = false;
this.currentStateView.View = System.Windows.Forms.View.Details;
@@ -95,10 +95,10 @@ this.value.Text = "Value";
this.value.Width = 99;
//
- // aliases
+ // prevValue
//
- this.aliases.Text = "Aliases";
- this.aliases.Width = 325;
+ this.prevValue.Text = "Previous";
+ this.prevValue.Width = 147;
//
// stateViewMenu
//
@@ -111,7 +111,7 @@ // dummyItemToolStripMenuItem
//
this.dummyItemToolStripMenuItem.Name = "dummyItemToolStripMenuItem";
- this.dummyItemToolStripMenuItem.Size = new System.Drawing.Size(119, 22);
+ this.dummyItemToolStripMenuItem.Size = new System.Drawing.Size(144, 22);
this.dummyItemToolStripMenuItem.Text = "Dummy item";
//
// splitContainer1
@@ -127,8 +127,8 @@ // splitContainer1.Panel2
//
this.splitContainer1.Panel2.Controls.Add(this.stateList);
- this.splitContainer1.Size = new System.Drawing.Size(1028, 796);
- this.splitContainer1.SplitterDistance = 761;
+ this.splitContainer1.Size = new System.Drawing.Size(915, 726);
+ this.splitContainer1.SplitterDistance = 677;
this.splitContainer1.TabIndex = 1;
//
// splitContainer2
@@ -148,8 +148,8 @@ this.splitContainer2.Panel2.Controls.Add(this.linkLabel1);
this.splitContainer2.Panel2.Controls.Add(this.label1);
this.splitContainer2.Panel2.Controls.Add(this.textBox1);
- this.splitContainer2.Size = new System.Drawing.Size(761, 796);
- this.splitContainer2.SplitterDistance = 612;
+ this.splitContainer2.Size = new System.Drawing.Size(677, 726);
+ this.splitContainer2.SplitterDistance = 558;
this.splitContainer2.TabIndex = 1;
//
// matchesList
@@ -168,7 +168,7 @@ this.matchesList.Name = "matchesList";
this.matchesList.OwnerDraw = true;
this.matchesList.ShowItemToolTips = true;
- this.matchesList.Size = new System.Drawing.Size(761, 151);
+ this.matchesList.Size = new System.Drawing.Size(677, 135);
this.matchesList.TabIndex = 4;
this.matchesList.UseCompatibleStateImageBehavior = false;
this.matchesList.View = System.Windows.Forms.View.Details;
@@ -192,7 +192,7 @@ //
this.linkLabel1.Anchor = ((System.Windows.Forms.AnchorStyles)((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Right)));
this.linkLabel1.AutoSize = true;
- this.linkLabel1.Location = new System.Drawing.Point(701, 5);
+ this.linkLabel1.Location = new System.Drawing.Point(617, 5);
this.linkLabel1.Name = "linkLabel1";
this.linkLabel1.Size = new System.Drawing.Size(57, 13);
this.linkLabel1.TabIndex = 3;
@@ -217,7 +217,7 @@ | System.Windows.Forms.AnchorStyles.Right)));
this.textBox1.Location = new System.Drawing.Point(53, 3);
this.textBox1.Name = "textBox1";
- this.textBox1.Size = new System.Drawing.Size(642, 20);
+ this.textBox1.Size = new System.Drawing.Size(558, 20);
this.textBox1.TabIndex = 1;
this.textBox1.TextChanged += new System.EventHandler(this.textBox1_TextChanged);
//
@@ -236,7 +236,7 @@ this.stateList.MultiSelect = false;
this.stateList.Name = "stateList";
this.stateList.ShowItemToolTips = true;
- this.stateList.Size = new System.Drawing.Size(263, 796);
+ this.stateList.Size = new System.Drawing.Size(234, 726);
this.stateList.TabIndex = 0;
this.stateList.UseCompatibleStateImageBehavior = false;
this.stateList.View = System.Windows.Forms.View.Details;
@@ -261,7 +261,7 @@ //
this.AutoScaleDimensions = new System.Drawing.SizeF(6F, 13F);
this.AutoScaleMode = System.Windows.Forms.AutoScaleMode.Font;
- this.ClientSize = new System.Drawing.Size(1028, 796);
+ this.ClientSize = new System.Drawing.Size(915, 726);
this.Controls.Add(this.splitContainer1);
this.Name = "Main";
this.Text = "Boogie Verification Debugger";
@@ -289,7 +289,7 @@ private System.Windows.Forms.ColumnHeader columnHeader1;
private System.Windows.Forms.ColumnHeader columnHeader2;
private System.Windows.Forms.ColumnHeader columnHeader3;
- private System.Windows.Forms.ColumnHeader aliases;
+ private System.Windows.Forms.ColumnHeader prevValue;
private System.Windows.Forms.SplitContainer splitContainer2;
private System.Windows.Forms.ListView matchesList;
private System.Windows.Forms.ColumnHeader columnHeader4;
diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs index 8c36de3c..e77b0178 100644 --- a/Source/ModelViewer/Namer.cs +++ b/Source/ModelViewer/Namer.cs @@ -116,11 +116,15 @@ namespace Microsoft.Boogie.ModelViewer }
}
#region field name sorting
- static bool HasAny(string s, string chrs)
+ static bool HasSpecialChars(string s)
{
- foreach (var c in s)
- if (chrs.Contains(c))
- return true;
+ for (int i = 0; i < s.Length; ++i)
+ switch (s[i]) {
+ case '[':
+ case '<':
+ case '>':
+ case ']': return true;
+ }
return false;
}
@@ -137,8 +141,8 @@ namespace Microsoft.Boogie.ModelViewer public virtual int CompareFields(string f1, string f2)
{
- bool s1 = HasAny(f1, "[<>]");
- bool s2 = HasAny(f2, "[<>]");
+ bool s1 = HasSpecialChars(f1);
+ bool s2 = HasSpecialChars(f2);
if (s1 && !s2)
return 1;
if (!s1 && s2)
|