explicit: refactor computeSteadyStateFormula

(preparation for the same functionality in CTMCModelChecker)

prism/src/explicit/DTMCModelChecker.java

@@ -2156,6 +2156,18 @@ public class DTMCModelChecker extends ProbModelChecker
 		return rv;
 	}
 
+	/**
+	 * Compute steady-state probabilities for an S operator, i.e., S=?[ b ].
+	 * @param dtmc the DTMC
+	 * @param b the satisfaction set of states for the inner state formula of the operators
+	 */
+	protected StateValues computeSteadyStateFormula(DTMC dtmc, BitSet b) throws PrismException
+	{
+		double multProbs[] = Utils.bitsetToDoubleArray(b, dtmc.getNumStates());
+		ModelCheckerResult res = computeSteadyStateBackwardsProbs(dtmc, multProbs);
+		return StateValues.createFromDoubleArray(res.soln, dtmc);
+	}
+
 	/**
 	 * Compute (forwards) steady-state probabilities
 	 * i.e. compute the long-run probability of being in each state,

prism/src/explicit/ProbModelChecker.java

@@ -1207,16 +1207,12 @@ public class ProbModelChecker extends NonProbModelChecker
 		BitSet b = checkExpression(model, expr, null).getBitSet();
 
 		// Compute/return the probabilities
-		ModelCheckerResult res = null;
 		switch (model.getModelType()) {
 		case DTMC:
-			double multProbs[] = Utils.bitsetToDoubleArray(b, model.getNumStates());
-			res = ((DTMCModelChecker) this).computeSteadyStateBackwardsProbs((DTMC) model, multProbs);
-			break;
+			return ((DTMCModelChecker) this).computeSteadyStateFormula((DTMC) model, b);
 		default:
 			throw new PrismNotSupportedException("Explicit engine does not yet handle the S operator for " + model.getModelType() + "s");
 		}
-		return StateValues.createFromDoubleArray(res.soln, model);
 	}
 
 	// Utility methods for probability distributions