Added an additional check to the AST transformer in order to prevent a unsound translation

src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java

 package de.tlc4b.analysis.transformation;
 
 import java.util.ArrayList;
+import java.util.HashSet;
 import java.util.Hashtable;
 import java.util.LinkedList;
+import java.util.List;
 import java.util.Set;
 
 import de.be4.classicalb.core.parser.Utils;
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
-import de.be4.classicalb.core.parser.node.ABooleanTrueExpression;
 import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
 import de.be4.classicalb.core.parser.node.AConjunctPredicate;
 import de.be4.classicalb.core.parser.node.ACoupleExpression;
@@ -20,7 +21,6 @@ import de.be4.classicalb.core.parser.node.Node;
 import de.be4.classicalb.core.parser.node.PExpression;
 import de.be4.classicalb.core.parser.node.PPredicate;
 import de.be4.classicalb.core.parser.node.Start;
-import de.tlc4b.util.UtilMethods;
 
 /**
  * This class performs an AST transformation on set comprehension nodes. For
@@ -47,6 +47,7 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
 
 	@Override
 	public void caseAComprehensionSetExpression(AComprehensionSetExpression node) {
+
 		final LinkedList<PExpression> identifiers = node.getIdentifiers();
 		final ArrayList<String> list = new ArrayList<String>();
 		final Hashtable<String, AIdentifierExpression> identifierTable = new Hashtable<String, AIdentifierExpression>();
@@ -77,7 +78,6 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
 		// If these conditions are not fulfilled, the AST transformation will
 		// not be applied.
 		// However, other optimization techniques may be applicable.
-
 		if ((values.size() > 0 || parentDomainExprsList.size() > 0)
 				&& values.size() < list.size()
 				&& list.size() - values.size() <= 2) {
@@ -139,10 +139,18 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
 			member.setRight(compre);
 
 			eventBcomprehension.setPredicates(member);
+			setSourcePosition(node, eventBcomprehension);
+			if (parentDomainExprsList.size() > 0) {
+				ADomainExpression aDomainExpression = parentDomainExprsList
+						.get(max - 1);
+				aDomainExpression.replaceBy(eventBcomprehension);
+			} else {
 				node.replaceBy(eventBcomprehension);
+			}
 			// eventBcomprehension.apply(this);
+		} else {
+			// node.getPredicates().apply(this);
 		}
-
 	}
 
 	/**
@@ -159,7 +167,8 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
 		if (node instanceof ADomainExpression) {
 			ArrayList<ADomainExpression> domExprList = collectParentDomainExpression(node
 					.parent());
-			domExprList.set(0, (ADomainExpression) node); // prepend the node
+			domExprList.add(0, (ADomainExpression) node); // prepend the
+															// node
 			return domExprList;
 		} else {
 			return new ArrayList<ADomainExpression>();
@@ -186,10 +195,11 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
 				AIdentifierExpression id = (AIdentifierExpression) equal
 						.getLeft();
 				String name = Utils.getIdentifierAsString(id.getIdentifier());
-
+				Set<String> names = new HashSet<String>(values.keySet());
+				names.add(name);
 				if (list.contains(name)
 						&& !DependenciesDetector.expressionContainsIdentifier(
-								equal.getRight(), values.keySet())) {
+								equal.getRight(), names)) {
 					equalList.add(equal);
 					values.put(name, equal.getRight());
 				}
@@ -198,9 +208,11 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
 				AIdentifierExpression id = (AIdentifierExpression) equal
 						.getRight();
 				String name = Utils.getIdentifierAsString(id.getIdentifier());
+				Set<String> names = new HashSet<String>(values.keySet());
+				names.add(name);
 				if (list.contains(name)
 						&& !DependenciesDetector.expressionContainsIdentifier(
-								equal.getLeft(), values.keySet())) {
+								equal.getLeft(), names)) {
 					equalList.add(equal);
 					values.put(name, equal.getLeft());
 				}

src/main/java/de/tlc4b/prettyprint/TLAPrinter.java

@@ -1892,7 +1892,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 		}
 	}
 
-	private boolean isElementOfRecursive(Node node) {
+	private boolean recursiveIsElementOfTest(Node node) {
 		Node parent = node.parent();
 		if (parent instanceof AMemberPredicate
 				&& !typeRestrictor.isARemovedNode(parent)
@@ -1900,8 +1900,10 @@ public class TLAPrinter extends DepthFirstAdapter {
 			return true;
 		} else {
 			String clazz = parent.getClass().getName();
+			// todo include all expressions which have an "element of"
+			// translation
 			if (clazz.contains("Total") || clazz.contains("Partial")) {
-				return isElementOfRecursive(node.parent());
+				return recursiveIsElementOfTest(node.parent());
 			} else
 				return false;
 		}
@@ -1914,7 +1916,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 		if (subtype instanceof FunctionType) {
 			moduleStringAppend(funcName);
 		} else {
-			if (isElementOfRecursive(node)) {
+			if (recursiveIsElementOfTest(node)) {
 				moduleStringAppend(relEleOfName);
 			} else {
 				moduleStringAppend(relName);
@@ -1973,7 +1975,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 				moduleStringAppend(funcName);
 			}
 		} else {
-			if (isElementOfRecursive(node)) {
+			if (recursiveIsElementOfTest(node)) {
 				moduleStringAppend(relEleOfName);
 			} else {
 				moduleStringAppend(relName);
@@ -2720,7 +2722,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 		SetType set = (SetType) typechecker.getType(node);
 		if (set.getSubtype() instanceof SetType) {
 
-			if (isElementOfRecursive(node.parent())
+			if (recursiveIsElementOfTest(node.parent())
 					&& !typeRestrictor.isARemovedNode(node.parent())) {
 				moduleStringAppend(REL_INJECTIVE_SEQUENCE_ELEMENT_OF);
 			} else {
@@ -2743,15 +2745,13 @@ public class TLAPrinter extends DepthFirstAdapter {
 	public void caseAIseq1Expression(AIseq1Expression node) {
 		SetType set = (SetType) typechecker.getType(node);
 		if (set.getSubtype() instanceof SetType) {
-			if (node.parent() instanceof AMemberPredicate
-					&& !typeRestrictor.isARemovedNode(node.parent())) {
+			if (recursiveIsElementOfTest(node)) {
 				moduleStringAppend(REL_INJECTIVE_SEQUENCE_1_ELEMENT_OF);
 			} else {
 				moduleStringAppend(REL_INJECTIVE_SEQUENCE_1);
 			}
 		} else {
-			if (node.parent() instanceof AMemberPredicate
-					&& !typeRestrictor.isARemovedNode(node.parent())) {
+			if (recursiveIsElementOfTest(node)) {
 				moduleStringAppend(INJECTIVE_SEQUENCE_1_ELEMENT_OF);
 			} else {
 				moduleStringAppend(INJECTIVE_SEQUENCE_1);

src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java

@@ -75,4 +75,38 @@ public class SetComprehensionOptimizerTest {
 				+ "======";
 		compare(expected, machine);
 	}
+	
+	@Test
+	public void testDomain() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES dom({x,y|  x : 1..10 & x = y}) /= {} \n" + "END";
+		String expected = "---- MODULE test----\n" 
+				+ "EXTENDS Naturals\n"
+				+ "ASSUME {y: y \\in {y \\in ((1 .. 10)): TRUE}} # {} \n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
+	@Test
+	public void testDoubleDomain() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES dom(dom({a,b,c|  a = 1 & b = 1 & c : 1..10 })) /= {} \n" + "END";
+		String expected = "---- MODULE test----\n" 
+				+ "EXTENDS Naturals\n"
+				+ "ASSUME {1: c \\in {c \\in ((1 .. 10)): TRUE}} # {} \n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
+	@Test
+	public void testSelfDependency() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES {x,y|  y : 1..10 & x = x + 1 -1} /= {} \n" + "END";
+		String expected = "---- MODULE test----\n" 
+				+ "EXTENDS Integers\n"
+				+ "ASSUME {<<x, y>> \\in ((Int) \\times ((1 .. 10))): x = (x + 1) - 1} # {} \n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
 }

src/test/java/testing/Testing.java

-package testing;
-
-import static de.tlc4b.tlc.TLCResults.TLCResult.*;
-
-import java.io.File;
-import java.util.ArrayList;
-
-import org.junit.Test;
-import org.junit.runner.RunWith;
-
-import de.tlc4b.TLC4B;
-import de.tlc4b.tlc.TLCResults.TLCResult;
-import de.tlc4b.util.AbstractParseMachineTest;
-import de.tlc4b.util.PolySuite;
-import de.tlc4b.util.TestPair;
-import de.tlc4b.util.PolySuite.Config;
-import de.tlc4b.util.PolySuite.Configuration;
-
-
-
-@RunWith(PolySuite.class)
-public class Testing extends AbstractParseMachineTest{
-
-	
-	private final File machine;
-
-	public Testing(File machine, TLCResult result) {
-		this.machine = machine;
-	}
-
-	@Test
-	public void testRunTLC() throws Exception {
-		if (!machine.getName().contains("Mch2")) {
-			return;
-		}
-		
-		String[] a = new String[] { machine.getPath() };
-		TLC4B.test(a, false);
-	}
-
-	@Config
-	public static Configuration getConfig() {
-		final ArrayList<TestPair> list = new ArrayList<TestPair>();
-		list.add(new TestPair(NoError, "/Users/hansen/git/thales/EngineeringRules-Generic/"));
-		return getConfiguration(list);
-	}
-}