From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/ModelViewer/BaseProvider.cs | 272 ++++++++++++++++++------------------- 1 file changed, 136 insertions(+), 136 deletions(-) (limited to 'Source/ModelViewer/BaseProvider.cs') diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs index 1e9e9cf9..8797fe1f 100644 --- a/Source/ModelViewer/BaseProvider.cs +++ b/Source/ModelViewer/BaseProvider.cs @@ -1,136 +1,136 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; - -namespace Microsoft.Boogie.ModelViewer.Base -{ - public class Provider : ILanguageProvider - { - public static Provider Instance = new Provider(); - private Provider() { } - - public bool IsMyModel(Model m) - { - return true; - } - - public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts) - { - return new GenericModel(m, opts); - } - } - - public class GenericModel : LanguageModel - { - List states = new List(); - - public GenericModel(Model m, ViewOptions opts) - : base(m, opts) - { - 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 override IEnumerable States - { - get { return states; } - } - } - - 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) - { - 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.model.Functions)); - nodes.Add(new ContainerNode("[Constants]", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.model.Functions)); - } - - public virtual SourceViewState ShowSource() - { - return null; - } - - IDisplayNode Function(Model.Func f) - { - 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 - { - 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(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; - var sb = new StringBuilder(); - sb.Append(t.Func.Name); - if (t.Args.Length > 0) { - sb.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(m.m, sb.ToString(), t.Args); - } - } - -} +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; + +namespace Microsoft.Boogie.ModelViewer.Base +{ + public class Provider : ILanguageProvider + { + public static Provider Instance = new Provider(); + private Provider() { } + + public bool IsMyModel(Model m) + { + return true; + } + + public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts) + { + return new GenericModel(m, opts); + } + } + + public class GenericModel : LanguageModel + { + List states = new List(); + + public GenericModel(Model m, ViewOptions opts) + : base(m, opts) + { + 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 override IEnumerable States + { + get { return states; } + } + } + + 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) + { + 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.model.Functions)); + nodes.Add(new ContainerNode("[Constants]", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.model.Functions)); + } + + public virtual SourceViewState ShowSource() + { + return null; + } + + IDisplayNode Function(Model.Func f) + { + 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 + { + 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(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; + var sb = new StringBuilder(); + sb.Append(t.Func.Name); + if (t.Args.Length > 0) { + sb.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(m.m, sb.ToString(), t.Args); + } + } + +} -- cgit v1.2.3