From ac44a0e0ba8679be11ce0759ec58e3891a1ad318 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Sun, 31 May 2015 14:05:58 -0700
Subject: added assume about gate after calls and parallel calls

---
 Source/Concurrency/OwickiGries.cs | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'Source/Concurrency')

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);
                     }
-- 
cgit v1.2.3