diff --git a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
index 707137ddf5faacb71e98fe298ef49aea0e5c5d49..f311207fe7fa61a1833e37d6bff70f4eb77a779f 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
@@ -1,13 +1,14 @@
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);
- node.replaceBy(eventBcomprehension);
+ 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());
}
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 0f2190c500b259351f805a4008d9036925b43ae9..cf6736babcbacfa1f32c3ce7f992baba6ca67cae 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/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);
@@ -2719,8 +2721,8 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseAIseqExpression(AIseqExpression node) {
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);
diff --git a/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java b/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java
index fd97378d87bfebf1053080b4906985bb9daa5444..e0d860f7124504b885572cd890b133c3ad8d2bee 100644
--- a/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java
+++ b/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);
+ }
+
}
diff --git a/src/test/java/testing/Testing.java b/src/test/java/testing/Testing.java
deleted file mode 100644
index 1ab3f574a914e47edc92e757d40305c715098c42..0000000000000000000000000000000000000000
--- a/src/test/java/testing/Testing.java
+++ /dev/null
@@ -1,47 +0,0 @@
-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);
- }
-}