diff --git a/prism/include/PrismSparse.h b/prism/include/PrismSparse.h index aaab1454..4a97de6b 100644 --- a/prism/include/PrismSparse.h +++ b/prism/include/PrismSparse.h @@ -146,10 +146,10 @@ JNIEXPORT jdoubleArray JNICALL Java_sparse_PrismSparse_PS_1NondetMultiObj /* * Class: sparse_PrismSparse * Method: PS_NondetMultiObjGS - * Signature: (JJIJIJIZJJJ[J[I[J[D[I)[D + * Signature: (JJIJIJIZJJJ[J[J[D)[D */ JNIEXPORT jdoubleArray JNICALL Java_sparse_PrismSparse_PS_1NondetMultiObjGS - (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jlong, jint, jboolean, jlong, jlong, jlong, jlongArray, jintArray, jlongArray, jdoubleArray, jintArray); + (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jlong, jint, jboolean, jlong, jlong, jlong, jlongArray, jlongArray, jdoubleArray); /* * Class: sparse_PrismSparse diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index e6f76cb0..567bef99 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -714,8 +714,9 @@ public class MultiObjModelChecker extends PrismComponent if (numberOfMaximizing >= 2) { return generateParetoCurve(modelProduct, yes_ones, maybe, st, targets, rewards, opsAndBounds); - } else + } else { return targetDrivenMultiReachProbs(modelProduct, yes_ones, maybe, st, targets, rewards, opsAndBounds); + } } protected TileList generateParetoCurve(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, final JDDNode st, JDDNode[] targets, @@ -733,6 +734,13 @@ public class MultiObjModelChecker extends PrismComponent double timer = System.currentTimeMillis(); boolean min = false; + // Determine whether we are using Gauss-Seidel value iteration + boolean useGS = (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL); + if (opsAndBounds.numberOfStepBounded() > 0) { + mainLog.println("Not using Guass-Seidel since there are step-bounded objectives"); + useGS = false; + } + //convert minimizing rewards to maximizing for (int i = 0; i < opsAndBounds.rewardSize(); i++) { if (opsAndBounds.getRewardOperator(i) == Operator.R_LE) { @@ -811,10 +819,9 @@ public class MultiObjModelChecker extends PrismComponent double[] weights = new double[dimProb + dimReward]; weights[i] = 1.0; - if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) { + if (useGS) { result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, - rewardStepBounds); + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, rewSparseMatrices, weights); } else { result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights, @@ -840,10 +847,9 @@ public class MultiObjModelChecker extends PrismComponent double[] result; double[] weights = new double[dimProb + dimReward]; weights[i] = 1.0; - if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) { + if (useGS) { result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, - rewardStepBounds); + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, rewSparseMatrices, weights); } else { result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights, @@ -893,10 +899,9 @@ public class MultiObjModelChecker extends PrismComponent } double[] result; - if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) { + if (useGS) { result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, - rewardStepBounds); + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, rewSparseMatrices, weights); } else { result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights, @@ -979,6 +984,13 @@ public class MultiObjModelChecker extends PrismComponent double timer = System.currentTimeMillis(); boolean min = false; + // Determine whether we are using Gauss-Seidel value iteration + boolean useGS = (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL); + if (opsAndBounds.numberOfStepBounded() > 0) { + mainLog.println("Not using Guass-Seidel since there are step-bounded objectives"); + useGS = false; + } + //convert minimizing rewards to maximizing for (int i = 0; i < opsAndBounds.rewardSize(); i++) { if (opsAndBounds.getRewardOperator(i) == Operator.R_LE) { @@ -1062,11 +1074,11 @@ public class MultiObjModelChecker extends PrismComponent } double[] result; - if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) { + if (useGS) { //System.out.println("Doing GS"); result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, null, null, new NDSparseMatrix[] { rewSparseMatrices[0] }, - new double[] { 1.0 }, new int[] { rewardStepBounds[0] }); + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, null, new NDSparseMatrix[] { rewSparseMatrices[0] }, + new double[] { 1.0 }); } else { //System.out.println("Not doing GS"); result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), @@ -1102,10 +1114,9 @@ public class MultiObjModelChecker extends PrismComponent } double[] result; - if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) { + if (useGS) { result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), - modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, - rewardStepBounds); + modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, rewSparseMatrices, weights); } else { result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights, diff --git a/prism/src/prism/OpsAndBoundsList.java b/prism/src/prism/OpsAndBoundsList.java index 90fd8195..64fee789 100644 --- a/prism/src/prism/OpsAndBoundsList.java +++ b/prism/src/prism/OpsAndBoundsList.java @@ -291,6 +291,20 @@ public class OpsAndBoundsList return num; } + /** + * Returns the number of step-bounded (<=k) objectives. + */ + public int numberOfStepBounded() + { + int num = 0; + for (int k : stepBounds) { + if (k != -1) { + num++; + } + } + return num; + } + @Override public String toString() { diff --git a/prism/src/sparse/PS_NondetMultiObjGS.cc b/prism/src/sparse/PS_NondetMultiObjGS.cc index 92e20cd3..91e70c5e 100644 --- a/prism/src/sparse/PS_NondetMultiObjGS.cc +++ b/prism/src/sparse/PS_NondetMultiObjGS.cc @@ -3,7 +3,7 @@ // Copyright (c) 2002- // Authors: // * Vojtech Forejt (University of Oxford) -// * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Dave Parker (University of Birmingham/Oxford) // //------------------------------------------------------------------------------ // @@ -63,10 +63,8 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet jlong _adversary, jlong __jlongpointer _ndsm, //pointer to trans sparse matrix jlongArray _yes_vec, //pointer to yes vector array - jintArray _prob_step_bounds, //step bounds for prob. Currently ignored. jlongArray _ndsm_r, //pointer to reward sparse matrix array - jdoubleArray _weights, //weights of rewards and yes_vec vectors - jintArray _ndsm_r_step_bounds + jdoubleArray _weights //weights of rewards and yes_vec vectors ) { // cast function parameters @@ -174,21 +172,6 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet 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; - - for(int rewi = 0; rewi < lenRew; rewi++) - if (step_bounds_r[rewi] != -1) { - PS_SetErrorMessage("Cannot do Gauss Seidel method for step bounded objectives!"); - throw 1; - } - - for(int probi = 0; probi < lenProb; probi++) - if (step_bounds[probi] != -1) { - PS_SetErrorMessage("Cannot do Gauss Seidel method for step bounded objectives!"); - throw 1; - } - // if needed, and if info is available, build a vector of action indices for the MDP actions = NULL; diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index 3a57b3fa..c1475169 100644 --- a/prism/src/sparse/PrismSparse.java +++ b/prism/src/sparse/PrismSparse.java @@ -29,11 +29,16 @@ package sparse; import java.io.FileNotFoundException; import java.util.List; -import prism.*; -import strat.MDStrategyIV; -import jdd.*; -import dv.*; -import odd.*; +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; +import odd.ODDNode; +import prism.NativeIntArray; +import prism.OpsAndBoundsList; +import prism.PrismException; +import prism.PrismLog; +import dv.DoubleVector; +import dv.IntegerVector; //---------------------------------------------------------------------------------------------- @@ -263,8 +268,8 @@ public class PrismSparse } - private static native double[] PS_NondetMultiObjGS(long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, boolean minmax, long start, long ptr_adversary, long ptr_TransSparseMatrix, long[] ptr_yes_vec, int[] probStepBounds, long[] ptr_RewSparseMatrix, double[] rewardWeights, int[] rewardStepBounds); - public static double[] NondetMultiObjGS(ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, boolean minmax, JDDNode start, NativeIntArray adversary, NDSparseMatrix transSparseMatrix, DoubleVector[] yes_vec, int[] probStepBounds, NDSparseMatrix[] rewSparseMatrix, double[] rewardWeights, int[] rewardStepBounds) throws PrismException + private static native double[] PS_NondetMultiObjGS(long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, boolean minmax, long start, long ptr_adversary, long ptr_TransSparseMatrix, long[] ptr_yes_vec, long[] ptr_RewSparseMatrix, double[] rewardWeights); + public static double[] NondetMultiObjGS(ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, boolean minmax, JDDNode start, NativeIntArray adversary, NDSparseMatrix transSparseMatrix, DoubleVector[] yes_vec, NDSparseMatrix[] rewSparseMatrix, double[] rewardWeights) throws PrismException { long[] ptr_ndsp_r = null; if (rewSparseMatrix != null) { @@ -280,7 +285,7 @@ public class PrismSparse ptr_yes_vec[i] = (yes_vec[i]!=null) ? yes_vec[i].getPtr() : 0; } - double[] ret = PS_NondetMultiObjGS(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), minmax, start.ptr(), adversary.getPtr(), transSparseMatrix.getPtr(), ptr_yes_vec, probStepBounds, ptr_ndsp_r, rewardWeights, rewardStepBounds); + double[] ret = PS_NondetMultiObjGS(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), minmax, start.ptr(), adversary.getPtr(), transSparseMatrix.getPtr(), ptr_yes_vec, ptr_ndsp_r, rewardWeights); if (ret == null) throw new PrismException(getErrorMessage()); else