s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Refactoring in multi-objective value iteration: move check for step-bounded with GS. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10882 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
41ba061916
commit
1493a0c6c5
5 changed files with 58 additions and 45 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      prism/include/PrismSparse.h
  2. 43
      prism/src/prism/MultiObjModelChecker.java
  3. 14
      prism/src/prism/OpsAndBoundsList.java
  4. 21
      prism/src/sparse/PS_NondetMultiObjGS.cc
  5. 21
      prism/src/sparse/PrismSparse.java

4
prism/include/PrismSparse.h
View File

@ -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

43
prism/src/prism/MultiObjModelChecker.java
View File

@ -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,

14
prism/src/prism/OpsAndBoundsList.java
View File

@ -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()
{

21
prism/src/sparse/PS_NondetMultiObjGS.cc
View File

@ -3,7 +3,7 @@
// Copyright (c) 2002-
// Authors:
// * Vojtech Forejt <vojtech.forejt@cs.ox.ac.uk> (University of Oxford)
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
// * Dave Parker <d.a.parker@cs.bham.ac.uk> (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;

21
prism/src/sparse/PrismSparse.java
View File

@ -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

Write Preview
Loading…
Cancel
Save