Separate setting explicit engine for linear equation system solution method.

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

prism/src/explicit/DTMCModelChecker.java

@@ -291,12 +291,15 @@ public class DTMCModelChecker extends ProbModelChecker
 		BitSet no, yes;
 		int i, n, numYes, numNo;
 		long timer, timerProb0, timerProb1;
+		// Local copy of setting
+		LinEqMethod linEqMethod = this.linEqMethod;
 
-		// Check for some unsupported combinations
-		if (solnMethod == SolnMethod.VALUE_ITERATION && valIterDir == ValIterDir.ABOVE && !(precomp && prob0)) {
-			throw new PrismException("Precomputation (Prob0) must be enabled for value iteration from above");
+		// Switch to a supported method, if necessary
+		if (!(linEqMethod == LinEqMethod.POWER || linEqMethod == LinEqMethod.GAUSS_SEIDEL)) {
+			linEqMethod = LinEqMethod.GAUSS_SEIDEL;
+			mainLog.printWarning("Switching to linear equation solution method \"" + linEqMethod.fullName() + "\"");
 		}
-
+		
 		// Start probabilistic reachability
 		timer = System.currentTimeMillis();
 		mainLog.println("Starting probabilistic reachability...");
@@ -338,15 +341,15 @@ public class DTMCModelChecker extends ProbModelChecker
 		mainLog.println("target=" + target.cardinality() + ", yes=" + numYes + ", no=" + numNo + ", maybe=" + (n - (numYes + numNo)));
 
 		// Compute probabilities
-		switch (solnMethod) {
-		case VALUE_ITERATION:
+		switch (linEqMethod) {
+		case POWER:
 			res = computeReachProbsValIter(dtmc, no, yes, init, known);
 			break;
 		case GAUSS_SEIDEL:
 			res = computeReachProbsGaussSeidel(dtmc, no, yes, init, known);
 			break;
 		default:
-			throw new PrismException("Unknown DTMC solution method " + solnMethod);
+			throw new PrismException("Unknown linear equation solution method " + linEqMethod.fullName());
 		}
 
 		// Finished probabilistic reachability
@@ -808,6 +811,14 @@ public class DTMCModelChecker extends ProbModelChecker
 		BitSet inf;
 		int i, n, numTarget, numInf;
 		long timer, timerProb1;
+		// Local copy of setting
+		LinEqMethod linEqMethod = this.linEqMethod;
+
+		// Switch to a supported method, if necessary
+		if (!(linEqMethod == LinEqMethod.POWER)) {
+			linEqMethod = LinEqMethod.POWER;
+			mainLog.printWarning("Switching to linear equation solution method \"" + linEqMethod.fullName() + "\"");
+		}
 
 		// Start expected reachability
 		timer = System.currentTimeMillis();
@@ -840,12 +851,12 @@ public class DTMCModelChecker extends ProbModelChecker
 		mainLog.println("target=" + numTarget + ", inf=" + numInf + ", rest=" + (n - (numTarget + numInf)));
 
 		// Compute rewards
-		switch (solnMethod) {
-		case VALUE_ITERATION:
+		switch (linEqMethod) {
+		case POWER:
 			res = computeReachRewardsValIter(dtmc, mcRewards, target, inf, init, known);
 			break;
 		default:
-			throw new PrismException("Unknown DTMC solution method " + solnMethod);
+			throw new PrismException("Unknown linear equation solution method " + linEqMethod.fullName());
 		}
 
 		// Finished expected reachability

prism/src/explicit/ProbModelChecker.java

@@ -47,6 +47,8 @@ public class ProbModelChecker extends StateModelChecker
 {
 	// Flags/settings
 
+	// Method used to solve linear equation systems
+	protected LinEqMethod linEqMethod = LinEqMethod.GAUSS_SEIDEL;
 	// Iterative numerical method termination criteria
 	protected TermCrit termCrit = TermCrit.RELATIVE;
 	// Parameter for iterative numerical method termination criteria
@@ -67,6 +69,32 @@ public class ProbModelChecker extends StateModelChecker
 
 	// Enums for flags/settings
 
+	// Method used for numerical solution
+	public enum LinEqMethod {
+		POWER, JACOBI, GAUSS_SEIDEL, BACKWARDS_GAUSS_SEIDEL, JOR, SOR, BACKWARDS_SOR;
+		public String fullName()
+		{
+			switch (this) {
+			case POWER:
+				return "Power method";
+			case JACOBI:
+				return "Jacobi";
+			case GAUSS_SEIDEL:
+				return "Gauss-Seidel";
+			case BACKWARDS_GAUSS_SEIDEL:
+				return "Backwards Gauss-Seidel";
+			case JOR:
+				return "JOR";
+			case SOR:
+				return "SOR";
+			case BACKWARDS_SOR:
+				return "Backwards SOR";
+			default:
+				return this.toString();
+			}
+		}
+	};
+
 	// Iterative numerical method termination criteria
 	public enum TermCrit {
 		ABSOLUTE, RELATIVE
@@ -83,13 +111,33 @@ public class ProbModelChecker extends StateModelChecker
 	};
 
 	// Settings methods
-	
+
 	/**
 	 * Set settings from a PRISMSettings object.
 	 */
-	public void setSettings(PrismSettings settings)
+	public void setSettings(PrismSettings settings) throws PrismException
 	{
 		String s;
+		// PRISM_LIN_EQ_METHOD
+		s = settings.getString(PrismSettings.PRISM_LIN_EQ_METHOD);
+		if (s.equals("Power")) {
+			setLinEqMethod(LinEqMethod.POWER);
+		} else if (s.equals("Jacobi")) {
+			setLinEqMethod(LinEqMethod.JACOBI);
+		} else if (s.equals("Gauss-Seidel")) {
+			setLinEqMethod(LinEqMethod.GAUSS_SEIDEL);
+		} else if (s.equals("Backwards Gauss-Seidel")) {
+			setLinEqMethod(LinEqMethod.BACKWARDS_GAUSS_SEIDEL);
+		} else if (s.equals("JOR")) {
+			setLinEqMethod(LinEqMethod.JOR);
+		} else if (s.equals("SOR")) {
+			setLinEqMethod(LinEqMethod.SOR);
+		} else if (s.equals("Backwards SOR")) {
+			setLinEqMethod(LinEqMethod.BACKWARDS_SOR);
+		} else {
+			throw new PrismException("Explicit engine does not support linear equation solution method \"" + s + "\"");
+		}
+
 		s = settings.getString(PrismSettings.PRISM_TERM_CRIT);
 		if (s.equals("Absolute")) {
 			setTermCrit(TermCrit.ABSOLUTE);
@@ -102,12 +150,6 @@ public class ProbModelChecker extends StateModelChecker
 		setProb0(settings.getBoolean(PrismSettings.PRISM_PROB0));
 		setProb1(settings.getBoolean(PrismSettings.PRISM_PROB1));
 		// valiterdir
-		s = settings.getString(PrismSettings.PRISM_LIN_EQ_METHOD);
-		if (s.equals("Gauss-Seidel")) {
-			setSolnMethod(SolnMethod.GAUSS_SEIDEL);
-		} else {
-			setSolnMethod(SolnMethod.VALUE_ITERATION);
-		}
 		s = settings.getString(PrismSettings.PRISM_MDP_SOLN_METHOD);
 		if (s.equals("Gauss-Seidel")) {
 			setSolnMethod(SolnMethod.GAUSS_SEIDEL);
@@ -146,6 +188,7 @@ public class ProbModelChecker extends StateModelChecker
 	public void printSettings()
 	{
 		super.printSettings();
+		mainLog.print("linEqMethod = " + linEqMethod + " ");
 		mainLog.print("termCrit = " + termCrit + " ");
 		mainLog.print("termCritParam = " + termCritParam + " ");
 		mainLog.print("maxIters = " + maxIters + " ");
@@ -166,6 +209,14 @@ public class ProbModelChecker extends StateModelChecker
 		this.verbosity = verbosity;
 	}
 
+	/**
+	 * Set method used to solve linear equation systems.
+	 */
+	public void setLinEqMethod(LinEqMethod linEqMethod)
+	{
+		this.linEqMethod = linEqMethod;
+	}
+
 	/**
 	 * Set termination criteria type for numerical iterative methods.
 	 */
@@ -237,6 +288,11 @@ public class ProbModelChecker extends StateModelChecker
 		return verbosity;
 	}
 
+	public LinEqMethod getLinEqMethod()
+	{
+		return linEqMethod;
+	}
+
 	public TermCrit getTermCrit()
 	{
 		return termCrit;
@@ -377,7 +433,7 @@ public class ProbModelChecker extends StateModelChecker
 			return StateValues.createFromBitSet(sol, model);
 		}
 	}
-	
+
 	/**
 	 * Model check an R operator expression and return the values for all states.
 	 */
@@ -448,7 +504,7 @@ public class ProbModelChecker extends StateModelChecker
 		default:
 			throw new PrismException("Cannot build rewards for " + modelType + "s");
 		}
-		
+
 		// Compute rewards
 		mainLog.println("Building reward structure...");
 		switch (modelType) {