1 files changed, 136 insertions, 136 deletions
diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index 1e9e9cf9..8797fe1f 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -1,136 +1,136 @@
-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, ViewOptions opts)
-    {
-      return new GenericModel(m, opts);
-    }
-  }
-
-  public class GenericModel : LanguageModel
-  {
-    List<BaseState> states = new List<BaseState>();
-
-    public GenericModel(Model m, ViewOptions opts)
-        : base(m, opts)
-    {
-      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 override IEnumerable<IState> States
-    {
-      get { return states; }
-    }
-  }
-
-  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)
-    {
-      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.model.Functions));
-      nodes.Add(new ContainerNode<Model.Func>("[Constants]", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.model.Functions));
-    }
-
-    public virtual SourceViewState ShowSource()
-    {
-      return null;
-    }
-
-    IDisplayNode Function(Model.Func f)
-    {
-      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
-  {
-    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(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;
-      var sb = new StringBuilder();
-      sb.Append(t.Func.Name);
-      if (t.Args.Length > 0) {
-        sb.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(m.m, sb.ToString(), t.Args);
-    }
-  }
-
-}
+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, ViewOptions opts)
+    {
+      return new GenericModel(m, opts);
+    }
+  }
+
+  public class GenericModel : LanguageModel
+  {
+    List<BaseState> states = new List<BaseState>();
+
+    public GenericModel(Model m, ViewOptions opts)
+        : base(m, opts)
+    {
+      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 override IEnumerable<IState> States
+    {
+      get { return states; }
+    }
+  }
+
+  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)
+    {
+      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.model.Functions));
+      nodes.Add(new ContainerNode<Model.Func>("[Constants]", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.model.Functions));
+    }
+
+    public virtual SourceViewState ShowSource()
+    {
+      return null;
+    }
+
+    IDisplayNode Function(Model.Func f)
+    {
+      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
+  {
+    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(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;
+      var sb = new StringBuilder();
+      sb.Append(t.Func.Name);
+      if (t.Args.Length > 0) {
+        sb.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(m.m, sb.ToString(), t.Args);
+    }
+  }
+
+}