From e5042c81e32e70348232e464f75552ce7ec44fcb Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Sat, 3 Oct 2015 14:50:28 +0200
Subject: [PATCH] update build.grade
---
build.gradle | 4 ++++
.../de/tlc4b/analysis/StandardMadules.java | 12 ++++--------
.../transformation/DefinitionCollector.java | 18 +++++++-----------
.../SetComprehensionOptimizer.java | 16 ++++++----------
.../UnchangedVariablesFinder.java | 3 ---
src/main/java/de/tlc4b/tla/TLAModule.java | 2 --
src/test/resources/basics/BBuiltInsTest.mch | 4 ++++
7 files changed, 25 insertions(+), 34 deletions(-)
diff --git a/build.gradle b/build.gradle
index ae55582..aab9a6c 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 76ef31d..15f51f4 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 068edbc..d772860 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 2aa937b..7424d46 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 0fe4427..3713b67 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 a13cd76..d373d37 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 5fc7a79..629ba6b 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}
--
GitLab