Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
QualitativeAnalysis.h
Go to the documentation of this file.
3
4namespace storm {
5namespace pomdp {
6namespace qualitative {
7template<typename ValueType>
9 storm::storage::BitVector const& surelyReachSinkStates) {
10 if (storm::utility::graph::checkIfECWithChoiceExists(pomdp.getTransitionMatrix(), pomdp.getBackwardTransitions(), ~targetStates & ~surelyReachSinkStates,
12 STORM_LOG_DEBUG("Lookahead (possibly) required.");
13 return true;
14 } else {
15 STORM_LOG_DEBUG("No lookahead required.");
16 return false;
17 }
18}
19} // namespace qualitative
20} // namespace pomdp
21} // namespace storm
storm::storage::SparseMatrix< ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:197
storm::storage::SparseMatrix< ValueType > getBackwardTransitions() const
Retrieves the backward transition relation of the model, i.e.
Definition Model.cpp:152
uint_fast64_t getNumberOfChoices(uint_fast64_t state) const
This class represents a partially observable Markov decision process.
Definition Pomdp.h:15
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
#define STORM_LOG_DEBUG(message)
Definition logging.h:23
bool isLookaheadRequired(storm::models::sparse::Pomdp< ValueType > const &pomdp, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &surelyReachSinkStates)
bool checkIfECWithChoiceExists(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &subsystem, storm::storage::BitVector const &choices)
Checks whether there is an End Component that.
Definition graph.cpp:182
LabParser.cpp.
Definition cli.cpp:18