Bug fix: computing next probs in explicit engine (was not converted to embedded DTMC).

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

prism/src/explicit/CTMCModelChecker.java

@@ -201,6 +201,19 @@ public class CTMCModelChecker extends DTMCModelChecker
 
 	// Numerical computation functions
 
+	/**
+	 * Compute next=state probabilities.
+	 * i.e. compute the probability of being in a state in {@code target} in the next step.
+	 * @param dtmc The DTMC
+	 * @param target Target states
+	 */
+	public ModelCheckerResult computeNextProbs(DTMC dtmc, BitSet target) throws PrismException
+	{
+		mainLog.println("Building embedded DTMC...");
+		DTMC dtmcEmb = ((CTMC) dtmc).buildImplicitEmbeddedDTMC();
+		return super.computeNextProbs(dtmcEmb, target);
+	}
+
 	/**
 	 * Compute reachability/until probabilities.
 	 * i.e. compute the probability of reaching a state in {@code target},