blob: 766768e26058dcc2763bdda60e083ed74098f0b5 (
plain)
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
|
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;
}
IEnumerable<IDisplayNode> GetStateNodes(Model m)
{
yield return GenericNodes.Functions(m);
yield return GenericNodes.Constants(m);
foreach (var s in m.States)
yield return new StateNode(s);
}
public IEnumerable<IState> GetStates(Model m)
{
yield return new TopState("TOP", GetStateNodes(m));
}
}
public class StateNode : DisplayNode
{
protected Model.CapturedState state;
public StateNode(Model.CapturedState s) : base(s.Name)
{
state = s;
}
public override IEnumerable<string> Values
{
get { foreach (var v in state.Variables) yield return v; }
}
public override bool Expandable { get { return state.VariableCount != 0; } }
public override IEnumerable<IDisplayNode> Expand()
{
foreach (var v in state.Variables) {
yield return new ElementNode(v, state.TryGet(v));
}
}
}
public class ElementNode : DisplayNode
{
protected Model.Element elt;
public ElementNode(string name, Model.Element elt) : base(name)
{
this.elt = elt;
}
public override IEnumerable<string> Values
{
get
{
if (!(elt is Model.Uninterpreted))
yield return elt.ToString();
foreach (var tupl in elt.Names) {
if (tupl.Func.Arity == 0)
yield return tupl.Func.Name;
}
}
}
}
public static class GenericNodes
{
public static IDisplayNode Function(Model.Func f)
{
return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(a), f.Apps);
}
public static IDisplayNode Functions(Model m)
{
return new ContainerNode<Model.Func>("Functions", f => f.Arity == 0 ? null : Function(f), m.Functions);
}
public static IDisplayNode Constants(Model m)
{
return new ContainerNode<Model.Func>("Constants", f => f.Arity != 0 ? null : new AppNode(f.Apps.First()), m.Functions);
}
}
public class AppNode : ElementNode
{
protected Model.FuncTuple tupl;
public AppNode(Model.FuncTuple t)
: base(t.Func.Name, t.Result)
{
tupl = t;
var sb = new StringBuilder();
sb.Append(t.Func.Name);
if (t.Args.Length > 0) {
sb.Append("(");
foreach (var a in t.Args)
sb.Append(a.ToString()).Append(", ");
sb.Length -= 2;
sb.Append(")");
}
name = sb.ToString();
}
}
}
|
