(explicit iteration refactoring) Expose topological value iterations via the -topological switch

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

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;

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);
 	}
 
 	/**

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
 	 */

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;

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 <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();
 		mainLog.println("MODEL CHECKING OPTIONS:");
 		mainLog.println("-nopre ......................... Skip precomputation algorithms (where optional)");