From 4e1900207a94116b4ed16f6c33fd7adffd10f3ca Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 30 Apr 2013 15:32:45 +0000 Subject: [PATCH] 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 --- prism/src/parser/ast/Expression.java | 21 +++++++++++++++++++++ prism/src/prism/NondetModelChecker.java | 22 +++++++++++----------- prism/src/prism/Prism.java | 17 ++++++++++++++++- prism/src/prism/PrismSettings.java | 6 ++++++ 4 files changed, 54 insertions(+), 12 deletions(-) diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index e8864e9f..4bc36c2a 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -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; + } } //------------------------------------------------------------------------------ diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index f91d7ef8..5ce997c2 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -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); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 0935f25d..4bb82716 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -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; diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 930c8515..6ec11223 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -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")) {