Implement unbounded iterations #69

Steffen Märcker · merkste · commit 554515076996 · 2022-02-15T11:10:17.000+01:00
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 &lt; max_iters) as +Infinity compares greater to
all integer values.
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
@@ -420,8 +420,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);
@@ -484,9 +484,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;
 		double error = 0.0;
 
 		int numSCCs = sccs.getNumSCCs();
@@ -597,8 +597,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;
 			double maxError = Double.POSITIVE_INFINITY;
 
@@ -691,9 +691,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;
 			double maxError = Double.POSITIVE_INFINITY;
 
 			PeriodicTimer updatesTimer = new PeriodicTimer(ProbModelChecker.UPDATE_DELAY);
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.0;
 	// Resolution for POMDP fixed grid approximation algorithm
 	protected int gridResolution = 10;
 	// Use precomputation algorithms in model checking?
@@ -221,7 +221,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_GRID_RESOLUTION
 			setGridResolution(settings.getInteger(PrismSettings.PRISM_GRID_RESOLUTION));
 			// PRISM_PRECOMPUTATION
@@ -347,8 +347,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;
 	}
 
@@ -453,7 +454,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);
 
@@ -1040,11 +1040,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);
 
@@ -1150,7 +1150,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
@@ -454,9 +454,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 setGridResolution(int i) throws PrismException
@@ -785,9 +788,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 int getGridResolution()
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
@@ -127,9 +127,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
@@ -119,10 +119,11 @@ public static double getTermCritParam()
 		return termCritParam;
 	}
 	
-	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
@@ -265,8 +265,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"},
 			{ INTEGER_TYPE,		PRISM_GRID_RESOLUTION,					"Fixed grid resolution",			    "4.5",			new Integer(10),															"1,",																						
@@ -1165,12 +1165,15 @@ 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]);
+					System.out.println(max);
+					System.out.println(Double.isInfinite(max));
+					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");
@@ -1831,9 +1834,9 @@ 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("-gridresolution <n> .............Set resolution for fixed grid approximation (POMDP) [default: 10]");
-		
+
 		mainLog.println();
 		mainLog.println("MODEL CHECKING OPTIONS:");
 		mainLog.println("-nopre ......................... Skip precomputation algorithms (where optional)");
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
@@ -346,8 +346,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);
 		PrismNative.resetModelCheckingInfo();

Original file line number	Diff line number	Diff line change
`@@ -454,9 +454,12 @@ public void setTermCritParam(double d) throws PrismException`
`454`	`454`	`settings.set(PrismSettings.PRISM_TERM_CRIT_PARAM, d);`
`455`	`455`	`}`
`456`	`456`
`457`		`- public void setMaxIters(int i) throws PrismException`
	`457`	`+ public void setMaxIters(double d) throws PrismException`
`458`	`458`	`{`
`459`		`- settings.set(PrismSettings.PRISM_MAX_ITERS, i);`
	`459`	`+ if (! (d > 0 && d <= Integer.MAX_VALUE && (d == Math.floor(d) \|\| Double.isInfinite(d)))) {`
	`460`	`+ throw new PrismException("Expected positive integer or 'Infinity'.");`
	`461`	`+ }`
	`462`	`+ settings.set(PrismSettings.PRISM_MAX_ITERS, d);`
`460`	`463`	`}`
`461`	`464`
`462`	`465`	`public void setGridResolution(int i) throws PrismException`
`@@ -785,9 +788,9 @@ public double getTermCritParam()`
`785`	`788`	`return settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM);`
`786`	`789`	`}`
`787`	`790`
`788`		`- public int getMaxIters()`
	`791`	`+ public double getMaxIters()`
`789`	`792`	`{`
`790`		`- return settings.getInteger(PrismSettings.PRISM_MAX_ITERS);`
	`793`	`+ return settings.getDouble(PrismSettings.PRISM_MAX_ITERS);`
`791`	`794`	`}`
`792`	`795`
`793`	`796`	`public int getGridResolution()`
Original file line number	Diff line number	Diff line change
`@@ -119,10 +119,11 @@ public static double getTermCritParam()`
`119`	`119`	`return termCritParam;`
`120`	`120`	`}`
`121`	`121`
`122`		`- private static native void PN_SetMaxIters(int i);`
`123`		`- public static void setMaxIters(int i)`
	`122`	`+ private static native void PN_SetMaxIters(double d);`
	`123`	`+ public static void setMaxIters(double d)`
`124`	`124`	`{`
`125`		`- PN_SetMaxIters(i);`
	`125`	`+ assert d > 0 && d <= Integer.MAX_VALUE && (d == Math.floor(d) \|\| Double.isInfinite(d));`
	`126`	`+ PN_SetMaxIters(d);`
`126`	`127`	`}`
`127`	`128`
`128`	`129`	`private static native void PN_SetSBMaxMem(int i);`