Improve initial states generation

prism/.classpath

@@ -1,7 +1,12 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <classpath>
 	<classpathentry kind="src" path="src"/>
-	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
+	<classpathentry kind="src" path="unit-tests"/>
+	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER">
+		<attributes>
+			<attribute name="module" value="true"/>
+		</attributes>
+	</classpathentry>
 	<classpathentry kind="lib" path="lib/epsgraphics.jar"/>
 	<classpathentry kind="lib" path="lib/jcommon.jar"/>
 	<classpathentry kind="lib" path="lib/jfreechart.jar" sourcepath="/jfreechart/source"/>
@@ -12,5 +17,6 @@
 	<classpathentry kind="lib" path="lib/jas.jar"/>
 	<classpathentry kind="lib" path="lib/log4j.jar"/>
 	<classpathentry kind="lib" path="lib/nailgun-server.jar"/>
+	<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/5"/>
 	<classpathentry kind="output" path="classes"/>
 </classpath>

prism/Makefile

@@ -14,6 +14,7 @@
 # If this is a problem, the best solution is to create symlinks.
 
 export PRISM_SRC_DIR     = src
+export PRISM_TESTS_DIR   = unit-tests
 export PRISM_CLASSES_DIR = classes
 export PRISM_OBJ_DIR     = obj
 export PRISM_LIB_DIR     = lib
@@ -176,6 +177,7 @@ else
 endif
 LD = $(CXX)
 JAVAC = javac
+JAVA = java
 
 export CC CXX LD JAVAC JAVACC
 
@@ -323,6 +325,7 @@ export CFLAGS CXXFLAGS LDFLAGS JFLAGS LIBPREFIX LIBSUFFIX
 ##########################################
 
 MAKE_DIRS = dd jdd odd dv prism mtbdd sparse hybrid parser settings userinterface pepa/compiler simulator jltl2ba jltl2dstar explicit pta param strat automata common cex
+TEST_DIRS = common
 
 EXT_PACKAGES = lpsolve55 lp_solve_5.5_java
 
@@ -368,7 +371,7 @@ extpackages: checks
 
 # Compile main PRISM code
 # (we also do some preparatory checks, and build launch scripts afterwards)
-prism: checks make_dirs bin_scripts
+prism: checks make_dirs bin_scripts make_tests
 
 # Compile each (top-level) source directory separately
 make_dirs:
@@ -397,6 +400,22 @@ make_dirs:
 		(dos2unix $(PRISM_INCLUDE_DIR)/jni/*.h) \
 	fi;
 
+make_tests:
+	@for dir in $(TEST_DIRS); do \
+	  echo Making $(PRISM_TESTS_DIR)/$$dir ...; \
+	  (cd $(PRISM_TESTS_DIR)/$$dir && \
+	  $(MAKE) \
+	  CUDD_DIR="$(CUDD_DIR)" \
+	  JAVA_INCLUDES="$(JAVA_INCLUDES)" \
+	  JAVA_JNI_H_DIR="$(JAVA_JNI_H_DIR)" \
+	  JAVA_JNI_MD_H_DIR="$(JAVA_JNI_MD_H_DIR)" \
+	  SHARED="$(SHARED)" \
+	  EXE="$(EXE)" \
+	  LIBMATH="$(LIBMATH)" \
+	  CLASSPATHSEP="$(CLASSPATHSEP)") \
+	  || exit 1; \
+	done; \
+
 # Copy/modify the launch scripts and put in the bin directory
 bin_scripts:
 	@for target in $(BIN_TARGETS); do \
@@ -472,6 +491,8 @@ count_loc:
 ###########
 # Testing #
 ###########
+unittests:
+	$(JAVA) -jar lib/junit-platform-console-standalone-1.7.2.jar -cp classes --scan-classpath
 
 # Run a single test case from the test suite (useful quick check that the build was ok)
 test:

prism/src/common/IntSet.java

@@ -3,6 +3,7 @@
 //	Copyright (c) 2016-
 //	Authors:
 //	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Steffen Maercker <steffen.maercker@tu-dresden.de> (TU Dresden)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -27,13 +28,18 @@
 package common;
 
 import java.util.BitSet;
+import java.util.Objects;
+import java.util.PrimitiveIterator;
 import java.util.Spliterator;
 import java.util.Spliterators;
-import java.util.PrimitiveIterator.OfInt;
+import java.util.function.IntPredicate;
 import java.util.stream.IntStream;
 import java.util.stream.StreamSupport;
 
 import common.IterableBitSet;
+import common.iterable.FunctionalPrimitiveIterable;
+import common.iterable.FunctionalPrimitiveIterator;
+import common.iterable.SingletonIterable;
 
 /**
  * Interface for an ordered set of integers that allows efficient
@@ -42,27 +48,24 @@
  * <br>
  * Provides static helpers for wrapping a BitSet or a singleton value.
  */
-public interface IntSet extends Iterable<Integer>
+public interface IntSet extends FunctionalPrimitiveIterable.OfInt
 {
-	/** Return a PrimitiveIterator.OfInt iterator for iteration, normal order */
-	public OfInt iterator();
-
-	/** Return a PrimitiveIterator.OfInt iterator for iteration, reversed order */
-	public OfInt reversedIterator();
+	/** Return a FunctionalPrimitiveIterator.OfInt iterator for iteration, reversed order */
+	FunctionalPrimitiveIterator.OfInt reversedIterator();
 
 	/** Return the cardinality (number of elements) for this set */
-	public int cardinality();
-
-	/** Return true if {@code index} is a member of this set */
-	public boolean contains(int index);
+	default long cardinality()
+	{
+		return count();
+	}
 
 	/**
 	 * Return true if {@code index} is a member of this set
 	 * (convenience method to ease migration from use of BitSet).
 	 * <p>
 	 * <i>Default implementation</i>: Calls contains(index).
 	 */
-	public default boolean get(int index)
+	default boolean get(int index)
 	{
 		return contains(index);
 	}
@@ -74,9 +77,9 @@ public default boolean get(int index)
 	 * <i>Default implementation</i>:
 	 * Tests via contains for all elements of other.
 	 */
-	public default boolean contains(IntSet other)
+	default boolean contains(IntSet other)
 	{
-		return other.stream().allMatch(this::contains);
+		return other.allMatch((IntPredicate) this::contains);
 	}
 
 	/**
@@ -86,7 +89,7 @@ public default boolean contains(IntSet other)
 	 * <i>Default implementation</i>:
 	 * Uses contains(IntSet other).
 	 */
-	public default boolean contains(BitSet other)
+	default boolean contains(BitSet other)
 	{
 		return contains(asIntSet(other));
 	}
@@ -97,23 +100,32 @@ public default boolean contains(BitSet other)
 	 * <i>Default implementation</i>:
 	 * Wrap iterator() into an intStream.
 	 */
-	public default IntStream stream() {
+	default IntStream stream()
+	{
 		return StreamSupport.intStream(
-				() -> Spliterators.spliterator(
-						iterator(), cardinality(),
-						Spliterator.DISTINCT),
+				() -> spliterator(),
 				Spliterator.SIZED | Spliterator.DISTINCT,
 				false);
 	}
 
+	@Override
+	default Spliterator.OfInt spliterator()
+	{
+		return Spliterators.spliterator(
+				iterator(),
+				cardinality(),
+				Spliterator.SIZED | Spliterator.DISTINCT);
+	}
+
 	/** Return this set as a String */
-	public default String asString()
+	@Override
+	default String asString()
 	{
 		// can't overload toString() with a default method in interface
 		StringBuffer sb = new StringBuffer();
 		sb.append("{");
 		boolean first = true;
-		for (OfInt it = iterator(); it.hasNext(); ) {
+		for (PrimitiveIterator.OfInt it = iterator(); it.hasNext(); ) {
 			if (!first)
 				sb.append(",");
 			first = false;
@@ -123,33 +135,36 @@ public default String asString()
 		return sb.toString();
 	}
 
+
+
 	/**
 	 * Wrapper class for obtaining an IntSet from a BitSet.
 	 * <p>
 	 * Note: The BitSet should not be modified as long as the
 	 * derived IntSet is in use.
 	 */
-	public static class IntSetFromBitSet implements IntSet
+	static class IntSetFromBitSet implements IntSet
 	{
 		/** The wrapped BitSet */
-		private BitSet bs;
+		protected BitSet bs;
 		/** The cardinality of the underlying BitSet (cached, -1 = not yet computed) */
 		int cardinality = -1;
 
 		/** Constructor */
 		public IntSetFromBitSet(BitSet bs)
 		{
+			Objects.requireNonNull(bs);
 			this.bs = bs;
 		}
 
 		@Override
-		public OfInt iterator()
+		public FunctionalPrimitiveIterator.OfInt iterator()
 		{
 			return IterableBitSet.getSetBits(bs).iterator();
 		}
 
 		@Override
-		public OfInt reversedIterator()
+		public FunctionalPrimitiveIterator.OfInt reversedIterator()
 		{
 			return IterableBitSet.getSetBitsReversed(bs).iterator();
 		}
@@ -161,7 +176,7 @@ public IntStream stream()
 		}
 
 		@Override
-		public int cardinality()
+		public long count()
 		{
 			// not yet computed?
 			if (cardinality == -1)
@@ -183,86 +198,53 @@ public String toString()
 		}
 	};
 
+
+
 	/** Convenience class for simulating a singleton set */
-	public static class SingletonIntSet implements IntSet
+	static class SingletonIntSet extends SingletonIterable.OfInt implements IntSet
 	{
-		/** The single member of this singleton set */
-		private int singleMember;
-
 		/**
 		 * Constructor.
 		 * @param singleMember the single member of this set
 		 */
 		public SingletonIntSet(int singleMember)
 		{
-			this.singleMember = singleMember;
+			super(singleMember);
 		}
 
 		@Override
-		public OfInt iterator()
-		{
-			return new OfInt() {
-				boolean done = false;
-				@Override
-				public boolean hasNext()
-				{
-					return !done;
-				}
-				@Override
-				public int nextInt()
-				{
-					done = true;
-					return singleMember;
-				}
-			};
-		}
-
-		@Override
-		public OfInt reversedIterator()
+		public FunctionalPrimitiveIterator.OfInt reversedIterator()
 		{
 			// iteration order does not matter for singleton set
 			return iterator();
 		}
 
-		@Override
-		public int cardinality()
-		{
-			return 1;
-		}
-
-		@Override
-		public boolean contains(int index)
-		{
-			return index == singleMember;
-		}
-
 		@Override
 		public String toString()
 		{
-			return "{" + singleMember + "}";
+			return "{" + element + "}";
 		}
-
 	}
 
 	/**
-	 * Static constructor for obtaining an IntSet from a BitSet
+	 * Factory method for obtaining an IntSet from a BitSet
 	 * <p>
 	 * Note: The BitSet should not be modified as long as the derived IntSet is in use.
+	 *
 	 * @param bs The underlying BitSet
 	 */
-	public static IntSet asIntSet(BitSet bs)
+	static IntSet asIntSet(BitSet bs)
 	{
 		return new IntSetFromBitSet(bs);
 	}
 
 	/**
-	 * Static constructor for obtaining an IntSet for a singleton set.
+	 * Factory method for obtaining an IntSet for a singleton set.
+	 *
 	 * @param singleMember The single member of the singleton set
 	 */
-	public static IntSet asIntSet(int singleMember)
+	static IntSet asIntSet(int singleMember)
 	{
 		return new SingletonIntSet(singleMember);
 	}
-
 }
-