renaming rules

boogie-org · May 29, 2024 · 75a4515 · 75a4515
1 parent 482bfaf
commit 75a4515
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 9 deletions.
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
@@ -122,7 +122,7 @@ public void TypeCheck()
       CreateSequentializations(actionDecls);
       foreach (var sequentialization in this.sequentializations.Where(x => x.rule == InductiveSequentializationRule.ISR))
       {
-        SEChecker(sequentialization);
+        DChecker(sequentialization);
       }
       AttributeEraser.Erase(this);
       YieldSufficiencyTypeChecker.TypeCheck(this);
@@ -386,14 +386,14 @@ private void CreateSequentializations(HashSet<ActionDecl> actionDecls)
       });
     }
 
-    private void SEChecker(Sequentialization seq)
+    private void DChecker(Sequentialization seq)
     {
       IEnumerable<string> elimActionNames = seq.EliminatedActions.Select(x => x.Name);
       foreach (var act in seq.EliminatedActions)
       {
         IEnumerable<string> createsList = act.ActionDecl.Creates.Select(x => x.ActionName);
         if (createsList.Intersect(elimActionNames).Count() != createsList.Count()){
-          Error(act.ActionDecl, $"SE checker failed for action {act.Name}" );
+          Error(act.ActionDecl, $"D checker failed for action {act.Name}" );
           break;
         }
       }

diff --git a/Source/Concurrency/InductiveSequentialization.cs b/Source/Concurrency/InductiveSequentialization.cs
@@ -43,14 +43,14 @@ protected virtual List<Declaration> GenerateCheckers()
       var decls = new List<Declaration>();
       if (rule == InductiveSequentializationRule.ISR)
       {
-        decls.AddRange(GenerateTTChecker(targetAction));
+        decls.AddRange(GeneratePChecker(targetAction));
         foreach (var elim in eliminatedActions)
         {
           if (elim == targetAction)
           {
             continue;
           }
-          decls.AddRange(GenerateTTChecker(elim));
+          decls.AddRange(GeneratePChecker(elim));
         }
       }
       return decls;
@@ -99,7 +99,7 @@ protected AssertCmd GetCheck(IToken tok, Expr expr, string msg)
       return CmdHelper.AssertCmd(tok, expr, msg);
     }
 
-    protected List<Declaration> GenerateTTChecker(Action act)
+    protected List<Declaration> GeneratePChecker(Action act)
     {
       var cmds = new List<Cmd>();
       var requires = new List<Requires>();
@@ -136,7 +136,7 @@ protected List<Declaration> GenerateTTChecker(Action act)
         exprrhs = Expr.And(exprrhs, expr);
       }
       var finalExpr = Expr.Imp(exprlhs, exprrhs);
-      cmds.Add(GetCheck(act.tok, finalExpr, "TT checker failed"));
+      cmds.Add(GetCheck(act.tok, finalExpr, "P checker failed"));
 
       List<Block> checkerBlocks = new List<Block>(listElim.Count);
       var locals = new List<Variable>();
@@ -159,14 +159,14 @@ protected List<Declaration> GenerateTTChecker(Action act)
           inputExprs.Add(ExprHelper.FieldAccess(Expr.Ident(paLocal), pendingAsyncCtor.InParams[i].Name));
         }
         cmds2.AddRange(outAction.GetGateAsserts(Substituter.SubstitutionFromDictionary(outAction.Impl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2)),
-        $"Gate of {outAction.Name} in TT Checker failed"));
+        $"Gate of {outAction.Name} in P Checker failed"));
 
         var block = BlockHelper.Block($"label_{paName}", cmds2);
         CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, block, ResolutionContext.State.Two);
         checkerBlocks.Add(block);
       }
 
-      string checkerName = civlTypeChecker.AddNamePrefix($"TTChecker_{act.Name}");
+      string checkerName = civlTypeChecker.AddNamePrefix($"PChecker_{act.Name}");
       List<Block> blocks = new List<Block>(listElim.Count + 1);
       blocks.Add(
         BlockHelper.Block(