diff options
author | 2010-10-14 21:45:14 +0000 | |
---|---|---|
committer | 2010-10-14 21:45:14 +0000 | |
commit | 6105f277f5d648e08987065dc697b5292ebf277d (patch) | |
tree | 45bd609e9a135d0678836b4daa9db95ec6277eb1 /Source/ModelViewer/DataModel.cs | |
parent | fe8c2be3f0d21c75981f16c76003148300a917ec (diff) |
Work on keeping the unfolding skeleton when switching between states
Diffstat (limited to 'Source/ModelViewer/DataModel.cs')
-rw-r--r-- | Source/ModelViewer/DataModel.cs | 84 |
1 files changed, 73 insertions, 11 deletions
diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs index bda154ca..f1b0b26f 100644 --- a/Source/ModelViewer/DataModel.cs +++ b/Source/ModelViewer/DataModel.cs @@ -5,6 +5,12 @@ using System.Text; namespace Microsoft.Boogie.ModelViewer
{
+ public interface ILanguageProvider
+ {
+ bool IsMyModel(Model m);
+ IEnumerable<IState> GetStates(Model m);
+ }
+
[Flags]
public enum NodeState
{
@@ -14,18 +20,54 @@ namespace Microsoft.Boogie.ModelViewer public interface IDisplayNode
{
- string Name { get; }
- IEnumerable<string> Values { get; }
+ /// <summary>
+ /// Used for indexing the state tree.
+ /// </summary>
+ string EdgeName { get; }
+
+ /// <summary>
+ /// Used to determine aliasing. Can be null.
+ /// </summary>
+ Model.Element Element { get; }
+
bool Expandable { get; }
IEnumerable<IDisplayNode> Expand();
- object ViewSync { get; set; }
+
+ // Things displayed to the user.
+ string Name { get; }
NodeState State { get; }
+ IEnumerable<string> Values { get; }
+
+ object ViewSync { get; set; }
}
- public interface ILanguageProvider
+ public interface IState
{
- bool IsMyModel(Model m);
- IEnumerable<IDisplayNode> GetStates(Model m);
+ string Name { get; }
+ IEnumerable<IDisplayNode> Nodes { get; }
+ }
+
+
+ public class TopState : IState
+ {
+ protected IDisplayNode[] children;
+ protected string name;
+
+ public TopState(string name, IEnumerable<IDisplayNode> nodes)
+ {
+ this.name = name;
+ children = nodes.ToArray();
+ }
+
+ public string Name
+ {
+ get { return name; }
+ }
+
+ public IEnumerable<IDisplayNode> Nodes
+ {
+ get { return children; }
+ }
}
public abstract class DisplayNode : IDisplayNode
@@ -57,13 +99,15 @@ namespace Microsoft.Boogie.ModelViewer public virtual NodeState State { get { return NodeState.Normal; } }
public object ViewSync { get; set; }
- }
- public static class SeqExtensions
- {
- public static IEnumerable<T> Map<S, T>(this IEnumerable<S> inp, Func<S, T> conv)
+ public virtual string EdgeName
{
- foreach (var s in inp) yield return conv(s);
+ get { return name; }
+ }
+
+ public virtual Model.Element Element
+ {
+ get { return null; }
}
}
@@ -90,4 +134,22 @@ namespace Microsoft.Boogie.ModelViewer }
+ public static class Util
+ {
+ public static void Assert(bool cond)
+ {
+ if (!cond) throw new System.Exception("assertion violation");
+ }
+
+ public static IEnumerable<T> Map<S, T>(this IEnumerable<S> inp, Func<S, T> conv)
+ {
+ foreach (var s in inp) yield return conv(s);
+ }
+
+ public static void Iter<T>(this IEnumerable<T> inp, Action<T> fn)
+ {
+ foreach (var s in inp) fn(s);
+ }
+ }
+
}
|