diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 478de7be..5f5f964b 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -693,7 +693,7 @@ public class DTMCModelChecker extends ProbModelChecker throw new PrismException("Unknown linear equation solution method " + linEqMethod.fullName()); } - res = doValueIterationReachProbs(dtmc, no, yes, init, known, iterationMethod, false); + res = doValueIterationReachProbs(dtmc, no, yes, init, known, iterationMethod, getDoTopologicalValueIteration()); // Finished probabilistic reachability timer = System.currentTimeMillis() - timer; @@ -1302,7 +1302,7 @@ public class DTMCModelChecker extends ProbModelChecker throw new PrismException("Unknown linear equation solution method " + linEqMethod.fullName()); } - res = doValueIterationReachRewards(dtmc, mcRewards, target, inf, init, known, iterationMethod, false); + res = doValueIterationReachRewards(dtmc, mcRewards, target, inf, init, known, iterationMethod, getDoTopologicalValueIteration()); // Finished expected reachability timer = System.currentTimeMillis() - timer; diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index b9120698..fc2206de 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -545,7 +545,7 @@ public class MDPModelChecker extends ProbModelChecker } if (res == null) { // not yet computed, use iterationMethod - res = doValueIterationReachProbs(mdp, no, yes, min, init, known, iterationMethod, false, strat); + res = doValueIterationReachProbs(mdp, no, yes, min, init, known, iterationMethod, getDoTopologicalValueIteration(), strat); } return res; @@ -1597,7 +1597,7 @@ public class MDPModelChecker extends ProbModelChecker } if (res == null) { // not yet computed, use iterationMethod - res = doValueIterationReachRewards(mdp, mdpRewards, iterationMethod, target, inf, min, init, known, false, strat); + res = doValueIterationReachRewards(mdp, mdpRewards, iterationMethod, target, inf, min, init, known, getDoTopologicalValueIteration(), strat); } return res; @@ -1620,7 +1620,7 @@ public class MDPModelChecker extends ProbModelChecker throws PrismException { IterationMethodPower iterationMethod = new IterationMethodPower(termCrit == TermCrit.ABSOLUTE, termCritParam); - return doValueIterationReachRewards(mdp, mdpRewards, iterationMethod, target, inf, min, init, known, min, strat); + return doValueIterationReachRewards(mdp, mdpRewards, iterationMethod, target, inf, min, init, known, false, strat); } /** @@ -1723,7 +1723,7 @@ public class MDPModelChecker extends ProbModelChecker BitSet known, int strat[]) throws PrismException { IterationMethodGS iterationMethod = new IterationMethodGS(termCrit == TermCrit.ABSOLUTE, termCritParam, false); - return doValueIterationReachRewards(mdp, mdpRewards, iterationMethod, target, inf, min, init, known, min, strat); + return doValueIterationReachRewards(mdp, mdpRewards, iterationMethod, target, inf, min, init, known, false, strat); } /** diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index f0200317..9627d1bf 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -117,6 +117,9 @@ public class StateModelChecker extends PrismComponent protected boolean doBisim = false; + // Do topological value iteration? + protected boolean doTopologicalValueIteration = false; + // For Pmax computation, collapse MECs to quotient MDP? protected boolean doPmaxQuotient = false; @@ -300,6 +303,14 @@ public class StateModelChecker extends PrismComponent this.doBisim = doBisim; } + /** + * Specify whether or not to do topological value iteration. + */ + public void setDoTopologicalValueIteration(boolean doTopologicalValueIteration) + { + this.doTopologicalValueIteration = doTopologicalValueIteration; + } + /** * Specify whether or not to perform MEC quotienting for Pmax. */ @@ -379,6 +390,14 @@ public class StateModelChecker extends PrismComponent return doBisim; } + /** + * Whether or not to do topological value iteration. + */ + public boolean getDoTopologicalValueIteration() + { + return doTopologicalValueIteration; + } + /** * Whether or not to do MEC quotient for Pmax */ diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 73b022cd..04e7356d 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3730,6 +3730,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener mc.setStoreVector(storeVector); mc.setGenStrat(genStrat); mc.setDoBisim(doBisim); + mc.setDoTopologicalValueIteration(settings.getBoolean(PrismSettings.PRISM_TOPOLOGICAL_VI)); mc.setDoPmaxQuotient(settings.getBoolean(PrismSettings.PRISM_PMAX_QUOTIENT)); return mc; diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index ea95fdcf..d598803e 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -84,6 +84,7 @@ public class PrismSettings implements Observer public static final String PRISM_COMPACT = "prism.compact"; 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_TOPOLOGICAL_VI = "prism.topologicalVI"; public static final String PRISM_PMAX_QUOTIENT = "prism.pmaxQuotient"; public static final String PRISM_MDP_SOLN_METHOD = "prism.mdpSolnMethod"; public static final String PRISM_MDP_MULTI_SOLN_METHOD = "prism.mdpMultiSolnMethod"; @@ -242,6 +243,8 @@ public class PrismSettings implements Observer "Which iterative method to use when solving linear equation systems." }, { DOUBLE_TYPE, PRISM_LIN_EQ_METHOD_PARAM, "Over-relaxation parameter", "2.1", new Double(0.9), "", "Over-relaxation parameter for iterative numerical methods such as JOR/SOR." }, + { BOOLEAN_TYPE, PRISM_TOPOLOGICAL_VI, "Use topological value iteration", "4.3.1", false, "", + "Use topological value iteration in iterative numerical methods."}, { BOOLEAN_TYPE, PRISM_PMAX_QUOTIENT, "For Pmax computations, compute in the MEC quotient", "4.3.1", false, "", "For Pmax computations, compute in the MEC quotient."}, { CHOICE_TYPE, PRISM_MDP_SOLN_METHOD, "MDP solution method", "4.0", "Value iteration", "Value iteration,Gauss-Seidel,Policy iteration,Modified policy iteration,Linear programming", @@ -995,6 +998,11 @@ public class PrismSettings implements Observer set(PRISM_PMAX_QUOTIENT, true); } + // Topological VI + else if (sw.equals("topological")) { + set(PRISM_TOPOLOGICAL_VI, true); + } + // Linear equation solver over-relaxation parameter else if (sw.equals("omega")) { if (i < args.length - 1) { @@ -1663,6 +1671,7 @@ public class PrismSettings implements Observer 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("-topological ................... Perform topological iterations (only explicit engine"); mainLog.println(); mainLog.println("MODEL CHECKING OPTIONS:"); mainLog.println("-nopre ......................... Skip precomputation algorithms (where optional)");