(interval iteration) prepare settings for interval iteration

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12137 bbc10eb1-c90d-0410-af57-cb519fbb1720

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

prism/src/prism/OptionsIntervalIteration.java

@@ -0,0 +1,278 @@
+//==============================================================================
+//	
+//	Copyright (c) 2017-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (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=<x>     Select upper bound heuristic for reward computations\n");
+		sb.append("   <x> is one of " + boundMethodsList + "\n");
+		sb.append(" lower=<d>           Manually specify lower bound for reward computations (double value)\n");
+		sb.append(" upper=<d>           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<String, String> 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<Pair<String,String>> splitOptionsString(String options)
+	{
+		List<Pair<String,String>> 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;
+	}
+}

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));
 

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 <x> (or -e <x>) ....... Set value of epsilon (for convergence check) [default: 1e-6]");
 		mainLog.println("-maxiters <n> .................. 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;
 	}
 	

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();