diff --git a/build.gradle b/build.gradle
index ae55582921f58b2eaf4d2514da3c0d61ae40631e..aab9a6c50521608620eeb37c80f924b184c2260a 100644
--- a/build.gradle
+++ b/build.gradle
@@ -31,6 +31,7 @@ def tlatools_version = '1.0.2-SNAPSHOT'
dependencies {
//compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
+ compile 'commons-cli:commons-cli:1.2'
compile (group: 'de.hhu.stups', name: 'tlatools', version: tlatools_version)
compile (group: 'de.hhu.stups', name: 'prologlib', version: parser_version)
@@ -123,6 +124,9 @@ signing {
sign configurations.archives
}
+javadoc {
+ failOnError = false
+}
task javadocJar(type: Jar) {
classifier = 'javadoc'
diff --git a/src/main/java/de/tlc4b/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java
index 76ef31d8a560291e45f9a4c05c0a26684e422b7d..15f51f4c6d8e1b4309e537e68387ef55ddc95ba1 100644
--- a/src/main/java/de/tlc4b/analysis/StandardMadules.java
+++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java
@@ -4,7 +4,6 @@ import java.util.ArrayList;
import java.util.HashSet;
import java.util.Set;
-import de.tlc4b.prettyprint.TLAPrinter;
public final class StandardMadules {
@@ -199,8 +198,8 @@ public final class StandardMadules {
public static final String FINITE_SUBSETS = "Fin";
public static final String FINITE_1_SUBSETS = "Fin1";
public static final String B_POWER_Of = "BPowerOf";
- public static final String B_MODULO = "BModulo";
- public static final String B_DIVISION = "BDivision";
+ public static final String B_MODULO = "BModulo";
+ public static final String B_DIVISION = "BDivision";
public static final String GENERAL_SUMMATION = "Sigma";
public static final String GENERAL_PRODUCT = "Pi";
@@ -234,7 +233,7 @@ public final class StandardMadules {
return Relations.contains(name);
}
- /**
+ /*
* External Functions
*
* All external functions must be defined in the standard module
@@ -244,8 +243,6 @@ public final class StandardMadules {
* ((STRING*STRING) --> (INTEGER<->STRING));) is not mandatory.
*
* The B definitions will be ignored in the {@link TLAPrinter}.
- *
- *
*/
public static final String EXTERNAL_printf = "printf";
@@ -269,8 +266,7 @@ public final class StandardMadules {
}
public static boolean isAbstractConstant(String name) {
- if (name.equals(SORT_SET)
- || name.equals(DECIMAL_TO_INT)) {
+ if (name.equals(SORT_SET) || name.equals(DECIMAL_TO_INT)) {
return true;
} else {
return false;
diff --git a/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java
index 068edbc5591a31f3dde4969f8085d5f566d10ac0..d772860df8b19a9c17fb5e5bd8ab8e9465b41361 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java
@@ -17,35 +17,32 @@ import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.Start;
/**
- * This class only collects all Definitions of a Machine. Definitions of other files which are included are not contained.
- *
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- *
+ * This class only collects all Definitions of a Machine. Definitions of other
+ * files which are included are not contained.
*/
-
public class DefinitionCollector extends DepthFirstAdapter {
private Hashtable<String, PDefinition> definitionsTable;
private ADefinitionsMachineClause definitionsMachineClause;
- public Hashtable<String, PDefinition> getDefinitions(){
+ public Hashtable<String, PDefinition> getDefinitions() {
return new Hashtable<String, PDefinition>(definitionsTable);
}
- public ADefinitionsMachineClause getDefinitionsMachineClause(){
+
+ public ADefinitionsMachineClause getDefinitionsMachineClause() {
return this.definitionsMachineClause;
}
-
+
public DefinitionCollector(Start tree) {
definitionsTable = new Hashtable<String, PDefinition>();
tree.apply(this);
}
-
+
@Override
public void inADefinitionsMachineClause(ADefinitionsMachineClause node) {
this.definitionsMachineClause = node;
}
-
@Override
public void caseAPredicateDefinitionDefinition(
@@ -86,7 +83,6 @@ public class DefinitionCollector extends DepthFirstAdapter {
public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
}
-
@Override
public void caseAInitialisationMachineClause(
AInitialisationMachineClause node) {
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
index 2aa937b98f315efbca0e6c767f1262b185033a83..7424d4605840cfa845982e802a31adf47266278d 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
@@ -21,23 +21,19 @@ import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.Start;
-/**
+/*
* This class performs an AST transformation on set comprehension nodes. For
* example the expression {a,b| a = b & b : 1..10} will be replaced by the
* Event-B set comprehension {b. b : 1..10 | b |-> b}. Moreover, if the parent
* of a set comprehension is a domain expression, this will also be used for the
* optimization, e.g. {a,b| a = b + 1 & b : 1..10} will be replaced by {b. b :
* 1..10 | b + 1}
- *
- * @author hansen
- *
*/
public class SetComprehensionOptimizer extends DepthFirstAdapter {
/**
* The method called by the translator.
- *
- * @param start
+ * @param start start node of abstract syntax tree
*/
public static void optimizeSetComprehensions(Start start) {
SetComprehensionOptimizer optimizer = new SetComprehensionOptimizer();
@@ -166,8 +162,8 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
if (node instanceof ADomainExpression) {
ArrayList<ADomainExpression> domExprList = collectParentDomainExpression(node
.parent());
- domExprList.add(0, (ADomainExpression) node); // prepend the
- // node
+ // prepend the node
+ domExprList.add(0, (ADomainExpression) node);
return domExprList;
} else {
return new ArrayList<ADomainExpression>();
@@ -289,11 +285,11 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
}
}
}
-
+
@Override
public void caseAIdentifierExpression(AIdentifierExpression node) {
String name = Utils.getIdentifierAsString(node.getIdentifier());
- //todo the name is not a unique of the node
+ // todo the name is not a unique of the node
PExpression value = values.get(name);
if (value != null) {
node.replaceBy((PExpression) value.clone());
diff --git a/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
index 0fe4427460cf29570ccf039f0151eeb4d5e1d901..3713b6730830c3ac506fe2cdac34daa5e572b8d5 100644
--- a/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
+++ b/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
@@ -36,9 +36,6 @@ import de.tlc4b.exceptions.SubstitutionException;
* assignments for each node inside a operation body. Missing variables
* assignments correspond to unchanged variables in TLA+. B definitions or the
* initialisation are not visited by this class.
- *
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- *
*/
public class UnchangedVariablesFinder extends DepthFirstAdapter {
diff --git a/src/main/java/de/tlc4b/tla/TLAModule.java b/src/main/java/de/tlc4b/tla/TLAModule.java
index a13cd764ab42dd15c35142803dd65ec61d2159b7..d373d37c99b9e9a37afb1e0b5cdb3ca9f4d5ee46 100644
--- a/src/main/java/de/tlc4b/tla/TLAModule.java
+++ b/src/main/java/de/tlc4b/tla/TLAModule.java
@@ -4,8 +4,6 @@ import java.util.ArrayList;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.POperation;
-import de.tlc4b.analysis.DefinitionsSorter;
-import de.tlc4b.analysis.MachineContext;
public class TLAModule {
diff --git a/src/test/resources/basics/BBuiltInsTest.mch b/src/test/resources/basics/BBuiltInsTest.mch
index 5fc7a79942d74518e1d0b7da0fa21d7336b1abed..629ba6b8f2b54f966e233bb3f0231267654b0e08 100644
--- a/src/test/resources/basics/BBuiltInsTest.mch
+++ b/src/test/resources/basics/BBuiltInsTest.mch
@@ -34,6 +34,10 @@ PROPERTIES
& FIN1({1}) = {{1}}
& FIN1({1,2}) = {{1}, {2}, {1,2}}
+/* generalised intersection over sets of sets */
+& inter({{1},{1,2},{1,3}}) = {1}
+& inter({{1},{2},{1,3}}) = {}
+
/* Quantified intersection */
& INTER(z).(z: {1,2}| {z}) = {}
& INTER(x1).(x1: {2,4}| {y1 | y1 : 0..10 & y1 <= x1}) = {0,1,2}