Implement unbounded iterations #69

The switch -maxiters recognizes a new argument, 'Infinity' to indicate that the number of iteration should not be bounded. If a number is given, it has to be between zero and Integer.MAX_VALUE. The implementation stores these values as doubles. This allows to stick to comparisons like if(iters < max_iters) as +Infinity compares greater to all integer values.
prismmodelchecker · May 10, 2019 · 6f5b76b · 6f5b76b
1 parent 809f10f
commit 6f5b76b
Show file tree

Hide file tree

Showing 12 changed files with 50 additions and 44 deletions.
diff --git a/prism/include/PrismNativeGlob.h b/prism/include/PrismNativeGlob.h
@@ -114,7 +114,7 @@ EXPORT extern int lin_eq_method;
 EXPORT extern double lin_eq_method_param;
 EXPORT extern int term_crit;
 EXPORT extern double term_crit_param;
-EXPORT extern int max_iters;
+EXPORT extern double max_iters;
 // use "compact modified" sparse matrix storage?
 EXPORT extern bool compact;
 // sparse bits info

diff --git a/prism/include/jni/prism_PrismNative.h b/prism/include/jni/prism_PrismNative.h
diff --git a/prism/include/jni/sparse_PrismSparse.h b/prism/include/jni/sparse_PrismSparse.h
diff --git a/prism/src/explicit/IterationMethod.java b/prism/src/explicit/IterationMethod.java
@@ -401,8 +401,8 @@ protected IterationMethod(boolean absolute, double termCritParam)
 	 */
 	public ModelCheckerResult doValueIteration(ProbModelChecker mc, String description, IterationValIter iteration, IntSet unknownStates, long startTime, ExportIterations iterationsExport) throws PrismException
 	{
+		double maxIters = mc.maxIters;
 		int iters = 0;
-		final int maxIters = mc.maxIters;
 		boolean done = false;
 
 		PeriodicTimer updatesTimer = new PeriodicTimer(ProbModelChecker.UPDATE_DELAY);
@@ -464,9 +464,9 @@ public ModelCheckerResult doValueIteration(ProbModelChecker mc, String descripti
 	public ModelCheckerResult doTopologicalValueIteration(ProbModelChecker mc, String description, SCCInfo sccs, IterationMethod.IterationValIter iterator, SingletonSCCSolver singletonSCCSolver, long startTime, ExportIterations iterationsExport) throws PrismException
 	{
 		// Start iterations
+		double maxIters = mc.maxIters;
 		int iters = 0;
 		long mvCount = 0;
-		final int maxIters = mc.maxIters;
 
 		int numSCCs = sccs.getNumSCCs();
 		int numNonSingletonSCCs = sccs.countNonSingletonSCCs();
@@ -572,8 +572,8 @@ public ModelCheckerResult doTopologicalValueIteration(ProbModelChecker mc, Strin
 	public ModelCheckerResult doIntervalIteration(ProbModelChecker mc, String description, IterationIntervalIter below, IterationIntervalIter above, IntSet unknownStates, long timer, ExportIterations iterationsExport) throws PrismException {
 		try {
 			// Start iterations
+			double maxIters = mc.maxIters;
 			int iters = 0;
-			final int maxIters = mc.maxIters;
 			boolean done = false;
 
 			PeriodicTimer updatesTimer = new PeriodicTimer(ProbModelChecker.UPDATE_DELAY);
@@ -664,9 +664,9 @@ public ModelCheckerResult doIntervalIteration(ProbModelChecker mc, String descri
 	public ModelCheckerResult doTopologicalIntervalIteration(ProbModelChecker mc, String description, SCCInfo sccs, IterationIntervalIter below, IterationIntervalIter above, SingletonSCCSolver singletonSCCSolver, long timer, ExportIterations iterationsExport) throws PrismException {
 		try {
 			// Start iterations
+			double maxIters = mc.maxIters;
 			int iters = 0;
 			long mvCount = 0;
-			final int maxIters = mc.maxIters;
 
 			PeriodicTimer updatesTimer = new PeriodicTimer(ProbModelChecker.UPDATE_DELAY);
 			updatesTimer.start();

diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
@@ -75,7 +75,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	// Parameter for iterative numerical method termination criteria
 	protected double termCritParam = 1e-8;
 	// Max iterations for numerical solution
-	protected int maxIters = 100000;
+	protected double maxIters = 100000;
 	// Use precomputation algorithms in model checking?
 	protected boolean precomp = true;
 	protected boolean prob0 = true;
@@ -219,7 +219,7 @@ public ProbModelChecker(PrismComponent parent) throws PrismException
 			// PRISM_TERM_CRIT_PARAM
 			setTermCritParam(settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM));
 			// PRISM_MAX_ITERS
-			setMaxIters(settings.getInteger(PrismSettings.PRISM_MAX_ITERS));
+			setMaxIters(settings.getDouble(PrismSettings.PRISM_MAX_ITERS));
 			// PRISM_PRECOMPUTATION
 			setPrecomp(settings.getBoolean(PrismSettings.PRISM_PRECOMPUTATION));
 			// PRISM_PROB0
@@ -341,8 +341,9 @@ public void setTermCritParam(double termCritParam)
 	/**
 	 * Set maximum number of iterations for numerical iterative methods.
 	 */
-	public void setMaxIters(int maxIters)
+	public void setMaxIters(double maxIters)
 	{
+		assert maxIters > 0 && maxIters <= Integer.MAX_VALUE && (maxIters == Math.floor(maxIters) || Double.isInfinite(maxIters));
 		this.maxIters = maxIters;
 	}
 
@@ -439,7 +440,7 @@ public double getTermCritParam()
 		return termCritParam;
 	}
 
-	public int getMaxIters()
+	public double getMaxIters()
 	{
 		return maxIters;
 	}

diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java
@@ -749,11 +749,11 @@ protected TileList generateParetoCurve(NondetModel modelProduct, JDDNode yes_one
 	{
 		//TODO this method does not work for more than 2 objectives
 		int numberOfPoints = 0;
-		int rewardStepBounds[] = new int[rewards.size()];
+		double rewardStepBounds[] = new double[rewards.size()];
 		for (int i = 0; i < rewardStepBounds.length; i++)
 			rewardStepBounds[i] = opsAndBounds.getRewardStepBound(i);
 
-		int probStepBounds[] = new int[targets.length];
+		double probStepBounds[] = new double[targets.length];
 		for (int i = 0; i < probStepBounds.length; i++)
 			probStepBounds[i] = opsAndBounds.getProbStepBound(i);
 
@@ -1035,11 +1035,11 @@ protected double targetDrivenMultiReachProbs(NondetModel modelProduct, JDDNode y
 			List<JDDNode> rewards, OpsAndBoundsList opsAndBounds) throws PrismException
 	{
 		int numberOfPoints = 0;
-		int rewardStepBounds[] = new int[rewards.size()];
+		double rewardStepBounds[] = new double[rewards.size()];
 		for (int i = 0; i < rewardStepBounds.length; i++)
 			rewardStepBounds[i] = opsAndBounds.getRewardStepBound(i);
 
-		int probStepBounds[] = new int[targets.length];
+		double probStepBounds[] = new double[targets.length];
 		for (int i = 0; i < probStepBounds.length; i++)
 			probStepBounds[i] = opsAndBounds.getProbStepBound(i);
 
@@ -1145,7 +1145,7 @@ protected double targetDrivenMultiReachProbs(NondetModel modelProduct, JDDNode y
 				//System.out.println("Not doing GS");
 				result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
 						modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), null, null,
-						new NDSparseMatrix[] { rewSparseMatrices[0] }, new double[] { 1.0 }, new int[] { rewardStepBounds[0] });
+						new NDSparseMatrix[] { rewSparseMatrices[0] }, new double[] { 1.0 }, new double[] { rewardStepBounds[0] });
 			}
 			numberOfPoints++;
 

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
@@ -444,9 +444,12 @@ public void setTermCritParam(double d) throws PrismException
 		settings.set(PrismSettings.PRISM_TERM_CRIT_PARAM, d);
 	}
 
-	public void setMaxIters(int i) throws PrismException
+	public void setMaxIters(double d) throws PrismException
 	{
-		settings.set(PrismSettings.PRISM_MAX_ITERS, i);
+		if (! (d > 0 && d <= Integer.MAX_VALUE && (d == Math.floor(d) || Double.isInfinite(d)))) {
+			throw new PrismException("Expected positive integer or 'Infinity'.");
+		}
+		settings.set(PrismSettings.PRISM_MAX_ITERS, d);
 	}
 
 	public void setCUDDMaxMem(String s) throws PrismException
@@ -770,9 +773,9 @@ public double getTermCritParam()
 		return settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM);
 	}
 
-	public int getMaxIters()
+	public double getMaxIters()
 	{
-		return settings.getInteger(PrismSettings.PRISM_MAX_ITERS);
+		return settings.getDouble(PrismSettings.PRISM_MAX_ITERS);
 	}
 
 	public boolean getVerbose()

diff --git a/prism/src/prism/PrismNative.cc b/prism/src/prism/PrismNative.cc
@@ -43,7 +43,7 @@ EXPORT int lin_eq_method;
 EXPORT double lin_eq_method_param;
 EXPORT int term_crit;
 EXPORT double term_crit_param;
-EXPORT int max_iters;
+EXPORT double max_iters;
 // use "compact modified" sparse matrix storage?
 EXPORT bool compact;
 // sparse bits info
@@ -124,9 +124,9 @@ JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetTermCritParam(JNIEnv *env,
 
 //------------------------------------------------------------------------------
 
-JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetMaxIters(JNIEnv *env, jclass cls, jint i)
+JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetMaxIters(JNIEnv *env, jclass cls, jdouble d)
 {
-	max_iters = i;
+	max_iters = d;
 }
 
 //------------------------------------------------------------------------------

diff --git a/prism/src/prism/PrismNative.java b/prism/src/prism/PrismNative.java
@@ -105,10 +105,11 @@ public static void setTermCritParam(double d)
 		PN_SetTermCritParam(d);
 	}
 
-	private static native void PN_SetMaxIters(int i);
-	public static void setMaxIters(int i)
+	private static native void PN_SetMaxIters(double d);
+	public static void setMaxIters(double d)
 	{
-		PN_SetMaxIters(i);
+		assert d > 0 && d <= Integer.MAX_VALUE && (d == Math.floor(d) || Double.isInfinite(d));
+		PN_SetMaxIters(d);
 	}
 
 	private static native void PN_SetSBMaxMem(int i);

diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java
@@ -261,8 +261,8 @@ public class PrismSettings implements Observer
 																			"Criteria to use for checking termination of iterative numerical methods." },
 			{ DOUBLE_TYPE,		PRISM_TERM_CRIT_PARAM,					"Termination epsilon",					"2.1",			new Double(1.0E-6),															"0.0,",																						
 																			"Epsilon value to use for checking termination of iterative numerical methods." },
-			{ INTEGER_TYPE,		PRISM_MAX_ITERS,						"Termination max. iterations",			"2.1",			new Integer(10000),															"0,",																						
-																			"Maximum number of iterations to perform if iterative methods do not converge." },
+			{ DOUBLE_TYPE,		PRISM_MAX_ITERS,						"Termination max. iterations",			"2.1",			Double.valueOf(10000),															"0,",																						
+																			"Maximum number of iterations to perform if iterative methods do not converge. Expects a positive integer of 'Infinity' for unbounded iterations." },
 			{ BOOLEAN_TYPE,		PRISM_EXPORT_ITERATIONS,				"Export iterations (debug/visualisation)",			"4.3.1",			false,														"",
 																			"Export solution vectors for iteration algorithms to iterations.html"},
 			// MODEL CHECKING OPTIONS:
@@ -1143,12 +1143,13 @@ else if (sw.equals("epsilon") || sw.equals("e")) {
 		else if (sw.equals("maxiters")) {
 			if (i < args.length - 1) {
 				try {
-					j = Integer.parseInt(args[++i]);
-					if (j < 0)
-						throw new NumberFormatException("");
-					set(PRISM_MAX_ITERS, j);
+					double max = Double.parseDouble(args[++i]);
+					if (! (max > 0 && max <= Integer.MAX_VALUE && (max == Math.floor(max) || Double.isInfinite(max)))) {
+						throw new NumberFormatException();
+					}
+					set(PRISM_MAX_ITERS, max);
 				} catch (NumberFormatException e) {
-					throw new PrismException("Invalid value for -" + sw + " switch");
+					throw new PrismException("Invalid value for -" + sw + " switch. Expected positive integer or 'Infinity'.");
 				}
 			} else {
 				throw new PrismException("No value specified for -" + sw + " switch");
@@ -1793,7 +1794,7 @@ public static void printHelp(PrismLog mainLog)
 		mainLog.println("-relative (or -rel) ............ Use relative error for detecting convergence [default]");
 		mainLog.println("-absolute (or -abs) ............ Use absolute error for detecting convergence");
 		mainLog.println("-epsilon <x> (or -e <x>) ....... Set value of epsilon (for convergence check) [default: 1e-6]");
-		mainLog.println("-maxiters <n> .................. Set max number of iterations [default: 10000]");
+		mainLog.println("-maxiters <n> .................. Set max number of iterations to positive integer [default: 10000] or 'Infinity' for unbounded interations.");
 
 		mainLog.println();
 		mainLog.println("MODEL CHECKING OPTIONS:");

diff --git a/prism/src/sparse/PS_NondetMultiObj.cc b/prism/src/sparse/PS_NondetMultiObj.cc
@@ -65,10 +65,10 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
  jlong __jlongpointer _ndsm, //pointer to trans sparse matrix
  jobject synchs,
  jlongArray _yes_vec, //pointer to yes vector array
- jintArray _prob_step_bounds, //step bounds for probabilistic operators
+ jdoubleArray _prob_step_bounds, //step bounds for probabilistic operators
  jlongArray  _ndsm_r, //pointer to reward sparse matrix array
  jdoubleArray _weights, //weights of rewards and yes_vec vectors
- jintArray _ndsm_r_step_bounds //step bounds for rewards
+ jdoubleArray _ndsm_r_step_bounds //step bounds for rewards
   )
 {
 	// cast function parameters
@@ -116,7 +116,7 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
 	// storage for result array (0 means error)
 	jdoubleArray ret = 0;
 	// local copy of max_iters, since we will change it
-	int max_iters_local = max_iters;
+	double max_iters_local = max_iters;
 	// whether to export individual solution vectors (with adversaries)
 	bool export_vectors = false;
 
@@ -128,8 +128,8 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
 	jlong *ptr_ndsm_r = (has_rewards) ? env->GetLongArrayElements(_ndsm_r, 0) : NULL;
 	jlong *ptr_yes_vec = (has_yes_vec) ? env->GetLongArrayElements(_yes_vec, 0) : NULL;
 	double* weights = env->GetDoubleArrayElements(_weights, 0);
-	int* step_bounds_r = (has_rewards) ? (int*)env->GetIntArrayElements(_ndsm_r_step_bounds, 0) : NULL;
-	int* step_bounds = (has_yes_vec) ? (int*)env->GetIntArrayElements(_prob_step_bounds, 0) : NULL;
+	double* step_bounds_r = (has_rewards) ? (double*)env->GetDoubleArrayElements(_ndsm_r_step_bounds, 0) : NULL;
+	double* step_bounds = (has_yes_vec) ? (double*)env->GetDoubleArrayElements(_prob_step_bounds, 0) : NULL;
 
 	// We will ignore one of the rewards and compute its value from the other ones and
 	// from the combined value. We must make sure that this reward has nonzero weight,
@@ -180,7 +180,7 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
 		for(int rewi = 0; rewi < lenRew; rewi++)
 			ndsm_r[rewi] = (NDSparseMatrix *) jlong_to_NDSparseMatrix(ptr_ndsm_r[rewi]);
 
-		int max_step_bound = 0;
+		double max_step_bound = 0;
 		for(int rewi = 0; rewi < lenRew; rewi++) {
 			if (step_bounds_r[rewi] == -1)
 				step_bounds_r[rewi] = max_iters_local;

diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java
@@ -345,8 +345,8 @@ public static DoubleVector NondetReachRewardInterval(JDDNode trans, JDDNode tran
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
-	private static native double[] PS_NondetMultiObj(long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, boolean minmax, long start, long ptr_adversary, long ptr_TransSparseMatrix, List<String> synchs, long[] ptr_yes_vec, int[] probStepBounds, long[] ptr_RewSparseMatrix, double[] rewardWeights, int[] rewardStepBounds);
-	public static double[] NondetMultiObj(ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, boolean minmax, JDDNode start, NativeIntArray adversary, NDSparseMatrix transSparseMatrix, List<String> synchs, DoubleVector[] yes_vec, int[] probStepBounds, NDSparseMatrix[] rewSparseMatrix, double[] rewardWeights, int[] rewardStepBounds) throws PrismException
+	private static native double[] PS_NondetMultiObj(long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, boolean minmax, long start, long ptr_adversary, long ptr_TransSparseMatrix, List<String> synchs, long[] ptr_yes_vec, double[] probStepBounds, long[] ptr_RewSparseMatrix, double[] rewardWeights, double[] rewardStepBounds);
+	public static double[] NondetMultiObj(ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, boolean minmax, JDDNode start, NativeIntArray adversary, NDSparseMatrix transSparseMatrix, List<String> synchs, DoubleVector[] yes_vec, double[] probStepBounds, NDSparseMatrix[] rewSparseMatrix, double[] rewardWeights, double[] rewardStepBounds) throws PrismException
 	{
 		checkNumStates(odd);