diff options
| author |  qadeer <unknown> | 2014-02-07 22:22:23 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-02-07 22:22:23 -0800 |
| commit | 1f0945b2744ff44091f8574237324506764cfe37 (patch) | |
| tree | abca71419bf02ef5dc6d04b395335fe28f0c02a5 /Source/Concurrency | |
| parent | de9be69954d167a71c74ff68dd27e8cc96ba9c12 (diff) | |
added another example and fixed a bug regarding initialization of pc/ok
snapshots per loop header
Diffstat (limited to 'Source/Concurrency')
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index d4ecab2e..f442c1af 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -917,6 +917,8 @@ namespace Microsoft.Boogie b.Cmds = newCmds;
}
+ List<Variable> oldPcs = new List<Variable>();
+ List<Variable> oldOks = new List<Variable>();
foreach (Block header in yieldingHeaders)
{
LocalVariable oldPc = null;
@@ -924,8 +926,10 @@ namespace Microsoft.Boogie if (pc != null)
{
oldPc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", pc.Name, header.Label), Type.Bool));
+ oldPcs.Add(oldPc);
impl.LocVars.Add(oldPc);
oldOk = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", ok.Name, header.Label), Type.Bool));
+ oldOks.Add(oldOk);
impl.LocVars.Add(oldOk);
}
Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar);
@@ -971,8 +975,18 @@ namespace Microsoft.Boogie {
lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)));
rhss.Add(Expr.False);
+ foreach (Variable oldPc in oldPcs)
+ {
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)));
+ rhss.Add(Expr.False);
+ }
lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)));
rhss.Add(Expr.False);
+ foreach (Variable oldOk in oldOks)
+ {
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)));
+ rhss.Add(Expr.False);
+ }
}
Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
foreach (var domainName in linearTypeChecker.linearDomains.Keys)
|