diff options
author | Ally Donaldson <unknown> | 2014-05-28 09:35:56 +0100 |
---|---|---|
committer | Ally Donaldson <unknown> | 2014-05-28 09:35:56 +0100 |
commit | 0c80b5c757bfa57d02e852d6f237faea05f2427c (patch) | |
tree | cd0693e1b0e75898824c7cd2e89af24820d50fc2 | |
parent | 858c77d6c370e13c9ac0960250ba1be1f80becbd (diff) |
Small cleanup in Staged Houdini
-rw-r--r-- | Source/Houdini/StagedHoudini.cs | 23 |
1 files changed, 6 insertions, 17 deletions
diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs index c306afd8..a3b02250 100644 --- a/Source/Houdini/StagedHoudini.cs +++ b/Source/Houdini/StagedHoudini.cs @@ -123,9 +123,7 @@ namespace Microsoft.Boogie.Houdini outcomes.Where(Item => plan.Contains(Item.Key)).
Select(Item => Item.Value).
Select(Item => Item.assignment).ToList();
- //outcomes.Values.Select(Item => Item.assignment).ToList();
completedStages = plan.GetDependences(s).Select(Item => Item.GetId());
- //completedStages = outcomes.Keys.Select(Item => Item.GetId());
}
if (relevantAssignments.Count() > 0)
@@ -158,23 +156,14 @@ namespace Microsoft.Boogie.Houdini private List<Houdini> AcquireHoudiniInstance()
{
- List<Houdini> h = null;
- do
- {
- foreach (var houdini in houdiniInstances)
- {
- if (Monitor.TryEnter(houdini))
- {
- h = houdini;
- break;
- }
- else
- {
- Thread.Sleep(20);
+ while(true) {
+ foreach (var houdini in houdiniInstances) {
+ if (Monitor.TryEnter(houdini)) {
+ return houdini;
}
+ Thread.Sleep(20);
}
- } while (h == null);
- return h;
+ }
}
private void EmitProgram(string filename)
|