From e4b3f4eeb9c5cdb7de9552f5efddcfba5c2ad4c9 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 3 Aug 2016 15:13:12 +0200 Subject: [PATCH] intermediate commit, come back after refactoring formulae Former-commit-id: 147133876fc1d13fda3785007ac048265b4204ce --- src/modelchecker/AbstractModelChecker.cpp | 175 ++++++++++++------ src/modelchecker/AbstractModelChecker.h | 61 +++--- .../csl/HybridCtmcCslModelChecker.cpp | 50 +++-- .../csl/HybridCtmcCslModelChecker.h | 34 ++-- .../csl/SparseCtmcCslModelChecker.cpp | 22 +-- .../csl/SparseCtmcCslModelChecker.h | 22 +-- .../SparseMarkovAutomatonCslModelChecker.cpp | 12 +- .../SparseMarkovAutomatonCslModelChecker.h | 12 +- .../SparseExplorationModelChecker.cpp | 4 +- .../SparseExplorationModelChecker.h | 6 +- .../prctl/HybridDtmcPrctlModelChecker.cpp | 18 +- .../prctl/HybridDtmcPrctlModelChecker.h | 18 +- .../prctl/HybridMdpPrctlModelChecker.cpp | 16 +- .../prctl/HybridMdpPrctlModelChecker.h | 18 +- .../prctl/SparseDtmcPrctlModelChecker.h | 22 +-- .../prctl/SparseMdpPrctlModelChecker.cpp | 20 +- .../prctl/SparseMdpPrctlModelChecker.h | 20 +- .../prctl/SymbolicDtmcPrctlModelChecker.cpp | 16 +- .../prctl/SymbolicDtmcPrctlModelChecker.h | 16 +- .../prctl/SymbolicMdpPrctlModelChecker.cpp | 16 +- .../prctl/SymbolicMdpPrctlModelChecker.h | 16 +- .../SparsePropositionalModelChecker.cpp | 6 +- .../SparsePropositionalModelChecker.h | 8 +- .../SymbolicPropositionalModelChecker.cpp | 54 +++--- .../SymbolicPropositionalModelChecker.h | 28 ++- .../SparseDtmcEliminationModelChecker.cpp | 14 +- src/modelchecker/results/CheckResult.h | 9 +- .../results/ExplicitQuantitativeCheckResult.h | 2 +- .../results/HybridQuantitativeCheckResult.h | 4 +- .../results/QuantitativeCheckResult.cpp | 15 +- .../results/QuantitativeCheckResult.h | 3 +- .../results/SymbolicQuantitativeCheckResult.h | 4 +- 32 files changed, 399 insertions(+), 342 deletions(-) diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 4fd86a13e..717421f64 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -9,9 +9,17 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InternalTypeErrorException.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Ctmc.h" +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/MarkovAutomaton.h" +#include "src/models/sparse/StandardRewardModel.h" + namespace storm { namespace modelchecker { - std::unique_ptr AbstractModelChecker::check(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::check(CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); STORM_LOG_THROW(this->canHandle(checkTask), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'."); if (formula.isStateFormula()) { @@ -19,8 +27,9 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } - - std::unique_ptr AbstractModelChecker::computeProbabilities(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeProbabilities(CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isBoundedUntilFormula()) { return this->computeBoundedUntilProbabilities(checkTask.substituteFormula(formula.asBoundedUntilFormula())); @@ -37,34 +46,41 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } - - std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula(); storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer()); return this->computeUntilProbabilities(checkTask.substituteFormula(newFormula)); } - - std::unique_ptr AbstractModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeNextProbabilities(CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::Formula const& rewardFormula = checkTask.getFormula(); if (rewardFormula.isCumulativeRewardFormula()) { return this->computeCumulativeRewards(rewardMeasureType, checkTask.substituteFormula(rewardFormula.asCumulativeRewardFormula())); @@ -79,44 +95,53 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' is invalid."); } - - std::unique_ptr AbstractModelChecker::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::Formula const& timeFormula = checkTask.getFormula(); if (timeFormula.isReachabilityTimeFormula()) { return this->computeReachabilityTimes(rewardMeasureType, checkTask.substituteFormula(timeFormula.asReachabilityTimeFormula())); } STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::checkStateFormula(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::checkStateFormula(CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isBinaryBooleanStateFormula()) { return this->checkBinaryBooleanStateFormula(checkTask.substituteFormula(stateFormula.asBinaryBooleanStateFormula())); @@ -141,24 +166,27 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); } - - std::unique_ptr AbstractModelChecker::checkAtomicExpressionFormula(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::checkAtomicExpressionFormula(CheckTask const& checkTask) { storm::logic::AtomicExpressionFormula const& stateFormula = checkTask.getFormula(); std::stringstream stream; stream << stateFormula.getExpression(); return this->checkAtomicLabelFormula(checkTask.substituteFormula(storm::logic::AtomicLabelFormula(stream.str()))); } - - std::unique_ptr AbstractModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::checkBinaryBooleanStateFormula(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::checkBinaryBooleanStateFormula(CheckTask const& checkTask) { storm::logic::BinaryBooleanStateFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(stateFormula.getLeftSubformula().isStateFormula() && stateFormula.getRightSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - std::unique_ptr leftResult = this->check(checkTask.substituteFormula(stateFormula.getLeftSubformula().asStateFormula())); - std::unique_ptr rightResult = this->check(checkTask.substituteFormula(stateFormula.getRightSubformula().asStateFormula())); + std::unique_ptr leftResult = this->check(checkTask.template substituteFormula(stateFormula.getLeftSubformula().asStateFormula())); + std::unique_ptr rightResult = this->check(checkTask.template substituteFormula(stateFormula.getRightSubformula().asStateFormula())); STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative results."); @@ -172,36 +200,40 @@ namespace storm { return leftResult; } - - std::unique_ptr AbstractModelChecker::checkBooleanLiteralFormula(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::checkBooleanLiteralFormula(CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - - std::unique_ptr AbstractModelChecker::checkProbabilityOperatorFormula(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::checkProbabilityOperatorFormula(CheckTask const& checkTask) { storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr result = this->computeProbabilities(checkTask.substituteFormula(stateFormula.getSubformula())); if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getThreshold()); + return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getThreshold()); } else { return result; } } - - std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(CheckTask const& checkTask) { storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr result = this->computeRewards(stateFormula.getMeasureType(), checkTask.substituteFormula(stateFormula.getSubformula())); if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } } - - std::unique_ptr AbstractModelChecker::checkTimeOperatorFormula(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::checkTimeOperatorFormula(CheckTask const& checkTask) { storm::logic::TimeOperatorFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(stateFormula.getSubformula().isReachabilityTimeFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); @@ -209,13 +241,14 @@ namespace storm { if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } } - - std::unique_ptr AbstractModelChecker::checkLongRunAverageOperatorFormula(CheckTask const& checkTask) { + + template + std::unique_ptr AbstractModelChecker::checkLongRunAverageOperatorFormula(CheckTask const& checkTask) { storm::logic::LongRunAverageOperatorFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); @@ -223,15 +256,16 @@ namespace storm { if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } } - std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(CheckTask const& checkTask) { + template + std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(CheckTask const& checkTask) { storm::logic::UnaryBooleanStateFormula const& stateFormula = checkTask.getFormula(); - std::unique_ptr subResult = this->check(checkTask.substituteFormula(stateFormula.getSubformula())); + std::unique_ptr subResult = this->check(checkTask.template substituteFormula(stateFormula.getSubformula())); STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result."); if (stateFormula.isNot()) { subResult->asQualitativeCheckResult().complement(); @@ -240,5 +274,28 @@ namespace storm { } return subResult; } + + // Explicitly instantiate the template class. + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + +#ifdef STORM_HAVE_CARL + template class AbstractModelChecker>>; + + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; +#endif } } diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index b6f009197..d65e9aad7 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -12,12 +12,15 @@ namespace storm { class CheckResult; enum class RewardType { Expectation, Variance }; - + + template class AbstractModelChecker { public: virtual ~AbstractModelChecker() { // Intentionally left empty. } + + typedef typename ModelType::ValueType ValueType; /*! * Determines whether the model checker can handle the given verification task. If this method returns @@ -26,7 +29,7 @@ namespace storm { * @param checkTask The task for which to check whether the model checker can handle it. * @return True iff the model checker can check the given task. */ - virtual bool canHandle(CheckTask const& checkTask) const = 0; + virtual bool canHandle(CheckTask const& checkTask) const = 0; /*! * Checks the provided formula. @@ -34,41 +37,41 @@ namespace storm { * @param checkTask The verification task to pursue. * @return The verification result. */ - virtual std::unique_ptr check(CheckTask const& checkTask); + virtual std::unique_ptr check(CheckTask const& checkTask); // The methods to compute probabilities for path formulas. - virtual std::unique_ptr computeProbabilities(CheckTask const& checkTask); - virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask); - virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask); - virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask); - virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask); - virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask); - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask); // The methods to compute the rewards for path formulas. - virtual std::unique_ptr computeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); - virtual std::unique_ptr computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); - virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); - virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); + virtual std::unique_ptr computeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); + virtual std::unique_ptr computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); + virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); + virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); // The methods to compute the long-run average probabilities and timing measures. - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask); - virtual std::unique_ptr computeTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); - virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); + virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); // The methods to check state formulas. - virtual std::unique_ptr checkStateFormula(CheckTask const& stateFormula); - virtual std::unique_ptr checkAtomicExpressionFormula(CheckTask const& checkTask); - virtual std::unique_ptr checkAtomicLabelFormula(CheckTask const& checkTask); - virtual std::unique_ptr checkBinaryBooleanStateFormula(CheckTask const& checkTask); - virtual std::unique_ptr checkBooleanLiteralFormula(CheckTask const& checkTask); - virtual std::unique_ptr checkProbabilityOperatorFormula(CheckTask const& checkTask); - virtual std::unique_ptr checkRewardOperatorFormula(CheckTask const& checkTask); - virtual std::unique_ptr checkTimeOperatorFormula(CheckTask const& checkTask); - virtual std::unique_ptr checkLongRunAverageOperatorFormula(CheckTask const& checkTask); - virtual std::unique_ptr checkUnaryBooleanStateFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkStateFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkAtomicExpressionFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkAtomicLabelFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkBinaryBooleanStateFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkBooleanLiteralFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkProbabilityOperatorFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkRewardOperatorFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkTimeOperatorFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkLongRunAverageOperatorFormula(CheckTask const& checkTask); + virtual std::unique_ptr checkUnaryBooleanStateFormula(CheckTask const& checkTask); }; } } diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index ade2717b0..22ddc1cc6 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -14,24 +14,24 @@ namespace storm { namespace modelchecker { - template - HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { + template + HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { // Intentionally left empty. } - template - HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + template + HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } - template - bool HybridCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { + template + bool HybridCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true)); } - template - std::unique_ptr HybridCtmcCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + template + std::unique_ptr HybridCtmcCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -41,8 +41,8 @@ namespace storm { return storm::modelchecker::helper::HybridCtmcCslHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template - std::unique_ptr HybridCtmcCslModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + template + std::unique_ptr HybridCtmcCslModelChecker::computeNextProbabilities(CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -50,13 +50,9 @@ namespace storm { return storm::modelchecker::helper::HybridCtmcCslHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector()); } - template - storm::models::symbolic::Ctmc const& HybridCtmcCslModelChecker::getModel() const { - return this->template getModelAs>(); - } - - template - std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + + template + std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -64,8 +60,8 @@ namespace storm { return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); } - template - std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + template + std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -84,20 +80,20 @@ namespace storm { return storm::modelchecker::helper::HybridCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); } - template - std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } - template - std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } - template - std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + template + std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -106,8 +102,8 @@ namespace storm { } // Explicitly instantiate the model checker. - template class HybridCtmcCslModelChecker; - template class HybridCtmcCslModelChecker; + template class HybridCtmcCslModelChecker>; + template class HybridCtmcCslModelChecker>; } // namespace modelchecker } // namespace storm \ No newline at end of file diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h index 0d69f5220..49f0feef5 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -9,26 +9,26 @@ namespace storm { namespace modelchecker { - - template - class HybridCtmcCslModelChecker : public SymbolicPropositionalModelChecker { + + template + class HybridCtmcCslModelChecker : public SymbolicPropositionalModelChecker { public: - explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model); - explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory); + typedef typename ModelType::ValueType ValueType; + static const storm::dd::DdType DdType = ModelType::DdType; + + explicit HybridCtmcCslModelChecker(ModelType const& model); + explicit HybridCtmcCslModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; - - protected: - storm::models::symbolic::Ctmc const& getModel() const override; - + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + private: // An object that is used for solving linear equations and performing matrix-vector multiplication. std::unique_ptr> linearEquationSolverFactory; diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 914b71cc1..42ca25ca7 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -34,26 +34,26 @@ namespace storm { } template - bool SparseCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { + bool SparseCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { return SparseCtmcCslModelChecker::canHandleImplementation(checkTask); } template template::SupportsExponential, int>::type> - bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { + bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true)); } template template::SupportsExponential, int>::type> - bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { + bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true)); } template - std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -74,7 +74,7 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeNextProbabilities(CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -83,7 +83,7 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -94,21 +94,21 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -118,7 +118,7 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -129,7 +129,7 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index f63aba841..d637493d6 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -22,22 +22,22 @@ namespace storm { explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; private: template::SupportsExponential, int>::type = 0> - bool canHandleImplementation(CheckTask const& checkTask) const; + bool canHandleImplementation(CheckTask const& checkTask) const; template::SupportsExponential, int>::type = 0> - bool canHandleImplementation(CheckTask const& checkTask) const; + bool canHandleImplementation(CheckTask const& checkTask) const; // An object that is used for solving linear equations and performing matrix-vector multiplication. std::unique_ptr> linearEquationSolverFactory; diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 7a49b563d..b12fb11ce 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -30,7 +30,7 @@ namespace storm { } template - bool SparseMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { + bool SparseMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::FragmentSpecification fragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setReachabilityRewardFormulasAllowed(true); fragment.setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true); @@ -38,7 +38,7 @@ namespace storm { } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.getLeftSubformula().isTrueFormula(), storm::exceptions::NotImplementedException, "Only bounded properties of the form 'true U[t1, t2] phi' are currently supported."); @@ -60,7 +60,7 @@ namespace storm { } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -72,7 +72,7 @@ namespace storm { } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton."); @@ -85,7 +85,7 @@ namespace storm { } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long-run average in non-closed Markov automaton."); @@ -97,7 +97,7 @@ namespace storm { } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute expected times in non-closed Markov automaton."); diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index ed5b5cd39..5fbfb85e4 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -20,12 +20,12 @@ namespace storm { explicit SparseMarkovAutomatonCslModelChecker(SparseMarkovAutomatonModelType const& model); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; private: // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. diff --git a/src/modelchecker/exploration/SparseExplorationModelChecker.cpp b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp index b98a3ca7c..795fc3af4 100644 --- a/src/modelchecker/exploration/SparseExplorationModelChecker.cpp +++ b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp @@ -40,14 +40,14 @@ namespace storm { } template - bool SparseExplorationModelChecker::canHandle(CheckTask const& checkTask) const { + bool SparseExplorationModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::FragmentSpecification fragment = storm::logic::reachability(); return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet(); } template - std::unique_ptr SparseExplorationModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseExplorationModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& untilFormula = checkTask.getFormula(); storm::logic::Formula const& conditionFormula = untilFormula.getLeftSubformula(); storm::logic::Formula const& targetFormula = untilFormula.getRightSubformula(); diff --git a/src/modelchecker/exploration/SparseExplorationModelChecker.h b/src/modelchecker/exploration/SparseExplorationModelChecker.h index bc41ace7a..d582fec38 100644 --- a/src/modelchecker/exploration/SparseExplorationModelChecker.h +++ b/src/modelchecker/exploration/SparseExplorationModelChecker.h @@ -31,16 +31,16 @@ namespace storm { using namespace exploration_detail; template - class SparseExplorationModelChecker : public AbstractModelChecker { + class SparseExplorationModelChecker : public AbstractModelChecker { public: typedef StateType ActionType; typedef std::vector> StateActionStack; SparseExplorationModelChecker(storm::prism::Program const& program); - virtual bool canHandle(CheckTask const& checkTask) const override; + virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; private: std::tuple performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const; diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index f0cd46154..82982b9cd 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -36,13 +36,13 @@ namespace storm { } template - bool HybridDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool HybridDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true)); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -52,7 +52,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -60,7 +60,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -68,7 +68,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -79,21 +79,21 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -106,7 +106,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index 620aa2952..5ae9dd360 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -17,15 +17,15 @@ namespace storm { explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; protected: storm::models::symbolic::Dtmc const& getModel() const override; diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 7d480fcf2..06b3696f7 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -30,13 +30,13 @@ namespace storm { } template - bool HybridMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool HybridMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr HybridMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -47,7 +47,7 @@ namespace storm { } template - std::unique_ptr HybridMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + std::unique_ptr HybridMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); @@ -56,7 +56,7 @@ namespace storm { } template - std::unique_ptr HybridMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + std::unique_ptr HybridMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); @@ -65,7 +65,7 @@ namespace storm { } template - std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); @@ -77,7 +77,7 @@ namespace storm { } template - std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); @@ -85,7 +85,7 @@ namespace storm { } template - std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); @@ -93,7 +93,7 @@ namespace storm { } template - std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h index fc09704ac..0da318b51 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -1,4 +1,4 @@ -#ifndef STORM_MODELCHECKER_HYBRIDMDPPRCTLMODELCHECKER_H_ + #ifndef STORM_MODELCHECKER_HYBRIDMDPPRCTLMODELCHECKER_H_ #define STORM_MODELCHECKER_HYBRIDMDPPRCTLMODELCHECKER_H_ #include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h" @@ -24,14 +24,14 @@ namespace storm { explicit HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; protected: storm::models::symbolic::Mdp const& getModel() const override; diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index d577676b0..31e97e378 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -19,18 +19,18 @@ namespace storm { explicit SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; private: // An object that is used for retrieving linear equation solvers. diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 25804c37a..c0bbe6efa 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -39,13 +39,13 @@ namespace storm { } template - bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true)); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -57,7 +57,7 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); @@ -67,7 +67,7 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -83,7 +83,7 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); @@ -93,7 +93,7 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidPropertyException, "Cannot compute conditional probabilities on MDPs with more than one initial state."); @@ -109,7 +109,7 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); @@ -118,7 +118,7 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); @@ -127,7 +127,7 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); @@ -137,7 +137,7 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(stateFormula); diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index c8dcf4489..4ff9f153d 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -17,16 +17,16 @@ namespace storm { explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model, std::unique_ptr>&& MinMaxLinearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; private: // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 9612608df..6c08ac856 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -33,13 +33,13 @@ namespace storm { } template - bool SymbolicDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool SymbolicDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -50,7 +50,7 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -59,7 +59,7 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -68,7 +68,7 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -80,7 +80,7 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); @@ -88,7 +88,7 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); @@ -96,7 +96,7 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index 883af5ba5..1f21466be 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -14,14 +14,14 @@ namespace storm { explicit SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; protected: storm::models::symbolic::Dtmc const& getModel() const override; diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index f9f2ca37b..5b29b82b2 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -32,13 +32,13 @@ namespace storm { } template - bool SymbolicMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool SymbolicMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -49,7 +49,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); @@ -58,7 +58,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); @@ -67,7 +67,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); @@ -79,7 +79,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); @@ -87,7 +87,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); @@ -95,7 +95,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SymbolicMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index 83cb17244..8cce0eaac 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -16,14 +16,14 @@ namespace storm { explicit SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; protected: storm::models::symbolic::Mdp const& getModel() const override; diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp index 0725cc4a2..6654e3aba 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -23,13 +23,13 @@ namespace storm { } template - bool SparsePropositionalModelChecker::canHandle(CheckTask const& checkTask) const { + bool SparsePropositionalModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::propositional()); } template - std::unique_ptr SparsePropositionalModelChecker::checkBooleanLiteralFormula(CheckTask const& checkTask) { + std::unique_ptr SparsePropositionalModelChecker::checkBooleanLiteralFormula(CheckTask const& checkTask) { storm::logic::BooleanLiteralFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isTrueFormula()) { return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true))); @@ -39,7 +39,7 @@ namespace storm { } template - std::unique_ptr SparsePropositionalModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { + std::unique_ptr SparsePropositionalModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { storm::logic::AtomicLabelFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getStates(stateFormula.getLabel()))); diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.h b/src/modelchecker/propositional/SparsePropositionalModelChecker.h index e0bd83bff..504a809b7 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.h +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.h @@ -8,7 +8,7 @@ namespace storm { namespace modelchecker { template - class SparsePropositionalModelChecker : public AbstractModelChecker { + class SparsePropositionalModelChecker : public AbstractModelChecker { public: typedef typename SparseModelType::ValueType ValueType; typedef typename SparseModelType::RewardModelType RewardModelType; @@ -16,9 +16,9 @@ namespace storm { explicit SparsePropositionalModelChecker(SparseModelType const& model); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr checkBooleanLiteralFormula(CheckTask const& checkTask) override; - virtual std::unique_ptr checkAtomicLabelFormula(CheckTask const& checkTask) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr checkBooleanLiteralFormula(CheckTask const& checkTask) override; + virtual std::unique_ptr checkAtomicLabelFormula(CheckTask const& checkTask) override; protected: /*! diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index eee71e3c8..d9de796d2 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -17,61 +17,55 @@ namespace storm { namespace modelchecker { - template - SymbolicPropositionalModelChecker::SymbolicPropositionalModelChecker(storm::models::symbolic::Model const& model) : model(model) { + template + SymbolicPropositionalModelChecker::SymbolicPropositionalModelChecker(storm::models::symbolic::Model const& model) : model(model) { // Intentionally left empty. } - template - bool SymbolicPropositionalModelChecker::canHandle(CheckTask const& checkTask) const { + template + bool SymbolicPropositionalModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::propositional()); } - template - std::unique_ptr SymbolicPropositionalModelChecker::checkBooleanLiteralFormula(CheckTask const& checkTask) { + template + std::unique_ptr SymbolicPropositionalModelChecker::checkBooleanLiteralFormula(CheckTask const& checkTask) { storm::logic::BooleanLiteralFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isTrueFormula()) { - return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getReachableStates())); + return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getReachableStates())); } else { - return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero())); + return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero())); } } - template - std::unique_ptr SymbolicPropositionalModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { + template + std::unique_ptr SymbolicPropositionalModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { storm::logic::AtomicLabelFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); - return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getStates(stateFormula.getLabel()))); + return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getStates(stateFormula.getLabel()))); } - template - std::unique_ptr SymbolicPropositionalModelChecker::checkAtomicExpressionFormula(CheckTask const& checkTask) { + template + std::unique_ptr SymbolicPropositionalModelChecker::checkAtomicExpressionFormula(CheckTask const& checkTask) { storm::logic::AtomicExpressionFormula const& stateFormula = checkTask.getFormula(); - return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getStates(stateFormula.getExpression()))); + return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getStates(stateFormula.getExpression()))); } - template - storm::models::symbolic::Model const& SymbolicPropositionalModelChecker::getModel() const { - return model; - } - - template template - ModelType const& SymbolicPropositionalModelChecker::getModelAs() const { - return dynamic_cast(model); + storm::models::symbolic::Model const& SymbolicPropositionalModelChecker::getModel() const { + return model; } + // Explicitly instantiate the template class. - template storm::models::symbolic::Dtmc const& SymbolicPropositionalModelChecker::getModelAs() const; - template storm::models::symbolic::Ctmc const& SymbolicPropositionalModelChecker::getModelAs() const; - template storm::models::symbolic::Mdp const& SymbolicPropositionalModelChecker::getModelAs() const; - template class SymbolicPropositionalModelChecker; - template storm::models::symbolic::Dtmc const& SymbolicPropositionalModelChecker::getModelAs() const; - template storm::models::symbolic::Ctmc const& SymbolicPropositionalModelChecker::getModelAs() const; - template storm::models::symbolic::Mdp const& SymbolicPropositionalModelChecker::getModelAs() const; - template class SymbolicPropositionalModelChecker; + + template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; } } \ No newline at end of file diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h index d11896900..c58af239d 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h @@ -15,16 +15,18 @@ namespace storm { namespace modelchecker { - template - class SymbolicPropositionalModelChecker : public AbstractModelChecker { + template + class SymbolicPropositionalModelChecker : public AbstractModelChecker { public: - explicit SymbolicPropositionalModelChecker(storm::models::symbolic::Model const& model); + typedef typename ModelType::ValueType ValueType; + static const storm::dd::DdType DdType = ModelType::DdType; + explicit SymbolicPropositionalModelChecker(ModelType const& model); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr checkBooleanLiteralFormula(CheckTask const& checkTask) override; - virtual std::unique_ptr checkAtomicLabelFormula(CheckTask const& checkTask) override; - virtual std::unique_ptr checkAtomicExpressionFormula(CheckTask const& checkTask) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr checkBooleanLiteralFormula(CheckTask const& checkTask) override; + virtual std::unique_ptr checkAtomicLabelFormula(CheckTask const& checkTask) override; + virtual std::unique_ptr checkAtomicExpressionFormula(CheckTask const& checkTask) override; protected: /*! @@ -32,19 +34,11 @@ namespace storm { * * @return The model associated with this model checker instance. */ - virtual storm::models::symbolic::Model const& getModel() const; - - /*! - * Retrieves the model associated with this model checker instance as the given template parameter type. - * - * @return The model associated with this model checker instance. - */ - template - ModelType const& getModelAs() const; + virtual ModelType const& getModel() const; private: // The model that is to be analyzed by the model checker. - storm::models::symbolic::Model const& model; + ModelType const& model; }; } diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index fdf541d97..3337fd14a 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -46,7 +46,7 @@ namespace storm { } template - bool SparseDtmcEliminationModelChecker::canHandle(CheckTask const& checkTask) const { + bool SparseDtmcEliminationModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::FragmentSpecification fragment = storm::logic::prctl().setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false); fragment.setNestedOperatorsAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true); @@ -54,7 +54,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); @@ -113,7 +113,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { // Do some sanity checks to establish some required properties. RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : ""); STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); @@ -320,7 +320,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); // Retrieve the appropriate bitvectors by model checking the subformulas. @@ -423,7 +423,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); // Retrieve the appropriate bitvectors by model checking the subformulas. @@ -497,7 +497,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); // Retrieve the appropriate bitvectors by model checking the subformulas. @@ -594,7 +594,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); // Retrieve the appropriate bitvectors by model checking the subformulas. diff --git a/src/modelchecker/results/CheckResult.h b/src/modelchecker/results/CheckResult.h index 152fc9e3b..b17a4dfc6 100644 --- a/src/modelchecker/results/CheckResult.h +++ b/src/modelchecker/results/CheckResult.h @@ -11,6 +11,7 @@ namespace storm { namespace modelchecker { // Forward-declare the existing subclasses. class QualitativeCheckResult; + template class QuantitativeCheckResult; class ExplicitQualitativeCheckResult; @@ -55,9 +56,11 @@ namespace storm { QualitativeCheckResult& asQualitativeCheckResult(); QualitativeCheckResult const& asQualitativeCheckResult() const; - QuantitativeCheckResult& asQuantitativeCheckResult(); - QuantitativeCheckResult const& asQuantitativeCheckResult() const; - + template + QuantitativeCheckResult& asQuantitativeCheckResult(); + template + QuantitativeCheckResult const& asQuantitativeCheckResult() const; + ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const; diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h index ee49b74ec..78f9766ca 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -14,7 +14,7 @@ namespace storm { namespace modelchecker { template - class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult { + class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult { public: typedef std::vector vector_type; typedef std::map map_type; diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h index 02e1dc4ed..7faacdb27 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.h +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h @@ -11,7 +11,7 @@ namespace storm { namespace modelchecker { template - class HybridQuantitativeCheckResult : public QuantitativeCheckResult { + class HybridQuantitativeCheckResult : public QuantitativeCheckResult { public: HybridQuantitativeCheckResult() = default; HybridQuantitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& symbolicStates, storm::dd::Add const& symbolicValues, storm::dd::Bdd const& explicitStates, storm::dd::Odd const& odd, std::vector const& explicitValues); @@ -23,7 +23,7 @@ namespace storm { HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult&& other) = default; #endif - virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override; + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType bound) const override; std::unique_ptr toExplicitQuantitativeCheckResult() const; diff --git a/src/modelchecker/results/QuantitativeCheckResult.cpp b/src/modelchecker/results/QuantitativeCheckResult.cpp index 6618f6231..533fc43d1 100644 --- a/src/modelchecker/results/QuantitativeCheckResult.cpp +++ b/src/modelchecker/results/QuantitativeCheckResult.cpp @@ -8,12 +8,21 @@ namespace storm { namespace modelchecker { - std::unique_ptr QuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + + template + std::unique_ptr QuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result."); } - + + template bool QuantitativeCheckResult::isQuantitative() const { return true; } + + template class QuantitativeCheckResult; + +#ifdef STORM_HAVE_CARL + template class QuantitativeCheckResult; +#endif } -} \ No newline at end of file +} diff --git a/src/modelchecker/results/QuantitativeCheckResult.h b/src/modelchecker/results/QuantitativeCheckResult.h index 32f348818..bb268ae3f 100644 --- a/src/modelchecker/results/QuantitativeCheckResult.h +++ b/src/modelchecker/results/QuantitativeCheckResult.h @@ -5,11 +5,12 @@ namespace storm { namespace modelchecker { + template class QuantitativeCheckResult : public CheckResult { public: virtual ~QuantitativeCheckResult() = default; - virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const; + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const; virtual void oneMinus() = 0; diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h index 9cbb272a3..74ed7fe99 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -9,7 +9,7 @@ namespace storm { namespace modelchecker { template - class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult { + class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult { public: SymbolicQuantitativeCheckResult() = default; SymbolicQuantitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Add const& values); @@ -21,7 +21,7 @@ namespace storm { SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult&& other) = default; #endif - virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override; + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType bound) const override; virtual bool isSymbolic() const override; virtual bool isResultForAllStates() const override;