diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 2a0a2e8d992a6a5e22b35a7b520be41a585190ad..d849dede3ff1b616fcffca3b01be583fcd8f098b 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -53,6 +53,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
private final ArrayList<ExprOrOpArgNode> beforeAfterPredicates;
private LinkedHashMap<SymbolNode, ExprOrOpArgNode> assignments = new LinkedHashMap<SymbolNode, ExprOrOpArgNode>();
private List<OpDeclNode> anyVariables;
+ private final SpecAnalyser specAnalyser;
final int SUBSTITUTE_PARAM = 29;
@@ -61,6 +62,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
this.name = name;
this.node = n;
this.existQuans = existQuans;
+ this.specAnalyser = specAnalyser;
this.unchangedVariablesList = new ArrayList<OpDeclNode>();
this.guards = new ArrayList<ExprOrOpArgNode>();
this.beforeAfterPredicates = new ArrayList<ExprOrOpArgNode>();
@@ -74,7 +76,6 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
public AOperation getBOperation(BAstCreator bASTCreator) {
-
AOperation operation = new AOperation();
List<PExpression> paramList = new ArrayList<PExpression>();
ArrayList<PPredicate> whereList = new ArrayList<PPredicate>();
@@ -214,7 +215,14 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
}
}
+ anyVariables = new ArrayList<OpDeclNode>();
+ for (OpDeclNode var : specAnalyser.getModuleNode().getVariableDecls()) {
+ anyVariables.add(var);
+ }
+// for (SymbolNode symbol : primedVariablesFinder.getAllVariables()) {
+// anyVariables.add((OpDeclNode) symbol);
+// }
anyVariables.removeAll(assignments.keySet());
}
@@ -305,7 +313,6 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
private void findUnchangedVariables() {
unchangedVariables = new ArrayList<String>();
findUnchangedVaribalesInSemanticNode(node);
- anyVariables.removeAll(unchangedVariablesList);
}
/**
@@ -387,7 +394,7 @@ class PrimedVariablesFinder extends AbstractASTVisitor {
this.all = new HashSet<SymbolNode>();
this.twiceUsedVariables = new HashSet<SymbolNode>();
this.table = new Hashtable<SemanticNode, Set<SymbolNode>>();
-
+
for (ExprOrOpArgNode exprOrOpArgNode : list) {
findPrimedVariables(exprOrOpArgNode);
}
@@ -404,7 +411,7 @@ class PrimedVariablesFinder extends AbstractASTVisitor {
case OPCODE_prime: // prime
{
- if (n.getArgs()[0] instanceof OpApplNode){
+ if (n.getArgs()[0] instanceof OpApplNode) {
OpApplNode varNode = (OpApplNode) n.getArgs()[0];
SymbolNode var = varNode.getOperator();
@@ -429,4 +436,7 @@ class PrimedVariablesFinder extends AbstractASTVisitor {
return this.twiceUsedVariables;
}
+ public Set<SymbolNode> getAllVariables() {
+ return this.all;
+ }
}
diff --git a/src/main/java/de/tla2b/translation/BMacroHandler.java b/src/main/java/de/tla2b/translation/BMacroHandler.java
index 21443fb9aed69c4ae5206561b762d7bb1c18bd76..6ef40fabb0796e0702235ba80beaa65a7bb5967d 100644
--- a/src/main/java/de/tla2b/translation/BMacroHandler.java
+++ b/src/main/java/de/tla2b/translation/BMacroHandler.java
@@ -41,16 +41,6 @@ public class BMacroHandler extends AbstractASTVisitor {
}
visitAssumptions(moduleNode.getAssumptions());
-
- for (BOperation op : specAnalyser.getBOperations()) {
- definitionParameters = new HashSet<FormalParamNode>();
- localVariables = new HashSet<FormalParamNode>();
-
- visitExprNode(op.getNode());
-
- definitionParameters = null;
- localVariables = null;
- }
}
private HashSet<FormalParamNode> definitionParameters;
@@ -97,10 +87,6 @@ public class BMacroHandler extends AbstractASTVisitor {
case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
{
- ExprNode[] in = n.getBdedQuantBounds();
- for (ExprNode exprNode : in) {
- visitExprNode(exprNode);
- }
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
HashSet<FormalParamNode> set = new HashSet<FormalParamNode>();
@@ -111,6 +97,10 @@ public class BMacroHandler extends AbstractASTVisitor {
}
}
localVariables.addAll(set);
+ ExprNode[] in = n.getBdedQuantBounds();
+ for (ExprNode exprNode : in) {
+ visitExprNode(exprNode);
+ }
ExprOrOpArgNode[] arguments = n.getArgs();
for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
visitExprOrOpArgNode(exprOrOpArgNode);
@@ -126,7 +116,7 @@ public class BMacroHandler extends AbstractASTVisitor {
}
}
-
+
private Set<String> getStringSet(Set<FormalParamNode> set) {
HashSet<String> stringSet = new HashSet<String>();
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 3366bc9e3ab857f6c9af06879dcdb9c3fadccf2a..d4da3ff1316d91a0789f08386dd68f26c501834f 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -442,7 +442,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
valueList);
any.setThen(assign);
operation.setOperationBody(any);
- //opList.add(operation);
+ // opList.add(operation);
opList.add(op.getBOperation(this));
}
@@ -823,7 +823,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
.getToolObject(SUBSTITUTE_PARAM);
if (e == null) {
if (recursiveFunctionHandler.isRecursiveFunction(param)) {
- ArrayList<SymbolNode> list = recursiveFunctionHandler.getAdditionalParams(param);
+ ArrayList<SymbolNode> list = recursiveFunctionHandler
+ .getAdditionalParams(param);
if (list.size() > 0) {
AFunctionExpression call = new AFunctionExpression();
call.setIdentifier(createIdentifierNode(param));
@@ -903,7 +904,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
if (specAnalyser.getRecursiveFunctions().contains(def)) {
- ArrayList<SymbolNode> list = recursiveFunctionHandler.getAdditionalParams(def);
+ ArrayList<SymbolNode> list = recursiveFunctionHandler
+ .getAdditionalParams(def);
if (list.size() > 0) {
AFunctionExpression call = new AFunctionExpression();
call.setIdentifier(createIdentifierNode(def));
@@ -1426,13 +1428,14 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
lambda.setExpression(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
if (recursiveFunctionHandler.isRecursiveFunction(n)) {
-
- ArrayList<SymbolNode> externParams = recursiveFunctionHandler.getAdditionalParams(n);
- if(externParams.size()>0){
+
+ ArrayList<SymbolNode> externParams = recursiveFunctionHandler
+ .getAdditionalParams(n);
+ if (externParams.size() > 0) {
ALambdaExpression lambda2 = new ALambdaExpression();
ArrayList<PExpression> shiftedParams = new ArrayList<PExpression>();
List<PPredicate> predList2 = new ArrayList<PPredicate>();
- for (SymbolNode p :externParams) {
+ for (SymbolNode p : externParams) {
shiftedParams.add(createIdentifierNode(p));
AMemberPredicate member = new AMemberPredicate();
@@ -1952,8 +1955,30 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
case OPCODE_unchanged: {
- return new AEqualPredicate(new ABooleanTrueExpression(),
- new ABooleanTrueExpression());
+ OpApplNode node = (OpApplNode) n.getArgs()[0];
+ if (node.getOperator().getKind() == VariableDeclKind) {
+ AEqualPredicate equal = new AEqualPredicate();
+ equal.setLeft(createIdentifierNode(getName(node.getOperator())
+ + "_n"));
+ equal.setRight(createIdentifierNode(node.getOperator()));
+ return equal;
+ } else if (node.getOperator().getKind() == UserDefinedOpKind) {
+ OpDefNode operator = (OpDefNode) node.getOperator();
+ ExprNode e = operator.getBody();
+ OpApplNode opApplNode = (OpApplNode) e;
+ node = opApplNode;
+ }
+
+ ArrayList<PPredicate> list = new ArrayList<PPredicate>();
+ for (int i = 0; i < node.getArgs().length; i++) {
+ OpApplNode var = (OpApplNode) node.getArgs()[i];
+ AEqualPredicate equal = new AEqualPredicate();
+ equal.setLeft(createIdentifierNode(getName(var.getOperator())
+ + "_n"));
+ equal.setRight(createIdentifierNode(var.getOperator()));
+ list.add(equal);
+ }
+ return createConjunction(list);
}
case OPCODE_uc: { // CHOOSE x : P
diff --git a/src/test/resources/prettyprint/OperationsTest/OperationsTest.mch b/src/test/resources/prettyprint/OperationsTest/OperationsTest.mch
index 7d8c2bc85a39abb63edfc6e6a3d3a9580da6d8b2..de6fddd4f7891dfd24e344879dc8bf8663bd231d 100644
--- a/src/test/resources/prettyprint/OperationsTest/OperationsTest.mch
+++ b/src/test/resources/prettyprint/OperationsTest/OperationsTest.mch
@@ -5,15 +5,15 @@ INVARIANT
INITIALISATION
a, b, c:((a = 1 & b = 2) & c = 3)
OPERATIONS
- begin1 = BEGIN skip END;
+ begin1 = BEGIN a,b,c := 1,2,3 END;
- begin2 = BEGIN a,b,c := 1,2,3 END;
+ any1 = ANY a_n, b_n, c_n WHERE (((a_n : INTEGER & b_n : INTEGER) & c_n : INTEGER) & a_n + 1 = 2) & (b_n = b & c_n = c) THEN a,b,c := a_n,b_n,c_n END;
- any1 = ANY a_n WHERE (a_n : INTEGER & a_n + 1 = 2) & TRUE = TRUE THEN a := a_n END;
+ any2 = ANY a_n, b_n, c_n WHERE ((((1 = 1 & a_n : INTEGER) & b_n : INTEGER) & c_n : INTEGER) & a_n + 1 = 2) & (b_n = b & c_n = c) THEN a,b,c := a_n,b_n,c_n END;
- any2 = ANY a_n WHERE ((1 = 1 & a_n : INTEGER) & a_n + 1 = 2) & TRUE = TRUE THEN a := a_n END;
+ any3 = ANY a_n, b_n, c_n WHERE ((((a_n : INTEGER & b_n : INTEGER) & c_n : INTEGER) & a_n = 2) & a_n > 1) & (b_n = b & c_n = c) THEN a,b,c := a_n,b_n,c_n END;
- any3 = ANY a_n WHERE ((a_n : INTEGER & a_n = 2) & a_n > 1) & TRUE = TRUE THEN a := a_n END;
+ any4 = ANY a_n, b_n, c_n WHERE ((a_n : INTEGER & b_n : INTEGER) & c_n : INTEGER) & ((a_n = a & b_n = b) & c_n = c) THEN a,b,c := a_n,b_n,c_n END;
select = SELECT 1 = 1 THEN a,b,c := 1,2,3 END
-END
+END
\ No newline at end of file
diff --git a/src/test/resources/prettyprint/OperationsTest/OperationsTest.tla b/src/test/resources/prettyprint/OperationsTest/OperationsTest.tla
index 6ba867cafcef0d110efa12a5141af9720017d7ac..2c89bf8f8f33e8bee7b62813316d477cb7508a75 100644
--- a/src/test/resources/prettyprint/OperationsTest/OperationsTest.tla
+++ b/src/test/resources/prettyprint/OperationsTest/OperationsTest.tla
@@ -3,20 +3,20 @@ EXTENDS Naturals
VARIABLES a,b,c
Init == a = 1 /\ b = 2 /\ c =3
-begin1 == UNCHANGED<<a,b,c>>
-begin2 == a' = 1 /\ b' = 2 /\ c' = 3
+
+begin1 == a' = 1 /\ b' = 2 /\ c' = 3
any1 == a' + 1 = 2 /\ UNCHANGED<<b,c>>
any2 == 1 = 1 /\ a' + 1 = 2 /\ UNCHANGED<<b,c>>
any3 == a'= 2 /\ a' >1 /\ UNCHANGED<<b,c>>
-
+any4 == UNCHANGED<<a,b,c>>
select == 1 = 1 /\ a' = 1 /\ b' = 2 /\ c' =3
Next ==
\/ begin1
- \/ begin2
\/ any1
\/ any2
\/ any3
+ \/ any4
\/ select
=================================
\ No newline at end of file