From 71070cb2818784cc0b26620f84f487b5f27cb3cd Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 26 Jan 2016 16:19:32 +0100 Subject: [PATCH] Implemented expected time on CTMC by reduction to DTMC with rewards Former-commit-id: ebd3603069d846c5c4237287417f374816f8e8f0 --- .../csl/SparseCtmcCslModelChecker.cpp | 15 ++++++++++++--- src/modelchecker/csl/SparseCtmcCslModelChecker.h | 1 + .../csl/helper/SparseCtmcCslHelper.cpp | 12 +++++++++++- src/modelchecker/csl/helper/SparseCtmcCslHelper.h | 2 ++ 4 files changed, 26 insertions(+), 4 deletions(-) diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 14631fba5..37eaaad52 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -31,7 +31,7 @@ namespace storm { template bool SparseCtmcCslModelChecker::canHandle(storm::logic::Formula const& formula) const { - return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula(); + return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula() || formula.isExpectedTimeOperatorFormula(); } template @@ -101,8 +101,17 @@ namespace storm { storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverage(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), qualitative, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); - } - + } + + template + std::unique_ptr SparseCtmcCslModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { + 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); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + // Explicitly instantiate the model checker. template class SparseCtmcCslModelChecker>; diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index 8423cac53..7e25376a1 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -28,6 +28,7 @@ namespace storm { virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), 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; virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: // An object that is used for solving linear equations and performing matrix-vector multiplication. diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 453496ce2..51c58848c 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -650,11 +650,21 @@ namespace storm { return result; } + 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) { + // 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); + } + 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); - } } } \ No newline at end of file diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h index fae4d8498..dfa0ef877 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -28,6 +28,8 @@ namespace storm { static std::vector computeLongRunAverage(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); + /*! * Computes the matrix representing the transitions of the uniformized CTMC. *