removed unchanged variable from ANY substitutions

src/main/java/de/tla2b/analysis/BOperation.java

@@ -94,15 +94,15 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 			whereList.add(bASTCreator.visitExprOrOpArgNodePredicate(g));
 		}
 
-		ArrayList<PExpression> left = new ArrayList<PExpression>();
-		ArrayList<PExpression> right = new ArrayList<PExpression>();
+		ArrayList<PExpression> leftSideOfAssigment = new ArrayList<PExpression>();
+		ArrayList<PExpression> rightSideOfAssigment = new ArrayList<PExpression>();
 		for (Entry<SymbolNode, ExprOrOpArgNode> entry : assignments.entrySet()) {
-			left.add(bASTCreator.createIdentifierNode(entry.getKey()));
-			right.add(bASTCreator.visitExprOrOpArgNodeExpression(entry
-					.getValue()));
+			leftSideOfAssigment.add(bASTCreator.createIdentifierNode(entry
+					.getKey()));
+			rightSideOfAssigment.add(bASTCreator
+					.visitExprOrOpArgNodeExpression(entry.getValue()));
 		}
 		AAssignSubstitution assign = new AAssignSubstitution();
-
 		if (anyVariables.size() > 0) { // ANY x_n WHERE P THEN A END
 			AAnySubstitution any = new AAnySubstitution();
 			any = new AAnySubstitution();
@@ -117,8 +117,10 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 				TLAType t = (TLAType) var.getToolObject(TYPE_ID);
 				member.setRight(t.getBNode());
 				whereList.add(member);
-				left.add(bASTCreator.createIdentifierNode(var));
-				right.add(BAstCreator.createIdentifierNode(nextName));
+				leftSideOfAssigment.add(bASTCreator.createIdentifierNode(var));
+				rightSideOfAssigment.add(BAstCreator
+						.createIdentifierNode(nextName));
+
 			}
 			any.setIdentifiers(anyParams);
 			whereList.addAll(createBeforeAfterPredicates(bASTCreator));
@@ -139,9 +141,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 			operation.setOperationBody(block);
 		}
 
-		if (left.size() > 0) {
-			assign.setLhsExpression(left);
-			assign.setRhsExpressions(right);
+		if (leftSideOfAssigment.size() > 0) {
+			assign.setLhsExpression(leftSideOfAssigment);
+			assign.setRhsExpressions(rightSideOfAssigment);
 		} else { // skip
 			assign.replaceBy(new ASkipSubstitution());
 		}
@@ -220,6 +222,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 		// anyVariables.add((OpDeclNode) symbol);
 		// }
 		anyVariables.removeAll(assignments.keySet());
+		anyVariables.removeAll(unchangedVariablesList);
 	}
 
 	private void separateGuardsAndBeforeAfterPredicates(ExprOrOpArgNode node) {

src/main/java/de/tla2b/global/TranslationGlobals.java

@@ -10,7 +10,7 @@ import java.util.Arrays;
 import tla2sany.semantic.FrontEnd;
 
 public interface TranslationGlobals {
-	final String VERSION_NUMBER = "1.0.7";
+	final String VERSION_NUMBER = "1.0.8";
 
 	final int TLCValueKind = 100;
 

src/main/java/de/tla2b/types/TupleOrFunction.java

@@ -127,14 +127,16 @@ public class TupleOrFunction extends AbstractHasFollowers {
 			return true;
 		}
 		if (o instanceof TupleType) {
-			TupleType t = (TupleType) o;
-			for (int i = 0; i < t.getTypes().size(); i++) {
-				if (this.types.containsKey(i + 1)) {
-					if (!t.getTypes().get(i).compare(this.types.get(i + 1))) {
+			TupleType tupleType = (TupleType) o;
+			for (Integer index : this.types.keySet()) {
+				if (index >= 1
+						&& index <= tupleType.getTypes().size()
+						&& this.types.get(index).compare(
+								tupleType.getTypes().get(index + -1))) {
+				} else {
 					return false;
 				}
 			}
-			}
 			return true;
 		}
 		if (o instanceof TupleOrFunction) {

src/main/java/de/tla2bAst/BAstCreator.java

@@ -350,81 +350,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		List<POperation> opList = new ArrayList<POperation>();
 		for (int i = 0; i < bOperations.size(); i++) {
 			BOperation op = bOperations.get(i);
-
-			String defName = op.getName();
-
-			List<PExpression> paramList = new ArrayList<PExpression>();
-			ArrayList<PPredicate> whereList = new ArrayList<PPredicate>();
-			for (int j = 0; j < op.getFormalParams().size(); j++) {
-				paramList
-						.add(createIdentifierNode(op.getFormalParams().get(j)));
-			}
-			for (int j = 0; j < op.getExistQuans().size(); j++) {
-				OpApplNode o = op.getExistQuans().get(j);
-				whereList.add(visitBoundsOfLocalVariables(o));
-			}
-
-			AOperation operation = new AOperation();
-			operation.setOpName(createTIdentifierLiteral(defName));
-			operation.setParameters(paramList);
-			operation.setReturnValues(new ArrayList<PExpression>());
-
-			AAnySubstitution any = new AAnySubstitution();
-			OpDeclNode[] vars = moduleNode.getVariableDecls();
-			List<PExpression> anyParams = new ArrayList<PExpression>();
-			for (int j = 0; j < vars.length; j++) {
-				String varName = getName(vars[j]);
-				String nextName = varName + "_n";
-				if (op.getUnchangedVariables().contains(varName))
-					continue;
-				anyParams.add(createIdentifierNode(nextName));
-
-				AMemberPredicate member = new AMemberPredicate();
-				member.setLeft(createIdentifierNode(nextName));
-				TLAType t = (TLAType) vars[j].getToolObject(TYPE_ID);
-				member.setRight(t.getBNode());
-				whereList.add(member);
-			}
-			any.setIdentifiers(anyParams);
-
-			PPredicate body = null;
-			if (op.getNode() instanceof OpApplNode) {
-				OpApplNode opApplNode = (OpApplNode) op.getNode();
-				if (opApplNode.getOperator().getKind() == UserDefinedOpKind
-						&& !BBuiltInOPs.contains(opApplNode.getOperator()
-								.getName())) {
-					OpDefNode def = (OpDefNode) opApplNode.getOperator();
-					FormalParamNode[] params = def.getParams();
-					for (int j = 0; j < params.length; j++) {
-						FormalParamNode param = params[j];
-						param.setToolObject(SUBSTITUTE_PARAM,
-								opApplNode.getArgs()[j]);
-					}
-					body = visitExprNodePredicate(def.getBody());
-				}
-			}
-			if (body == null) {
-				body = visitExprOrOpArgNodePredicate(op.getNode());
-			}
-			whereList.add(body);
-			any.setWhere(createConjunction(whereList));
-
-			List<PExpression> varList = new ArrayList<PExpression>();
-			List<PExpression> valueList = new ArrayList<PExpression>();
-			for (int j = 0; j < vars.length; j++) {
-				String varName = getName(vars[j]);
-				if (op.getUnchangedVariables().contains(varName))
-					continue;
-				varList.add(createIdentifierNode(vars[j]));
-
-				valueList.add(createIdentifierNode(varName + "_n"));
-			}
-			AAssignSubstitution assign = new AAssignSubstitution(varList,
-					valueList);
-			any.setThen(assign);
-			operation.setOperationBody(any);
-			// opList.add(operation);
-
 			opList.add(op.getBOperation(this));
 		}
 
@@ -1601,7 +1526,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 			set.setExpressions(list);
 			union.setExpression(set);
 
-			
 			return union;
 		}
 
@@ -2423,13 +2347,16 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 			break;
 		}
 		case OPCODE_unchanged: {
+			//System.out.println("hier");
 			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;
+				return new AEqualPredicate(new ABooleanTrueExpression(),
+						new ABooleanTrueExpression());
+				//return equal;
 			} else if (node.getOperator().getKind() == UserDefinedOpKind) {
 				OpDefNode operator = (OpDefNode) node.getOperator();
 				ExprNode e = operator.getBody();
@@ -2446,7 +2373,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 				equal.setRight(createIdentifierNode(var.getOperator()));
 				list.add(equal);
 			}
-			returnNode = createConjunction(list);
+			//returnNode = createConjunction(list);
+			returnNode = new AEqualPredicate(new ABooleanTrueExpression(),
+					new ABooleanTrueExpression());
 			break;
 		}
 		case OPCODE_uc: { // CHOOSE x : P

src/test/java/de/tla2b/prettyprintb/EventsTest.java → src/test/java/de/tla2b/prettyprintb/ActionsTest.java

@@ -2,9 +2,10 @@ package de.tla2b.prettyprintb;
 
 import static de.tla2b.util.TestUtil.compare;
 
+import org.junit.Ignore;
 import org.junit.Test;
 
-public class EventsTest {
+public class ActionsTest {
 
 	
 	@Test
@@ -20,7 +21,7 @@ public class EventsTest {
 				+ "VARIABLES x, y\n"
 				+ "INVARIANT x : INTEGER & y : INTEGER \n"
 				+ "INITIALISATION  x, y:(x = 1 & y = 1) \n"
-				+ "OPERATIONS Next = ANY y_n WHERE y_n : INTEGER & y_n = y THEN x,y := 1,y_n END \n"
+				+ "OPERATIONS Next = BEGIN x := 1 END \n"
 				+ "END";
 		compare(expected, module);
 	}

src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java

@@ -6,6 +6,7 @@ import org.junit.Test;
 
 import de.tla2b.exceptions.FrontEndException;
 import de.tla2b.exceptions.TLA2BException;
+import de.tla2b.exceptions.TypeErrorException;
 import de.tla2b.util.TestTypeChecker;
 import de.tla2b.util.TestUtil;
 
@@ -69,6 +70,7 @@ public class TupleVsSequenceTest {
 		assertEquals("INTEGER*INTEGER", t.getConstantType("k"));
 	}
 	
+	
 	@Test  
 	public void testTupleVsSequence6() throws FrontEndException, TLA2BException {
 		final String module = "-------------- MODULE Testing ----------------\n"
@@ -79,4 +81,12 @@ public class TupleVsSequenceTest {
 		assertEquals("INTEGER*INTEGER", t.getConstantType("k"));
 	}
 
+	@Test (expected = TypeErrorException.class)
+	public void testTupleVsSequence7() throws FrontEndException, TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME 1 = <<1,TRUE>>[3] \n"
+				+ "=================================";
+		TestUtil.typeCheckString(module);
+	}
+	
 }