Bug fix in explicit engine CTMC until model checking (spotted by Chris Dehnert) (probably due to recent ProbModelChecker refactoring).

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

prism/src/explicit/CTMCModelChecker.java

@@ -230,6 +230,34 @@ public class CTMCModelChecker extends DTMCModelChecker
 		return super.computeNextProbs(dtmcEmb, target);
 	}
 
+	/**
+	 * Compute reachability probabilities.
+	 * i.e. compute the probability of reaching a state in {@code target}.
+	 * @param ctmc The CTMC
+	 * @param target Target states
+	 */
+	public ModelCheckerResult computeReachProbs(CTMC ctmc, BitSet target) throws PrismException
+	{
+		mainLog.println("Building embedded DTMC...");
+		DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC();
+		return super.computeReachProbs(dtmcEmb, target);
+	}
+
+	/**
+	 * Compute until probabilities.
+	 * i.e. compute the probability of reaching a state in {@code target},
+	 * while remaining in those in @{code remain}.
+	 * @param dtmc The CTMC
+	 * @param remain Remain in these states (optional: null means "all")
+	 * @param target Target states
+	 */
+	public ModelCheckerResult computeUntilProbs(CTMC ctmc, BitSet remain, BitSet target) throws PrismException
+	{
+		mainLog.println("Building embedded DTMC...");
+		DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC();
+		return super.computeUntilProbs(dtmcEmb, remain, target);
+	}
+
 	/**
 	 * Compute reachability/until probabilities.
 	 * i.e. compute the probability of reaching a state in {@code target},