Add DisplayNode class with default IDisplayNode implementation. Add IDisplayNode.State.

4 files changed, 101 insertions, 113 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index d7f78bfd..42302d00 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -265,6 +265,10 @@ namespace Microsoft.Boogie
 

       public IEnumerable<string> Variables { get { return vars; } }

       public int VariableCount { get { return vars.Count; } }

+      public bool HasBinding(string varname)

+      {

+        return valuations.ContainsKey(varname);

+      }

       public Element TryGet(string varname)

       {

         CapturedState curr = this;

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index e2d82fd9..a4c61589 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -24,54 +24,40 @@ namespace Microsoft.Boogie.ModelViewer.Base
     }

   }

 

-  public class StateNode : IDisplayNode

+  public class StateNode : DisplayNode

   {

     protected Model.CapturedState state;

 

-    public StateNode(Model.CapturedState s)

+    public StateNode(Model.CapturedState s) : base(s.Name)

     {

       state = s;

     }

 

-    public virtual string Name

-    {

-      get { return state.Name; }

-    }

-

-    public virtual IEnumerable<string> Values

+    public override IEnumerable<string> Values

     {

       get { foreach (var v in state.Variables) yield return v; }

     }

 

-    public virtual bool Expandable { get { return state.VariableCount != 0; } }

+    public override bool Expandable { get { return state.VariableCount != 0; } }

 

-    public virtual IEnumerable<IDisplayNode> Expand()

+    public override IEnumerable<IDisplayNode> Expand()

     {

       foreach (var v in state.Variables) {

         yield return new ElementNode(v, state.TryGet(v));

       }

     }

-

-    public object ViewSync { get; set; }

   }

 

-  public class ElementNode : IDisplayNode

+  public class ElementNode : DisplayNode

   {

     protected Model.Element elt;

-    protected string name;

 

-    public ElementNode(string name, Model.Element elt)

+    public ElementNode(string name, Model.Element elt) : base(name)

     {

-      this.name = name;

       this.elt = elt;

     }

 

-    public virtual string Name

-    {

-      get { return name; }

-    }

-

-    public virtual IEnumerable<string> Values

+    public override IEnumerable<string> Values

     {

       get

       {

@@ -83,11 +69,6 @@ namespace Microsoft.Boogie.ModelViewer.Base
         }

       }

     }

-

-    public virtual bool Expandable { get { return false; } }

-    public virtual IEnumerable<IDisplayNode> Expand() { yield break; }

-

-    public object ViewSync { get; set; }

   }

 

   public static class GenericNodes

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index 6f8811e9..bda154ca 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -5,6 +5,13 @@ using System.Text;
 

 namespace Microsoft.Boogie.ModelViewer

 {

+  [Flags]

+  public enum NodeState

+  {

+    Normal = 0,

+    Changed = 1

+  }

+

   public interface IDisplayNode

   {

     string Name { get; }

@@ -12,6 +19,7 @@ namespace Microsoft.Boogie.ModelViewer
     bool Expandable { get; }

     IEnumerable<IDisplayNode> Expand();

     object ViewSync { get; set; }

+    NodeState State { get; }

   }

 

   public interface ILanguageProvider

@@ -20,18 +28,11 @@ namespace Microsoft.Boogie.ModelViewer
     IEnumerable<IDisplayNode> GetStates(Model m);

   }

 

-  public class ContainerNode<T> : IDisplayNode

+  public abstract class DisplayNode : IDisplayNode

   {

     protected string name;

-    protected Func<T, IDisplayNode> convert;

-    protected IEnumerable<T> data;

 

-    public ContainerNode(string name, Func<T, IDisplayNode> convert, IEnumerable<T> data)

-    {

-      this.name = name;

-      this.convert = convert;

-      this.data = data;

-    }

+    public DisplayNode(string n) { name = n; }

 

     public virtual string Name

     {

@@ -43,18 +44,49 @@ namespace Microsoft.Boogie.ModelViewer
       get { yield break; }

     }

 

-    public virtual bool Expandable { get { return true; } }

+    public virtual bool Expandable

+    {

+      get { return false; }

+    }

 

     public virtual IEnumerable<IDisplayNode> Expand()

     {

+      yield break;

+    }

+

+    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)

+    {

+      foreach (var s in inp) yield return conv(s);

+    }

+  }

+

+  public class ContainerNode<T> : DisplayNode

+  {

+    protected Func<T, IDisplayNode> convert;

+    protected IEnumerable<T> data;

+

+    public ContainerNode(string name, Func<T, IDisplayNode> convert, IEnumerable<T> data) : base(name)

+    {

+      this.convert = convert;

+      this.data = data;

+    }

+

+    public override bool Expandable { get { return true; } }

+    public override IEnumerable<IDisplayNode> Expand()

+    {

       foreach (var f in data) {

         var res = convert(f);

         if (res != null)

           yield return res;

       }

     }

-

-    public object ViewSync { get; set; }

   }

 

 

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index e6323045..0f713d9e 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -17,64 +17,77 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

     public IEnumerable<IDisplayNode> GetStates(Model m)

     {

-      foreach (var s in m.States)

-        yield return new StateNode(s);

+      var vm = new VccModel();

+      foreach (var s in m.States) {

+        var sn = new StateNode(vm, s);

+        vm.states.Add(sn);

+      }

+      return vm.states;

+    }

+  }

+

+  class VccModel

+  {

+    public List<StateNode> states = new List<StateNode>();

+    public string GetUserVariableName(string name)

+    {

+      if (name.StartsWith("L#") || name.StartsWith("P#"))

+        return name.Substring(2);

+      return null;

     }

   }

 

-  public class StateNode : IDisplayNode

+  class StateNode : DisplayNode

   {

-    protected Model.CapturedState state;

-    protected string name;

+    Model.CapturedState state;

+    VccModel parent;

+    List<VariableNode> vars = new List<VariableNode>();

 

-    public StateNode(Model.CapturedState s)

+    public StateNode(VccModel parent, Model.CapturedState s) : base(s.Name)

     {

-      name = s.Name;

+      this.parent = parent;

+      state = s;

+

       var idx = name.LastIndexOfAny(new char[] { '\\', '/' });

       if (idx > 0)

         name = name.Substring(idx + 1);

-      state = s;

-    }

 

-    public virtual string Name

-    {

-      get { return name; }

+      var prev = parent.states.Last();

+

+      foreach (var v in state.Variables) {

+        var n = parent.GetUserVariableName(v);

+        if (n != null){

+          var vn = new VariableNode(n, state.TryGet(v));

+          vn.realName = n;

+          vars.Add(vn);

+        }

+      }

     }

 

-    public virtual IEnumerable<string> Values

+    public override IEnumerable<string> Values

     {

-      get { foreach (var v in state.Variables) yield return v; }

+      get { return vars.Map(v => v.Name); }

     }

 

-    public virtual bool Expandable { get { return state.VariableCount != 0; } }

-

-    public virtual IEnumerable<IDisplayNode> Expand()

+    public override bool Expandable { get { return true; } }

+    public override IEnumerable<IDisplayNode> Expand()

     {

-      foreach (var v in state.Variables) {

-        yield return new ElementNode(v, state.TryGet(v));

-      }

+      foreach (var v in vars) yield return v;

     }

-

-    public object ViewSync { get; set; }

   }

 

-  public class ElementNode : IDisplayNode

+  public class VariableNode : DisplayNode

   {

     protected Model.Element elt;

-    protected string name;

+    public string realName;

+    public bool updatedHere;

 

-    public ElementNode(string name, Model.Element elt)

+    public VariableNode(string name, Model.Element elt) : base(name)

     {

-      this.name = name;

       this.elt = elt;

     }

 

-    public virtual string Name

-    {

-      get { return name; }

-    }

-

-    public virtual IEnumerable<string> Values

+    public override IEnumerable<string> Values

     {

       get

       {

@@ -86,49 +99,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         }

       }

     }

-

-    public virtual bool Expandable { get { return false; } }

-    public virtual IEnumerable<IDisplayNode> Expand() { yield break; }

-

-    public object ViewSync { get; set; }

   }

 

-

-  public class ContainerNode<T> : IDisplayNode

-  {

-    protected string name;

-    protected Func<T, IDisplayNode> convert;

-    protected IEnumerable<T> data;

-

-    public ContainerNode(string name, Func<T, IDisplayNode> convert, IEnumerable<T> data)

-    {

-      this.name = name;

-      this.convert = convert;

-      this.data = data;

-    }

-

-    public virtual string Name

-    {

-      get { return name; }

-    }

-

-    public virtual IEnumerable<string> Values

-    {

-      get { yield break; }

-    }

-

-    public virtual bool Expandable { get { return true; } }

-

-    public virtual IEnumerable<IDisplayNode> Expand()

-    {

-      foreach (var f in data) {

-        var res = convert(f);

-        if (res != null)

-          yield return res;

-      }

-    }

-

-    public object ViewSync { get; set; }

-  }

   

 }