From 5c33a555ac85465393c30609e0f253cfd1b839aa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= Date: Tue, 7 May 2019 12:28:42 +0200 Subject: [PATCH] Move BSCC post processing into steady-state computation for BSCCs --- prism/src/explicit/DTMCModelChecker.java | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index f2c46618..f9449602 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -2256,10 +2256,7 @@ public class DTMCModelChecker extends ProbModelChecker if (initInOneBSCC > -1) { mainLog.println("\nInitial states are all in one BSCC (so no reachability probabilities computed)"); BitSet bscc = bsccs.get(initInOneBSCC); - computeSteadyStateProbsForBSCC(dtmc, bscc, solnProbs); - if (bsccPostProcessor != null) { - bsccPostProcessor.apply(solnProbs, bscc); - } + computeSteadyStateProbsForBSCC(dtmc, bscc, solnProbs, bsccPostProcessor); } // Otherwise, have to consider all the BSCCs @@ -2285,10 +2282,7 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.println("\nComputing steady-state probabilities for BSCC " + (b + 1)); BitSet bscc = bsccs.get(b); // Compute steady-state probabilities for the BSCC - computeSteadyStateProbsForBSCC(dtmc, bscc, solnProbs); - if (bsccPostProcessor != null) { - bsccPostProcessor.apply(solnProbs, bscc); - } + computeSteadyStateProbsForBSCC(dtmc, bscc, solnProbs, bsccPostProcessor); // Multiply by BSCC reach prob for (int i = bscc.nextSetBit(0); i >= 0; i = bscc.nextSetBit(i + 1)) solnProbs[i] *= probBSCCs[b]; @@ -2354,10 +2348,7 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.println("\nComputing steady state probabilities for BSCC " + (b + 1)); BitSet bscc = bsccs.get(b); // Compute steady-state probabilities for the BSCC - computeSteadyStateProbsForBSCC(dtmc, bscc, ssProbs); - if (bsccPostProcessor != null) { - bsccPostProcessor.apply(ssProbs, bscc); - } + computeSteadyStateProbsForBSCC(dtmc, bscc, ssProbs, bsccPostProcessor); // Compute weighted sum of probabilities with mult valueBSCCs[b] = 0.0; if (mult == null) { @@ -2448,9 +2439,10 @@ public class DTMCModelChecker extends ProbModelChecker *

* @param dtmc The DTMC * @param states The BSCC to be analysed + * @param bsccPostProcessor Post-processor for the values of each BSCC (optional: null means no post-processing) * @param result Storage for result (ignored if null) */ - public ModelCheckerResult computeSteadyStateProbsForBSCC(DTMC dtmc, BitSet states, double result[]) throws PrismException + public ModelCheckerResult computeSteadyStateProbsForBSCC(DTMC dtmc, BitSet states, double result[], BSCCPostProcessor bsccPostProcessor) throws PrismException { if (dtmc.getModelType() != ModelType.DTMC) { throw new PrismNotSupportedException("Explicit engine currently does not support steady-state computation for " + dtmc.getModelType()); @@ -2574,11 +2566,17 @@ public class DTMCModelChecker extends ProbModelChecker throw new PrismException(msg); } + // Apply post processing + if (bsccPostProcessor != null) { + bsccPostProcessor.apply(result, states); + } + // Return results ModelCheckerResult res = new ModelCheckerResult(); res.soln = result; res.numIters = iters; res.timeTaken = watch.elapsedSeconds(); + return res; }