Improve the generic model viewer

1 files changed, 70 insertions, 18 deletions

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index cf5f9909..dddc8c30 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -23,44 +23,91 @@ namespace Microsoft.Boogie.ModelViewer.Base
 

   public class GenericModel : LanguageModel

   {

-    Model m;

+    internal Model m;

+    List<BaseState> states = new List<BaseState>();

 

     public GenericModel(Model m)

     {

       this.m = m;

+      foreach (var s in m.States)

+        states.Add(new BaseState(this, s) { Name = s.Name });

+      foreach (var s in states)

+        this.Flush(s.nodes);

     }

 

-    public IDisplayNode Function(Model.Func f)

+    public override IEnumerable<IState> States

     {

-      return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(this, a), f.Apps);

+      get { return states; }

     }

+  }

 

-    IEnumerable<IDisplayNode> GetStateNodes(Model.CapturedState st)

+  public class BaseState : IState

+  {

+    internal GenericModel m;

+    Model.CapturedState st;

+

+    internal List<IDisplayNode> nodes = new List<IDisplayNode>();

+    internal Dictionary<Model.Element, string> niceName = new Dictionary<Model.Element, string>();

+

+    public BaseState(GenericModel m, 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);

+      this.st = st;

+      this.m = m;

+

+      foreach (var v in st.AllVariables) {

+        var e = st.TryGet(v);

+        m.RegisterLocalValue(v, e);

+        nodes.Add(new ElementNode(this, v, e));

+

+        niceName[e] = v;

+        foreach (var r in e.References) {

+          if (r.Args.Length == 1 && r.Args[0] == e) {

+            if (!niceName.ContainsKey(e))

+              niceName[e] = r.Func.Name + "(" + v + ")";

+          }

+        }

+      }

+

+      nodes.Add(new ContainerNode<Model.Func>("[Functions]", f => f.Arity == 0 ? null : Function(f), m.m.Functions));

+      nodes.Add(new ContainerNode<Model.Func>("[Constants]", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.m.Functions));

     }

 

-    public override IEnumerable<IState> States

+    IDisplayNode Function(Model.Func f)

     {

-      get {

-        foreach (var s in m.States)

-          yield return new TopState(s.Name, GetStateNodes(s));

-      }

+      return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(this, a), f.Apps);

+    }

+

+    public virtual string Name { get; set; }

+

+    public virtual IEnumerable<IDisplayNode> Nodes

+    {

+      get { return nodes; }

     }

   }

+

   public class ElementNode : DisplayNode

   {

-    public ElementNode(ILanguageSpecificModel p, string name, Model.Element elt) : base(p, name, elt) {}

+    BaseState st;

+

+    public ElementNode(BaseState st, string name, Model.Element elt) : base(st.m, name, elt) { this.st = st; }

+

+    protected override void ComputeChildren()

+    {

+      children.Add(new ContainerNode<Model.FuncTuple>(" == ", e => new AppNode(st, e), Element.References.Where(t => t.Result == Element)));

+      foreach (var e in Element.References) {

+        if (e.Args.Contains(Element))

+          children.Add(new AppNode(st, e, x => x == Element ? "*" : st.niceName.GetWithDefault(x, null)));

+      }

+    }

   }

 

   public class AppNode : ElementNode

   {

     protected Model.FuncTuple tupl;

 

-    public AppNode(ILanguageSpecificModel m, Model.FuncTuple t)

+    public AppNode(BaseState m, Model.FuncTuple t) : this(m, t, _ => null) { }

+

+    public AppNode(BaseState m, Model.FuncTuple t, Func<Model.Element, string> nameElement)

       : base(m, t.Func.Name, t.Result)

     {

       tupl = t;

@@ -68,12 +115,17 @@ namespace Microsoft.Boogie.ModelViewer.Base
       sb.Append(t.Func.Name);

       if (t.Args.Length > 0) {

         sb.Append("(");

-        foreach (var a in t.Args)

-          sb.Append(a.ToString()).Append(", ");

+        for (int i = 0; i < t.Args.Length; ++i) {

+          var n = nameElement(t.Args[i]);

+          if (n == null)

+            sb.AppendFormat("%{0}, ", i);

+          else

+            sb.AppendFormat("{0}, ", n);

+        }

         sb.Length -= 2;

         sb.Append(")");

       }

-      name = new EdgeName(sb.ToString());

+      name = new EdgeName(m.m, sb.ToString(), t.Args);

     }

   }