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<class ValueType> - SparseCtmcCslModelChecker<ValueType>::SparseCtmcCslModelChecker(storm::models::sparse::Ctmc<ValueType> const& model) : SparsePropositionalModelChecker<ValueType>(model), linearEquationSolverFactory(new storm::utility::solver::LinearEquationSolverFactory<ValueType>()) { + template <typename SparseCtmcModelType> + SparseCtmcCslModelChecker<SparseCtmcModelType>::SparseCtmcCslModelChecker(SparseCtmcModelType const& model) : SparsePropositionalModelChecker<ValueType>(model), linearEquationSolverFactory(new storm::utility::solver::LinearEquationSolverFactory<ValueType>()) { // Intentionally left empty. } - template<class ValueType> - SparseCtmcCslModelChecker<ValueType>::SparseCtmcCslModelChecker(storm::models::sparse::Ctmc<ValueType> const& model, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : SparsePropositionalModelChecker<ValueType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + template <typename SparseCtmcModelType> + SparseCtmcCslModelChecker<SparseCtmcModelType>::SparseCtmcCslModelChecker(SparseCtmcModelType const& model, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : SparsePropositionalModelChecker<ValueType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } - template<class ValueType> - bool SparseCtmcCslModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const { + template <typename SparseCtmcModelType> + bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandle(storm::logic::Formula const& formula) const { return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula(); } - template<class ValueType> - std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<ValueType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { + template <typename SparseCtmcModelType> + std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; @@ -54,16 +54,16 @@ namespace storm { return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound))); } - template<class ValueType> - std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { + template <typename SparseCtmcModelType> + std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector<ValueType> result = SparseDtmcPrctlModelChecker<ValueType>::computeNextProbabilitiesHelper(this->computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), subResult.getTruthValuesVector(), *this->linearEquationSolverFactory); return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(result))); } - template<class ValueType> - std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { + template <typename SparseCtmcModelType> + std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -71,13 +71,13 @@ namespace storm { return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeUntilProbabilitiesHelper(this->computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory))); } - template<class ValueType> - storm::models::sparse::Ctmc<ValueType> const& SparseCtmcCslModelChecker<ValueType>::getModel() const { + template <typename SparseCtmcModelType> + storm::models::sparse::Ctmc<ValueType> const& SparseCtmcCslModelChecker<SparseCtmcModelType>::getModel() const { return this->template getModelAs<storm::models::sparse::Ctmc<ValueType>>(); } - template<class ValueType> - std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& exitRates, bool qualitative, double lowerBound, double upperBound) const { + template <typename SparseCtmcModelType> + std::vector<ValueType> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& exitRates, bool qualitative, double lowerBound, double upperBound) const { // If the time bounds are [0, inf], we rather call untimed reachability. storm::utility::ConstantsComparator<ValueType> comparator; if (comparator.isZero(lowerBound) && comparator.isInfinity(upperBound)) { @@ -240,8 +240,8 @@ namespace storm { return result; } - template<class ValueType> - storm::storage::SparseMatrix<ValueType> SparseCtmcCslModelChecker<ValueType>::computeUniformizedMatrix(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, ValueType uniformizationRate, std::vector<ValueType> const& exitRates) { + template <typename SparseCtmcModelType> + storm::storage::SparseMatrix<ValueType> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeUniformizedMatrix(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, ValueType uniformizationRate, std::vector<ValueType> 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<class ValueType> + template <typename SparseCtmcModelType> template<bool computeCumulativeReward> - std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, std::vector<ValueType> const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { + std::vector<ValueType> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, std::vector<ValueType> const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { ValueType lambda = timeBound * uniformizationRate; @@ -350,18 +350,18 @@ namespace storm { return result; } - template<class ValueType> - std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeUntilProbabilitiesHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { + template <typename SparseCtmcModelType> + std::vector<ValueType> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeUntilProbabilitiesHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { return SparseDtmcPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolverFactory); } - template<class ValueType> - std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<ValueType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { + template <typename SparseCtmcModelType> + std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(rewardPathFormula.getContinuousTimeBound()))); } - template<class ValueType> - std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeInstantaneousRewardsHelper(double timeBound) const { + template <typename SparseCtmcModelType> + std::vector<ValueType> SparseCtmcCslModelChecker<SparseCtmcModelType>::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<class ValueType> - std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<ValueType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { + template <typename SparseCtmcModelType> + std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(rewardPathFormula.getContinuousTimeBound()))); } - template<class ValueType> - std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeCumulativeRewardsHelper(double timeBound) const { + template <typename SparseCtmcModelType> + std::vector<ValueType> SparseCtmcCslModelChecker<SparseCtmcModelType>::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<true>(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, *this->linearEquationSolverFactory); } - template<class ValueType> - storm::storage::SparseMatrix<ValueType> SparseCtmcCslModelChecker<ValueType>::computeProbabilityMatrix(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRates) { + template <typename SparseCtmcModelType> + storm::storage::SparseMatrix<ValueType> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeProbabilityMatrix(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRates) { // Turn the rates into probabilities by scaling each row with the exit rate of the state. storm::storage::SparseMatrix<ValueType> result(rateMatrix); for (uint_fast64_t row = 0; row < result.getRowCount(); ++row) { @@ -438,8 +438,8 @@ namespace storm { return result; } - template<class ValueType> - storm::storage::SparseMatrix<ValueType> SparseCtmcCslModelChecker<ValueType>::computeGeneratorMatrix(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRates) { + template <typename SparseCtmcModelType> + storm::storage::SparseMatrix<ValueType> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeGeneratorMatrix(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRates) { storm::storage::SparseMatrix<ValueType> generatorMatrix(rateMatrix, true); // Place the negative exit rate on the diagonal. @@ -454,8 +454,8 @@ namespace storm { return generatorMatrix; } - template<class ValueType> - std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { + template <typename SparseCtmcModelType> + std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); storm::storage::SparseMatrix<ValueType> probabilityMatrix = computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); @@ -473,8 +473,8 @@ namespace storm { return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(SparseDtmcPrctlModelChecker<ValueType>::computeReachabilityRewardsHelper(probabilityMatrix, modifiedStateRewardVector, this->getModel().getOptionalTransitionRewardMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *linearEquationSolverFactory, qualitative))); } - template<class ValueType> - std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<ValueType>::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { + template <typename SparseCtmcModelType> + std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -483,7 +483,7 @@ namespace storm { } template<typename ValueType> - std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeLongRunAverageHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { + std::vector<ValueType> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeLongRunAverageHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> 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<double>; + template class SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>>; } // 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<storm::dd::DdType DdType, typename ValueType> class HybridCtmcCslModelChecker; - template<typename ValueType> + template<typename SparseDtmcModelType> class SparseDtmcPrctlModelChecker; - template<class ValueType> - class SparseCtmcCslModelChecker : public SparsePropositionalModelChecker<ValueType> { + template<class SparseCtmcModelType> + class SparseCtmcCslModelChecker : public SparsePropositionalModelChecker<SparseCtmcModelType> { public: + typedef typename SparseCtmcModelType::ValueType ValueType; + friend class HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, ValueType>; - friend class SparseDtmcPrctlModelChecker<ValueType>; + friend class SparseDtmcPrctlModelChecker<SparseCtmcModelType>; - explicit SparseCtmcCslModelChecker(storm::models::sparse::Ctmc<ValueType> const& model); - explicit SparseCtmcCslModelChecker(storm::models::sparse::Ctmc<ValueType> const& model, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory); + explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model); + explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>>&& 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<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override; virtual std::unique_ptr<CheckResult> computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override; - protected: - storm::models::sparse::Ctmc<ValueType> const& getModel() const override; - private: // The methods that perform the actual checking. std::vector<ValueType> computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& exitRates, bool qualitative, double lowerBound, double upperBound) const;