diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java index c7a1c1c18c1536d098d48048994ad7d1291eee48..d25f0fe674df1cdc01a76c216e00348b473a380a 100644 --- a/src/main/java/de/tla2b/analysis/BOperation.java +++ b/src/main/java/de/tla2b/analysis/BOperation.java @@ -222,7 +222,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants, // anyVariables.add((OpDeclNode) symbol); // } anyVariables.removeAll(assignments.keySet()); - anyVariables.removeAll(unchangedVariablesList); + //anyVariables.removeAll(unchangedVariablesList); } private void separateGuardsAndBeforeAfterPredicates(ExprOrOpArgNode node) { diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java index f718e109222ecbcebc25f9f8728db90de4d68632..0c9cfa33fe86c47f248d92ab74363fdeb9be7b76 100644 --- a/src/main/java/de/tla2bAst/BAstCreator.java +++ b/src/main/java/de/tla2bAst/BAstCreator.java @@ -2354,9 +2354,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, equal.setLeft(createIdentifierNode(getName(node.getOperator()) + "_n")); equal.setRight(createIdentifierNode(node.getOperator())); - return new AEqualPredicate(new ABooleanTrueExpression(), - new ABooleanTrueExpression()); - //return equal; +// return new AEqualPredicate(new ABooleanTrueExpression(), +// new ABooleanTrueExpression()); + return equal; } else if (node.getOperator().getKind() == UserDefinedOpKind) { OpDefNode operator = (OpDefNode) node.getOperator(); ExprNode e = operator.getBody(); @@ -2373,9 +2373,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, equal.setRight(createIdentifierNode(var.getOperator())); list.add(equal); } - //returnNode = createConjunction(list); - returnNode = new AEqualPredicate(new ABooleanTrueExpression(), - new ABooleanTrueExpression()); + returnNode = createConjunction(list); +// returnNode = new AEqualPredicate(new ABooleanTrueExpression(), +// new ABooleanTrueExpression()); break; } case OPCODE_uc: { // CHOOSE x : P diff --git a/src/test/java/de/tla2b/prettyprintb/ActionsTest.java b/src/test/java/de/tla2b/prettyprintb/ActionsTest.java index 869d4234e68d862d8179695e95201546884eda98..1cb55bb7d30450efd05e0d4abb9ec83126ff7c10 100644 --- a/src/test/java/de/tla2b/prettyprintb/ActionsTest.java +++ b/src/test/java/de/tla2b/prettyprintb/ActionsTest.java @@ -21,7 +21,9 @@ public class ActionsTest { + "VARIABLES x, y\n" + "INVARIANT x : INTEGER & y : INTEGER \n" + "INITIALISATION x, y:(x = 1 & y = 1) \n" - + "OPERATIONS Next = BEGIN x := 1 END \n" + + "OPERATIONS \n" + + " Next = ANY y_n WHERE y_n : INTEGER " + + " & y_n = y THEN x,y := 1,y_n END \n" + "END"; compare(expected, module); }