From 4cd409aee5d51bed37baaebd833f92f6767edf23 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 11 Dec 2015 22:30:39 +0100
Subject: [PATCH] fixed bug
---
src/main/java/de/tla2b/analysis/BOperation.java | 2 +-
src/main/java/de/tla2bAst/BAstCreator.java | 12 ++++++------
src/test/java/de/tla2b/prettyprintb/ActionsTest.java | 4 +++-
3 files changed, 10 insertions(+), 8 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index c7a1c1c..d25f0fe 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 f718e10..0c9cfa3 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 869d423..1cb55bb 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);
}
--
GitLab