1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
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)
{
return new GenericModel(m);
}
}
public class GenericModel : LanguageModel
{
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 override IEnumerable<IState> States
{
get { return states; }
}
}
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)
{
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));
}
IDisplayNode Function(Model.Func f)
{
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
{
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(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;
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);
}
}
}
|
