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
|
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
{
Model m;
public GenericModel(Model m)
{
this.m = m;
}
public IDisplayNode Function(Model.Func f)
{
return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(this, a), f.Apps);
}
IEnumerable<IDisplayNode> GetStateNodes(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);
}
public override IEnumerable<IState> States
{
get {
foreach (var s in m.States)
yield return new TopState(s.Name, GetStateNodes(s));
}
}
}
public class ElementNode : DisplayNode
{
public ElementNode(ILanguageSpecificModel p, string name, Model.Element elt) : base(p, name, elt) {}
}
public class AppNode : ElementNode
{
protected Model.FuncTuple tupl;
public AppNode(ILanguageSpecificModel m, Model.FuncTuple t)
: 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("(");
foreach (var a in t.Args)
sb.Append(a.ToString()).Append(", ");
sb.Length -= 2;
sb.Append(")");
}
name = new EdgeName(sb.ToString());
}
}
}
|
