Add option -nobackward to PrismSettings (disables computations relying on the predecessor relation). [from Joachim Klein]

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

prism/src/explicit/ProbModelChecker.java

@@ -72,6 +72,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	protected boolean precomp = true;
 	protected boolean prob0 = true;
 	protected boolean prob1 = true;
+	protected boolean useBackward = true;
 	// Direction of convergence for value iteration (lfp/gfp)
 	protected ValIterDir valIterDir = ValIterDir.BELOW;
 	// Method used for numerical solution
@@ -210,6 +211,8 @@ public class ProbModelChecker extends NonProbModelChecker
 			setProb0(settings.getBoolean(PrismSettings.PRISM_PROB0));
 			// PRISM_PROB1
 			setProb1(settings.getBoolean(PrismSettings.PRISM_PROB1));
+			// PRISM_USE_PRE
+			setUseBackward(settings.getBoolean(PrismSettings.PRISM_USE_BACKWARD));
 			// PRISM_FAIRNESS
 			if (settings.getBoolean(PrismSettings.PRISM_FAIRNESS)) {
 				throw new PrismNotSupportedException("The explicit engine does not support model checking MDPs under fairness");
@@ -340,6 +343,14 @@ public class ProbModelChecker extends NonProbModelChecker
 		this.prob1 = prob1;
 	}
 
+	/**
+	 * Set whether or not to use precomputed Pre relation
+	 */
+	public void setUseBackward(boolean useBackward)
+	{
+		this.useBackward = useBackward;
+	}
+
 	/**
 	 * Set direction of convergence for value iteration (lfp/gfp).
 	 */
@@ -421,6 +432,11 @@ public class ProbModelChecker extends NonProbModelChecker
 		return prob1;
 	}
 
+	public boolean getUseBackward()
+	{
+		return useBackward;
+	}
+
 	public ValIterDir getValIterDir()
 	{
 		return valIterDir;

prism/src/prism/Prism.java

@@ -775,6 +775,11 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	{
 		return settings.getBoolean(PrismSettings.PRISM_PROB1);
 	}
+	
+	public boolean getUseBackward()
+	{
+		return settings.getBoolean(PrismSettings.PRISM_USE_BACKWARD);
+	}
 
 	public boolean getFairness()
 	{

prism/src/prism/PrismSettings.java

@@ -77,6 +77,7 @@ public class PrismSettings implements Observer
 	public static final	String PRISM_PRECOMPUTATION					= "prism.precomputation";
 	public static final	String PRISM_PROB0							= "prism.prob0";
 	public static final	String PRISM_PROB1							= "prism.prob1";
+	public static final	String PRISM_USE_BACKWARD					= "prism.useBackward";
 	public static final	String PRISM_FIX_DEADLOCKS					= "prism.fixDeadlocks";
 	public static final	String PRISM_DO_PROB_CHECKS					= "prism.doProbChecks";
 	public static final	String PRISM_SUM_ROUND_OFF					= "prism.sumRoundOff";
@@ -248,6 +249,8 @@ public class PrismSettings implements Observer
 																			"Whether to use model checking precomputation algorithm Prob0 (if precomputation enabled)." },
 			{ BOOLEAN_TYPE,		PRISM_PROB1,							"Use Prob1 precomputation",				"4.0.2",		new Boolean(true),															"",																							
 																			"Whether to use model checking precomputation algorithm Prob1 (if precomputation enabled)." },
+			{ BOOLEAN_TYPE,		PRISM_USE_BACKWARD,							"Use backward reachability (Pre relation)",		"4.2.1",		new Boolean(true),											"",
+																			"Whether to use a precomputed Pre relation in several algorithms." },
 			{ BOOLEAN_TYPE,		PRISM_FAIRNESS,							"Use fairness",							"2.1",			new Boolean(false),															"",																							
 																			"Constrain to fair adversaries when model checking MDPs." },
 			{ BOOLEAN_TYPE,		PRISM_FIX_DEADLOCKS,					"Automatically fix deadlocks",			"4.0.3",		new Boolean(true),															"",																							
@@ -1015,6 +1018,9 @@ public class PrismSettings implements Observer
 		else if (sw.equals("noprob1")) {
 			set(PRISM_PROB1, false);
 		}
+		else if (sw.equals("nobackward")) {
+			set(PRISM_USE_BACKWARD, false);
+		}
 		// Fix deadlocks on/off
 		else if (sw.equals("fixdl")) {
 			set(PRISM_FIX_DEADLOCKS, true);