using attribute

boogie-org · May 22, 2024 · 5a8510d · 5a8510d
1 parent 64b6e62
commit 5a8510d
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 12 deletions.
diff --git a/Source/Concurrency/InductiveSequentialization.cs b/Source/Concurrency/InductiveSequentialization.cs
@@ -176,8 +176,8 @@ private Cmd Transform(Dictionary<CtorType, Implementation> eliminatedPendingAsyn
   }
   public enum InductiveSequentializationRule
   {
-    IS1,
-    IS2
+    ISL,
+    ISR
   }
   public class InductiveSequentialization : Sequentialization
   {
@@ -193,17 +193,17 @@ public InductiveSequentialization(CivlTypeChecker civlTypeChecker, Action target
       // - the modified set of each of each eliminated and abstract action associated with this invariant.
       // - the target and refined action of every application of inductive sequentialization that refers to this invariant.
       this.invariantAction = invariantAction;
-      if (invariantAction.Name.StartsWith("left"))
+      choice = Expr.Ident(invariantAction.ImplWithChoice.OutParams.Last());
+      newPAs = invariantAction.PendingAsyncs.ToDictionary(decl => decl.PendingAsyncType,
+        decl => (Variable)civlTypeChecker.LocalVariable($"newPAs_{decl.Name}", decl.PendingAsyncMultisetType));
+      if (QKeyValue.FindAttribute(targetAction.ActionDecl.RefinedAction.Attributes, x => x.Key == CivlAttributes.IS2_LEFT) != null)
       {
-        rule = InductiveSequentializationRule.IS1;
+        rule = InductiveSequentializationRule.ISL;
       }
-      else if (invariantAction.Name.StartsWith("right"))
+      else if (QKeyValue.FindAttribute(targetAction.ActionDecl.RefinedAction.Attributes, x => x.Key == CivlAttributes.IS2_RIGHT) != null)
       {
-        rule = InductiveSequentializationRule.IS2;
+        rule = InductiveSequentializationRule.ISR;
       }
-      choice = Expr.Ident(invariantAction.ImplWithChoice.OutParams.Last());
-      newPAs = invariantAction.PendingAsyncs.ToDictionary(decl => decl.PendingAsyncType,
-        decl => (Variable)civlTypeChecker.LocalVariable($"newPAs_{decl.Name}", decl.PendingAsyncMultisetType));
     }
 
     private List<Declaration> GenerateTTChecker(Action act)
@@ -581,7 +581,7 @@ protected override List<Declaration> GenerateCheckers()
       {
         decls.AddRange(GenerateStepChecker(elim));
       }
-      if (rule == InductiveSequentializationRule.IS2)
+      if (QKeyValue.FindAttribute(targetAction.ActionDecl.RefinedAction.Attributes, x => x.Key == CivlAttributes.IS2_RIGHT) != null)
       {
         decls.AddRange(GenerateTTChecker(targetAction));
         foreach (var elim in eliminatedActions)

diff --git a/Test/civl/inductive-sequentialization/snapshot-IS2-part.bpl b/Test/civl/inductive-sequentialization/snapshot-IS2-part.bpl
@@ -17,7 +17,7 @@ var {:layer 0,2} r1: [Tid][int]StampedValue;
 
 // M =  main_f , \elim = read_f, I = Inv, M' = main_f'
 action {:layer 1} main_f({:linear_in} tid: One Tid)
-refines {:IS2_right} main_f' using right_Inv;
+refines {:IS2_right} main_f' using Inv;
 creates read_f;
 {
     assume {:add_to_pool "A", 0} true;
@@ -58,7 +58,7 @@ modifies mem;
     mem[i] := StampedValue(x->ts + 1, v);
 }
 
-action {:layer 1} right_Inv({:linear_in} tid: One Tid)
+action {:layer 1} Inv({:linear_in} tid: One Tid)
 modifies r1;
 creates read_f;
 {