summaryrefslogtreecommitdiff
path: root/Source/Concurrency/SimulationRelation.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Concurrency/SimulationRelation.cs')
-rw-r--r--Source/Concurrency/SimulationRelation.cs394
1 files changed, 197 insertions, 197 deletions
diff --git a/Source/Concurrency/SimulationRelation.cs b/Source/Concurrency/SimulationRelation.cs
index 7f130f76..c97ebfb7 100644
--- a/Source/Concurrency/SimulationRelation.cs
+++ b/Source/Concurrency/SimulationRelation.cs
@@ -1,197 +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;
- }
- }
-}
+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;
+ }
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 13:13:19 +0000