diff options
| author |  qadeer <unknown> | 2013-12-25 16:16:53 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2013-12-25 16:16:53 -0800 |
| commit | 01851d0ad1e1976c7659d80e1d97c7e8f86724e1 (patch) | |
| tree | e327a3e58069c43b6988dc0ba07c7111bef6312f /Source/Concurrency/MoverCheck.cs | |
| parent | 147b155073406f7d279ab8d3884fd2468227b5a3 (diff) | |
fixed a bug in mover checking; wasn't generating enough commutativity checks
Diffstat (limited to 'Source/Concurrency/MoverCheck.cs')
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 31 |
1 files changed, 19 insertions, 12 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 579c9cf6..76a4b098 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -109,25 +109,32 @@ namespace Microsoft.Boogie Program program = moverTypeChecker.program;
MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);
- foreach (int phaseNum in pools.Keys)
+ foreach (int phaseNum1 in pools.Keys)
{
- foreach (ActionInfo first in pools[phaseNum])
+ foreach (ActionInfo first in pools[phaseNum1])
{
Debug.Assert(first.moverType != MoverType.Top);
if (first.moverType == MoverType.Atomic)
continue;
- foreach (ActionInfo second in pools[phaseNum])
+ foreach (int phaseNum2 in pools.Keys)
{
- if (first.IsRightMover)
+ if (phaseNum2 < phaseNum1) continue;
+ foreach (ActionInfo second in pools[phaseNum2])
{
- moverChecking.CreateCommutativityChecker(program, first, second);
- moverChecking.CreateGatePreservationChecker(program, second, first);
- }
- if (first.IsLeftMover)
- {
- moverChecking.CreateCommutativityChecker(program, second, first);
- moverChecking.CreateGatePreservationChecker(program, first, second);
- moverChecking.CreateFailurePreservationChecker(program, second, first);
+ if (second.phaseNum < phaseNum1)
+ {
+ if (first.IsRightMover)
+ {
+ moverChecking.CreateCommutativityChecker(program, first, second);
+ moverChecking.CreateGatePreservationChecker(program, second, first);
+ }
+ if (first.IsLeftMover)
+ {
+ moverChecking.CreateCommutativityChecker(program, second, first);
+ moverChecking.CreateGatePreservationChecker(program, first, second);
+ moverChecking.CreateFailurePreservationChecker(program, second, first);
+ }
+ }
}
}
}
|