From 661ba7d16f37e879d0426377c6a79cc9711b4f40 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Aug 2015 22:58:35 +0200 Subject: [PATCH] Further work on new reward model Former-commit-id: c3873a2dec1d15f5641bd7c875bc785bb7aa7fb5 --- .../csl/SparseCtmcCslModelChecker.cpp | 80 +++++++++---------- .../csl/SparseCtmcCslModelChecker.h | 17 ++-- 2 files changed, 48 insertions(+), 49 deletions(-) diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 9b6818884..ccffd7b3d 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -20,23 +20,23 @@ namespace storm { namespace modelchecker { - template - SparseCtmcCslModelChecker::SparseCtmcCslModelChecker(storm::models::sparse::Ctmc const& model) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::LinearEquationSolverFactory()) { + template + SparseCtmcCslModelChecker::SparseCtmcCslModelChecker(SparseCtmcModelType const& model) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::LinearEquationSolverFactory()) { // Intentionally left empty. } - template - SparseCtmcCslModelChecker::SparseCtmcCslModelChecker(storm::models::sparse::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + template + SparseCtmcCslModelChecker::SparseCtmcCslModelChecker(SparseCtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } - template - bool SparseCtmcCslModelChecker::canHandle(storm::logic::Formula const& formula) const { + template + bool SparseCtmcCslModelChecker::canHandle(storm::logic::Formula const& formula) const { return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula(); } - template - std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + template + std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; @@ -54,16 +54,16 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound))); } - template - std::unique_ptr SparseCtmcCslModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + template + std::unique_ptr SparseCtmcCslModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector result = SparseDtmcPrctlModelChecker::computeNextProbabilitiesHelper(this->computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), subResult.getTruthValuesVector(), *this->linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } - template - std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + template + std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -71,13 +71,13 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeUntilProbabilitiesHelper(this->computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory))); } - template - storm::models::sparse::Ctmc const& SparseCtmcCslModelChecker::getModel() const { + template + storm::models::sparse::Ctmc const& SparseCtmcCslModelChecker::getModel() const { return this->template getModelAs>(); } - template - std::vector SparseCtmcCslModelChecker::computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound) const { + template + std::vector SparseCtmcCslModelChecker::computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound) const { // If the time bounds are [0, inf], we rather call untimed reachability. storm::utility::ConstantsComparator comparator; if (comparator.isZero(lowerBound) && comparator.isInfinity(upperBound)) { @@ -240,8 +240,8 @@ namespace storm { return result; } - template - storm::storage::SparseMatrix SparseCtmcCslModelChecker::computeUniformizedMatrix(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, ValueType uniformizationRate, std::vector const& exitRates) { + template + storm::storage::SparseMatrix SparseCtmcCslModelChecker::computeUniformizedMatrix(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, ValueType uniformizationRate, std::vector const& exitRates) { STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << "."); STORM_LOG_DEBUG("Keeping " << maybeStates.getNumberOfSetBits() << " rows."); @@ -267,9 +267,9 @@ namespace storm { return uniformizedMatrix; } - template + template template - std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { ValueType lambda = timeBound * uniformizationRate; @@ -350,18 +350,18 @@ namespace storm { return result; } - template - std::vector SparseCtmcCslModelChecker::computeUntilProbabilitiesHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + template + std::vector SparseCtmcCslModelChecker::computeUntilProbabilitiesHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return SparseDtmcPrctlModelChecker::computeUntilProbabilitiesHelper(transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolverFactory); } - template - std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + template + std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeInstantaneousRewardsHelper(rewardPathFormula.getContinuousTimeBound()))); } - template - std::vector SparseCtmcCslModelChecker::computeInstantaneousRewardsHelper(double timeBound) const { + template + std::vector SparseCtmcCslModelChecker::computeInstantaneousRewardsHelper(double timeBound) const { // Only compute the result if the model has a state-based reward this->getModel(). STORM_LOG_THROW(this->getModel().hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -384,13 +384,13 @@ namespace storm { return result; } - template - std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + template + std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeCumulativeRewardsHelper(rewardPathFormula.getContinuousTimeBound()))); } - template - std::vector SparseCtmcCslModelChecker::computeCumulativeRewardsHelper(double timeBound) const { + template + std::vector SparseCtmcCslModelChecker::computeCumulativeRewardsHelper(double timeBound) const { // Only compute the result if the model has a state-based reward this->getModel(). STORM_LOG_THROW(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -426,8 +426,8 @@ namespace storm { return this->computeTransientProbabilities(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, *this->linearEquationSolverFactory); } - template - storm::storage::SparseMatrix SparseCtmcCslModelChecker::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates) { + template + storm::storage::SparseMatrix SparseCtmcCslModelChecker::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates) { // Turn the rates into probabilities by scaling each row with the exit rate of the state. storm::storage::SparseMatrix result(rateMatrix); for (uint_fast64_t row = 0; row < result.getRowCount(); ++row) { @@ -438,8 +438,8 @@ namespace storm { return result; } - template - storm::storage::SparseMatrix SparseCtmcCslModelChecker::computeGeneratorMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates) { + template + storm::storage::SparseMatrix SparseCtmcCslModelChecker::computeGeneratorMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates) { storm::storage::SparseMatrix generatorMatrix(rateMatrix, true); // Place the negative exit rate on the diagonal. @@ -454,8 +454,8 @@ namespace storm { return generatorMatrix; } - template - std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + template + std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); @@ -473,8 +473,8 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(SparseDtmcPrctlModelChecker::computeReachabilityRewardsHelper(probabilityMatrix, modifiedStateRewardVector, this->getModel().getOptionalTransitionRewardMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *linearEquationSolverFactory, qualitative))); } - template - std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + template + std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -483,7 +483,7 @@ namespace storm { } template - std::vector SparseCtmcCslModelChecker::computeLongRunAverageHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslModelChecker::computeLongRunAverageHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // If there are no goal states, we avoid the computation and directly return zero. uint_fast64_t numOfStates = transitionMatrix.getRowCount(); if (psiStates.empty()) { @@ -708,7 +708,7 @@ namespace storm { // Explicitly instantiate the model checker. - template class SparseCtmcCslModelChecker; + template class SparseCtmcCslModelChecker>; } // namespace modelchecker } // namespace storm \ No newline at end of file diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index af1c9394a..498eea05b 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -13,17 +13,19 @@ namespace storm { template class HybridCtmcCslModelChecker; - template + template class SparseDtmcPrctlModelChecker; - template - class SparseCtmcCslModelChecker : public SparsePropositionalModelChecker { + template + class SparseCtmcCslModelChecker : public SparsePropositionalModelChecker { public: + typedef typename SparseCtmcModelType::ValueType ValueType; + friend class HybridCtmcCslModelChecker; - friend class SparseDtmcPrctlModelChecker; + friend class SparseDtmcPrctlModelChecker; - explicit SparseCtmcCslModelChecker(storm::models::sparse::Ctmc const& model); - explicit SparseCtmcCslModelChecker(storm::models::sparse::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory); + explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model); + explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; @@ -35,9 +37,6 @@ namespace storm { virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, 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; - protected: - storm::models::sparse::Ctmc const& getModel() const override; - private: // The methods that perform the actual checking. std::vector computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound) const;