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

Separate MDP multi-objective setting from main MDP one. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6729 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
2b614526e1
commit
4e1900207a
4 changed files with 54 additions and 12 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. 21
      prism/src/parser/ast/Expression.java
  2. 22
      prism/src/prism/NondetModelChecker.java
  3. 17
      prism/src/prism/Prism.java
  4. 6
      prism/src/prism/PrismSettings.java

21
prism/src/parser/ast/Expression.java
View File

@ -659,6 +659,27 @@ public abstract class Expression extends ASTElement
}
return false;
}
/**
* Test if an expression contains a multi(...) property within
*/
public static boolean containsMultiObjective(Expression expr)
{
try {
ASTTraverse astt = new ASTTraverse()
{
public void visitPost(ExpressionFunc e) throws PrismLangException
{
if (e.getNameCode() == ExpressionFunc.MULTI)
throw new PrismLangException("Found one", e);
}
};
expr.accept(astt);
} catch (PrismLangException e) {
return true;
}
return false;
}
}
//------------------------------------------------------------------------------

22
prism/src/prism/NondetModelChecker.java
View File

@ -996,7 +996,7 @@ public class NondetModelChecker extends NonProbModelChecker
// Add a dummy LTL formula to get generate target states when there is no LTL formula in the query
// TODO most probably this is not needed for non-LP solution methods
if (targetDDs.isEmpty() && prism.getMDPSolnMethod() == Prism.MDP_LP) {
if (targetDDs.isEmpty() && prism.getMDPSolnMethod() == Prism.MDP_MULTI_LP) {
addDummyFormula(modelProduct, mcLtl, targetDDs, opsAndBounds);
}
@ -2096,13 +2096,13 @@ public class NondetModelChecker extends NonProbModelChecker
}
mainLog.println("Engine: " + Prism.getEngineString(engine));
int method = prism.getMDPSolnMethod();
int method = prism.getMDPMultiSolnMethod();
try {
if (engine != Prism.SPARSE)
throw new PrismException("Currently only sparse engine supports multi-objective properties");
if (method == Prism.MDP_LP) {
if (method == Prism.MDP_MULTI_LP) {
//LP currently does not support Pareto
if (opsAndBounds.numberOfNumerical() > 1) {
throw new PrismException("Linear programming method currently does not support generating of Pareto curves.");
@ -2129,7 +2129,7 @@ public class NondetModelChecker extends NonProbModelChecker
targets, opsAndBounds, maybe, st);
}
}
} else if (method == Prism.MDP_GAUSSSEIDEL || method == Prism.MDP_VALITER) {
} else if (method == Prism.MDP_MULTI_GAUSSSEIDEL || method == Prism.MDP_MULTI_VALITER) {
double timePre = System.currentTimeMillis();
value = weightedMultiReachProbs(modelProduct, yes, maybe, st, labels, rewards, opsAndBounds);
double timePost = System.currentTimeMillis();
@ -2483,7 +2483,7 @@ public class NondetModelChecker extends NonProbModelChecker
double[] weights = new double[dimProb + dimReward];
weights[i] = 1.0;
/*if (prism.getMDPSolnMethod() == Prism.MDP_GAUSSSEIDEL) {
/*if (prism.getMDPMultiSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
//System.out.println("Doing GS");
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, new DoubleVector[] {probDoubleVectors[i]}, new int[] {probStepBounds[i]}, null,
@ -2494,7 +2494,7 @@ public class NondetModelChecker extends NonProbModelChecker
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, new DoubleVector[] {probDoubleVectors[i]}, new int[] {probStepBounds[i]}, null,
new double[] { 1.0 }, null);
}*/
if (prism.getMDPSolnMethod() == Prism.MDP_GAUSSSEIDEL) {
if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);
@ -2522,7 +2522,7 @@ public class NondetModelChecker extends NonProbModelChecker
double[] weights = new double[dimProb + dimReward];
weights[i] = 1.0;
/*System.out.println(prism.getMDPSolnMethod());
if (prism.getMDPSolnMethod() == Prism.MDP_GAUSSSEIDEL) {
if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
//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[i] },
@ -2533,7 +2533,7 @@ public class NondetModelChecker extends NonProbModelChecker
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, null, null, new NDSparseMatrix[] { rewSparseMatrices[i] },
new double[] { 1.0 }, new int[] { rewardStepBounds[i] });
}*/
if (prism.getMDPSolnMethod() == Prism.MDP_GAUSSSEIDEL) {
if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);
@ -2577,7 +2577,7 @@ public class NondetModelChecker extends NonProbModelChecker
}
double[] result;
if (prism.getMDPSolnMethod() == Prism.MDP_GAUSSSEIDEL) {
if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);
@ -2748,7 +2748,7 @@ public class NondetModelChecker extends NonProbModelChecker
}
double[] result;
if (prism.getMDPSolnMethod() == Prism.MDP_GAUSSSEIDEL) {
if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
//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] },
@ -2789,7 +2789,7 @@ public class NondetModelChecker extends NonProbModelChecker
}
double[] result;
if (prism.getMDPSolnMethod() == Prism.MDP_GAUSSSEIDEL) {
if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);

17
prism/src/prism/Prism.java
View File

@ -96,6 +96,11 @@ public class Prism implements PrismSettingsListener
public static final int MDP_MODPOLITER = 4;
public static final int MDP_LP = 5;
// methods for solving multi-objective queries on MDPs
public static final int MDP_MULTI_VALITER = 1;
public static final int MDP_MULTI_GAUSSSEIDEL = 2;
public static final int MDP_MULTI_LP = 3;
// termination criterion for iterative methods
public static final int ABSOLUTE = 1;
public static final int RELATIVE = 2;
@ -372,6 +377,11 @@ public class Prism implements PrismSettingsListener
settings.set(PrismSettings.PRISM_MDP_SOLN_METHOD, i - 1); // note index offset correction
}
public void setMDPMultiSolnMethod(int i) throws PrismException
{
settings.set(PrismSettings.PRISM_MDP_MULTI_SOLN_METHOD, i - 1); // note index offset correction
}
public void setTermCrit(int i) throws PrismException
{
settings.set(PrismSettings.PRISM_TERM_CRIT, i - 1); // note index offset correction
@ -638,6 +648,11 @@ public class Prism implements PrismSettingsListener
return settings.getInteger(PrismSettings.PRISM_MDP_SOLN_METHOD) + 1;
} //NOTE THE CORRECTION for the ChoiceSetting index
public int getMDPMultiSolnMethod()
{
return settings.getInteger(PrismSettings.PRISM_MDP_MULTI_SOLN_METHOD) + 1;
} //NOTE THE CORRECTION for the ChoiceSetting index
public int getTermCrit()
{
return settings.getInteger(PrismSettings.PRISM_TERM_CRIT) + 1;
@ -2381,7 +2396,7 @@ public class Prism implements PrismSettingsListener
}
// Auto-switch engine if required
if (currentModelType == ModelType.MDP) {
if (currentModelType == ModelType.MDP && !Expression.containsMultiObjective(prop.getExpression())) {
if (getMDPSolnMethod() != Prism.MDP_VALITER && !getExplicit()) {
mainLog.printWarning("Switching to explicit engine to allow use of chosen MDP solution method.");
engineSwitch = true;

6
prism/src/prism/PrismSettings.java
View File

@ -80,6 +80,7 @@ public class PrismSettings implements Observer
public static final String PRISM_LIN_EQ_METHOD = "prism.linEqMethod";//"prism.iterativeMethod";
public static final String PRISM_LIN_EQ_METHOD_PARAM = "prism.linEqMethodParam";//"prism.overRelaxation";
public static final String PRISM_MDP_SOLN_METHOD = "prism.mdpSolnMethod";
public static final String PRISM_MDP_MULTI_SOLN_METHOD = "prism.mdpMultiSolnMethod";
public static final String PRISM_TERM_CRIT = "prism.termCrit";//"prism.termination";
public static final String PRISM_TERM_CRIT_PARAM = "prism.termCritParam";//"prism.terminationEpsilon";
public static final String PRISM_MAX_ITERS = "prism.maxIters";//"prism.maxIterations";
@ -204,6 +205,8 @@ public class PrismSettings implements Observer
"Over-relaxation parameter for iterative numerical methods such as JOR/SOR." },
{ CHOICE_TYPE, PRISM_MDP_SOLN_METHOD, "MDP solution method", "4.0", "Value iteration", "Value iteration,Gauss-Seidel,Policy iteration,Modified policy iteration,Linear programming",
"Which method to use when solving Markov decision processes." },
{ CHOICE_TYPE, PRISM_MDP_MULTI_SOLN_METHOD, "MDP multi-objective solution method", "4.0.3", "Value iteration", "Value iteration,Gauss-Seidel,Linear programming",
"Which method to use when solving multi-objective queries on Markov decision processes." },
{ CHOICE_TYPE, PRISM_TERM_CRIT, "Termination criteria", "2.1", "Relative", "Absolute,Relative",
"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,",
@ -789,6 +792,7 @@ public class PrismSettings implements Observer
} else if (sw.equals("gaussseidel") || sw.equals("gs")) {
set(PRISM_LIN_EQ_METHOD, "Gauss-Seidel");
set(PRISM_MDP_SOLN_METHOD, "Gauss-Seidel");
set(PRISM_MDP_MULTI_SOLN_METHOD, "Gauss-Seidel");
} else if (sw.equals("bgaussseidel") || sw.equals("bgs")) {
set(PRISM_LIN_EQ_METHOD, "Backwards Gauss-Seidel");
} else if (sw.equals("pgaussseidel") || sw.equals("pgs")) {
@ -807,12 +811,14 @@ public class PrismSettings implements Observer
set(PRISM_LIN_EQ_METHOD, "Backwards Pseudo-SOR");
} else if (sw.equals("valiter")) {
set(PRISM_MDP_SOLN_METHOD, "Value iteration");
set(PRISM_MDP_MULTI_SOLN_METHOD, "Value iteration");
} else if (sw.equals("politer")) {
set(PRISM_MDP_SOLN_METHOD, "Policy iteration");
} else if (sw.equals("modpoliter")) {
set(PRISM_MDP_SOLN_METHOD, "Modified policy iteration");
} else if (sw.equals("linprog") || sw.equals("lp")) {
set(PRISM_MDP_SOLN_METHOD, "Linear programming");
set(PRISM_MDP_MULTI_SOLN_METHOD, "Linear programming");
}
// Linear equation solver over-relaxation parameter
else if (sw.equals("omega")) {

Write Preview
Loading…
Cancel
Save