summaryrefslogtreecommitdiff
path: root/Source/ModelViewer/DafnyProvider.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/ModelViewer/DafnyProvider.cs')
-rw-r--r--Source/ModelViewer/DafnyProvider.cs776
1 files changed, 388 insertions, 388 deletions
diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index 602df7aa..45c7dada 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -1,388 +1,388 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Text.RegularExpressions;
-using System.Diagnostics.Contracts;
-
-namespace Microsoft.Boogie.ModelViewer.Dafny
-{
- public class Provider : ILanguageProvider
- {
- public static Provider Instance = new Provider();
- private Provider() { }
-
- public bool IsMyModel(Model m)
- {
- return m.TryGetFunc("$$Language$Dafny") != null;
- }
-
- public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts)
- {
- var dm = new DafnyModel(m, opts);
- foreach (var s in m.States) {
- var sn = new StateNode(dm.states.Count, dm, s);
- dm.states.Add(sn);
- }
- dm.FinishStates();
- return dm;
- }
- }
-
- public class DafnyModel : LanguageModel
- {
- public readonly Model.Func f_heap_select, f_set_select, f_seq_length, f_seq_index, f_box, f_dim, f_index_field, f_multi_index_field, f_dtype, f_null;
- public readonly Dictionary<Model.Element, Model.Element[]> ArrayLengths = new Dictionary<Model.Element, Model.Element[]>();
- public readonly Dictionary<Model.Element, Model.FuncTuple> DatatypeValues = new Dictionary<Model.Element, Model.FuncTuple>();
- Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();
- public List<StateNode> states = new List<StateNode>();
-
- public DafnyModel(Model m, ViewOptions opts)
- : base(m, opts)
- {
- f_heap_select = m.MkFunc("[3]", 3);
- f_set_select = m.MkFunc("[2]", 2);
- f_seq_length = m.MkFunc("Seq#Length", 1);
- f_seq_index = m.MkFunc("Seq#Index", 2);
- f_box = m.MkFunc("$Box", 1);
- f_dim = m.MkFunc("FDim", 1);
- f_index_field = m.MkFunc("IndexField", 1);
- f_multi_index_field = m.MkFunc("MultiIndexField", 2);
- f_dtype = m.MkFunc("dtype", 1);
- f_null = m.MkFunc("null", 0);
-
- // collect the array dimensions from the various array.Length functions, and
- // collect all known datatype values
- foreach (var fn in m.Functions) {
- if (Regex.IsMatch(fn.Name, "^_System.array[0-9]*.Length[0-9]*$")) {
- int j = fn.Name.IndexOf('.', 13);
- int dims = j == 13 ? 1 : int.Parse(fn.Name.Substring(13, j - 13));
- int idx = j == 13 ? 0 : int.Parse(fn.Name.Substring(j + 7));
- foreach (var tpl in fn.Apps) {
- var elt = tpl.Args[0];
- var len = tpl.Result;
- Model.Element[] ar;
- if (!ArrayLengths.TryGetValue(elt, out ar)) {
- ar = new Model.Element[dims];
- ArrayLengths.Add(elt, ar);
- }
- Contract.Assert(ar[idx] == null);
- ar[idx] = len;
- }
- } else if (fn.Name.StartsWith("#") && fn.Name.IndexOf('.') != -1 && fn.Name[1] != '#') {
- foreach (var tpl in fn.Apps) {
- var elt = tpl.Result;
- DatatypeValues.Add(elt, tpl);
- }
- }
- }
- }
-
- internal void FinishStates()
- {
- GenerateSourceLocations(states);
- }
-
- public override IEnumerable<IState> States
- {
- get { return states; }
- }
-
- public string GetUserVariableName(string name)
- {
- if (name.StartsWith("$")) // this covers $Heap and $_Frame and $nw...
- return null;
- if (name.Contains("##")) // a temporary variable of the translation
- return null;
-#if SOMETIME_AGAIN
- var hash = name.IndexOf('#');
- if (0 < hash)
- return name.Substring(0, hash);
-#endif
- return name;
- }
-
- public Model.Element Image(Model.Element elt, Model.Func f)
- {
- var r = f.AppWithResult(elt);
- if (r != null)
- return r.Args[0];
- return null;
- }
-
- protected override string CanonicalBaseName(Model.Element elt, out NameSeqSuffix suff)
- {
- Model.FuncTuple fnTuple;
- suff = NameSeqSuffix.WhenNonZero;
- if (DatatypeValues.TryGetValue(elt, out fnTuple)) {
- // elt is s a datatype value, make its name be the name of the datatype constructor
- string nm = fnTuple.Func.Name;
- if (fnTuple.Func.Arity == 0)
- return nm;
- else
- return nm + "(...)";
- }
- var seqLen = f_seq_length.AppWithArg(0, elt);
- if (seqLen != null) {
- // elt is a sequence
- return string.Format("[Length {0}]", seqLen.Result.AsInt());
- }
-
- if (elt == f_null.GetConstant())
- return "null";
-
- var tp = f_dtype.TryEval(elt);
- if (tp != null) {
- foreach (var app in tp.References) {
- if (app.Args.Length == 0 && app.Func.Name.StartsWith("class.")) {
- suff = NameSeqSuffix.Always;
- return app.Func.Name.Substring(6);
- }
- }
- }
-
- return base.CanonicalBaseName(elt, out suff);
- }
-
- public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt)
- {
- List<ElementNode> result = new List<ElementNode>();
-
- if (elt.Kind != Model.ElementKind.Uninterpreted)
- return result;
-
- // Perhaps elt is a known datatype value
- Model.FuncTuple fnTuple;
- if (DatatypeValues.TryGetValue(elt, out fnTuple)) {
- // elt is a datatype value
- int i = 0;
- foreach (var arg in fnTuple.Args) {
- var edgname = new EdgeName(this, i.ToString());
- result.Add(new FieldNode(state, edgname, arg));
- i++;
- }
- return result;
- }
-
- // Perhaps elt is a sequence
- var seqLen = f_seq_length.AppWithArg(0, elt);
- if (seqLen != null) {
- // elt is a sequence
- foreach (var tpl in f_seq_index.AppsWithArg(0, elt)) {
- var edgname = new EdgeName(this, "[%0]", tpl.Args[1]);
- result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));
- }
- return result;
- }
-
- // Perhaps elt is a set
- foreach (var tpl in f_set_select.AppsWithArg(0, elt)) {
- var setElement = tpl.Args[1];
- var containment = tpl.Result;
- var edgname = new EdgeName(this, "[%0]", Unbox(setElement));
- result.Add(new FieldNode(state, edgname, containment));
- }
- if (result.Count != 0)
- return result; // elt is a set
-
- // It seems elt is an object or array
- Model.Element[] lengths;
- if (ArrayLengths.TryGetValue(elt, out lengths)) {
- int i = 0;
- foreach (var len in lengths) {
- var name = lengths.Length == 1 ? "Length" : "Length" + i;
- var edgname = new EdgeName(this, name);
- result.Add(new FieldNode(state, edgname, len));
- i++;
- }
- }
- var heap = state.State.TryGet("$Heap");
- if (heap != null) {
- foreach (var tpl in f_heap_select.AppsWithArgs(0, heap, 1, elt)) {
- var field = new FieldName(tpl.Args[2], this);
- if (field.NameFormat != "alloc") {
- var edgname = new EdgeName(this, field.NameFormat, field.NameArgs);
- result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));
- }
- }
- }
- return result;
- }
-
- class FieldName
- {
- public readonly Model.Element Field;
- public readonly int Dims;
- public readonly string NameFormat;
- public readonly Model.Element[] NameArgs;
-
- public FieldName(Model.Element elt, DafnyModel dm) {
- Field = elt;
- NameArgs = new Model.Element[Dims];
- var tpl = dm.f_dim.AppWithArg(0, elt);
- if (tpl != null) {
- Dims = tpl.Result.AsInt();
- NameArgs = new Model.Element[Dims];
- for (int i = Dims; 0 <= --i; ) {
- if (i == 0) {
- tpl = dm.f_index_field.AppWithResult(elt);
- NameArgs[i] = tpl.Args[0];
- } else {
- tpl = dm.f_multi_index_field.AppWithResult(elt);
- NameArgs[i] = tpl.Args[1];
- elt = tpl.Args[0];
- }
- }
- }
- // now for the name
- if (Dims == 0) {
- NameFormat = Field.ToString();
- foreach (var n in Field.Names) {
- NameFormat = n.Func.Name;
- int dot = NameFormat.LastIndexOf('.');
- if (0 <= dot)
- NameFormat = NameFormat.Substring(dot + 1);
- break;
- }
- } else {
- NameFormat = "[";
- string sep = "";
- for (int i = 0; i < Dims; i++) {
- NameFormat += sep + "%" + i;
- sep = ",";
- }
- NameFormat += "]";
- }
- }
- }
-
- Model.Element Unbox(Model.Element elt) {
- var unboxed = f_box.AppWithResult(elt);
- if (unboxed != null)
- return unboxed.Args[0];
- else
- return elt;
- }
- }
-
- public class StateNode : NamedState
- {
- internal readonly DafnyModel dm;
- public readonly List<VariableNode> Vars = new List<VariableNode>();
- internal readonly List<VariableNode> skolems;
- internal readonly int index;
-
- public StateNode(int i, DafnyModel parent, Model.CapturedState s)
- : base(s, parent)
- {
- dm = parent;
- state = s;
- index = i;
-
- skolems = new List<VariableNode>(SkolemVars());
- SetupVars();
- }
-
- void SetupVars()
- {
- var names = Util.Empty<string>();
-
- if (dm.states.Count > 0) {
- var prev = dm.states.Last();
- names = prev.Vars.Map(v => v.realName);
- }
-
- names = names.Concat(state.Variables).Distinct();
-
- var curVars = state.Variables.ToDictionary(x => x);
- foreach (var v in names) {
- if (dm.GetUserVariableName(v) != null) {
- var val = state.TryGet(v);
- var shortName = Regex.Replace(v, @"#\d+$", "");
- var vn = new VariableNode(this, v, val, names.Any(n => n != v && Regex.Replace(n, @"#\d+$", "") == shortName) ? v : shortName);
- vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v);
- if (curVars.ContainsKey(v))
- dm.RegisterLocalValue(vn.Name, val);
- Vars.Add(vn);
- }
- }
-
- dm.Flush(Nodes);
- }
-
- IEnumerable<VariableNode> SkolemVars() {
- foreach (var f in dm.model.Functions) {
- if (f.Arity != 0) continue;
- int n = f.Name.IndexOf('!');
- if (n == -1) continue;
- string name = f.Name.Substring(0, n);
- if (!name.Contains('#')) continue;
- yield return new VariableNode(this, name, f.GetConstant(), name);
- }
- }
-
- public override IEnumerable<IDisplayNode> Nodes
- {
- get {
- return Vars.Concat(skolems);
- }
- }
- }
-
- public class ElementNode : DisplayNode
- {
- protected StateNode stateNode;
- protected Model.Element elt;
- protected DafnyModel vm { get { return stateNode.dm; } }
-
- public ElementNode(StateNode st, EdgeName name, Model.Element elt)
- : base(st.dm, name, elt)
- {
- this.stateNode = st;
- this.elt = elt;
- }
-
- public ElementNode(StateNode st, string name, Model.Element elt)
- : this(st, new EdgeName(name), elt) { }
-
- protected override void ComputeChildren()
- {
- children.AddRange(vm.GetExpansion(stateNode, elt));
- }
- }
-
- class FieldNode : ElementNode
- {
- public FieldNode(StateNode par, EdgeName realName, Model.Element elt)
- : base(par, realName, elt)
- {
- /*
- var idx = realName.LastIndexOf('.');
- if (idx > 0)
- name = realName.Substring(idx + 1);
- */
- }
- }
-
- class MapletNode : ElementNode
- {
- public MapletNode(StateNode par, EdgeName realName, Model.Element elt)
- : base(par, realName, elt)
- {
- }
- }
-
- public class VariableNode : ElementNode
- {
- public bool updatedHere;
- public string realName;
-
- public VariableNode(StateNode par, string realName, Model.Element elt, string shortName)
- : base(par, realName, elt)
- {
- this.realName = realName;
- name = new EdgeName(vm.GetUserVariableName(realName));
- ShortName = shortName;
- }
- }
-}
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Text.RegularExpressions;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie.ModelViewer.Dafny
+{
+ public class Provider : ILanguageProvider
+ {
+ public static Provider Instance = new Provider();
+ private Provider() { }
+
+ public bool IsMyModel(Model m)
+ {
+ return m.TryGetFunc("$$Language$Dafny") != null;
+ }
+
+ public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts)
+ {
+ var dm = new DafnyModel(m, opts);
+ foreach (var s in m.States) {
+ var sn = new StateNode(dm.states.Count, dm, s);
+ dm.states.Add(sn);
+ }
+ dm.FinishStates();
+ return dm;
+ }
+ }
+
+ public class DafnyModel : LanguageModel
+ {
+ public readonly Model.Func f_heap_select, f_set_select, f_seq_length, f_seq_index, f_box, f_dim, f_index_field, f_multi_index_field, f_dtype, f_null;
+ public readonly Dictionary<Model.Element, Model.Element[]> ArrayLengths = new Dictionary<Model.Element, Model.Element[]>();
+ public readonly Dictionary<Model.Element, Model.FuncTuple> DatatypeValues = new Dictionary<Model.Element, Model.FuncTuple>();
+ Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();
+ public List<StateNode> states = new List<StateNode>();
+
+ public DafnyModel(Model m, ViewOptions opts)
+ : base(m, opts)
+ {
+ f_heap_select = m.MkFunc("[3]", 3);
+ f_set_select = m.MkFunc("[2]", 2);
+ f_seq_length = m.MkFunc("Seq#Length", 1);
+ f_seq_index = m.MkFunc("Seq#Index", 2);
+ f_box = m.MkFunc("$Box", 1);
+ f_dim = m.MkFunc("FDim", 1);
+ f_index_field = m.MkFunc("IndexField", 1);
+ f_multi_index_field = m.MkFunc("MultiIndexField", 2);
+ f_dtype = m.MkFunc("dtype", 1);
+ f_null = m.MkFunc("null", 0);
+
+ // collect the array dimensions from the various array.Length functions, and
+ // collect all known datatype values
+ foreach (var fn in m.Functions) {
+ if (Regex.IsMatch(fn.Name, "^_System.array[0-9]*.Length[0-9]*$")) {
+ int j = fn.Name.IndexOf('.', 13);
+ int dims = j == 13 ? 1 : int.Parse(fn.Name.Substring(13, j - 13));
+ int idx = j == 13 ? 0 : int.Parse(fn.Name.Substring(j + 7));
+ foreach (var tpl in fn.Apps) {
+ var elt = tpl.Args[0];
+ var len = tpl.Result;
+ Model.Element[] ar;
+ if (!ArrayLengths.TryGetValue(elt, out ar)) {
+ ar = new Model.Element[dims];
+ ArrayLengths.Add(elt, ar);
+ }
+ Contract.Assert(ar[idx] == null);
+ ar[idx] = len;
+ }
+ } else if (fn.Name.StartsWith("#") && fn.Name.IndexOf('.') != -1 && fn.Name[1] != '#') {
+ foreach (var tpl in fn.Apps) {
+ var elt = tpl.Result;
+ DatatypeValues.Add(elt, tpl);
+ }
+ }
+ }
+ }
+
+ internal void FinishStates()
+ {
+ GenerateSourceLocations(states);
+ }
+
+ public override IEnumerable<IState> States
+ {
+ get { return states; }
+ }
+
+ public string GetUserVariableName(string name)
+ {
+ if (name.StartsWith("$")) // this covers $Heap and $_Frame and $nw...
+ return null;
+ if (name.Contains("##")) // a temporary variable of the translation
+ return null;
+#if SOMETIME_AGAIN
+ var hash = name.IndexOf('#');
+ if (0 < hash)
+ return name.Substring(0, hash);
+#endif
+ return name;
+ }
+
+ public Model.Element Image(Model.Element elt, Model.Func f)
+ {
+ var r = f.AppWithResult(elt);
+ if (r != null)
+ return r.Args[0];
+ return null;
+ }
+
+ protected override string CanonicalBaseName(Model.Element elt, out NameSeqSuffix suff)
+ {
+ Model.FuncTuple fnTuple;
+ suff = NameSeqSuffix.WhenNonZero;
+ if (DatatypeValues.TryGetValue(elt, out fnTuple)) {
+ // elt is s a datatype value, make its name be the name of the datatype constructor
+ string nm = fnTuple.Func.Name;
+ if (fnTuple.Func.Arity == 0)
+ return nm;
+ else
+ return nm + "(...)";
+ }
+ var seqLen = f_seq_length.AppWithArg(0, elt);
+ if (seqLen != null) {
+ // elt is a sequence
+ return string.Format("[Length {0}]", seqLen.Result.AsInt());
+ }
+
+ if (elt == f_null.GetConstant())
+ return "null";
+
+ var tp = f_dtype.TryEval(elt);
+ if (tp != null) {
+ foreach (var app in tp.References) {
+ if (app.Args.Length == 0 && app.Func.Name.StartsWith("class.")) {
+ suff = NameSeqSuffix.Always;
+ return app.Func.Name.Substring(6);
+ }
+ }
+ }
+
+ return base.CanonicalBaseName(elt, out suff);
+ }
+
+ public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt)
+ {
+ List<ElementNode> result = new List<ElementNode>();
+
+ if (elt.Kind != Model.ElementKind.Uninterpreted)
+ return result;
+
+ // Perhaps elt is a known datatype value
+ Model.FuncTuple fnTuple;
+ if (DatatypeValues.TryGetValue(elt, out fnTuple)) {
+ // elt is a datatype value
+ int i = 0;
+ foreach (var arg in fnTuple.Args) {
+ var edgname = new EdgeName(this, i.ToString());
+ result.Add(new FieldNode(state, edgname, arg));
+ i++;
+ }
+ return result;
+ }
+
+ // Perhaps elt is a sequence
+ var seqLen = f_seq_length.AppWithArg(0, elt);
+ if (seqLen != null) {
+ // elt is a sequence
+ foreach (var tpl in f_seq_index.AppsWithArg(0, elt)) {
+ var edgname = new EdgeName(this, "[%0]", tpl.Args[1]);
+ result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));
+ }
+ return result;
+ }
+
+ // Perhaps elt is a set
+ foreach (var tpl in f_set_select.AppsWithArg(0, elt)) {
+ var setElement = tpl.Args[1];
+ var containment = tpl.Result;
+ var edgname = new EdgeName(this, "[%0]", Unbox(setElement));
+ result.Add(new FieldNode(state, edgname, containment));
+ }
+ if (result.Count != 0)
+ return result; // elt is a set
+
+ // It seems elt is an object or array
+ Model.Element[] lengths;
+ if (ArrayLengths.TryGetValue(elt, out lengths)) {
+ int i = 0;
+ foreach (var len in lengths) {
+ var name = lengths.Length == 1 ? "Length" : "Length" + i;
+ var edgname = new EdgeName(this, name);
+ result.Add(new FieldNode(state, edgname, len));
+ i++;
+ }
+ }
+ var heap = state.State.TryGet("$Heap");
+ if (heap != null) {
+ foreach (var tpl in f_heap_select.AppsWithArgs(0, heap, 1, elt)) {
+ var field = new FieldName(tpl.Args[2], this);
+ if (field.NameFormat != "alloc") {
+ var edgname = new EdgeName(this, field.NameFormat, field.NameArgs);
+ result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));
+ }
+ }
+ }
+ return result;
+ }
+
+ class FieldName
+ {
+ public readonly Model.Element Field;
+ public readonly int Dims;
+ public readonly string NameFormat;
+ public readonly Model.Element[] NameArgs;
+
+ public FieldName(Model.Element elt, DafnyModel dm) {
+ Field = elt;
+ NameArgs = new Model.Element[Dims];
+ var tpl = dm.f_dim.AppWithArg(0, elt);
+ if (tpl != null) {
+ Dims = tpl.Result.AsInt();
+ NameArgs = new Model.Element[Dims];
+ for (int i = Dims; 0 <= --i; ) {
+ if (i == 0) {
+ tpl = dm.f_index_field.AppWithResult(elt);
+ NameArgs[i] = tpl.Args[0];
+ } else {
+ tpl = dm.f_multi_index_field.AppWithResult(elt);
+ NameArgs[i] = tpl.Args[1];
+ elt = tpl.Args[0];
+ }
+ }
+ }
+ // now for the name
+ if (Dims == 0) {
+ NameFormat = Field.ToString();
+ foreach (var n in Field.Names) {
+ NameFormat = n.Func.Name;
+ int dot = NameFormat.LastIndexOf('.');
+ if (0 <= dot)
+ NameFormat = NameFormat.Substring(dot + 1);
+ break;
+ }
+ } else {
+ NameFormat = "[";
+ string sep = "";
+ for (int i = 0; i < Dims; i++) {
+ NameFormat += sep + "%" + i;
+ sep = ",";
+ }
+ NameFormat += "]";
+ }
+ }
+ }
+
+ Model.Element Unbox(Model.Element elt) {
+ var unboxed = f_box.AppWithResult(elt);
+ if (unboxed != null)
+ return unboxed.Args[0];
+ else
+ return elt;
+ }
+ }
+
+ public class StateNode : NamedState
+ {
+ internal readonly DafnyModel dm;
+ public readonly List<VariableNode> Vars = new List<VariableNode>();
+ internal readonly List<VariableNode> skolems;
+ internal readonly int index;
+
+ public StateNode(int i, DafnyModel parent, Model.CapturedState s)
+ : base(s, parent)
+ {
+ dm = parent;
+ state = s;
+ index = i;
+
+ skolems = new List<VariableNode>(SkolemVars());
+ SetupVars();
+ }
+
+ void SetupVars()
+ {
+ var names = Util.Empty<string>();
+
+ if (dm.states.Count > 0) {
+ var prev = dm.states.Last();
+ names = prev.Vars.Map(v => v.realName);
+ }
+
+ names = names.Concat(state.Variables).Distinct();
+
+ var curVars = state.Variables.ToDictionary(x => x);
+ foreach (var v in names) {
+ if (dm.GetUserVariableName(v) != null) {
+ var val = state.TryGet(v);
+ var shortName = Regex.Replace(v, @"#\d+$", "");
+ var vn = new VariableNode(this, v, val, names.Any(n => n != v && Regex.Replace(n, @"#\d+$", "") == shortName) ? v : shortName);
+ vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v);
+ if (curVars.ContainsKey(v))
+ dm.RegisterLocalValue(vn.Name, val);
+ Vars.Add(vn);
+ }
+ }
+
+ dm.Flush(Nodes);
+ }
+
+ IEnumerable<VariableNode> SkolemVars() {
+ foreach (var f in dm.model.Functions) {
+ if (f.Arity != 0) continue;
+ int n = f.Name.IndexOf('!');
+ if (n == -1) continue;
+ string name = f.Name.Substring(0, n);
+ if (!name.Contains('#')) continue;
+ yield return new VariableNode(this, name, f.GetConstant(), name);
+ }
+ }
+
+ public override IEnumerable<IDisplayNode> Nodes
+ {
+ get {
+ return Vars.Concat(skolems);
+ }
+ }
+ }
+
+ public class ElementNode : DisplayNode
+ {
+ protected StateNode stateNode;
+ protected Model.Element elt;
+ protected DafnyModel vm { get { return stateNode.dm; } }
+
+ public ElementNode(StateNode st, EdgeName name, Model.Element elt)
+ : base(st.dm, name, elt)
+ {
+ this.stateNode = st;
+ this.elt = elt;
+ }
+
+ public ElementNode(StateNode st, string name, Model.Element elt)
+ : this(st, new EdgeName(name), elt) { }
+
+ protected override void ComputeChildren()
+ {
+ children.AddRange(vm.GetExpansion(stateNode, elt));
+ }
+ }
+
+ class FieldNode : ElementNode
+ {
+ public FieldNode(StateNode par, EdgeName realName, Model.Element elt)
+ : base(par, realName, elt)
+ {
+ /*
+ var idx = realName.LastIndexOf('.');
+ if (idx > 0)
+ name = realName.Substring(idx + 1);
+ */
+ }
+ }
+
+ class MapletNode : ElementNode
+ {
+ public MapletNode(StateNode par, EdgeName realName, Model.Element elt)
+ : base(par, realName, elt)
+ {
+ }
+ }
+
+ public class VariableNode : ElementNode
+ {
+ public bool updatedHere;
+ public string realName;
+
+ public VariableNode(StateNode par, string realName, Model.Element elt, string shortName)
+ : base(par, realName, elt)
+ {
+ this.realName = realName;
+ name = new EdgeName(vm.GetUserVariableName(realName));
+ ShortName = shortName;
+ }
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 06:00:14 +0000