diff --git a/prism/include/PrismNativeGlob.h b/prism/include/PrismNativeGlob.h index af85536b48..b2af213a19 100644 --- 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 index b8e7f14f09..4bdd105ff2 100644 --- a/prism/include/jni/prism_PrismNative.h +++ b/prism/include/jni/prism_PrismNative.h @@ -66,10 +66,10 @@ JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetTermCritParam /* * Class: prism_PrismNative * Method: PN_SetMaxIters - * Signature: (I)V + * Signature: (D)V */ JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetMaxIters - (JNIEnv *, jclass, jint); + (JNIEnv *, jclass, jdouble); /* * Class: prism_PrismNative diff --git a/prism/include/jni/sparse_PrismSparse.h b/prism/include/jni/sparse_PrismSparse.h index 0a95f212f3..f627790968 100644 --- a/prism/include/jni/sparse_PrismSparse.h +++ b/prism/include/jni/sparse_PrismSparse.h @@ -178,10 +178,10 @@ JNIEXPORT jlong JNICALL Java_sparse_PrismSparse_PS_1NondetReachRewardInterval /* * Class: sparse_PrismSparse * Method: PS_NondetMultiObj - * Signature: (JJIJIJIZJJJLjava/util/List;[J[I[J[D[I)[D + * Signature: (JJIJIJIZJJJLjava/util/List;[J[D[J[D[D)[D */ JNIEXPORT jdoubleArray JNICALL Java_sparse_PrismSparse_PS_1NondetMultiObj - (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jlong, jint, jboolean, jlong, jlong, jlong, jobject, jlongArray, jintArray, jlongArray, jdoubleArray, jintArray); + (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jlong, jint, jboolean, jlong, jlong, jlong, jobject, jlongArray, jdoubleArray, jlongArray, jdoubleArray, jdoubleArray); /* * Class: sparse_PrismSparse diff --git a/prism/src/explicit/IterationMethod.java b/prism/src/explicit/IterationMethod.java index 9c7d611549..062234eccb 100644 --- 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 index 5cf4d12068..0e9cceae1d 100644 --- 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 index 085338cef4..df74c58b6e 100644 --- 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 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 index 72e903567c..892e3c8b70 100644 --- 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 index c90df83a19..9a9588fcba 100644 --- 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 index e966834865..818e947073 100644 --- 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 index 8bd175f461..be72fb37e0 100644 --- 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 (or -e ) ....... Set value of epsilon (for convergence check) [default: 1e-6]"); - mainLog.println("-maxiters .................. Set max number of iterations [default: 10000]"); + mainLog.println("-maxiters .................. Set max number of iterations to positive integer [default: 10000] or 'Infinity' for unbounded interations."); mainLog.println("-gridresolution .............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 index c3d28f5995..b9f18e5dc6 100644 --- 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 index c98d44e869..2ec2600bef 100644 --- 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 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 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 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 synchs, DoubleVector[] yes_vec, double[] probStepBounds, NDSparseMatrix[] rewSparseMatrix, double[] rewardWeights, double[] rewardStepBounds) throws PrismException { checkNumStates(odd); PrismNative.resetModelCheckingInfo();