diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 4bf9d5b2..836df459 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -249,17 +249,12 @@ public class DTMCModelChecker extends ProbModelChecker int invMap[] = pair.second; int modelProductSize = modelProduct.getNumStates(); - // Find accepting maximum end components - mainLog.println("\nFinding accepting end components..."); - - // Compute accepting BSCCs + // Find accepting BSCCs + compute reachability probabilities + mainLog.println("\nFinding accepting BSCCs..."); BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCs(dra, modelProduct, invMap, sccMethod); mainLog.println(acceptingBSCCs); - - // Compute reachability probabilities mainLog.println("\nComputing reachability probabilities..."); mcProduct = new DTMCModelChecker(); - probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acceptingBSCCs).soln, modelProduct); // Mapping probabilities in the original model