diff options
| author |  qadeer <unknown> | 2014-04-20 21:08:11 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-04-20 21:08:11 -0700 |
| commit | b23a93d04bd66014854af44258264f9867c73f55 (patch) | |
| tree | cdc58392e8428189951ed390745a9f772218d4d0 /Source/Concurrency/SimulationRelation.cs | |
| parent | 2e190e24541eb9608e1d4ba18874c2403156e792 (diff) | |
added simulation relation computation to yield type checking
updated the type check to incorporate {:terminates} annotation
Diffstat (limited to 'Source/Concurrency/SimulationRelation.cs')
| -rw-r--r-- | Source/Concurrency/SimulationRelation.cs | 197 |
1 files changed, 197 insertions, 0 deletions
diff --git a/Source/Concurrency/SimulationRelation.cs b/Source/Concurrency/SimulationRelation.cs new file mode 100644 index 00000000..7f130f76 --- /dev/null +++ b/Source/Concurrency/SimulationRelation.cs @@ -0,0 +1,197 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie.GraphUtil;
+
+namespace Microsoft.Boogie
+{
+ public class SimulationRelation<A, B, L>
+ {
+ class Graph<T>
+ {
+ HashSet<T> nodes;
+ Dictionary<T, Dictionary<L, List<T>>> successors;
+ Dictionary<T, Dictionary<L, List<T>>> predecessors;
+
+ public Graph(List<Tuple<T, L, T>> edges)
+ {
+ nodes = new HashSet<T>();
+ successors = new Dictionary<T, Dictionary<L, List<T>>>();
+ predecessors = new Dictionary<T, Dictionary<L, List<T>>>();
+ foreach (Tuple<T, L, T> edge in edges)
+ {
+ T source = edge.Item1;
+ L label = edge.Item2;
+ T dest = edge.Item3;
+ nodes.Add(source);
+ nodes.Add(dest);
+ if (!successors.ContainsKey(source))
+ {
+ successors[source] = new Dictionary<L, List<T>>();
+ }
+ if (!successors[source].ContainsKey(label))
+ {
+ successors[source][label] = new List<T>();
+ }
+ if (!predecessors.ContainsKey(dest))
+ {
+ predecessors[dest] = new Dictionary<L, List<T>>();
+ }
+ if (!predecessors[dest].ContainsKey(label))
+ {
+ predecessors[dest][label] = new List<T>();
+ }
+ successors[source][label].Add(dest);
+ predecessors[dest][label].Add(source);
+ }
+ }
+
+ public IEnumerable<T> Nodes { get { return nodes; } }
+
+ public IEnumerable<T> Post(T t, L l)
+ {
+ if (successors.ContainsKey(t) && successors[t].ContainsKey(l))
+ {
+ return successors[t][l];
+ }
+ else
+ {
+ return Enumerable.Empty<T>();
+ }
+ }
+
+ public IEnumerable<T> Post(IEnumerable<T> set, L l)
+ {
+ return set.Select(x => Post(x, l)).Aggregate(Enumerable.Empty<T>(), (p, q) => p.Concat(q));
+ }
+
+ public IEnumerable<T> Pre(T t, L l)
+ {
+ if (predecessors.ContainsKey(t) && predecessors[t].ContainsKey(l))
+ {
+ return predecessors[t][l];
+ }
+ else
+ {
+ return Enumerable.Empty<T>();
+ }
+ }
+
+ public IEnumerable<T> Pre(IEnumerable<T> set, L l)
+ {
+ return set.Select(x => Pre(x, l)).Aggregate(Enumerable.Empty<T>(), (p, q) => p.Concat(q));
+ }
+
+ public IEnumerable<L> PostLabels(T t)
+ {
+ if (successors.ContainsKey(t))
+ {
+ return successors[t].Keys;
+ }
+ else
+ {
+ return Enumerable.Empty<L>();
+ }
+ }
+
+ public IEnumerable<L> PreLabels(T t)
+ {
+ if (predecessors.ContainsKey(t))
+ {
+ return predecessors[t].Keys;
+ }
+ else
+ {
+ return Enumerable.Empty<L>();
+ }
+ }
+ }
+
+ Graph<A> aGraph;
+ Graph<B> bGraph;
+ Dictionary<A, HashSet<B>> initialConstraints;
+
+ public SimulationRelation(List<Tuple<A, L, A>> aEdges, List<Tuple<B, L, B>> bEdges, Dictionary<A, HashSet<B>> initialConstraints)
+ {
+ this.aGraph = new Graph<A>(aEdges);
+ this.bGraph = new Graph<B>(bEdges);
+ this.initialConstraints = initialConstraints;
+ }
+
+ public Dictionary<A, HashSet<B>> ComputeSimulationRelation()
+ {
+ Dictionary<A, HashSet<B>> prevsim;
+ Dictionary<A, HashSet<B>> sim;
+ Dictionary<Tuple<A, L>, HashSet<B>> remove;
+ Queue<Tuple<A,L>> workQueue;
+
+ prevsim = new Dictionary<A, HashSet<B>>();
+ sim = new Dictionary<A, HashSet<B>>();
+ remove = new Dictionary<Tuple<A, L>, HashSet<B>>();
+ workQueue = new Queue<Tuple<A,L>>();
+ foreach (var a in aGraph.Nodes)
+ {
+ prevsim[a] = new HashSet<B>(bGraph.Nodes);
+ sim[a] = new HashSet<B>();
+ HashSet<L> aOutgoingLabels = new HashSet<L>(aGraph.PostLabels(a));
+ foreach (var b in bGraph.Nodes)
+ {
+ IEnumerable<L> bOutgoingLabels = bGraph.PostLabels(b);
+ if (aOutgoingLabels.IsSubsetOf(bOutgoingLabels))
+ {
+ sim[a].Add(b);
+ }
+ }
+ if (initialConstraints.ContainsKey(a))
+ {
+ sim[a].IntersectWith(initialConstraints[a]);
+ }
+
+ foreach (var l in aGraph.PreLabels(a))
+ {
+ Tuple<A, L> x = new Tuple<A, L>(a, l);
+ remove[x] = new HashSet<B>(bGraph.Pre(prevsim[a], l).Except(bGraph.Pre(sim[a], l)));
+ if (remove[x].Count > 0)
+ {
+ workQueue.Enqueue(x);
+ }
+ }
+ }
+
+ while (workQueue.Count > 0)
+ {
+ Tuple<A,L> x = workQueue.Dequeue();
+ A v = x.Item1;
+ foreach (A u in aGraph.Pre(v, x.Item2))
+ {
+ foreach (B w in remove[x])
+ {
+ if (sim[u].Contains(w))
+ {
+ sim[u].Remove(w);
+ foreach (L l in bGraph.PreLabels(w))
+ {
+ foreach (B b in bGraph.Pre(w, l))
+ {
+ if (bGraph.Post(b, l).Intersect(sim[u]).Count() == 0)
+ {
+ Tuple<A, L> z = new Tuple<A, L>(u, l);
+ if (!remove.ContainsKey(z))
+ remove[z] = new HashSet<B>();
+ remove[z].Add(b);
+ workQueue.Enqueue(z);
+ }
+ }
+ }
+ }
+ }
+ }
+ prevsim[v] = new HashSet<B>(sim[v]);
+ remove[x] = new HashSet<B>();
+ }
+
+ return sim;
+ }
+ }
+}
|