diff options
| author |  qadeer <qadeer@microsoft.com> | 2015-05-31 14:05:58 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2015-05-31 14:05:58 -0700 |
| commit | ac44a0e0ba8679be11ce0759ec58e3891a1ad318 (patch) | |
| tree | 1f610d36cd56b18687170972913a48d426cf0c20 /Source/Concurrency | |
| parent | fe892b18dbc8e0c2b5b20e509080d6e98814116c (diff) | |
added assume about gate after calls and parallel calls
Diffstat (limited to 'Source/Concurrency')
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index dbd1dcbd..626f2c4a 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -919,6 +919,15 @@ namespace Microsoft.Boogie {
HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(callCmd));
linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars);
+
+ if (!callCmd.IsAsync && globalMods.Count > 0 && pc != null)
+ {
+ // assume pc || alpha(i, g);
+ Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
+ assumeExpr.Type = Type.Bool;
+ newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
+ }
+
Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
}
@@ -930,6 +939,15 @@ namespace Microsoft.Boogie DesugarParallelCallCmd(newCmds, parCallCmd);
HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));
linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);
+
+ if (globalMods.Count > 0 && pc != null)
+ {
+ // assume pc || alpha(i, g);
+ Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
+ assumeExpr.Type = Type.Bool;
+ newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
+ }
+
Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
}
|