sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

refactored model checkers st all are templated in the model, have to handle rational function bounds next 

Former-commit-id: b665709a52
main
sjunges 9 years ago
parent
fc365c8ec2
commit
f7a3e02fb6
33 changed files with 274 additions and 263 deletions
Unified View
  1. 8
      src/logic/Bound.h
  2. 3
      src/logic/OperatorFormula.h
  3. 15
      src/modelchecker/AbstractModelChecker.cpp
  4. 8
      src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  5. 8
      src/modelchecker/csl/SparseCtmcCslModelChecker.h
  6. 85
      src/modelchecker/exploration/SparseExplorationModelChecker.cpp
  7. 5
      src/modelchecker/exploration/SparseExplorationModelChecker.h
  8. 56
      src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
  9. 14
      src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
  10. 52
      src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
  11. 16
      src/modelchecker/prctl/HybridMdpPrctlModelChecker.h
  12. 22
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  13. 52
      src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
  14. 16
      src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h
  15. 51
      src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
  16. 15
      src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h
  17. 2
      src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
  18. 2
      src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
  19. 2
      src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
  20. 4
      src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
  21. 1
      src/modelchecker/propositional/SymbolicPropositionalModelChecker.h
  22. 14
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
  23. 11
      src/modelchecker/results/CheckResult.cpp
  24. 9
      src/modelchecker/results/CheckResult.h
  25. 20
      src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
  26. 2
      src/modelchecker/results/ExplicitQuantitativeCheckResult.h
  27. 2
      src/modelchecker/results/HybridQuantitativeCheckResult.cpp
  28. 2
      src/modelchecker/results/HybridQuantitativeCheckResult.h
  29. 5
      src/modelchecker/results/QuantitativeCheckResult.cpp
  30. 2
      src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
  31. 5
      src/modelchecker/results/SymbolicQuantitativeCheckResult.h
  32. 6
      src/utility/constants.cpp
  33. 22
      src/utility/storm.h

8
src/logic/Bound.h
View File

@ -12,10 +12,10 @@ namespace storm {
// Intentionally left empty. // Intentionally left empty.
} }
template<typename OtherValueType> //template<typename OtherValueType>
Bound<OtherValueType> convertToOtherValueType() const { //Bound<OtherValueType> convertToOtherValueType() const {
return Bound<OtherValueType>(comparisonType, storm::utility::convertNumber<OtherValueType>(threshold)); // return Bound<OtherValueType>(comparisonType, storm::utility::convertNumber<OtherValueType>(threshold));
} //}
ComparisonType comparisonType; ComparisonType comparisonType;
ValueType threshold; ValueType threshold;

3
src/logic/OperatorFormula.h
View File

@ -11,7 +11,8 @@
#include "src/utility/constants.h" #include "src/utility/constants.h"
namespace storm { namespace storm {
namespace logic { namespace logic {
struct OperatorInformation { struct OperatorInformation {
OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection = boost::none, boost::optional<Bound<RationalNumber>> const& bound = boost::none); OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection = boost::none, boost::optional<Bound<RationalNumber>> const& bound = boost::none);

15
src/modelchecker/AbstractModelChecker.cpp
View File

@ -12,8 +12,13 @@
#include "src/models/sparse/Dtmc.h" #include "src/models/sparse/Dtmc.h"
#include "src/models/sparse/Ctmc.h" #include "src/models/sparse/Ctmc.h"
#include "src/models/sparse/Mdp.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/MarkovAutomaton.h"
#include "src/models/sparse/StandardRewardModel.h" #include "src/models/sparse/StandardRewardModel.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Bdd.h"
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
@ -275,7 +280,10 @@ namespace storm {
return subResult; return subResult;
} }
///////////////////////////////////////////////
// Explicitly instantiate the template class. // Explicitly instantiate the template class.
///////////////////////////////////////////////
// Sparse
template class AbstractModelChecker<storm::models::sparse::Model<double>>; template class AbstractModelChecker<storm::models::sparse::Model<double>>;
template class AbstractModelChecker<storm::models::sparse::Dtmc<double>>; template class AbstractModelChecker<storm::models::sparse::Dtmc<double>>;
template class AbstractModelChecker<storm::models::sparse::Ctmc<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::Mdp<storm::RationalFunction>>;
template class AbstractModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>; template class AbstractModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>;
#endif #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>>;
} }
} }

8
src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
View File

@ -39,15 +39,15 @@ namespace storm {
} }
template <typename SparseCtmcModelType> template <typename SparseCtmcModelType>
template<typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type> template<typename CValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true)); return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true));
} }
template <typename SparseCtmcModelType> template <typename SparseCtmcModelType>
template<typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type> template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true)); return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true));
} }

8
src/modelchecker/csl/SparseCtmcCslModelChecker.h
View File

@ -33,11 +33,11 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override; virtual std::unique_ptr<CheckResult> computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
private: private:
template<typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0> template<typename CValueType = ValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>
bool canHandleImplementation(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const; bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const;
template<typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0> template<typename CValueType = ValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>
bool canHandleImplementation(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const; bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const;
// An object that is used for solving linear equations and performing matrix-vector multiplication. // An object that is used for solving linear equations and performing matrix-vector multiplication.
std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory; std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;

85
src/modelchecker/exploration/SparseExplorationModelChecker.cpp
View File

@ -17,6 +17,8 @@
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/models/sparse/StandardRewardModel.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/SettingsManager.h"
#include "src/settings/modules/CoreSettings.h" #include "src/settings/modules/CoreSettings.h"
@ -34,20 +36,20 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
template<typename ValueType, typename StateType> template<typename ModelType, 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()) { 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. // Intentionally left empty.
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
bool SparseExplorationModelChecker<ValueType, StateType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { bool SparseExplorationModelChecker<ModelType, StateType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
storm::logic::FragmentSpecification fragment = storm::logic::reachability(); storm::logic::FragmentSpecification fragment = storm::logic::reachability();
return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet(); return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet();
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
std::unique_ptr<CheckResult> SparseExplorationModelChecker<ValueType, StateType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SparseExplorationModelChecker<ModelType, StateType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
storm::logic::UntilFormula const& untilFormula = checkTask.getFormula(); storm::logic::UntilFormula const& untilFormula = checkTask.getFormula();
storm::logic::Formula const& conditionFormula = untilFormula.getLeftSubformula(); storm::logic::Formula const& conditionFormula = untilFormula.getLeftSubformula();
storm::logic::Formula const& targetFormula = untilFormula.getRightSubformula(); 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)); return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState));
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
std::tuple<StateType, ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const { 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. // Generate the initial state so we know where to start the simulation.
stateGeneration.computeInitialStates(); stateGeneration.computeInitialStates();
STORM_LOG_THROW(stateGeneration.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the exploration engine."); 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)); return std::make_tuple(initialStateIndex, bounds.getLowerBoundForState(initialStateIndex, explorationInformation), bounds.getUpperBoundForState(initialStateIndex, explorationInformation));
} }
template<typename ValueType, typename StateType> template<typename ModelType, 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 { 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. // Start the search from the initial state.
stack.push_back(std::make_pair(stateGeneration.getFirstInitialState(), 0)); stack.push_back(std::make_pair(stateGeneration.getFirstInitialState(), 0));
@ -182,8 +184,8 @@ namespace storm {
return foundTerminalState; return foundTerminalState;
} }
template<typename ValueType, typename StateType> template<typename ModelType, 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 { 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 isTerminalState = false;
bool isTargetState = false; bool isTargetState = false;
@ -284,8 +286,8 @@ namespace storm {
return isTerminalState; return isTerminalState;
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
typename SparseExplorationModelChecker<ValueType, StateType>::ActionType SparseExplorationModelChecker<ValueType, StateType>::sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { 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. // Determine the values of all available actions.
std::vector<std::pair<ActionType, ValueType>> actionValues; std::vector<std::pair<ActionType, ValueType>> actionValues;
StateType rowGroup = explorationInformation.getRowGroup(currentStateId); StateType rowGroup = explorationInformation.getRowGroup(currentStateId);
@ -322,8 +324,8 @@ namespace storm {
return actionValues[distribution(randomGenerator)].first; return actionValues[distribution(randomGenerator)].first;
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
StateType SparseExplorationModelChecker<ValueType, StateType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { 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); std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& row = explorationInformation.getRowOfMatrix(chosenAction);
if (row.size() == 1) { if (row.size() == 1) {
return row.front().getColumn(); return row.front().getColumn();
@ -354,8 +356,8 @@ namespace storm {
} }
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
bool SparseExplorationModelChecker<ValueType, StateType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const { bool SparseExplorationModelChecker<ModelType, StateType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
++stats.numberOfPrecomputations; ++stats.numberOfPrecomputations;
// Outline: // Outline:
@ -487,8 +489,8 @@ namespace storm {
return true; return true;
} }
template<typename ValueType, typename StateType> template<typename ModelType, 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 { 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; bool containsTargetState = false;
// Now we record all actions leaving the EC. // Now we record all actions leaving the EC.
@ -556,8 +558,8 @@ namespace storm {
} }
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
ValueType SparseExplorationModelChecker<ValueType, StateType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { 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>(); ValueType result = storm::utility::zero<ValueType>();
for (auto const& element : explorationInformation.getRowOfMatrix(action)) { for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation); result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation);
@ -565,8 +567,8 @@ namespace storm {
return result; return result;
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
ValueType SparseExplorationModelChecker<ValueType, StateType>::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { 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>(); ValueType result = storm::utility::zero<ValueType>();
for (auto const& element : explorationInformation.getRowOfMatrix(action)) { for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation); result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation);
@ -574,8 +576,8 @@ namespace storm {
return result; return result;
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { 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? // TODO: take into account self-loops?
std::pair<ValueType, ValueType> result = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>()); std::pair<ValueType, ValueType> result = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
for (auto const& element : explorationInformation.getRowOfMatrix(action)) { for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
@ -585,8 +587,8 @@ namespace storm {
return result; return result;
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { 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); StateType group = explorationInformation.getRowGroup(currentStateId);
std::pair<ValueType, ValueType> result = getLowestBounds(explorationInformation.getOptimizationDirection()); std::pair<ValueType, ValueType> result = getLowestBounds(explorationInformation.getOptimizationDirection());
for (ActionType action = explorationInformation.getStartRowOfGroup(group); action < explorationInformation.getStartRowOfGroup(group + 1); ++action) { for (ActionType action = explorationInformation.getStartRowOfGroup(group); action < explorationInformation.getStartRowOfGroup(group + 1); ++action) {
@ -596,8 +598,8 @@ namespace storm {
return result; return result;
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
void SparseExplorationModelChecker<ValueType, StateType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { void SparseExplorationModelChecker<ModelType, StateType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
stack.pop_back(); stack.pop_back();
while (!stack.empty()) { while (!stack.empty()) {
updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds); updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds);
@ -605,8 +607,8 @@ namespace storm {
} }
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
void SparseExplorationModelChecker<ValueType, StateType>::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { 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. // Compute the new lower/upper values of the action.
std::pair<ValueType, ValueType> newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds); std::pair<ValueType, ValueType> newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds);
@ -640,8 +642,8 @@ namespace storm {
} }
} }
template<typename ValueType, typename StateType> template<typename ModelType, 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 { 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()); ValueType bound = getLowestBound(explorationInformation.getOptimizationDirection());
ActionType group = explorationInformation.getRowGroup(state); ActionType group = explorationInformation.getRowGroup(state);
@ -659,14 +661,14 @@ namespace storm {
return bound; return bound;
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::getLowestBounds(storm::OptimizationDirection const& direction) const { std::pair<typename ModelType::ValueType, typename ModelType::ValueType> SparseExplorationModelChecker<ModelType, StateType>::getLowestBounds(storm::OptimizationDirection const& direction) const {
ValueType val = getLowestBound(direction); ValueType val = getLowestBound(direction);
return std::make_pair(val, val); return std::make_pair(val, val);
} }
template<typename ValueType, typename StateType> template<typename ModelType, typename StateType>
ValueType SparseExplorationModelChecker<ValueType, StateType>::getLowestBound(storm::OptimizationDirection const& direction) const { typename ModelType::ValueType SparseExplorationModelChecker<ModelType, StateType>::getLowestBound(storm::OptimizationDirection const& direction) const {
if (direction == storm::OptimizationDirection::Maximize) { if (direction == storm::OptimizationDirection::Maximize) {
return storm::utility::zero<ValueType>(); return storm::utility::zero<ValueType>();
} else { } else {
@ -674,8 +676,8 @@ namespace storm {
} }
} }
template<typename ValueType, typename StateType> template<typename ModelType, 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 { 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) { if (direction == storm::OptimizationDirection::Maximize) {
return std::make_pair(std::max(bounds1.first, bounds2.first), std::max(bounds1.second, bounds2.second)); return std::make_pair(std::max(bounds1.first, bounds2.first), std::max(bounds1.second, bounds2.second));
} else { } 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>;
} }
} }

5
src/modelchecker/exploration/SparseExplorationModelChecker.h
View File

@ -30,9 +30,10 @@ namespace storm {
using namespace exploration_detail; using namespace exploration_detail;
template<typename ValueType, typename StateType = uint32_t> template<typename ModelType, typename StateType = uint32_t>
class SparseExplorationModelChecker : public AbstractModelChecker<ValueType> { class SparseExplorationModelChecker : public AbstractModelChecker<ModelType> {
public: public:
typedef typename ModelType::ValueType ValueType;
typedef StateType ActionType; typedef StateType ActionType;
typedef std::vector<std::pair<StateType, ActionType>> StateActionStack; typedef std::vector<std::pair<StateType, ActionType>> StateActionStack;

56
src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
View File

@ -25,24 +25,24 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
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)) { HybridDtmcPrctlModelChecker<ModelType>::HybridDtmcPrctlModelChecker(ModelType const& model, std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) {
// Intentionally left empty. // Intentionally left empty.
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
HybridDtmcPrctlModelChecker<DdType, ValueType>::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(std::make_unique<storm::solver::GeneralLinearEquationSolverFactory<ValueType>>()) { HybridDtmcPrctlModelChecker<ModelType>::HybridDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(std::make_unique<storm::solver::GeneralLinearEquationSolverFactory<ValueType>>()) {
// Intentionally left empty. // Intentionally left empty.
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
bool HybridDtmcPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { bool HybridDtmcPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true)); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true));
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) {
storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) {
storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); storm::logic::NextFormula const& pathFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); 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()); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) { 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::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) { 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::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { 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(); storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula()); std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); 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); 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<typename ModelType>
template<storm::dd::DdType DdType, typename ValueType> std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) {
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) {
storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula); std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); 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))); 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::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;
template class HybridDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double>; template class HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>;
} }
} }

14
src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
View File

@ -10,11 +10,14 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType, ValueType> { class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker<ModelType> {
public: public:
explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model); typedef typename ModelType::ValueType ValueType;
explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory); 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. // The implemented methods of the AbstractModelChecker interface.
virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override; 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> 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; 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: private:
// An object that is used for retrieving linear equation solvers. // An object that is used for retrieving linear equation solvers.
std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory; std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;

52
src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
View File

@ -19,24 +19,24 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
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)) { HybridMdpPrctlModelChecker<ModelType>::HybridMdpPrctlModelChecker(ModelType const& model, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) {
// Intentionally left empty. // Intentionally left empty.
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
HybridMdpPrctlModelChecker<DdType, ValueType>::HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(std::make_unique<storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType>>()) { HybridMdpPrctlModelChecker<ModelType>::HybridMdpPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(std::make_unique<storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType>>()) {
// Intentionally left empty. // Intentionally left empty.
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
bool HybridMdpPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { bool HybridMdpPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false));
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); 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."); 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()); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) {
storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); 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."); 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()); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) {
storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); 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."); 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()); 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()); return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); 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(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."); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) { 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::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(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."); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) { 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::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(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."); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { 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::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(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()); std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); 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); 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 class HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
template<storm::dd::DdType DdType, typename ValueType> template class HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>;
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>;
} }
} }

16
src/modelchecker/prctl/HybridMdpPrctlModelChecker.h
View File

@ -17,11 +17,14 @@ namespace storm {
namespace modelchecker { namespace modelchecker {
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType, ValueType> { class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<ModelType> {
public: public:
explicit HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model); typedef typename ModelType::ValueType ValueType;
explicit HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory); 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. // The implemented methods of the AbstractModelChecker interface.
virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override; 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> 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> 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; 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: private:
// An object that is used for retrieving linear equation solvers. // An object that is used for retrieving linear equation solvers.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ValueType>> linearEquationSolverFactory; std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;

22
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -34,13 +34,13 @@ namespace storm {
} }
template<typename SparseDtmcModelType> 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(); storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true)); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true));
} }
template<typename SparseDtmcModelType> 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::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); 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()); std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
@ -53,7 +53,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> 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(); storm::logic::NextFormula const& pathFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
@ -62,7 +62,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> 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(); storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
@ -73,7 +73,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> 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(); storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
@ -82,7 +82,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> 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::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); 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); 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> 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::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); 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); 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> 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(); storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula()); std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
@ -107,7 +107,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> 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(); storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula); std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
@ -116,7 +116,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> 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::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();
STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); 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."); STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
@ -131,7 +131,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> 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::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();
STORM_LOG_THROW(conditionalFormula.getSubformula().isReachabilityRewardFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); 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."); STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");

52
src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
View File

@ -22,24 +22,24 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
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)) { 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. // Intentionally left empty.
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
SymbolicDtmcPrctlModelChecker<DdType, ValueType>::SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>()) { SymbolicDtmcPrctlModelChecker<ModelType>::SymbolicDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>()) {
// Intentionally left empty. // Intentionally left empty.
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
bool SymbolicDtmcPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { bool SymbolicDtmcPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false));
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); 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)); return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) {
storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); 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)); return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) {
storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); storm::logic::NextFormula const& pathFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); 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)); return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); 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()); 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)); return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) { 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::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); 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); 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)); return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) { 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::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); 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); 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)); return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { 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(); storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula()); std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); 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); 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)); return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
} }
template class SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;
template<storm::dd::DdType DdType, typename ValueType> template class SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>;
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>;
} }
} }

16
src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h
View File

@ -7,11 +7,14 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
class SymbolicDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType, ValueType> { class SymbolicDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker<ModelType> {
public: public:
explicit SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model); typedef typename ModelType::ValueType ValueType;
explicit SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType, ValueType> const& model, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory); 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. // The implemented methods of the AbstractModelChecker interface.
virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override; 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> 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> 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; 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: private:
// An object that is used for retrieving linear equation solvers. // An object that is used for retrieving linear equation solvers.
std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>> linearEquationSolverFactory; std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>> linearEquationSolverFactory;

51
src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
View File

@ -21,24 +21,24 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
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)) { 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. // Intentionally left empty.
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
SymbolicMdpPrctlModelChecker<DdType, ValueType>::SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model) : SymbolicPropositionalModelChecker<DdType, ValueType>(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>()) { SymbolicMdpPrctlModelChecker<ModelType>::SymbolicMdpPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>()) {
// Intentionally left empty. // Intentionally left empty.
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
bool SymbolicMdpPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { bool SymbolicMdpPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false));
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); 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."); 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()); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) {
storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); 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."); 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()); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) {
storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); 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."); 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()); 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()); return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
} }
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); 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(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."); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) { 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::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(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."); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) { 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::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(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."); 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); 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> template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { 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::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(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()); std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); 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); 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 class SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
template<storm::dd::DdType DdType, typename ValueType> template class SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>;
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>;
} }
} }

15
src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h
View File

@ -9,11 +9,14 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
template<storm::dd::DdType DdType, typename ValueType> template<typename ModelType>
class SymbolicMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType, ValueType> { class SymbolicMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<ModelType> {
public: public:
explicit SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model); typedef typename ModelType::ValueType ValueType;
explicit SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType, ValueType> const& model, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory); 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. // The implemented methods of the AbstractModelChecker interface.
virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override; 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> 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; 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: private:
// An object that is used for retrieving linear equation solvers. // An object that is used for retrieving linear equation solvers.
std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>> linearEquationSolverFactory; std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>> linearEquationSolverFactory;

2
src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
View File

@ -85,7 +85,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType> 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> 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); std::unique_ptr<CheckResult> result = computeUntilProbabilities(model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory);
result->asQuantitativeCheckResult().oneMinus(); result->asQuantitativeCheckResult<ValueType>().oneMinus();
return result; return result;
} }

2
src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
View File

@ -89,7 +89,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType> 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> 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); 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; return result;
} }

2
src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
View File

@ -78,7 +78,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType> 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> 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); 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; return result;
} }

4
src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
View File

@ -18,7 +18,7 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
template<typename ModelType> 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. // Intentionally left empty.
} }
@ -52,7 +52,7 @@ namespace storm {
} }
template<typename ModelType> template<typename ModelType>
storm::models::symbolic::Model<Type, ValueType> const& SymbolicPropositionalModelChecker<ModelType>::getModel() const { ModelType const& SymbolicPropositionalModelChecker<ModelType>::getModel() const {
return model; return model;
} }

1
src/modelchecker/propositional/SymbolicPropositionalModelChecker.h
View File

@ -20,6 +20,7 @@ namespace storm {
public: public:
typedef typename ModelType::ValueType ValueType; typedef typename ModelType::ValueType ValueType;
static const storm::dd::DdType DdType = ModelType::DdType; static const storm::dd::DdType DdType = ModelType::DdType;
explicit SymbolicPropositionalModelChecker(ModelType const& model); explicit SymbolicPropositionalModelChecker(ModelType const& model);
// The implemented methods of the AbstractModelChecker interface. // The implemented methods of the AbstractModelChecker interface.

14
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
View File

@ -30,13 +30,13 @@ namespace storm {
explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc<ValueType> const& model); explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc<ValueType> const& model);
// The implemented methods of the AbstractModelChecker interface. // The implemented methods of the AbstractModelChecker interface.
virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override; virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) 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> 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> 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> 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> 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> const& checkTask) override; virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
// Static helper methods // 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); 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);

11
src/modelchecker/results/CheckResult.cpp
View File

@ -88,15 +88,8 @@ namespace storm {
QualitativeCheckResult const& CheckResult::asQualitativeCheckResult() const { QualitativeCheckResult const& CheckResult::asQualitativeCheckResult() const {
return dynamic_cast<QualitativeCheckResult const&>(*this); 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> template <storm::dd::DdType Type>
SymbolicQualitativeCheckResult<Type>& CheckResult::asSymbolicQualitativeCheckResult() { SymbolicQualitativeCheckResult<Type>& CheckResult::asSymbolicQualitativeCheckResult() {
return dynamic_cast<SymbolicQualitativeCheckResult<Type>&>(*this); return dynamic_cast<SymbolicQualitativeCheckResult<Type>&>(*this);

9
src/modelchecker/results/CheckResult.h
View File

@ -57,9 +57,14 @@ namespace storm {
QualitativeCheckResult const& asQualitativeCheckResult() const; QualitativeCheckResult const& asQualitativeCheckResult() const;
template<typename ValueType> template<typename ValueType>
QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult(); QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult() {
return static_cast<QuantitativeCheckResult<ValueType> &>(*this);
}
template<typename ValueType> template<typename ValueType>
QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const; QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const {
return static_cast<QuantitativeCheckResult<ValueType> const&>(*this);
}
ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const; ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const;

20
src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
View File

@ -128,35 +128,35 @@ namespace storm {
} }
template<typename ValueType> 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()) { if (this->isResultForAllStates()) {
vector_type const& valuesAsVector = boost::get<vector_type>(values); vector_type const& valuesAsVector = boost::get<vector_type>(values);
storm::storage::BitVector result(valuesAsVector.size()); storm::storage::BitVector result(valuesAsVector.size());
switch (comparisonType) { switch (comparisonType) {
case logic::ComparisonType::Less: case logic::ComparisonType::Less:
for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { 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); result.set(index);
} }
} }
break; break;
case logic::ComparisonType::LessEqual: case logic::ComparisonType::LessEqual:
for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { 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); result.set(index);
} }
} }
break; break;
case logic::ComparisonType::Greater: case logic::ComparisonType::Greater:
for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { 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); result.set(index);
} }
} }
break; break;
case logic::ComparisonType::GreaterEqual: case logic::ComparisonType::GreaterEqual:
for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { 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); result.set(index);
} }
} }
@ -169,22 +169,22 @@ namespace storm {
switch (comparisonType) { switch (comparisonType) {
case logic::ComparisonType::Less: case logic::ComparisonType::Less:
for (auto const& element : valuesAsMap) { for (auto const& element : valuesAsMap) {
result[element.first] = element.second < storm::utility::convertNumber<ValueType, double>(bound); result[element.first] = element.second < bound;
} }
break; break;
case logic::ComparisonType::LessEqual: case logic::ComparisonType::LessEqual:
for (auto const& element : valuesAsMap) { for (auto const& element : valuesAsMap) {
result[element.first] = element.second <= storm::utility::convertNumber<ValueType, double>(bound); result[element.first] = element.second <= bound;
} }
break; break;
case logic::ComparisonType::Greater: case logic::ComparisonType::Greater:
for (auto const& element : valuesAsMap) { for (auto const& element : valuesAsMap) {
result[element.first] = element.second > storm::utility::convertNumber<ValueType, double>(bound); result[element.first] = element.second > bound;
} }
break; break;
case logic::ComparisonType::GreaterEqual: case logic::ComparisonType::GreaterEqual:
for (auto const& element : valuesAsMap) { for (auto const& element : valuesAsMap) {
result[element.first] = element.second >= storm::utility::convertNumber<ValueType, double>(bound); result[element.first] = element.second >= bound;
} }
break; break;
} }
@ -194,7 +194,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template<> 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. // Since it is not possible to compare rational functions against bounds, we simply call the base class method.
return QuantitativeCheckResult::compareAgainstBound(comparisonType, bound); return QuantitativeCheckResult::compareAgainstBound(comparisonType, bound);
} }

2
src/modelchecker/results/ExplicitQuantitativeCheckResult.h
View File

@ -37,7 +37,7 @@ namespace storm {
ValueType& operator[](storm::storage::sparse::state_type state); ValueType& operator[](storm::storage::sparse::state_type state);
ValueType const& operator[](storm::storage::sparse::state_type state) const; 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 isExplicit() const override;
virtual bool isResultForAllStates() const override; virtual bool isResultForAllStates() const override;

2
src/modelchecker/results/HybridQuantitativeCheckResult.cpp
View File

@ -17,7 +17,7 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ValueType> 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; storm::dd::Bdd<Type> symbolicResult;
// First compute the symbolic part of the result. // First compute the symbolic part of the result.

2
src/modelchecker/results/HybridQuantitativeCheckResult.h
View File

@ -23,7 +23,7 @@ namespace storm {
HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult&& other) = default; HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult&& other) = default;
#endif #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; std::unique_ptr<CheckResult> toExplicitQuantitativeCheckResult() const;

5
src/modelchecker/results/QuantitativeCheckResult.cpp
View File

@ -10,12 +10,12 @@ namespace storm {
namespace modelchecker { namespace modelchecker {
template<typename ValueType> 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."); STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result.");
} }
template<typename ValueType> template<typename ValueType>
bool QuantitativeCheckResult::isQuantitative() const { bool QuantitativeCheckResult<ValueType>::isQuantitative() const {
return true; return true;
} }
@ -23,6 +23,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class QuantitativeCheckResult<RationalNumber>; template class QuantitativeCheckResult<RationalNumber>;
template class QuantitativeCheckResult<RationalFunction>;
#endif #endif
} }
} }

2
src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
View File

@ -16,7 +16,7 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ValueType> 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; storm::dd::Bdd<Type> states;
if (comparisonType == storm::logic::ComparisonType::Less) { if (comparisonType == storm::logic::ComparisonType::Less) {
states = values.less(bound); states = values.less(bound);

5
src/modelchecker/results/SymbolicQuantitativeCheckResult.h
View File

@ -21,8 +21,9 @@ namespace storm {
SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult&& other) = default; SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult&& other) = default;
#endif #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 isSymbolic() const override;
virtual bool isResultForAllStates() const override; virtual bool isResultForAllStates() const override;

6
src/utility/constants.cpp
View File

@ -156,6 +156,11 @@ namespace storm {
return carl::rationalize<RationalNumber>(number); return carl::rationalize<RationalNumber>(number);
} }
template<>
RationalNumber convertNumber(RationalNumber const& number){
return number;
}
template<> template<>
RationalFunction convertNumber(double const& number){ RationalFunction convertNumber(double const& number){
return RationalFunction(carl::rationalize<RationalNumber>(number)); return RationalFunction(carl::rationalize<RationalNumber>(number));
@ -268,6 +273,7 @@ namespace storm {
template double convertNumber(storm::RationalNumber const& number); template double convertNumber(storm::RationalNumber const& number);
template storm::RationalNumber convertNumber(double 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); template storm::RationalNumber abs(storm::RationalNumber const& number);

22
src/utility/storm.h
View File

@ -264,7 +264,7 @@ namespace storm {
} }
template<typename ValueType> 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; 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()) { 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); storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
@ -285,7 +285,7 @@ namespace storm {
} }
template<typename ValueType> 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; std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc); storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
if (modelchecker.canHandle(task)) { if (modelchecker.canHandle(task)) {
@ -297,7 +297,7 @@ namespace storm {
} }
template<typename ValueType> 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; std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp); storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
if (modelchecker.canHandle(task)) { if (modelchecker.canHandle(task)) {
@ -310,7 +310,7 @@ namespace storm {
template<typename ValueType> 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) { 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; std::unique_ptr<storm::modelchecker::CheckResult> result;
if (model->getType() == storm::models::ModelType::Dtmc) { if (model->getType() == storm::models::ModelType::Dtmc) {
@ -337,7 +337,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template<> 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) { 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; std::unique_ptr<storm::modelchecker::CheckResult> result;
if (model->getType() == storm::models::ModelType::Dtmc) { if (model->getType() == storm::models::ModelType::Dtmc) {
@ -370,7 +370,7 @@ namespace storm {
template<> 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) { 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; std::unique_ptr<storm::modelchecker::CheckResult> result;
if (model->getType() == storm::models::ModelType::Dtmc) { if (model->getType() == storm::models::ModelType::Dtmc) {
@ -394,19 +394,19 @@ namespace storm {
storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
if (model->getType() == storm::models::ModelType::Dtmc) { if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>(); 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)) { if (modelchecker.canHandle(task)) {
result = modelchecker.check(task); result = modelchecker.check(task);
} }
} else if (model->getType() == storm::models::ModelType::Ctmc) { } 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>>(); 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)) { if (modelchecker.canHandle(task)) {
result = modelchecker.check(task); result = modelchecker.check(task);
} }
} else if (model->getType() == storm::models::ModelType::Mdp) { } 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>>(); 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)) { if (modelchecker.canHandle(task)) {
result = modelchecker.check(task); result = modelchecker.check(task);
} }
@ -423,13 +423,13 @@ namespace storm {
storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
if (model->getType() == storm::models::ModelType::Dtmc) { if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>(); 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)) { if (modelchecker.canHandle(task)) {
result = modelchecker.check(task); result = modelchecker.check(task);
} }
} else if (model->getType() == storm::models::ModelType::Mdp) { } 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>>(); 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)) { if (modelchecker.canHandle(task)) {
result = modelchecker.check(task); result = modelchecker.check(task);
} }

Write Preview
|||||||
100:0
Loading…
Cancel
Save