diff --git a/build.gradle b/build.gradle
index 1567c3d2787dfedd6ee225c88642d6ad3e3d4099..4ed156ddcc2168bee24b47d9c8cf96ebb0d7d6ac 100644
--- a/build.gradle
+++ b/build.gradle
@@ -82,7 +82,7 @@ task jacocoIntegrationTestReport(type: JacocoReport) {
tasks.withType(FindBugs) {
// disable findbugs by default
- // in order to run findbugs type 'gradle tlc4b findbugsMain findbugsTest'
+ // in order to run findbugs type 'gradle build findbugsMain findbugsTest'
task -> enabled = gradle.startParameter.taskNames.contains(task.name)
reports {
diff --git a/src/main/java/de/tlc4b/analysis/DefinitionsAnalyser.java b/src/main/java/de/tlc4b/analysis/DefinitionsAnalyser.java
index 3a6278f4303a509c806178fe69b10fdfdfd4d78b..4164bc3d36b2ae7d7144f6eb42daa6e3c244b6a6 100644
--- a/src/main/java/de/tlc4b/analysis/DefinitionsAnalyser.java
+++ b/src/main/java/de/tlc4b/analysis/DefinitionsAnalyser.java
@@ -14,10 +14,11 @@ import de.be4.classicalb.core.parser.node.AIntervalExpression;
import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.tlc4b.TLC4BGlobals;
+import de.tlc4b.exceptions.TranslationException;
/**
- * @author hansen
- * In this class we search for preferences set in the definitions clause, e.g. minint or maxint.
+ * @author hansen In this class we search for preferences set in the definitions
+ * clause, e.g. minint or maxint.
*/
public class DefinitionsAnalyser extends DepthFirstAdapter {
@@ -34,7 +35,7 @@ public class DefinitionsAnalyser extends DepthFirstAdapter {
HashSet<Node> deferredSets = new HashSet<Node>(machineContext
.getDeferredSets().values());
- findMaxMin();
+ findDefaultSizesInDefinitions();
if (deferredSets.size() == 0)
return;
@@ -74,16 +75,33 @@ public class DefinitionsAnalyser extends DepthFirstAdapter {
}
}
- private void findMaxMin() {
- Node node = machineContext.getDefinitions().get("SET_PREF_MAXINT");
+ private void findDefaultSizesInDefinitions() {
+ Node node = machineContext.getDefinitions().get(
+ "SET_PREF_DEFAULT_SETSIZE");
if (null != node) {
try {
AExpressionDefinitionDefinition d = (AExpressionDefinitionDefinition) node;
AIntegerExpression sizeExpr = (AIntegerExpression) d.getRhs();
int value = Integer.parseInt(sizeExpr.getLiteral().getText());
- TLC4BGlobals.setMAX_INT(value);
+ TLC4BGlobals.setDEFERRED_SET_SIZE(value);
} catch (ClassCastException e) {
+ throw new TranslationException(
+ "Unable to determine the default set size from definition SET_PREF_DEFAULT_SETSIZE: "
+ + node.getEndPos());
+ }
+ }
+ node = machineContext.getDefinitions().get("SET_PREF_MAXINT");
+ if (null != node) {
+ try {
+ AExpressionDefinitionDefinition d = (AExpressionDefinitionDefinition) node;
+ AIntegerExpression sizeExpr = (AIntegerExpression) d.getRhs();
+ int value = Integer.parseInt(sizeExpr.getLiteral().getText());
+ TLC4BGlobals.setMAX_INT(value);
+ } catch (ClassCastException e) {
+ throw new TranslationException(
+ "Unable to determine MAXINT from definition SET_PREF_MAXINT: "
+ + node.getEndPos());
}
}
@@ -93,17 +111,19 @@ public class DefinitionsAnalyser extends DepthFirstAdapter {
AExpressionDefinitionDefinition d = (AExpressionDefinitionDefinition) node;
AIntegerExpression sizeExpr = null;
Integer value = null;
- if (d.getRhs() instanceof AUnaryMinusExpression){
- AUnaryMinusExpression minus = (AUnaryMinusExpression) d.getRhs();
+ if (d.getRhs() instanceof AUnaryMinusExpression) {
+ AUnaryMinusExpression minus = (AUnaryMinusExpression) d
+ .getRhs();
sizeExpr = (AIntegerExpression) minus.getExpression();
- value = - Integer.parseInt(sizeExpr.getLiteral().getText());
- }else{
+ value = -Integer.parseInt(sizeExpr.getLiteral().getText());
+ } else {
sizeExpr = (AIntegerExpression) d.getRhs();
value = Integer.parseInt(sizeExpr.getLiteral().getText());
}
TLC4BGlobals.setMIN_INT(value);
} catch (ClassCastException e) {
- e.printStackTrace();
+ throw new TranslationException(
+ "Unable to determine the MININT from definition SET_PREF_MININT: " + node.getEndPos());
}
}
}
diff --git a/src/test/java/de/tlc4b/exceptions/DefinitionsAnalyserTest.java b/src/test/java/de/tlc4b/exceptions/DefinitionsAnalyserTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..9a986ae228fa3d786a4de6a54eb9d8c02074ca41
--- /dev/null
+++ b/src/test/java/de/tlc4b/exceptions/DefinitionsAnalyserTest.java
@@ -0,0 +1,35 @@
+package de.tlc4b.exceptions;
+
+import static de.tlc4b.util.TestUtil.checkMachine;
+
+import org.junit.Test;
+
+public class DefinitionsAnalyserTest {
+
+
+
+ @Test (expected = TranslationException.class)
+ public void testMaxIntException() throws Exception {
+ String machine = "MACHINE test\n"
+ + "DEFINITIONS SET_PREF_MAXINT == TRUE; \n"
+ + "END";
+ checkMachine(machine);
+ }
+
+ @Test (expected = TranslationException.class)
+ public void testMinIntException() throws Exception {
+ String machine = "MACHINE test\n"
+ + "DEFINITIONS SET_PREF_MININT == TRUE; \n"
+ + "END";
+ checkMachine(machine);
+ }
+
+ @Test (expected = TranslationException.class)
+ public void testDefaultSetSizeException() throws Exception {
+ String machine = "MACHINE test\n"
+ + "DEFINITIONS SET_PREF_DEFAULT_SETSIZE == TRUE; \n"
+ + "END";
+ checkMachine(machine);
+ }
+
+}
diff --git a/src/test/java/de/tlc4b/tlc/integration/AnalysisTest.java b/src/test/java/de/tlc4b/tlc/integration/AnalysisTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..26798e7bd77219669bb09376452b9dad24a50908
--- /dev/null
+++ b/src/test/java/de/tlc4b/tlc/integration/AnalysisTest.java
@@ -0,0 +1,57 @@
+package de.tlc4b.tlc.integration;
+
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.testString;
+import static org.junit.Assert.assertEquals;
+
+import org.junit.Test;
+
+public class AnalysisTest {
+
+ @Test
+ public void testDefaultSizes() throws Exception {
+ String machine = "MACHINE Test\n"
+ + "SETS S \n"
+ + "DEFINITIONS \n"
+ + "SET_PREF_MININT == 7; \n"
+ + "SET_PREF_MAXINT == 8; \n"
+ + "SET_PREF_DEFAULT_SETSIZE == 9; \n"
+ + "PROPERTIES MININT = 7 & MAXINT = 8 & (1=1 => card(S) = 9) \n"
+ + "END";
+ assertEquals(NoError, testString(machine));
+ }
+
+ @Test
+ public void testMinInt() throws Exception {
+ String machine = "MACHINE Test\n"
+ + "SETS S \n"
+ + "DEFINITIONS \n"
+ + "SET_PREF_MININT == 7; \n"
+ + "PROPERTIES MININT = 8 \n"
+ + "END";
+ assertEquals(PropertiesError, testString(machine));
+ }
+
+ @Test
+ public void testMaxInt() throws Exception {
+ String machine = "MACHINE Test\n"
+ + "SETS S \n"
+ + "DEFINITIONS \n"
+ + "SET_PREF_MAXINT == 7; \n"
+ + "PROPERTIES MAXINT = 8 \n"
+ + "END";
+ assertEquals(PropertiesError, testString(machine));
+ }
+
+ @Test
+ public void testDefaultSetSize() throws Exception {
+ String machine = "MACHINE Test\n"
+ + "SETS S \n"
+ + "DEFINITIONS \n"
+ + "SET_PREF_DEFAULT_SETSIZE == 9; \n"
+ + "PROPERTIES (1=1 => card(S) = 10) \n"
+ + "END";
+ assertEquals(PropertiesError, testString(machine));
+ }
+
+}