From 7ebb3951a5e0fc40e90984448a080c41d63e7f27 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Fri, 19 Mar 2021 11:41:26 +0100
Subject: [PATCH] add comments and debug prints
---
src/main/java/de/tla2b/analysis/BOperation.java | 17 +++++++++++------
src/main/java/de/tla2bAst/BAstCreator.java | 2 +-
2 files changed, 12 insertions(+), 7 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 106d7b7..f8e0945 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -64,7 +64,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
.getModuleNode().getVariableDecls()));
evalParams();
+ // System.out.println("Construction B Operation for TLA+ action: " + name);
findUnchangedVariables();
+ // System.out.println(" UNCHANGED = " + unchangedVariables.toString());
separateGuardsAndBeforeAfterPredicates(node);
findAssignments();
}
@@ -186,19 +188,22 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
if (OPCODE_eq == getOpCode(opApplNode.getOperator()
.getName())) {
- ExprOrOpArgNode arg1 = opApplNode.getArgs()[0];
+ ExprOrOpArgNode arg1 = opApplNode.getArgs()[0]; // we have equality arg1 = RHS
try {
OpApplNode arg11 = (OpApplNode) arg1;
if (getOpCode(arg11.getOperator().getName()) == OPCODE_prime) {
OpApplNode v = (OpApplNode) arg11.getArgs()[0];
SymbolNode var = v.getOperator();
+ // we have equality var' = RHS
if (!primedVariablesFinder
.getTwiceUsedVariables().contains(var)) {
- // var is only used once in all before after
- // predicates
+ // var' is only used once in all before after predicates
+ // meaning we do not need it as parameter of the ANY
+ // and can add an assignment var := RHS
assignments.put(v.getOperator(),
- opApplNode.getArgs()[1]);
+ opApplNode.getArgs()[1]); // RHS of assignment
beforeAfterPredicates.remove(node);
+ // System.out.println("Detected assignment " + var.getName().toString() + "' = <RHS>");
}
}
@@ -241,8 +246,8 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
return;
}
default: {
- if (opApplNode.level < 2) {
- guards.add(node);
+ if (opApplNode.level < 2) {
+ guards.add(node); // should we be checking nonLeibnizParams is empty ?
return;
} else {
beforeAfterPredicates.add(node);
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 8fd68c5..663673f 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -2186,8 +2186,8 @@ public class BAstCreator extends BuiltInOPs
break;
}
case OPCODE_unchanged: {
- // System.out.println("hier");
OpApplNode node = (OpApplNode) n.getArgs()[0];
+ // System.out.println(" Translating UNCHANGED : " + node.toString());
if (node.getOperator().getKind() == VariableDeclKind) {
AEqualPredicate equal = new AEqualPredicate();
equal.setLeft(createIdentifierNode(getName(node.getOperator()) + "_n"));
--
GitLab