From 67fc54f87988135c316f5d3b4ef2d90b59ba2374 Mon Sep 17 00:00:00 2001 From: MichalMoskal Date: Sat, 6 Nov 2010 01:21:28 +0000 Subject: Improve the generic model viewer --- Source/Model/Model.cs | 9 ++++ Source/ModelViewer/BaseProvider.cs | 88 +++++++++++++++++++++++++++++-------- Source/ModelViewer/DataModel.cs | 8 ++++ Source/ModelViewer/Main.Designer.cs | 34 +++++++------- Source/ModelViewer/Namer.cs | 16 ++++--- 5 files changed, 114 insertions(+), 41 deletions(-) (limited to 'Source') 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 Variables { get { return vars; } } + public IEnumerable 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 states = new List(); 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 States { - return new ContainerNode(f.Name, a => new AppNode(this, a), f.Apps); + get { return states; } } + } - IEnumerable GetStateNodes(Model.CapturedState st) + public class BaseState : IState + { + internal GenericModel m; + Model.CapturedState st; + + internal List nodes = new List(); + internal Dictionary niceName = new Dictionary(); + + 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("[Functions]", f => f.Arity == 0 ? null : Function(f), m.Functions); - yield return new ContainerNode("[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("[Functions]", f => f.Arity == 0 ? null : Function(f), m.m.Functions)); + nodes.Add(new ContainerNode("[Constants]", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.m.Functions)); } - public override IEnumerable States + IDisplayNode Function(Model.Func f) { - get { - foreach (var s in m.States) - yield return new TopState(s.Name, GetStateNodes(s)); - } + return new ContainerNode(f.Name, a => new AppNode(this, a), f.Apps); + } + + public virtual string Name { get; set; } + + public virtual IEnumerable 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(" == ", 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 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(this Dictionary 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) -- cgit v1.2.3