diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 9627d1bf..fc5ca04a 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -123,6 +123,9 @@ public class StateModelChecker extends PrismComponent // For Pmax computation, collapse MECs to quotient MDP? protected boolean doPmaxQuotient = false; + // Do interval iteration? + protected boolean doIntervalIteration = false; + // Model info (for reward structures, etc.) protected ModulesFile modulesFile = null; protected ModelInfo modelInfo = null; @@ -218,6 +221,7 @@ public class StateModelChecker extends PrismComponent setStoreVector(other.getStoreVector()); setGenStrat(other.getGenStrat()); setDoBisim(other.getDoBisim()); + setDoIntervalIteration(other.getDoIntervalIteration()); setDoPmaxQuotient(other.getDoPmaxQuotient()); } @@ -319,6 +323,14 @@ public class StateModelChecker extends PrismComponent this.doPmaxQuotient = doPmaxQuotient; } + /** + * Specify whether or not to use interval iteration. + */ + public void setDoIntervalIteration(boolean doIntervalIteration) + { + this.doIntervalIteration = doIntervalIteration; + } + // Get methods for flags/settings public int getVerbosity() @@ -406,6 +418,14 @@ public class StateModelChecker extends PrismComponent return doPmaxQuotient; } + /** + * Whether or not to use interval iteration. + */ + public boolean getDoIntervalIteration() + { + return doIntervalIteration; + } + /** Get the constant values (both from the modules file and the properties file) */ public Values getConstantValues() { diff --git a/prism/src/prism/OptionsIntervalIteration.java b/prism/src/prism/OptionsIntervalIteration.java new file mode 100644 index 00000000..7c0b1cd6 --- /dev/null +++ b/prism/src/prism/OptionsIntervalIteration.java @@ -0,0 +1,278 @@ +//============================================================================== +// +// Copyright (c) 2017- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +import java.util.ArrayList; +import java.util.List; +import java.util.Map.Entry; + +/** Option handling for interval iteration */ +public class OptionsIntervalIteration +{ + /** + * The different methods for computing upper bounds for reward computations, + * and DEFAULT to choose the default method. + */ + public enum BoundMethod { + DEFAULT, + VARIANT_1_COARSE, + VARIANT_1_FINE, + VARIANT_2, + DSMPI, + }; + + /** The method for computing upper bounds for reward computations */ + private BoundMethod boundMethod = BoundMethod.DEFAULT; + + /** Verbose upper bound computations? (default false) */ + private boolean boundComputationVerbose = false; + + /** Select midpoint in results? (default true) */ + private boolean resultSelectMidpoint = true; + + /** Check for monotonicity in iterations? (default false) */ + private boolean checkMonotonicity = false; + + /** Enforce monotonicity in iteration from below? (default true) */ + private boolean enforceMonotonicityBelow = true; + + /** Enforce monotonicity in iteration from above? (default true) */ + private boolean enforceMonotonicityAbove = true; + + /** Manual lower bound (default none) */ + private Double manualLowerBound = null; + + /** Manual upper bound (default none) */ + private Double manualUpperBound = null; + + /* List of valid bound methods, for helper texts */ + final private static String boundMethodsList = "default, variant-1-coarse, variant-1-fine, variant-2, dsmpi"; + + /** Constructor from options String, throws PrismException on errors */ + public OptionsIntervalIteration(String options) throws PrismException + { + fromOptionsString(options); + } + + /** Static constructor from PrismComponent settings, throws PrismException on errors */ + public static OptionsIntervalIteration from(PrismComponent parent) throws PrismException + { + return from(parent.getSettings()); + } + + /** Static constructor from PrismSettings, throws PrismException on errors */ + public static OptionsIntervalIteration from(PrismSettings settings) throws PrismException + { + return new OptionsIntervalIteration(settings.getString(PrismSettings.PRISM_INTERVAL_ITER_OPTIONS)); + } + + /** Validate an options String, throws PrismException on errors */ + public static void validate(String optionsString) throws PrismException + { + new OptionsIntervalIteration(optionsString); + } + + /** The method for computing upper bounds for reward computations */ + public BoundMethod getBoundMethod() + { + return boundMethod; + } + + /** Verbose upper bound computations? */ + public boolean isBoundComputationVerbose() + { + return boundComputationVerbose; + } + + /** Select midpoint in results? */ + public boolean isSelectMidpointForResult() + { + return resultSelectMidpoint; + } + + /** Check for monotonicity in iterations? */ + public boolean isCheckMonotonicity() + { + return checkMonotonicity; + } + + /** Enforce monotonicity in iteration from below? */ + public boolean isEnforceMonotonicityFromBelow() + { + return enforceMonotonicityBelow; + } + + /** Enforce monotonicity in iteration from above? */ + public boolean isEnforceMonotonicityFromAbove() + { + return enforceMonotonicityAbove; + } + + /** Is there a manual lower bound? */ + public boolean hasManualLowerBound() + { + return manualLowerBound != null; + } + + /** Get manual lower bound (or null) */ + public Double getManualLowerBound() + { + return manualLowerBound; + } + + /** Is there a manual upper bound? */ + public boolean hasManualUpperBound() + { + return manualUpperBound != null; + } + + /** Get manual upper bound (or null) */ + public Double getManualUpperBound() + { + return manualUpperBound; + } + + /** Get helper text for the options */ + public static String getOptionsDescription() + { + StringBuffer sb = new StringBuffer(); + sb.append(" boundmethod= Select upper bound heuristic for reward computations\n"); + sb.append(" is one of " + boundMethodsList + "\n"); + sb.append(" lower= Manually specify lower bound for reward computations (double value)\n"); + sb.append(" upper= Manually specify upper bound for reward computations (double value)\n"); + sb.append(" [no]boundverbose Verbose output for upper bound computations (default = no)\n"); + sb.append(" [no]selectmidpoint Select midpoint between upper and lower as the result (default = yes)\n"); + sb.append(" [no]monotonicbelow Enforce monotonicity in iteration from below (default = yes)\n"); + sb.append(" [no]monotonicabove Enforce monotonicity in iteration from above (default = yes)\n"); + sb.append(" [no]checkmonotonic Check monotonicity, for testing (default = no)\n"); + sb.append("\nExample: boundmethod=default,upper=3.0,noselectmidpoint,checkmonotonic\n"); + + return sb.toString(); + } + + /** Parse options string, throw on error */ + private void fromOptionsString(String options) throws PrismException + { + for (Entry entry : splitOptionsString(options)){ + String option = entry.getKey(); + String extra = entry.getValue(); + + boolean isBooleanOption = true; + switch (option) { + case "boundverbose": + case "noboundverbose": + boundComputationVerbose = !option.startsWith("no"); + break; + case "selectmidpoint": + case "noselectmidpoint": + resultSelectMidpoint = !option.startsWith("no"); + break; + case "checkmonotonic": + case "nocheckmonotonic": + checkMonotonicity = !option.startsWith("no"); + break; + case "monotonicbelow": + case "nomonotonicbelow": + enforceMonotonicityBelow = !option.startsWith("no"); + break; + case "monotonicabove": + case "nomonotonicabove": + enforceMonotonicityAbove = !option.startsWith("no"); + break; + case "lower": + case "upper": { + if (extra == null) + throw new PrismException("Missing argument to interval iteration option '" + option + "'"); + try { + Double value = Double.parseDouble(extra); + if (option.equals("lower")) { + manualLowerBound = value; + } else { + manualUpperBound = value; + } + } catch (NumberFormatException e) { + throw new PrismException("Illegal argument to interval iteration option '" + option + "': " + e.getMessage()); + } + isBooleanOption = false; + break; + } + case "boundmethod": { + if (extra == null) + throw new PrismException("Missing argument to interval iteration option '" + option + "'"); + switch (extra) { + case "default": + boundMethod = BoundMethod.DEFAULT; + break; + case "variant-1-coarse": + boundMethod = BoundMethod.DEFAULT; + break; + case "variant-1-fine": + boundMethod = BoundMethod.DEFAULT; + break; + case "variant-2": + boundMethod = BoundMethod.DEFAULT; + break; + case "dsmpi": + boundMethod = BoundMethod.DEFAULT; + break; + default: + throw new PrismException("Unknown argument to interval iteration option '" + option + "', expected one of " + + boundMethodsList); + } + isBooleanOption = false; + break; + } + default: + throw new PrismException("Unknown interval iteration option '" + option + "'"); + } + + if (isBooleanOption) { + if (extra != null) { + throw new PrismException("Interval iteration option '" + option + "' has additional argument (" + extra + "), but is boolean option"); + } + } + } + } + + /** Split options string into list of pairs */ + private static List> splitOptionsString(String options) + { + List> list = new ArrayList<>(); + if ("".equals(options)) + return list; + + for (String option : options.split(",")) { + int j = option.indexOf("="); + if (j == -1) { + list.add(new Pair<>(option.trim(), null)); + } else { + list.add(new Pair<>(option.substring(0,j).trim(), option.substring(j+1).trim())); + } + } + return list; + } +} diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 04e7356d..cbc22327 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -990,6 +990,30 @@ public class Prism extends PrismComponent implements PrismSettingsListener return reachMethod; } + /** + * Returns an integer containing flags for the C++ implementation of interval iteration, + * derived from the current settings object. + */ + public int getIntervalIterationFlags() throws PrismException + { + int flags = 0; + + OptionsIntervalIteration iiOptions = OptionsIntervalIteration.from(settings); + + if (iiOptions.isEnforceMonotonicityFromBelow()) + flags += 1; + + if (iiOptions.isEnforceMonotonicityFromAbove()) + flags += 2; + + if (iiOptions.isSelectMidpointForResult()) + flags += 4; // select midpoint for result + + return flags; + } + + + public void addModelListener(PrismModelListener listener) { modelListeners.add(listener); @@ -3730,6 +3754,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener mc.setStoreVector(storeVector); mc.setGenStrat(genStrat); mc.setDoBisim(doBisim); + mc.setDoIntervalIteration(settings.getBoolean(PrismSettings.PRISM_INTERVAL_ITER)); mc.setDoTopologicalValueIteration(settings.getBoolean(PrismSettings.PRISM_TOPOLOGICAL_VI)); mc.setDoPmaxQuotient(settings.getBoolean(PrismSettings.PRISM_PMAX_QUOTIENT)); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index b4ade202..ff560413 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -86,6 +86,8 @@ public class PrismSettings implements Observer 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_INTERVAL_ITER = "prism.intervalIter"; + public static final String PRISM_INTERVAL_ITER_OPTIONS = "prism.intervalIterOptions"; 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"; @@ -247,6 +249,10 @@ public class PrismSettings implements Observer "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."}, + { BOOLEAN_TYPE, PRISM_INTERVAL_ITER, "Use interval iterations", "4.3.1", false, "", + "Use interval iteration (from above and below) in iterative numerical methods."}, + { STRING_TYPE, PRISM_INTERVAL_ITER_OPTIONS, "Interval iteration options", "4.3.1", "", "", + "Interval iteration options, a comma-separated list of the following:\n" + OptionsIntervalIteration.getOptionsDescription() }, { 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", @@ -994,6 +1000,29 @@ public class PrismSettings implements Observer set(PRISM_MDP_MULTI_SOLN_METHOD, "Linear programming"); } + // Interval iterations + else if (sw.equals("intervaliter") || + sw.equals("ii")) { + set(PRISM_INTERVAL_ITER, true); + + if (optionsString != null) { + optionsString = optionsString.trim(); + try { + OptionsIntervalIteration.validate(optionsString); + } catch (PrismException e) { + throw new PrismException("In options for -" + sw + " switch: " + e.getMessage()); + } + + // append options to existing ones + String iiOptions = getString(PRISM_INTERVAL_ITER_OPTIONS); + if ("".equals(iiOptions)) + iiOptions = optionsString; + else + iiOptions += "," + optionsString; + set(PRISM_INTERVAL_ITER_OPTIONS, iiOptions); + } + } + // Pmax quotient else if (sw.equals("pmaxquotient")) { set(PRISM_PMAX_QUOTIENT, true); @@ -1692,6 +1721,8 @@ public class PrismSettings implements Observer 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("-intervaliter (or -ii) ......... Perform interval iteration (for options see -help -ii)"); + mainLog.println(); mainLog.println("MODEL CHECKING OPTIONS:"); mainLog.println("-nopre ......................... Skip precomputation algorithms (where optional)"); @@ -1774,6 +1805,14 @@ public class PrismSettings implements Observer QuantAbstractRefine.printOptions(mainLog); return true; } + else if (sw.equals("ii") || sw.equals("intervaliter")) { + mainLog.println("Switch: -intervaliter (or -ii) optionally takes a comma-separated list of options:\n"); + mainLog.println(" -intervaliter:option1,option2,...\n"); + mainLog.println("where the options are one of the following:\n"); + mainLog.println(OptionsIntervalIteration.getOptionsDescription()); + return true; + } + return false; } diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index c2badabd..739d4742 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -82,6 +82,8 @@ public class StateModelChecker extends PrismComponent implements ModelChecker protected int engine; // Parameter for termination criterion protected double termCritParam; + // Use interval iteration? + protected boolean doIntervalIteration; // Verbose mode? protected boolean verbose; // Store the final results vector after model checking? @@ -119,6 +121,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker // Store locally and/or pass onto engines engine = prism.getEngine(); termCritParam = prism.getTermCritParam(); + doIntervalIteration = prism.getSettings().getBoolean(PrismSettings.PRISM_INTERVAL_ITER); verbose = prism.getVerbose(); storeVector = prism.getStoreVector(); genStrat = prism.getGenStrat();