From f7a3e02fb6beea6b48d61963d58a9a6d6b60cc36 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 3 Aug 2016 21:33:49 +0200 Subject: [PATCH] refactored model checkers st all are templated in the model, have to handle rational function bounds next Former-commit-id: b665709a52ee22b68c24107a30d6f430b6ecf8f5 --- src/logic/Bound.h | 8 +- src/logic/OperatorFormula.h | 3 +- src/modelchecker/AbstractModelChecker.cpp | 15 ++++ .../csl/SparseCtmcCslModelChecker.cpp | 8 +- .../csl/SparseCtmcCslModelChecker.h | 8 +- .../SparseExplorationModelChecker.cpp | 85 ++++++++++--------- .../SparseExplorationModelChecker.h | 5 +- .../prctl/HybridDtmcPrctlModelChecker.cpp | 56 ++++++------ .../prctl/HybridDtmcPrctlModelChecker.h | 14 +-- .../prctl/HybridMdpPrctlModelChecker.cpp | 52 ++++++------ .../prctl/HybridMdpPrctlModelChecker.h | 16 ++-- .../prctl/SparseDtmcPrctlModelChecker.cpp | 22 ++--- .../prctl/SymbolicDtmcPrctlModelChecker.cpp | 52 ++++++------ .../prctl/SymbolicDtmcPrctlModelChecker.h | 16 ++-- .../prctl/SymbolicMdpPrctlModelChecker.cpp | 51 +++++------ .../prctl/SymbolicMdpPrctlModelChecker.h | 15 ++-- .../prctl/helper/HybridDtmcPrctlHelper.cpp | 2 +- .../prctl/helper/HybridMdpPrctlHelper.cpp | 2 +- .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 2 +- .../SymbolicPropositionalModelChecker.cpp | 4 +- .../SymbolicPropositionalModelChecker.h | 1 + .../SparseDtmcEliminationModelChecker.h | 14 +-- src/modelchecker/results/CheckResult.cpp | 11 +-- src/modelchecker/results/CheckResult.h | 9 +- .../ExplicitQuantitativeCheckResult.cpp | 20 ++--- .../results/ExplicitQuantitativeCheckResult.h | 2 +- .../results/HybridQuantitativeCheckResult.cpp | 2 +- .../results/HybridQuantitativeCheckResult.h | 2 +- .../results/QuantitativeCheckResult.cpp | 5 +- .../SymbolicQuantitativeCheckResult.cpp | 2 +- .../results/SymbolicQuantitativeCheckResult.h | 5 +- src/utility/constants.cpp | 6 ++ src/utility/storm.h | 22 ++--- 33 files changed, 274 insertions(+), 263 deletions(-) diff --git a/src/logic/Bound.h b/src/logic/Bound.h index e56a2c04f..7c9769f8a 100644 --- a/src/logic/Bound.h +++ b/src/logic/Bound.h @@ -12,10 +12,10 @@ namespace storm { // Intentionally left empty. } - template - Bound convertToOtherValueType() const { - return Bound(comparisonType, storm::utility::convertNumber(threshold)); - } + //template + //Bound convertToOtherValueType() const { + // return Bound(comparisonType, storm::utility::convertNumber(threshold)); + //} ComparisonType comparisonType; ValueType threshold; diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index 04324e2d9..a1247d431 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -11,7 +11,8 @@ #include "src/utility/constants.h" namespace storm { - namespace logic { + namespace logic { + struct OperatorInformation { OperatorInformation(boost::optional const& optimizationDirection = boost::none, boost::optional> const& bound = boost::none); diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 5f9d2fbf7..616dcf828 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -12,8 +12,13 @@ #include "src/models/sparse/Dtmc.h" #include "src/models/sparse/Ctmc.h" #include "src/models/sparse/Mdp.h" +#include "src/models/symbolic/Dtmc.h" +#include "src/models/symbolic/Ctmc.h" +#include "src/models/symbolic/Mdp.h" #include "src/models/sparse/MarkovAutomaton.h" #include "src/models/sparse/StandardRewardModel.h" +#include "src/storage/dd/Add.h" +#include "src/storage/dd/Bdd.h" namespace storm { namespace modelchecker { @@ -275,7 +280,10 @@ namespace storm { return subResult; } + /////////////////////////////////////////////// // Explicitly instantiate the template class. + /////////////////////////////////////////////// + // Sparse template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; @@ -297,5 +305,12 @@ namespace storm { template class AbstractModelChecker>; template class AbstractModelChecker>; #endif + // DD + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; } } diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 42ca25ca7..f8eae1206 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -39,15 +39,15 @@ namespace storm { } template - template::SupportsExponential, int>::type> - bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { + template::SupportsExponential, int>::type> + 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 { + template::SupportsExponential, int>::type> + 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)); } diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index d637493d6..1a062d5ca 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -33,11 +33,11 @@ namespace storm { 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; + template::SupportsExponential, int>::type = 0> + bool canHandleImplementation(CheckTask const& checkTask) const; - template::SupportsExponential, int>::type = 0> - bool canHandleImplementation(CheckTask const& checkTask) const; + template::SupportsExponential, int>::type = 0> + 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/exploration/SparseExplorationModelChecker.cpp b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp index 795fc3af4..328c80796 100644 --- a/src/modelchecker/exploration/SparseExplorationModelChecker.cpp +++ b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp @@ -17,6 +17,8 @@ #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/models/sparse/StandardRewardModel.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/CoreSettings.h" @@ -34,20 +36,20 @@ namespace storm { namespace modelchecker { - template - SparseExplorationModelChecker::SparseExplorationModelChecker(storm::prism::Program const& program) : program(program.substituteConstants()), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule().getPrecision()) { + template + SparseExplorationModelChecker::SparseExplorationModelChecker(storm::prism::Program const& program) : program(program.substituteConstants()), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule().getPrecision()) { // Intentionally left empty. } - template - bool SparseExplorationModelChecker::canHandle(CheckTask const& checkTask) const { + template + 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) { + template + 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(); @@ -67,8 +69,8 @@ namespace storm { return std::make_unique>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState)); } - template - std::tuple SparseExplorationModelChecker::performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const { + template + std::tuple SparseExplorationModelChecker::performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const { // Generate the initial state so we know where to start the simulation. stateGeneration.computeInitialStates(); STORM_LOG_THROW(stateGeneration.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the exploration engine."); @@ -120,8 +122,8 @@ namespace storm { return std::make_tuple(initialStateIndex, bounds.getLowerBoundForState(initialStateIndex, explorationInformation), bounds.getUpperBoundForState(initialStateIndex, explorationInformation)); } - template - bool SparseExplorationModelChecker::samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, Bounds& bounds, Statistics& stats) const { + template + bool SparseExplorationModelChecker::samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, Bounds& bounds, Statistics& stats) const { // Start the search from the initial state. stack.push_back(std::make_pair(stateGeneration.getFirstInitialState(), 0)); @@ -182,8 +184,8 @@ namespace storm { return foundTerminalState; } - template - bool SparseExplorationModelChecker::exploreState(StateGeneration& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation& explorationInformation, Bounds& bounds, Statistics& stats) const { + template + bool SparseExplorationModelChecker::exploreState(StateGeneration& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation& explorationInformation, Bounds& bounds, Statistics& stats) const { bool isTerminalState = false; bool isTargetState = false; @@ -284,8 +286,8 @@ namespace storm { return isTerminalState; } - template - typename SparseExplorationModelChecker::ActionType SparseExplorationModelChecker::sampleActionOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, Bounds& bounds) const { + template + typename SparseExplorationModelChecker::ActionType SparseExplorationModelChecker::sampleActionOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, Bounds& bounds) const { // Determine the values of all available actions. std::vector> actionValues; StateType rowGroup = explorationInformation.getRowGroup(currentStateId); @@ -322,8 +324,8 @@ namespace storm { return actionValues[distribution(randomGenerator)].first; } - template - StateType SparseExplorationModelChecker::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { + template + StateType SparseExplorationModelChecker::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { std::vector> const& row = explorationInformation.getRowOfMatrix(chosenAction); if (row.size() == 1) { return row.front().getColumn(); @@ -354,8 +356,8 @@ namespace storm { } } - template - bool SparseExplorationModelChecker::performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, Bounds& bounds, Statistics& stats) const { + template + bool SparseExplorationModelChecker::performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, Bounds& bounds, Statistics& stats) const { ++stats.numberOfPrecomputations; // Outline: @@ -487,8 +489,8 @@ namespace storm { return true; } - template - void SparseExplorationModelChecker::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector const& relevantStates, storm::storage::SparseMatrix const& relevantStatesMatrix, ExplorationInformation& explorationInformation, Bounds& bounds) const { + template + void SparseExplorationModelChecker::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector const& relevantStates, storm::storage::SparseMatrix const& relevantStatesMatrix, ExplorationInformation& explorationInformation, Bounds& bounds) const { bool containsTargetState = false; // Now we record all actions leaving the EC. @@ -556,8 +558,8 @@ namespace storm { } } - template - ValueType SparseExplorationModelChecker::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { + template + typename ModelType::ValueType SparseExplorationModelChecker::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { ValueType result = storm::utility::zero(); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation); @@ -565,8 +567,8 @@ namespace storm { return result; } - template - ValueType SparseExplorationModelChecker::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { + template + typename ModelType::ValueType SparseExplorationModelChecker::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { ValueType result = storm::utility::zero(); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation); @@ -574,8 +576,8 @@ namespace storm { return result; } - template - std::pair SparseExplorationModelChecker::computeBoundsOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { + template + std::pair SparseExplorationModelChecker::computeBoundsOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { // TODO: take into account self-loops? std::pair result = std::make_pair(storm::utility::zero(), storm::utility::zero()); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { @@ -585,8 +587,8 @@ namespace storm { return result; } - template - std::pair SparseExplorationModelChecker::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { + template + std::pair SparseExplorationModelChecker::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { StateType group = explorationInformation.getRowGroup(currentStateId); std::pair result = getLowestBounds(explorationInformation.getOptimizationDirection()); for (ActionType action = explorationInformation.getStartRowOfGroup(group); action < explorationInformation.getStartRowOfGroup(group + 1); ++action) { @@ -596,8 +598,8 @@ namespace storm { return result; } - template - void SparseExplorationModelChecker::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, Bounds& bounds) const { + template + void SparseExplorationModelChecker::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, Bounds& bounds) const { stack.pop_back(); while (!stack.empty()) { updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds); @@ -605,8 +607,8 @@ namespace storm { } } - template - void SparseExplorationModelChecker::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, Bounds& bounds) const { + template + void SparseExplorationModelChecker::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, Bounds& bounds) const { // Compute the new lower/upper values of the action. std::pair newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds); @@ -640,8 +642,8 @@ namespace storm { } } - template - ValueType SparseExplorationModelChecker::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { + template + typename ModelType::ValueType SparseExplorationModelChecker::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { ValueType bound = getLowestBound(explorationInformation.getOptimizationDirection()); ActionType group = explorationInformation.getRowGroup(state); @@ -659,14 +661,14 @@ namespace storm { return bound; } - template - std::pair SparseExplorationModelChecker::getLowestBounds(storm::OptimizationDirection const& direction) const { + template + std::pair SparseExplorationModelChecker::getLowestBounds(storm::OptimizationDirection const& direction) const { ValueType val = getLowestBound(direction); return std::make_pair(val, val); } - template - ValueType SparseExplorationModelChecker::getLowestBound(storm::OptimizationDirection const& direction) const { + template + typename ModelType::ValueType SparseExplorationModelChecker::getLowestBound(storm::OptimizationDirection const& direction) const { if (direction == storm::OptimizationDirection::Maximize) { return storm::utility::zero(); } else { @@ -674,8 +676,8 @@ namespace storm { } } - template - std::pair SparseExplorationModelChecker::combineBounds(storm::OptimizationDirection const& direction, std::pair const& bounds1, std::pair const& bounds2) const { + template + std::pair SparseExplorationModelChecker::combineBounds(storm::OptimizationDirection const& direction, std::pair const& bounds1, std::pair const& bounds2) const { if (direction == storm::OptimizationDirection::Maximize) { return std::make_pair(std::max(bounds1.first, bounds2.first), std::max(bounds1.second, bounds2.second)); } else { @@ -683,6 +685,7 @@ namespace storm { } } - template class SparseExplorationModelChecker; + template class SparseExplorationModelChecker, uint32_t>; + template class SparseExplorationModelChecker, uint32_t>; } } diff --git a/src/modelchecker/exploration/SparseExplorationModelChecker.h b/src/modelchecker/exploration/SparseExplorationModelChecker.h index d582fec38..220b358be 100644 --- a/src/modelchecker/exploration/SparseExplorationModelChecker.h +++ b/src/modelchecker/exploration/SparseExplorationModelChecker.h @@ -30,9 +30,10 @@ namespace storm { using namespace exploration_detail; - template - class SparseExplorationModelChecker : public AbstractModelChecker { + template + class SparseExplorationModelChecker : public AbstractModelChecker { public: + typedef typename ModelType::ValueType ValueType; typedef StateType ActionType; typedef std::vector> StateActionStack; diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 82982b9cd..8187efcc2 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -25,24 +25,24 @@ namespace storm { namespace modelchecker { - template - HybridDtmcPrctlModelChecker::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + template + HybridDtmcPrctlModelChecker::HybridDtmcPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } - template - HybridDtmcPrctlModelChecker::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { + template + HybridDtmcPrctlModelChecker::HybridDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { // Intentionally left empty. } - template - bool HybridDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + template + 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) { + template + 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()); @@ -51,24 +51,24 @@ namespace storm { return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template - std::unique_ptr HybridDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + template + 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(); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template - std::unique_ptr HybridDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + template + 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(); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } - template - std::unique_ptr HybridDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + template + 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()); @@ -78,35 +78,31 @@ namespace storm { return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template - std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + 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) { + template + 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) { + template + 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(); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - - template - storm::models::symbolic::Dtmc const& HybridDtmcPrctlModelChecker::getModel() const { - return this->template getModelAs>(); - } - - template - std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + + + template + 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(); @@ -120,7 +116,7 @@ namespace storm { return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().template getAddZero(), this->getModel().getReachableStates(), std::move(odd), std::move(result))); } - template class HybridDtmcPrctlModelChecker; - template class HybridDtmcPrctlModelChecker; + template class HybridDtmcPrctlModelChecker>; + template class HybridDtmcPrctlModelChecker>; } } \ No newline at end of file diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index 5ae9dd360..d6164e137 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -10,11 +10,14 @@ namespace storm { namespace modelchecker { - template - class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker { + template + class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker { public: - explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model); - explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory); + typedef typename ModelType::ValueType ValueType; + static const storm::dd::DdType DdType = ModelType::DdType; + + explicit HybridDtmcPrctlModelChecker(ModelType const& model); + explicit HybridDtmcPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -27,9 +30,6 @@ namespace storm { 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; - private: // An object that is used for retrieving linear equation solvers. std::unique_ptr> linearEquationSolverFactory; diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 06b3696f7..dee111fc7 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -19,24 +19,24 @@ namespace storm { namespace modelchecker { - template - HybridMdpPrctlModelChecker::HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + template + HybridMdpPrctlModelChecker::HybridMdpPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } - template - HybridMdpPrctlModelChecker::HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { + template + HybridMdpPrctlModelChecker::HybridMdpPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { // Intentionally left empty. } - template - bool HybridMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + template + 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) { + template + 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()); @@ -46,8 +46,8 @@ namespace storm { return storm::modelchecker::helper::HybridMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template - std::unique_ptr HybridMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + template + 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()); @@ -55,8 +55,8 @@ namespace storm { return storm::modelchecker::helper::HybridMdpPrctlHelper::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template - std::unique_ptr HybridMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + template + 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()); @@ -64,8 +64,8 @@ namespace storm { return storm::modelchecker::helper::HybridMdpPrctlHelper::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } - template - std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + template + 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."); @@ -76,37 +76,33 @@ namespace storm { return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template - std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + 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."); return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template - std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + 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."); return storm::modelchecker::helper::HybridMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template - std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + 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()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - - template - storm::models::symbolic::Mdp const& HybridMdpPrctlModelChecker::getModel() const { - return this->template getModelAs>(); - } - - template class HybridMdpPrctlModelChecker; - template class HybridMdpPrctlModelChecker; + + + template class HybridMdpPrctlModelChecker>; + template class HybridMdpPrctlModelChecker>; } } \ No newline at end of file diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h index 0da318b51..8ae267547 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -17,11 +17,14 @@ namespace storm { namespace modelchecker { - template - class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker { + template + class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker { public: - explicit HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model); - explicit HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model, std::unique_ptr>&& linearEquationSolverFactory); + typedef typename ModelType::ValueType ValueType; + static const storm::dd::DdType DdType = ModelType::DdType; + + explicit HybridMdpPrctlModelChecker(ModelType const& model); + explicit HybridMdpPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -32,10 +35,7 @@ namespace storm { 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; - + private: // An object that is used for retrieving linear equation solvers. std::unique_ptr> linearEquationSolverFactory; diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 1b36dd820..74ff03df7 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -34,13 +34,13 @@ namespace storm { } template - bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true)); } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcPrctlModelChecker::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()); @@ -53,7 +53,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -62,7 +62,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcPrctlModelChecker::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()); @@ -73,7 +73,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -82,7 +82,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseDtmcPrctlModelChecker::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."); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); @@ -90,7 +90,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseDtmcPrctlModelChecker::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."); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); @@ -98,7 +98,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseDtmcPrctlModelChecker::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(); @@ -107,7 +107,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -116,7 +116,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); @@ -131,7 +131,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); STORM_LOG_THROW(conditionalFormula.getSubformula().isReachabilityRewardFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 6c08ac856..eb88f6a7b 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -22,24 +22,24 @@ namespace storm { namespace modelchecker { - template - SymbolicDtmcPrctlModelChecker::SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + template + SymbolicDtmcPrctlModelChecker::SymbolicDtmcPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } - template - SymbolicDtmcPrctlModelChecker::SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicLinearEquationSolverFactory()) { + template + SymbolicDtmcPrctlModelChecker::SymbolicDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicLinearEquationSolverFactory()) { // Intentionally left empty. } - template - bool SymbolicDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + template + 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) { + template + 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()); @@ -49,8 +49,8 @@ namespace storm { return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } - template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + template + 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(); @@ -58,8 +58,8 @@ namespace storm { return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } - template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + template + 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(); @@ -67,8 +67,8 @@ namespace storm { return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } - template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + template + 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()); @@ -79,37 +79,33 @@ namespace storm { return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } - template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + 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); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } - template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + 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); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } - template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + 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(); storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } - - template - storm::models::symbolic::Dtmc const& SymbolicDtmcPrctlModelChecker::getModel() const { - return this->template getModelAs>(); - } - - template class SymbolicDtmcPrctlModelChecker; - template class SymbolicDtmcPrctlModelChecker; + + + template class SymbolicDtmcPrctlModelChecker>; + template class SymbolicDtmcPrctlModelChecker>; } } diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index 1f21466be..f550b4926 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -7,11 +7,14 @@ namespace storm { namespace modelchecker { - template - class SymbolicDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker { + template + class SymbolicDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker { public: - explicit SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model); - explicit SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory); + typedef typename ModelType::ValueType ValueType; + static const storm::dd::DdType DdType = ModelType::DdType; + + explicit SymbolicDtmcPrctlModelChecker(ModelType const& model); + explicit SymbolicDtmcPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -22,10 +25,7 @@ namespace storm { 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; - + private: // An object that is used for retrieving linear equation solvers. std::unique_ptr> linearEquationSolverFactory; diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 5b29b82b2..cee5c9d23 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -21,24 +21,24 @@ namespace storm { namespace modelchecker { - template - SymbolicMdpPrctlModelChecker::SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + template + SymbolicMdpPrctlModelChecker::SymbolicMdpPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } - template - SymbolicMdpPrctlModelChecker::SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory()) { + template + SymbolicMdpPrctlModelChecker::SymbolicMdpPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory()) { // Intentionally left empty. } - template - bool SymbolicMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + template + 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) { + template + 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()); @@ -48,8 +48,8 @@ namespace storm { return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + template + 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()); @@ -57,8 +57,8 @@ namespace storm { return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + template + 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()); @@ -66,8 +66,8 @@ namespace storm { return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } - template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + template + 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."); @@ -78,37 +78,32 @@ namespace storm { return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + 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."); return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + 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."); return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + template + 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()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - - template - storm::models::symbolic::Mdp const& SymbolicMdpPrctlModelChecker::getModel() const { - return this->template getModelAs>(); - } - - template class SymbolicMdpPrctlModelChecker; - template class SymbolicMdpPrctlModelChecker; + + template class SymbolicMdpPrctlModelChecker>; + template class SymbolicMdpPrctlModelChecker>; } } diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index 8cce0eaac..3f6324ed6 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -9,11 +9,14 @@ namespace storm { namespace modelchecker { - template - class SymbolicMdpPrctlModelChecker : public SymbolicPropositionalModelChecker { + template + class SymbolicMdpPrctlModelChecker : public SymbolicPropositionalModelChecker { public: - explicit SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model); - explicit SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model, std::unique_ptr>&& linearEquationSolverFactory); + typedef typename ModelType::ValueType ValueType; + static const storm::dd::DdType DdType = ModelType::DdType; + + explicit SymbolicMdpPrctlModelChecker(ModelType const& model); + explicit SymbolicMdpPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -25,9 +28,7 @@ namespace storm { 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; - + private: // An object that is used for retrieving linear equation solvers. std::unique_ptr> linearEquationSolverFactory; diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index e9fe53f2e..de96be8c8 100644 --- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -85,7 +85,7 @@ namespace storm { template std::unique_ptr HybridDtmcPrctlHelper::computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { std::unique_ptr result = computeUntilProbabilities(model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); - result->asQuantitativeCheckResult().oneMinus(); + result->asQuantitativeCheckResult().oneMinus(); return result; } diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 2f3111a7f..e8e8043d9 100644 --- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -89,7 +89,7 @@ namespace storm { template std::unique_ptr HybridMdpPrctlHelper::computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { std::unique_ptr result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Maximize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); - result->asQuantitativeCheckResult().oneMinus(); + result->asQuantitativeCheckResult().oneMinus(); return result; } diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index d3cec71e4..d09fa94b9 100644 --- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -78,7 +78,7 @@ namespace storm { template std::unique_ptr SymbolicMdpPrctlHelper::computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { std::unique_ptr result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); - result->asQuantitativeCheckResult().oneMinus(); + result->asQuantitativeCheckResult().oneMinus(); return result; } diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index d9de796d2..4ab6e8340 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -18,7 +18,7 @@ namespace storm { namespace modelchecker { template - SymbolicPropositionalModelChecker::SymbolicPropositionalModelChecker(storm::models::symbolic::Model const& model) : model(model) { + SymbolicPropositionalModelChecker::SymbolicPropositionalModelChecker(ModelType const& model) : model(model) { // Intentionally left empty. } @@ -52,7 +52,7 @@ namespace storm { } template - storm::models::symbolic::Model const& SymbolicPropositionalModelChecker::getModel() const { + ModelType const& SymbolicPropositionalModelChecker::getModel() const { return model; } diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h index c58af239d..6bfe61195 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h @@ -20,6 +20,7 @@ namespace storm { public: 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. diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index e1ec35ffa..080f0e233 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -30,13 +30,13 @@ namespace storm { explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc 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 computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, 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 computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; // Static helper methods static std::unique_ptr computeUntilProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly); diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp index 7d8fcd1ac..3fb587a1e 100644 --- a/src/modelchecker/results/CheckResult.cpp +++ b/src/modelchecker/results/CheckResult.cpp @@ -88,15 +88,8 @@ namespace storm { QualitativeCheckResult const& CheckResult::asQualitativeCheckResult() const { return dynamic_cast(*this); } - - QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult() { - return dynamic_cast(*this); - } - - QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const { - return dynamic_cast(*this); - } - + + template SymbolicQualitativeCheckResult& CheckResult::asSymbolicQualitativeCheckResult() { return dynamic_cast&>(*this); diff --git a/src/modelchecker/results/CheckResult.h b/src/modelchecker/results/CheckResult.h index b17a4dfc6..9cbea96f7 100644 --- a/src/modelchecker/results/CheckResult.h +++ b/src/modelchecker/results/CheckResult.h @@ -57,9 +57,14 @@ namespace storm { QualitativeCheckResult const& asQualitativeCheckResult() const; template - QuantitativeCheckResult& asQuantitativeCheckResult(); + QuantitativeCheckResult& asQuantitativeCheckResult() { + return static_cast &>(*this); + } template - QuantitativeCheckResult const& asQuantitativeCheckResult() const; + QuantitativeCheckResult const& asQuantitativeCheckResult() const { + return static_cast const&>(*this); + } + ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const; diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index dfe624f2a..6233216d9 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -128,35 +128,35 @@ namespace storm { } template - std::unique_ptr ExplicitQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + std::unique_ptr ExplicitQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { if (this->isResultForAllStates()) { vector_type const& valuesAsVector = boost::get(values); storm::storage::BitVector result(valuesAsVector.size()); switch (comparisonType) { case logic::ComparisonType::Less: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { - if (valuesAsVector[index] < storm::utility::convertNumber(bound)) { + if (valuesAsVector[index] < bound) { result.set(index); } } break; case logic::ComparisonType::LessEqual: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { - if (valuesAsVector[index] <= storm::utility::convertNumber(bound)) { + if (valuesAsVector[index] <= bound) { result.set(index); } } break; case logic::ComparisonType::Greater: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { - if (valuesAsVector[index] > storm::utility::convertNumber(bound)) { + if (valuesAsVector[index] > bound) { result.set(index); } } break; case logic::ComparisonType::GreaterEqual: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { - if (valuesAsVector[index] >= storm::utility::convertNumber(bound)) { + if (valuesAsVector[index] >= bound) { result.set(index); } } @@ -169,22 +169,22 @@ namespace storm { switch (comparisonType) { case logic::ComparisonType::Less: for (auto const& element : valuesAsMap) { - result[element.first] = element.second < storm::utility::convertNumber(bound); + result[element.first] = element.second < bound; } break; case logic::ComparisonType::LessEqual: for (auto const& element : valuesAsMap) { - result[element.first] = element.second <= storm::utility::convertNumber(bound); + result[element.first] = element.second <= bound; } break; case logic::ComparisonType::Greater: for (auto const& element : valuesAsMap) { - result[element.first] = element.second > storm::utility::convertNumber(bound); + result[element.first] = element.second > bound; } break; case logic::ComparisonType::GreaterEqual: for (auto const& element : valuesAsMap) { - result[element.first] = element.second >= storm::utility::convertNumber(bound); + result[element.first] = element.second >= bound; } break; } @@ -194,7 +194,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - std::unique_ptr ExplicitQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + std::unique_ptr ExplicitQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, storm::RationalFunction const& bound) const { // Since it is not possible to compare rational functions against bounds, we simply call the base class method. return QuantitativeCheckResult::compareAgainstBound(comparisonType, bound); } diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h index 78f9766ca..639da4fa7 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -37,7 +37,7 @@ namespace storm { ValueType& operator[](storm::storage::sparse::state_type state); ValueType const& operator[](storm::storage::sparse::state_type state) const; - virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override; + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override; virtual bool isExplicit() const override; virtual bool isResultForAllStates() const override; diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp index 0f0ad01e2..a32095e40 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -17,7 +17,7 @@ namespace storm { } template - std::unique_ptr HybridQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + std::unique_ptr HybridQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { storm::dd::Bdd symbolicResult; // First compute the symbolic part of the result. diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h index 7faacdb27..8b7db1cea 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.h +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h @@ -23,7 +23,7 @@ namespace storm { HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult&& other) = default; #endif - virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType bound) const override; + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override; std::unique_ptr toExplicitQuantitativeCheckResult() const; diff --git a/src/modelchecker/results/QuantitativeCheckResult.cpp b/src/modelchecker/results/QuantitativeCheckResult.cpp index 533fc43d1..5828e9def 100644 --- a/src/modelchecker/results/QuantitativeCheckResult.cpp +++ b/src/modelchecker/results/QuantitativeCheckResult.cpp @@ -10,12 +10,12 @@ namespace storm { namespace modelchecker { template - std::unique_ptr QuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + std::unique_ptr QuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result."); } template - bool QuantitativeCheckResult::isQuantitative() const { + bool QuantitativeCheckResult::isQuantitative() const { return true; } @@ -23,6 +23,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template class QuantitativeCheckResult; + template class QuantitativeCheckResult; #endif } } diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index 0acd3ada3..57f68bdf1 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -16,7 +16,7 @@ namespace storm { } template - std::unique_ptr SymbolicQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + std::unique_ptr SymbolicQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { storm::dd::Bdd states; if (comparisonType == storm::logic::ComparisonType::Less) { states = values.less(bound); diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h index 74ed7fe99..fd03da786 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -21,8 +21,9 @@ namespace storm { SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult&& other) = default; #endif - virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType bound) const override; - + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override; + + virtual bool isSymbolic() const override; virtual bool isResultForAllStates() const override; diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index eafe4f1bd..aa89e521f 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -156,6 +156,11 @@ namespace storm { return carl::rationalize(number); } + template<> + RationalNumber convertNumber(RationalNumber const& number){ + return number; + } + template<> RationalFunction convertNumber(double const& number){ return RationalFunction(carl::rationalize(number)); @@ -268,6 +273,7 @@ namespace storm { template double convertNumber(storm::RationalNumber const& number); template storm::RationalNumber convertNumber(double const& number); + template storm::RationalNumber convertNumber(storm::RationalNumber const& number); template storm::RationalNumber abs(storm::RationalNumber const& number); diff --git a/src/utility/storm.h b/src/utility/storm.h index d6b074832..a3cfc608a 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -264,7 +264,7 @@ namespace storm { } template - std::unique_ptr verifySparseDtmc(std::shared_ptr> dtmc, storm::modelchecker::CheckTask const& task) { + std::unique_ptr verifySparseDtmc(std::shared_ptr> dtmc, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule().isUseDedicatedModelCheckerSet()) { storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); @@ -285,7 +285,7 @@ namespace storm { } template - std::unique_ptr verifySparseCtmc(std::shared_ptr> ctmc, storm::modelchecker::CheckTask const& task) { + std::unique_ptr verifySparseCtmc(std::shared_ptr> ctmc, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); if (modelchecker.canHandle(task)) { @@ -297,7 +297,7 @@ namespace storm { } template - std::unique_ptr verifySparseMdp(std::shared_ptr> mdp, storm::modelchecker::CheckTask const& task) { + std::unique_ptr verifySparseMdp(std::shared_ptr> mdp, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); if (modelchecker.canHandle(task)) { @@ -310,7 +310,7 @@ namespace storm { template std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { @@ -337,7 +337,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { @@ -370,7 +370,7 @@ namespace storm { template<> inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { @@ -394,19 +394,19 @@ namespace storm { storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker modelchecker(*dtmc); + storm::modelchecker::HybridDtmcPrctlModelChecker> modelchecker(*dtmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Ctmc) { std::shared_ptr> ctmc = model->template as>(); - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc); + storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Mdp) { std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::HybridMdpPrctlModelChecker modelchecker(*mdp); + storm::modelchecker::HybridMdpPrctlModelChecker> modelchecker(*mdp); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } @@ -423,13 +423,13 @@ namespace storm { storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker modelchecker(*dtmc); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> modelchecker(*dtmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Mdp) { std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker modelchecker(*mdp); + storm::modelchecker::SymbolicMdpPrctlModelChecker> modelchecker(*mdp); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); }