From e83aeaa7cafcec63079a10765cc2a13ae53d0c9e Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 26 Jul 2018 11:22:03 +0200 Subject: [PATCH] explicit: refactor computeSteadyStateFormula (preparation for the same functionality in CTMCModelChecker) --- prism/src/explicit/DTMCModelChecker.java | 12 ++++++++++++ prism/src/explicit/ProbModelChecker.java | 6 +----- 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index f96f0af3..8e62701e 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -2156,6 +2156,18 @@ public class DTMCModelChecker extends ProbModelChecker return rv; } + /** + * Compute steady-state probabilities for an S operator, i.e., S=?[ b ]. + * @param dtmc the DTMC + * @param b the satisfaction set of states for the inner state formula of the operators + */ + protected StateValues computeSteadyStateFormula(DTMC dtmc, BitSet b) throws PrismException + { + double multProbs[] = Utils.bitsetToDoubleArray(b, dtmc.getNumStates()); + ModelCheckerResult res = computeSteadyStateBackwardsProbs(dtmc, multProbs); + return StateValues.createFromDoubleArray(res.soln, dtmc); + } + /** * Compute (forwards) steady-state probabilities * i.e. compute the long-run probability of being in each state, diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 892c05f6..1de83d2c 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -1207,16 +1207,12 @@ public class ProbModelChecker extends NonProbModelChecker BitSet b = checkExpression(model, expr, null).getBitSet(); // Compute/return the probabilities - ModelCheckerResult res = null; switch (model.getModelType()) { case DTMC: - double multProbs[] = Utils.bitsetToDoubleArray(b, model.getNumStates()); - res = ((DTMCModelChecker) this).computeSteadyStateBackwardsProbs((DTMC) model, multProbs); - break; + return ((DTMCModelChecker) this).computeSteadyStateFormula((DTMC) model, b); default: throw new PrismNotSupportedException("Explicit engine does not yet handle the S operator for " + model.getModelType() + "s"); } - return StateValues.createFromDoubleArray(res.soln, model); } // Utility methods for probability distributions