From 3e4ddbea8c285e0b7cfa943e1618b7f53ff4d060 Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 28 Jan 2016 14:27:24 +0100 Subject: [PATCH] Integrated expected time on parametric CTMCs Former-commit-id: 2f892ad8db092a0db585d13c40aacec1b354e8ee --- .../csl/SparseCtmcCslModelChecker.cpp | 2 +- .../csl/helper/SparseCtmcCslHelper.cpp | 16 +++++- .../csl/helper/SparseCtmcCslHelper.h | 2 +- .../SparseDtmcEliminationModelChecker.cpp | 56 +++++++++++-------- .../SparseDtmcEliminationModelChecker.h | 1 + src/utility/storm.h | 19 ++++++- 6 files changed, 66 insertions(+), 30 deletions(-) diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 16ab12244..a9b86d8c8 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -108,7 +108,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeExpectedTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeExpectedTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), this->getModel().getInitialStates(), subResult.getTruthValuesVector(), qualitative/*, *linearEquationSolverFactory*/); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 5cf10fd84..145eed1b1 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -1,6 +1,7 @@ #include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h" #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" +#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/models/sparse/StandardRewardModel.h" @@ -11,6 +12,8 @@ #include "src/storage/StronglyConnectedComponentDecomposition.h" +#include "src/adapters/CarlAdapter.h" + #include "src/utility/macros.h" #include "src/utility/vector.h" #include "src/utility/graph.h" @@ -647,20 +650,27 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative/*, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory*/) { // Compute expected time on CTMC by reduction to DTMC with rewards storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); std::vector totalRewardVector; for (auto exitRate : exitRateVector) { - totalRewardVector.push_back(1 / exitRate); + totalRewardVector.push_back(storm::utility::one() / exitRate); } - return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); + + return storm::modelchecker::SparseDtmcEliminationModelChecker>::computeReachabilityRewards(probabilityMatrix, backwardTransitions, initialStates, targetStates, totalRewardVector, false, qualitative); + // Enable again, if RationalFunction finally is supported + //return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); } template class SparseCtmcCslHelper; template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + +#ifdef STORM_HAVE_CARL + template std::vector SparseCtmcCslHelper::computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative/*, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory*/); +#endif } } } \ No newline at end of file diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h index ef744045e..94752a974 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -28,7 +28,7 @@ namespace storm { static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative/*, storm::utility::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory*/); /*! * Computes the matrix representing the transitions of the uniformized CTMC. diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 6ec1e6d86..41324957b 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -578,27 +578,40 @@ namespace storm { std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); - storm::storage::BitVector phiStates(this->getModel().getNumberOfStates(), true); - storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector targetStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); // Do some sanity checks to establish some required properties. RewardModelType const& rewardModel = this->getModel().getRewardModel(rewardModelName ? rewardModelName.get() : ""); + std::vector stateRewardValues = rewardModel.getTotalRewardVector(trueStates.getNumberOfSetBits(), this->getModel().getTransitionMatrix(), trueStates); + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); + std::vector result = computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates, stateRewardValues, this->computeResultsForInitialStatesOnly, qualitative, optimalityType); + + // Construct check result + std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); + return checkResult; + } + + template + std::vector SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector const& stateRewardValues, bool computeForInitialStatesOnly, bool qualitative, boost::optional const& optimalityType) { + + uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); - // Then, compute the subset of states that has a reachability reward less than infinity. - storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel().getBackwardTransitions(), trueStates, psiStates); + // Compute the subset of states that has a reachability reward less than infinity. + storm::storage::BitVector trueStates(numberOfStates, true); + storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(backwardTransitions, trueStates, targetStates); infinityStates.complement(); - storm::storage::BitVector maybeStates = ~psiStates & ~infinityStates; + storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly) { - if (this->getModel().getInitialStates().isSubsetOf(infinityStates)) { + if (computeForInitialStatesOnly) { + if (initialStates.isSubsetOf(infinityStates)) { STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); furtherComputationNeeded = false; } - if (this->getModel().getInitialStates().isSubsetOf(psiStates)) { + if (initialStates.isSubsetOf(targetStates)) { STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); furtherComputationNeeded = false; } @@ -608,40 +621,37 @@ namespace storm { if (furtherComputationNeeded) { // If we compute the results for the initial states only, we can cut off all maybe state that are not // reachable from them. - if (computeResultsForInitialStatesOnly) { + if (computeForInitialStatesOnly) { // Determine the set of states that is reachable from the initial state without jumping over a target state. - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, psiStates); + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(probabilityMatrix, initialStates, maybeStates, targetStates); // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). maybeStates &= reachableStates; } // Determine the set of initial states of the sub-model. - storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; + storm::storage::BitVector newInitialStates = initialStates % maybeStates; // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrix = probabilityMatrix.getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); // Project the state reward vector to all maybe-states. - std::vector stateRewardValues = rewardModel.getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel().getTransitionMatrix(), maybeStates); - - std::vector subresult = computeReachabilityValues(submatrix, stateRewardValues, submatrixTransposed, newInitialStates, computeResultsForInitialStatesOnly, phiStates, psiStates, this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates)); + std::vector rewardValues = storm::utility::vector::filterVector(stateRewardValues, maybeStates); + storm::storage::BitVector phiStates(numberOfStates, true); + std::vector subresult = computeReachabilityValues(submatrix, rewardValues, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, phiStates, targetStates, probabilityMatrix.getConstrainedRowSumVector(maybeStates, targetStates)); storm::utility::vector::setVectorValues(result, maybeStates, subresult); } // Construct full result. storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); - storm::utility::vector::setVectorValues(result, psiStates, storm::utility::zero()); - - // Construct check result based on whether we have computed values for all states or just the initial states. - std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + storm::utility::vector::setVectorValues(result, targetStates, storm::utility::zero()); + if (computeForInitialStatesOnly) { // If we computed the results for the initial (and inf) states only, we need to filter the result to // only communicate these results. - checkResult->filter(ExplicitQualitativeCheckResult(~maybeStates | this->getModel().getInitialStates())); + result = storm::utility::vector::filterVector(result, ~maybeStates | initialStates); } - return checkResult; + return result; } template diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 692a6be57..a840cef88 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -28,6 +28,7 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector const& stateRewardValues, bool computeForInitialStatesOnly, bool qualitative, boost::optional const& optimalityType = boost::optional()); virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; diff --git a/src/utility/storm.h b/src/utility/storm.h index a3d2e58ca..4bdf22556 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -58,6 +58,7 @@ #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" +#include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -329,8 +330,22 @@ namespace storm { std::shared_ptr> mdp = model->template as>(); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support MDPs."); } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = model->template as>(); - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support CTMCs."); + // Hack to avoid instantiating the CTMC Model Checker which currently does not work for rational functions + if (formula->isExpectedTimeOperatorFormula()) { + // We can only solve expected time for pCTMCs at the moment + std::shared_ptr> ctmc = model->template as>(); + + // Compute goal states + storm::logic::EventuallyFormula eventuallyFormula = formula->asExpectedTimeOperatorFormula().getSubformula().asEventuallyFormula(); + storm::modelchecker::SparsePropositionalModelChecker> propositionalModelchecker(*ctmc); + std::unique_ptr subResultPointer = propositionalModelchecker.check(eventuallyFormula.getSubformula()); + storm::modelchecker::ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeExpectedTimes(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), subResult.getTruthValuesVector(), false); + result = std::unique_ptr(new storm::modelchecker::ExplicitQuantitativeCheckResult(std::move(numericResult))); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support this property on CTMCs."); + } } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support " << model->getType()); }