Storm 1.10.0.1
A Modern Probabilistic Model Checker
|
Classes | |
struct | NormalFormData |
class | WeightedReachabilityHelper |
A helper class that computes (weighted) reachability probabilities for a given MDP in normal form. More... | |
Enumerations | |
enum class | BisectionMethodBounds { Simple , Advanced } |
Functions | |
template<typename ValueType > | |
void | eliminateEndComponents (storm::storage::BitVector possibleEcStates, bool addRowAtRepresentativeState, std::optional< uint64_t > representativeRowEntry, storm::storage::SparseMatrix< ValueType > &matrix, uint64_t &initialState, storm::storage::BitVector &rowsWithSum1, std::vector< ValueType > &rowValues1, storm::OptionalRef< std::vector< ValueType > > rowValues2={}) |
template<typename ValueType , typename SolutionType = ValueType> | |
SolutionType | solveMinMaxEquationSystem (storm::Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix, std::vector< ValueType > const &rowValues, storm::storage::BitVector const &rowsWithSum1, storm::solver::OptimizationDirection const dir, uint64_t const initialState) |
template<typename ValueType > | |
void | computeReachabilityProbabilities (Environment const &env, std::map< uint64_t, ValueType > &nonZeroResults, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &allowedStates, storm::storage::BitVector const &targetStates) |
Computes the reachability probabilities for the given target states and inserts all non-zero values into the given map. | |
template<typename ValueType > | |
NormalFormData< ValueType > | obtainNormalForm (Environment const &env, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &relevantStates, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates) |
template<typename ValueType , typename SolutionType = ValueType> | |
SolutionType | computeViaRestartMethod (Environment const &env, uint64_t const initialState, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, NormalFormData< ValueType > const &normalForm) |
Uses the restart method by Baier et al. | |
template<typename ValueType , typename SolutionType = ValueType> | |
SolutionType | computeViaBisection (Environment const &env, BisectionMethodBounds boundOption, uint64_t const initialState, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, NormalFormData< ValueType > const &normalForm) |
template<typename ValueType , typename SolutionType = ValueType> | |
SolutionType | computeViaPolicyIteration (Environment const &env, uint64_t const initialState, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, NormalFormData< ValueType > const &normalForm) |
template<typename ValueType , typename SolutionType = ValueType> | |
std::optional< SolutionType > | handleTrivialCases (uint64_t const initialState, NormalFormData< ValueType > const &normalForm) |
|
strong |
Enumerator | |
---|---|
Simple | |
Advanced |
Definition at line 535 of file ConditionalHelper.cpp.
void storm::modelchecker::internal::computeReachabilityProbabilities | ( | Environment const & | env, |
std::map< uint64_t, ValueType > & | nonZeroResults, | ||
storm::solver::OptimizationDirection const | dir, | ||
storm::storage::SparseMatrix< ValueType > const & | transitionMatrix, | ||
storm::storage::BitVector const & | initialStates, | ||
storm::storage::BitVector const & | allowedStates, | ||
storm::storage::BitVector const & | targetStates | ||
) |
Computes the reachability probabilities for the given target states and inserts all non-zero values into the given map.
Definition at line 112 of file ConditionalHelper.cpp.
SolutionType storm::modelchecker::internal::computeViaBisection | ( | Environment const & | env, |
BisectionMethodBounds | boundOption, | ||
uint64_t const | initialState, | ||
storm::solver::OptimizationDirection const | dir, | ||
storm::storage::SparseMatrix< ValueType > const & | transitionMatrix, | ||
NormalFormData< ValueType > const & | normalForm | ||
) |
Definition at line 537 of file ConditionalHelper.cpp.
SolutionType storm::modelchecker::internal::computeViaPolicyIteration | ( | Environment const & | env, |
uint64_t const | initialState, | ||
storm::solver::OptimizationDirection const | dir, | ||
storm::storage::SparseMatrix< ValueType > const & | transitionMatrix, | ||
NormalFormData< ValueType > const & | normalForm | ||
) |
Definition at line 635 of file ConditionalHelper.cpp.
SolutionType storm::modelchecker::internal::computeViaRestartMethod | ( | Environment const & | env, |
uint64_t const | initialState, | ||
storm::solver::OptimizationDirection const | dir, | ||
storm::storage::SparseMatrix< ValueType > const & | transitionMatrix, | ||
NormalFormData< ValueType > const & | normalForm | ||
) |
Uses the restart method by Baier et al.
Definition at line 226 of file ConditionalHelper.cpp.
void storm::modelchecker::internal::eliminateEndComponents | ( | storm::storage::BitVector | possibleEcStates, |
bool | addRowAtRepresentativeState, | ||
std::optional< uint64_t > | representativeRowEntry, | ||
storm::storage::SparseMatrix< ValueType > & | matrix, | ||
uint64_t & | initialState, | ||
storm::storage::BitVector & | rowsWithSum1, | ||
std::vector< ValueType > & | rowValues1, | ||
storm::OptionalRef< std::vector< ValueType > > | rowValues2 = {} |
||
) |
Definition at line 30 of file ConditionalHelper.cpp.
std::optional< SolutionType > storm::modelchecker::internal::handleTrivialCases | ( | uint64_t const | initialState, |
NormalFormData< ValueType > const & | normalForm | ||
) |
Definition at line 670 of file ConditionalHelper.cpp.
NormalFormData< ValueType > storm::modelchecker::internal::obtainNormalForm | ( | Environment const & | env, |
storm::solver::OptimizationDirection const | dir, | ||
storm::storage::SparseMatrix< ValueType > const & | transitionMatrix, | ||
storm::storage::SparseMatrix< ValueType > const & | backwardTransitions, | ||
storm::storage::BitVector const & | relevantStates, | ||
storm::storage::BitVector const & | targetStates, | ||
storm::storage::BitVector const & | conditionStates | ||
) |
Definition at line 172 of file ConditionalHelper.cpp.
SolutionType storm::modelchecker::internal::solveMinMaxEquationSystem | ( | storm::Environment const & | env, |
storm::storage::SparseMatrix< ValueType > const & | matrix, | ||
std::vector< ValueType > const & | rowValues, | ||
storm::storage::BitVector const & | rowsWithSum1, | ||
storm::solver::OptimizationDirection const | dir, | ||
uint64_t const | initialState | ||
) |
Definition at line 87 of file ConditionalHelper.cpp.