From 20545b000869cab17248cbe3a8cc5afc14921cca Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 18 Jul 2013 21:10:25 +0000 Subject: [PATCH] Minor tweaks to new DTMC-LTL code. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7086 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) 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