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<typename OtherValueType> - Bound<OtherValueType> convertToOtherValueType() const { - return Bound<OtherValueType>(comparisonType, storm::utility::convertNumber<OtherValueType>(threshold)); - } + //template<typename OtherValueType> + //Bound<OtherValueType> convertToOtherValueType() const { + // return Bound<OtherValueType>(comparisonType, storm::utility::convertNumber<OtherValueType>(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<storm::solver::OptimizationDirection> const& optimizationDirection = boost::none, boost::optional<Bound<RationalNumber>> 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<storm::models::sparse::Model<double>>; template class AbstractModelChecker<storm::models::sparse::Dtmc<double>>; template class AbstractModelChecker<storm::models::sparse::Ctmc<double>>; @@ -297,5 +305,12 @@ namespace storm { template class AbstractModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>>; template class AbstractModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>; #endif + // DD + template class AbstractModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>; + template class AbstractModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>; + template class AbstractModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>; + template class AbstractModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>; + template class AbstractModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double>>; + template class AbstractModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double>>; } } 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 <typename SparseCtmcModelType> - template<typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type> - bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { + template<typename CValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type> + bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> 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 <typename SparseCtmcModelType> - template<typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type> - bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { + template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type> + bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> 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<CheckResult> computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override; private: - template<typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0> - bool canHandleImplementation(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const; + template<typename CValueType = ValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0> + bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const; - template<typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0> - bool canHandleImplementation(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const; + template<typename CValueType = ValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0> + bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const; // An object that is used for solving linear equations and performing matrix-vector multiplication. std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>> 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<typename ValueType, typename StateType> - SparseExplorationModelChecker<ValueType, StateType>::SparseExplorationModelChecker(storm::prism::Program const& program) : program(program.substituteConstants()), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision()) { + template<typename ModelType, typename StateType> + SparseExplorationModelChecker<ModelType, StateType>::SparseExplorationModelChecker(storm::prism::Program const& program) : program(program.substituteConstants()), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision()) { // Intentionally left empty. } - template<typename ValueType, typename StateType> - bool SparseExplorationModelChecker<ValueType, StateType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { + template<typename ModelType, typename StateType> + bool SparseExplorationModelChecker<ModelType, StateType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::FragmentSpecification fragment = storm::logic::reachability(); return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet(); } - template<typename ValueType, typename StateType> - std::unique_ptr<CheckResult> SparseExplorationModelChecker<ValueType, StateType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { + template<typename ModelType, typename StateType> + std::unique_ptr<CheckResult> SparseExplorationModelChecker<ModelType, StateType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> 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<ExplicitQuantitativeCheckResult<ValueType>>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState)); } - template<typename ValueType, typename StateType> - std::tuple<StateType, ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const { + template<typename ModelType, typename StateType> + std::tuple<StateType, typename ModelType::ValueType, typename ModelType::ValueType> SparseExplorationModelChecker<ModelType, StateType>::performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, typename ModelType::ValueType>& 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<typename ValueType, typename StateType> - bool SparseExplorationModelChecker<ValueType, StateType>::samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const { + template<typename ModelType, typename StateType> + bool SparseExplorationModelChecker<ModelType, StateType>::samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& 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<typename ValueType, typename StateType> - bool SparseExplorationModelChecker<ValueType, StateType>::exploreState(StateGeneration<StateType, ValueType>& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const { + template<typename ModelType, typename StateType> + bool SparseExplorationModelChecker<ModelType, StateType>::exploreState(StateGeneration<StateType, ValueType>& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const { bool isTerminalState = false; bool isTargetState = false; @@ -284,8 +286,8 @@ namespace storm { return isTerminalState; } - template<typename ValueType, typename StateType> - typename SparseExplorationModelChecker<ValueType, StateType>::ActionType SparseExplorationModelChecker<ValueType, StateType>::sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { + template<typename ModelType, typename StateType> + typename SparseExplorationModelChecker<ModelType, StateType>::ActionType SparseExplorationModelChecker<ModelType, StateType>::sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { // Determine the values of all available actions. std::vector<std::pair<ActionType, ValueType>> actionValues; StateType rowGroup = explorationInformation.getRowGroup(currentStateId); @@ -322,8 +324,8 @@ namespace storm { return actionValues[distribution(randomGenerator)].first; } - template<typename ValueType, typename StateType> - StateType SparseExplorationModelChecker<ValueType, StateType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { + template<typename ModelType, typename StateType> + StateType SparseExplorationModelChecker<ModelType, StateType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& row = explorationInformation.getRowOfMatrix(chosenAction); if (row.size() == 1) { return row.front().getColumn(); @@ -354,8 +356,8 @@ namespace storm { } } - template<typename ValueType, typename StateType> - bool SparseExplorationModelChecker<ValueType, StateType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const { + template<typename ModelType, typename StateType> + bool SparseExplorationModelChecker<ModelType, StateType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const { ++stats.numberOfPrecomputations; // Outline: @@ -487,8 +489,8 @@ namespace storm { return true; } - template<typename ValueType, typename StateType> - void SparseExplorationModelChecker<ValueType, StateType>::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds) const { + template<typename ModelType, typename StateType> + void SparseExplorationModelChecker<ModelType, StateType>::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds) const { bool containsTargetState = false; // Now we record all actions leaving the EC. @@ -556,8 +558,8 @@ namespace storm { } } - template<typename ValueType, typename StateType> - ValueType SparseExplorationModelChecker<ValueType, StateType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { + template<typename ModelType, typename StateType> + typename ModelType::ValueType SparseExplorationModelChecker<ModelType, StateType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { ValueType result = storm::utility::zero<ValueType>(); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation); @@ -565,8 +567,8 @@ namespace storm { return result; } - template<typename ValueType, typename StateType> - ValueType SparseExplorationModelChecker<ValueType, StateType>::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { + template<typename ModelType, typename StateType> + typename ModelType::ValueType SparseExplorationModelChecker<ModelType, StateType>::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { ValueType result = storm::utility::zero<ValueType>(); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation); @@ -574,8 +576,8 @@ namespace storm { return result; } - template<typename ValueType, typename StateType> - std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { + template<typename ModelType, typename StateType> + std::pair<typename ModelType::ValueType, typename ModelType::ValueType> SparseExplorationModelChecker<ModelType, StateType>::computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { // TODO: take into account self-loops? std::pair<ValueType, ValueType> result = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>()); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { @@ -585,8 +587,8 @@ namespace storm { return result; } - template<typename ValueType, typename StateType> - std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { + template<typename ModelType, typename StateType> + std::pair<typename ModelType::ValueType, typename ModelType::ValueType> SparseExplorationModelChecker<ModelType, StateType>::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { StateType group = explorationInformation.getRowGroup(currentStateId); std::pair<ValueType, ValueType> 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<typename ValueType, typename StateType> - void SparseExplorationModelChecker<ValueType, StateType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { + template<typename ModelType, typename StateType> + void SparseExplorationModelChecker<ModelType, StateType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { stack.pop_back(); while (!stack.empty()) { updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds); @@ -605,8 +607,8 @@ namespace storm { } } - template<typename ValueType, typename StateType> - void SparseExplorationModelChecker<ValueType, StateType>::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { + template<typename ModelType, typename StateType> + void SparseExplorationModelChecker<ModelType, StateType>::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { // Compute the new lower/upper values of the action. std::pair<ValueType, ValueType> newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds); @@ -640,8 +642,8 @@ namespace storm { } } - template<typename ValueType, typename StateType> - ValueType SparseExplorationModelChecker<ValueType, StateType>::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { + template<typename ModelType, typename StateType> + typename ModelType::ValueType SparseExplorationModelChecker<ModelType, StateType>::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { ValueType bound = getLowestBound(explorationInformation.getOptimizationDirection()); ActionType group = explorationInformation.getRowGroup(state); @@ -659,14 +661,14 @@ namespace storm { return bound; } - template<typename ValueType, typename StateType> - std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::getLowestBounds(storm::OptimizationDirection const& direction) const { + template<typename ModelType, typename StateType> + std::pair<typename ModelType::ValueType, typename ModelType::ValueType> SparseExplorationModelChecker<ModelType, StateType>::getLowestBounds(storm::OptimizationDirection const& direction) const { ValueType val = getLowestBound(direction); return std::make_pair(val, val); } - template<typename ValueType, typename StateType> - ValueType SparseExplorationModelChecker<ValueType, StateType>::getLowestBound(storm::OptimizationDirection const& direction) const { + template<typename ModelType, typename StateType> + typename ModelType::ValueType SparseExplorationModelChecker<ModelType, StateType>::getLowestBound(storm::OptimizationDirection const& direction) const { if (direction == storm::OptimizationDirection::Maximize) { return storm::utility::zero<ValueType>(); } else { @@ -674,8 +676,8 @@ namespace storm { } } - template<typename ValueType, typename StateType> - std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::combineBounds(storm::OptimizationDirection const& direction, std::pair<ValueType, ValueType> const& bounds1, std::pair<ValueType, ValueType> const& bounds2) const { + template<typename ModelType, typename StateType> + std::pair<typename ModelType::ValueType, typename ModelType::ValueType> SparseExplorationModelChecker<ModelType, StateType>::combineBounds(storm::OptimizationDirection const& direction, std::pair<ValueType, ValueType> const& bounds1, std::pair<ValueType, ValueType> 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<double, uint32_t>; + template class SparseExplorationModelChecker<storm::models::sparse::Dtmc<double>, uint32_t>; + template class SparseExplorationModelChecker<storm::models::sparse::Mdp<double>, 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<typename ValueType, typename StateType = uint32_t> - class SparseExplorationModelChecker : public AbstractModelChecker<ValueType> { + template<typename ModelType, typename StateType = uint32_t> + class SparseExplorationModelChecker : public AbstractModelChecker<ModelType> { public: + typedef typename ModelType::ValueType ValueType; typedef StateType ActionType; typedef std::vector<std::pair<StateType, ActionType>> 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<storm::dd::DdType DdType, typename ValueType> - HybridDtmcPrctlModelChecker<DdType, ValueType>::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + template<typename ModelType> + HybridDtmcPrctlModelChecker<ModelType>::HybridDtmcPrctlModelChecker(ModelType const& model, std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } - template<storm::dd::DdType DdType, typename ValueType> - HybridDtmcPrctlModelChecker<DdType, ValueType>::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(std::make_unique<storm::solver::GeneralLinearEquationSolverFactory<ValueType>>()) { + template<typename ModelType> + HybridDtmcPrctlModelChecker<ModelType>::HybridDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(std::make_unique<storm::solver::GeneralLinearEquationSolverFactory<ValueType>>()) { // Intentionally left empty. } - template<storm::dd::DdType DdType, typename ValueType> - bool HybridDtmcPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { + template<typename ModelType> + bool HybridDtmcPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true)); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -51,24 +51,24 @@ namespace storm { return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> 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<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -78,35 +78,31 @@ namespace storm { return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> 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<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> 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<DdType, ValueType>::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - - template<storm::dd::DdType DdType, typename ValueType> - storm::models::symbolic::Dtmc<DdType, ValueType> const& HybridDtmcPrctlModelChecker<DdType, ValueType>::getModel() const { - return this->template getModelAs<storm::models::symbolic::Dtmc<DdType, ValueType>>(); - } - - template<storm::dd::DdType DdType, class ValueType> - std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) { + + + template<typename ModelType> + std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); @@ -120,7 +116,7 @@ namespace storm { return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().template getAddZero<ValueType>(), this->getModel().getReachableStates(), std::move(odd), std::move(result))); } - template class HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double>; - template class HybridDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double>; + template class HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>; + template class HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>; } } \ 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<storm::dd::DdType DdType, typename ValueType> - class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType, ValueType> { + template<typename ModelType> + class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker<ModelType> { public: - explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model); - explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>>&& 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<storm::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override; @@ -27,9 +30,6 @@ namespace storm { virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override; virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override; - protected: - storm::models::symbolic::Dtmc<DdType, ValueType> const& getModel() const override; - private: // An object that is used for retrieving linear equation solvers. std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>> 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<storm::dd::DdType DdType, typename ValueType> - HybridMdpPrctlModelChecker<DdType, ValueType>::HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + template<typename ModelType> + HybridMdpPrctlModelChecker<ModelType>::HybridMdpPrctlModelChecker(ModelType const& model, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } - template<storm::dd::DdType DdType, typename ValueType> - HybridMdpPrctlModelChecker<DdType, ValueType>::HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(std::make_unique<storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType>>()) { + template<typename ModelType> + HybridMdpPrctlModelChecker<ModelType>::HybridMdpPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(std::make_unique<storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType>>()) { // Intentionally left empty. } - template<storm::dd::DdType DdType, typename ValueType> - bool HybridMdpPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { + template<typename ModelType> + bool HybridMdpPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> 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<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -46,8 +46,8 @@ namespace storm { return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> 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<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); @@ -55,8 +55,8 @@ namespace storm { return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> 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<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); @@ -64,8 +64,8 @@ namespace storm { return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> 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<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> 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<DdType, ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> 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<DdType, ValueType>::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> 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<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::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::dd::DdType DdType, typename ValueType> - storm::models::symbolic::Mdp<DdType, ValueType> const& HybridMdpPrctlModelChecker<DdType, ValueType>::getModel() const { - return this->template getModelAs<storm::models::symbolic::Mdp<DdType, ValueType>>(); - } - - template class HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double>; - template class HybridMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double>; + + + template class HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>; + template class HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>; } } \ 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<storm::dd::DdType DdType, typename ValueType> - class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType, ValueType> { + template<typename ModelType> + class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<ModelType> { public: - explicit HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model); - explicit HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& 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<storm::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override; @@ -32,10 +35,7 @@ namespace storm { virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) override; virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) override; virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override; - - protected: - storm::models::symbolic::Mdp<DdType, ValueType> const& getModel() const override; - + private: // An object that is used for retrieving linear equation solvers. std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ValueType>> 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<typename SparseDtmcModelType> - bool SparseDtmcPrctlModelChecker<SparseDtmcModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const { + bool SparseDtmcPrctlModelChecker<SparseDtmcModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> 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<typename SparseDtmcModelType> - std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) { + std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> 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<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -53,7 +53,7 @@ namespace storm { } template<typename SparseDtmcModelType> - std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) { + std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -62,7 +62,7 @@ namespace storm { } template<typename SparseDtmcModelType> - std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) { + std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -73,7 +73,7 @@ namespace storm { } template<typename SparseDtmcModelType> - std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) { + std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -82,7 +82,7 @@ namespace storm { } template<typename SparseDtmcModelType> - std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) { + std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> 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<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); @@ -90,7 +90,7 @@ namespace storm { } template<typename SparseDtmcModelType> - std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) { + std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> 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<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); @@ -98,7 +98,7 @@ namespace storm { } template<typename SparseDtmcModelType> - std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) { + std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -107,7 +107,7 @@ namespace storm { } template<typename SparseDtmcModelType> - std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) { + std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -116,7 +116,7 @@ namespace storm { } template<typename SparseDtmcModelType> - std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) { + std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula, ValueType> 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<typename SparseDtmcModelType> - std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula> const& checkTask) { + std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula, ValueType> 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<storm::dd::DdType DdType, typename ValueType> - SymbolicDtmcPrctlModelChecker<DdType, ValueType>::SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + template<typename ModelType> + SymbolicDtmcPrctlModelChecker<ModelType>::SymbolicDtmcPrctlModelChecker(ModelType const& model, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } - template<storm::dd::DdType DdType, typename ValueType> - SymbolicDtmcPrctlModelChecker<DdType, ValueType>::SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>()) { + template<typename ModelType> + SymbolicDtmcPrctlModelChecker<ModelType>::SymbolicDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>()) { // Intentionally left empty. } - template<storm::dd::DdType DdType, typename ValueType> - bool SymbolicDtmcPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { + template<typename ModelType> + bool SymbolicDtmcPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -49,8 +49,8 @@ namespace storm { return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult)); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); @@ -58,8 +58,8 @@ namespace storm { return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult)); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); @@ -67,8 +67,8 @@ namespace storm { return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult)); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> 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<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -79,37 +79,33 @@ namespace storm { return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult)); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> 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<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult)); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> 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<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult)); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::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<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult)); } - - template<storm::dd::DdType DdType, typename ValueType> - storm::models::symbolic::Dtmc<DdType, ValueType> const& SymbolicDtmcPrctlModelChecker<DdType, ValueType>::getModel() const { - return this->template getModelAs<storm::models::symbolic::Dtmc<DdType, ValueType>>(); - } - - template class SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double>; - template class SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double>; + + + template class SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>; + template class SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>; } } 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<storm::dd::DdType DdType, typename ValueType> - class SymbolicDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType, ValueType> { + template<typename ModelType> + class SymbolicDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker<ModelType> { public: - explicit SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model); - explicit SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& 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<storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override; @@ -22,10 +25,7 @@ namespace storm { virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) override; virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) override; virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override; - - protected: - storm::models::symbolic::Dtmc<DdType, ValueType> const& getModel() const override; - + private: // An object that is used for retrieving linear equation solvers. std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>> 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<storm::dd::DdType DdType, typename ValueType> - SymbolicMdpPrctlModelChecker<DdType, ValueType>::SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + template<typename ModelType> + SymbolicMdpPrctlModelChecker<ModelType>::SymbolicMdpPrctlModelChecker(ModelType const& model, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } - template<storm::dd::DdType DdType, typename ValueType> - SymbolicMdpPrctlModelChecker<DdType, ValueType>::SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>()) { + template<typename ModelType> + SymbolicMdpPrctlModelChecker<ModelType>::SymbolicMdpPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>()) { // Intentionally left empty. } - template<storm::dd::DdType DdType, typename ValueType> - bool SymbolicMdpPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { + template<typename ModelType> + bool SymbolicMdpPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> 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<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -48,8 +48,8 @@ namespace storm { return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> 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<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); @@ -57,8 +57,8 @@ namespace storm { return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> 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<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); @@ -66,8 +66,8 @@ namespace storm { return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> 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<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> 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<DdType, ValueType>::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> 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<DdType, ValueType>::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } - template<storm::dd::DdType DdType, typename ValueType> - std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { + template<typename ModelType> + std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> 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<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::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::dd::DdType DdType, typename ValueType> - storm::models::symbolic::Mdp<DdType, ValueType> const& SymbolicMdpPrctlModelChecker<DdType, ValueType>::getModel() const { - return this->template getModelAs<storm::models::symbolic::Mdp<DdType>>(); - } - - template class SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double>; - template class SymbolicMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double>; + + template class SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>; + template class SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>; } } 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<storm::dd::DdType DdType, typename ValueType> - class SymbolicMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType, ValueType> { + template<typename ModelType> + class SymbolicMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<ModelType> { public: - explicit SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model); - explicit SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>>&& 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<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override; @@ -25,9 +28,7 @@ namespace storm { virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) override; virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override; - protected: - storm::models::symbolic::Mdp<DdType, ValueType> const& getModel() const override; - + private: // An object that is used for retrieving linear equation solvers. std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>> 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<storm::dd::DdType DdType, typename ValueType> std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { std::unique_ptr<CheckResult> result = computeUntilProbabilities(model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); - result->asQuantitativeCheckResult().oneMinus(); + result->asQuantitativeCheckResult<ValueType>().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<storm::dd::DdType DdType, typename ValueType> std::unique_ptr<CheckResult> HybridMdpPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { std::unique_ptr<CheckResult> result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Maximize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); - result->asQuantitativeCheckResult().oneMinus(); + result->asQuantitativeCheckResult<ValueType>().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<storm::dd::DdType DdType, typename ValueType> std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) { std::unique_ptr<CheckResult> result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); - result->asQuantitativeCheckResult().oneMinus(); + result->asQuantitativeCheckResult<ValueType>().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<typename ModelType> - SymbolicPropositionalModelChecker<ModelType>::SymbolicPropositionalModelChecker(storm::models::symbolic::Model<DdType, ValueType> const& model) : model(model) { + SymbolicPropositionalModelChecker<ModelType>::SymbolicPropositionalModelChecker(ModelType const& model) : model(model) { // Intentionally left empty. } @@ -52,7 +52,7 @@ namespace storm { } template<typename ModelType> - storm::models::symbolic::Model<Type, ValueType> const& SymbolicPropositionalModelChecker<ModelType>::getModel() const { + ModelType const& SymbolicPropositionalModelChecker<ModelType>::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<ValueType> const& model); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override; - virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) override; - virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override; - virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override; - virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) override; - virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override; - virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override; + virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override; + virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override; + virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) override; + virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override; + virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override; + virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) override; + virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override; // Static helper methods static std::unique_ptr<CheckResult> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> 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<QualitativeCheckResult const&>(*this); } - - QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult() { - return dynamic_cast<QuantitativeCheckResult&>(*this); - } - - QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const { - return dynamic_cast<QuantitativeCheckResult const&>(*this); - } - + + template <storm::dd::DdType Type> SymbolicQualitativeCheckResult<Type>& CheckResult::asSymbolicQualitativeCheckResult() { return dynamic_cast<SymbolicQualitativeCheckResult<Type>&>(*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<typename ValueType> - QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult(); + QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult() { + return static_cast<QuantitativeCheckResult<ValueType> &>(*this); + } template<typename ValueType> - QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const; + QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const { + return static_cast<QuantitativeCheckResult<ValueType> 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<typename ValueType> - std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { if (this->isResultForAllStates()) { vector_type const& valuesAsVector = boost::get<vector_type>(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<ValueType, double>(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<ValueType, double>(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<ValueType, double>(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<ValueType, double>(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<ValueType, double>(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<ValueType, double>(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<ValueType, double>(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<ValueType, double>(bound); + result[element.first] = element.second >= bound; } break; } @@ -194,7 +194,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<storm::RationalFunction>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<storm::RationalFunction>::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<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override; + virtual std::unique_ptr<CheckResult> 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<storm::dd::DdType Type, typename ValueType> - std::unique_ptr<CheckResult> HybridQuantitativeCheckResult<Type, ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + std::unique_ptr<CheckResult> HybridQuantitativeCheckResult<Type, ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { storm::dd::Bdd<Type> 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<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType bound) const override; + virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override; std::unique_ptr<CheckResult> 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<typename ValueType> - std::unique_ptr<CheckResult> QuantitativeCheckResult<ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + std::unique_ptr<CheckResult> QuantitativeCheckResult<ValueType>::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<typename ValueType> - bool QuantitativeCheckResult::isQuantitative() const { + bool QuantitativeCheckResult<ValueType>::isQuantitative() const { return true; } @@ -23,6 +23,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template class QuantitativeCheckResult<RationalNumber>; + template class QuantitativeCheckResult<RationalFunction>; #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<storm::dd::DdType Type, typename ValueType> - std::unique_ptr<CheckResult> SymbolicQuantitativeCheckResult<Type, ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + std::unique_ptr<CheckResult> SymbolicQuantitativeCheckResult<Type, ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { storm::dd::Bdd<Type> 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<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType bound) const override; - + virtual std::unique_ptr<CheckResult> 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<RationalNumber>(number); } + template<> + RationalNumber convertNumber(RationalNumber const& number){ + return number; + } + template<> RationalFunction convertNumber(double const& number){ return RationalFunction(carl::rationalize<RationalNumber>(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<typename ValueType> - std::unique_ptr<storm::modelchecker::CheckResult> verifySparseDtmc(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc, storm::modelchecker::CheckTask<storm::logic::Formula> const& task) { + std::unique_ptr<storm::modelchecker::CheckResult> verifySparseDtmc(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) { std::unique_ptr<storm::modelchecker::CheckResult> result; if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) { storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc); @@ -285,7 +285,7 @@ namespace storm { } template<typename ValueType> - std::unique_ptr<storm::modelchecker::CheckResult> verifySparseCtmc(std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc, storm::modelchecker::CheckTask<storm::logic::Formula> const& task) { + std::unique_ptr<storm::modelchecker::CheckResult> verifySparseCtmc(std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) { std::unique_ptr<storm::modelchecker::CheckResult> result; storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc); if (modelchecker.canHandle(task)) { @@ -297,7 +297,7 @@ namespace storm { } template<typename ValueType> - std::unique_ptr<storm::modelchecker::CheckResult> verifySparseMdp(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp, storm::modelchecker::CheckTask<storm::logic::Formula> const& task) { + std::unique_ptr<storm::modelchecker::CheckResult> verifySparseMdp(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) { std::unique_ptr<storm::modelchecker::CheckResult> result; storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp); if (modelchecker.canHandle(task)) { @@ -310,7 +310,7 @@ namespace storm { template<typename ValueType> std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant = false) { - storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task(*formula, onlyInitialStatesRelevant); std::unique_ptr<storm::modelchecker::CheckResult> result; if (model->getType() == storm::models::ModelType::Dtmc) { @@ -337,7 +337,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant) { - storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask<storm::logic::Formula, RationalNumber> task(*formula, onlyInitialStatesRelevant); std::unique_ptr<storm::modelchecker::CheckResult> result; if (model->getType() == storm::models::ModelType::Dtmc) { @@ -370,7 +370,7 @@ namespace storm { template<> inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant) { - storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalNumber> task(*formula, onlyInitialStatesRelevant); std::unique_ptr<storm::modelchecker::CheckResult> result; if (model->getType() == storm::models::ModelType::Dtmc) { @@ -394,19 +394,19 @@ namespace storm { storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>(); - storm::modelchecker::HybridDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc); + storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType>> modelchecker(*dtmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Ctmc) { std::shared_ptr<storm::models::symbolic::Ctmc<DdType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType>>(); - storm::modelchecker::HybridCtmcCslModelChecker<DdType, double> modelchecker(*ctmc); + storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<DdType>> modelchecker(*ctmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Mdp) { std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>(); - storm::modelchecker::HybridMdpPrctlModelChecker<DdType, double> modelchecker(*mdp); + storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType>> modelchecker(*mdp); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } @@ -423,13 +423,13 @@ namespace storm { storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc); + storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType>> modelchecker(*dtmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Mdp) { std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker<DdType, double> modelchecker(*mdp); + storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType>> modelchecker(*mdp); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); }