default set size can be defined by a definition (SET_PREF_DEFAULT_SETSIZE)

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 {

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());
 			}
 		}
 
@@ -94,7 +112,8 @@ public class DefinitionsAnalyser extends DepthFirstAdapter {
 				AIntegerExpression sizeExpr = null;
 				Integer value = null;
 				if (d.getRhs() instanceof AUnaryMinusExpression) {
-					AUnaryMinusExpression minus = (AUnaryMinusExpression) d.getRhs();
+					AUnaryMinusExpression minus = (AUnaryMinusExpression) d
+							.getRhs();
 					sizeExpr = (AIntegerExpression) minus.getExpression();
 					value = -Integer.parseInt(sizeExpr.getLiteral().getText());
 				} else {
@@ -103,7 +122,8 @@ public class DefinitionsAnalyser extends DepthFirstAdapter {
 				}
 				TLC4BGlobals.setMIN_INT(value);
 			} catch (ClassCastException e) {
-				e.printStackTrace();
+				throw new TranslationException(
+						"Unable to determine the MININT from definition SET_PREF_MININT: " + node.getEndPos());
 			}
 		}
 	}

src/test/java/de/tlc4b/exceptions/DefinitionsAnalyserTest.java

+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);
+	}
+	
+}

src/test/java/de/tlc4b/tlc/integration/AnalysisTest.java

+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));
+	}
+	
+}