Storm
A Modern Probabilistic Model Checker
|
Functions | |
bool | eliminationOrderNeedsDistances (storm::settings::modules::EliminationSettings::EliminationOrder const &order) |
bool | eliminationOrderNeedsForwardDistances (storm::settings::modules::EliminationSettings::EliminationOrder const &order) |
bool | eliminationOrderNeedsReversedDistances (storm::settings::modules::EliminationSettings::EliminationOrder const &order) |
bool | eliminationOrderIsPenaltyBased (storm::settings::modules::EliminationSettings::EliminationOrder const &order) |
bool | eliminationOrderIsStatic (storm::settings::modules::EliminationSettings::EliminationOrder const &order) |
template<typename ValueType > | |
uint_fast64_t | estimateComplexity (ValueType const &) |
template<typename ValueType > | |
uint_fast64_t | computeStatePenalty (storm::storage::sparse::state_type const &state, storm::storage::FlexibleSparseMatrix< ValueType > const &transitionMatrix, storm::storage::FlexibleSparseMatrix< ValueType > const &backwardTransitions, std::vector< ValueType > const &oneStepProbabilities) |
template<typename ValueType > | |
uint_fast64_t | computeStatePenaltyRegularExpression (storm::storage::sparse::state_type const &state, storm::storage::FlexibleSparseMatrix< ValueType > const &transitionMatrix, storm::storage::FlexibleSparseMatrix< ValueType > const &backwardTransitions, std::vector< ValueType > const &) |
template<typename ValueType > | |
std::shared_ptr< StatePriorityQueue > | createStatePriorityQueue (boost::optional< std::vector< uint_fast64_t > > const &distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix< ValueType > const &transitionMatrix, storm::storage::FlexibleSparseMatrix< ValueType > const &backwardTransitions, std::vector< ValueType > const &oneStepProbabilities, storm::storage::BitVector const &states) |
std::shared_ptr< StatePriorityQueue > | createStatePriorityQueue (storm::storage::BitVector const &states) |
std::shared_ptr< StatePriorityQueue > | createStatePriorityQueue (std::vector< storm::storage::sparse::state_type > const &states) |
template<typename ValueType > | |
std::vector< uint_fast64_t > | getDistanceBasedPriorities (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &transitionMatrixTransposed, storm::storage::BitVector const &initialStates, std::vector< ValueType > const &oneStepProbabilities, bool forward, bool reverse) |
template<typename ValueType > | |
std::vector< uint_fast64_t > | getStateDistances (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &transitionMatrixTransposed, storm::storage::BitVector const &initialStates, std::vector< ValueType > const &oneStepProbabilities, bool forward) |
template uint_fast64_t | estimateComplexity (double const &value) |
template std::shared_ptr< StatePriorityQueue > | createStatePriorityQueue (boost::optional< std::vector< uint_fast64_t > > const &distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix< double > const &transitionMatrix, storm::storage::FlexibleSparseMatrix< double > const &backwardTransitions, std::vector< double > const &oneStepProbabilities, storm::storage::BitVector const &states) |
template uint_fast64_t | computeStatePenalty (storm::storage::sparse::state_type const &state, storm::storage::FlexibleSparseMatrix< double > const &transitionMatrix, storm::storage::FlexibleSparseMatrix< double > const &backwardTransitions, std::vector< double > const &oneStepProbabilities) |
template uint_fast64_t | computeStatePenaltyRegularExpression (storm::storage::sparse::state_type const &state, storm::storage::FlexibleSparseMatrix< double > const &transitionMatrix, storm::storage::FlexibleSparseMatrix< double > const &backwardTransitions, std::vector< double > const &oneStepProbabilities) |
template std::vector< uint_fast64_t > | getDistanceBasedPriorities (storm::storage::SparseMatrix< double > const &transitionMatrix, storm::storage::SparseMatrix< double > const &transitionMatrixTransposed, storm::storage::BitVector const &initialStates, std::vector< double > const &oneStepProbabilities, bool forward, bool reverse) |
template std::vector< uint_fast64_t > | getStateDistances (storm::storage::SparseMatrix< double > const &transitionMatrix, storm::storage::SparseMatrix< double > const &transitionMatrixTransposed, storm::storage::BitVector const &initialStates, std::vector< double > const &oneStepProbabilities, bool forward) |
template uint_fast64_t storm::utility::stateelimination::computeStatePenalty | ( | storm::storage::sparse::state_type const & | state, |
storm::storage::FlexibleSparseMatrix< double > const & | transitionMatrix, | ||
storm::storage::FlexibleSparseMatrix< double > const & | backwardTransitions, | ||
std::vector< double > const & | oneStepProbabilities | ||
) |
uint_fast64_t storm::utility::stateelimination::computeStatePenalty | ( | storm::storage::sparse::state_type const & | state, |
storm::storage::FlexibleSparseMatrix< ValueType > const & | transitionMatrix, | ||
storm::storage::FlexibleSparseMatrix< ValueType > const & | backwardTransitions, | ||
std::vector< ValueType > const & | oneStepProbabilities | ||
) |
Definition at line 71 of file stateelimination.cpp.
template uint_fast64_t storm::utility::stateelimination::computeStatePenaltyRegularExpression | ( | storm::storage::sparse::state_type const & | state, |
storm::storage::FlexibleSparseMatrix< double > const & | transitionMatrix, | ||
storm::storage::FlexibleSparseMatrix< double > const & | backwardTransitions, | ||
std::vector< double > const & | oneStepProbabilities | ||
) |
uint_fast64_t storm::utility::stateelimination::computeStatePenaltyRegularExpression | ( | storm::storage::sparse::state_type const & | state, |
storm::storage::FlexibleSparseMatrix< ValueType > const & | transitionMatrix, | ||
storm::storage::FlexibleSparseMatrix< ValueType > const & | backwardTransitions, | ||
std::vector< ValueType > const & | |||
) |
Definition at line 97 of file stateelimination.cpp.
template std::shared_ptr< StatePriorityQueue > storm::utility::stateelimination::createStatePriorityQueue | ( | boost::optional< std::vector< uint_fast64_t > > const & | distanceBasedStatePriorities, |
storm::storage::FlexibleSparseMatrix< double > const & | transitionMatrix, | ||
storm::storage::FlexibleSparseMatrix< double > const & | backwardTransitions, | ||
std::vector< double > const & | oneStepProbabilities, | ||
storm::storage::BitVector const & | states | ||
) |
std::shared_ptr< StatePriorityQueue > storm::utility::stateelimination::createStatePriorityQueue | ( | boost::optional< std::vector< uint_fast64_t > > const & | distanceBasedStatePriorities, |
storm::storage::FlexibleSparseMatrix< ValueType > const & | transitionMatrix, | ||
storm::storage::FlexibleSparseMatrix< ValueType > const & | backwardTransitions, | ||
std::vector< ValueType > const & | oneStepProbabilities, | ||
storm::storage::BitVector const & | states | ||
) |
Definition at line 104 of file stateelimination.cpp.
std::shared_ptr< StatePriorityQueue > storm::utility::stateelimination::createStatePriorityQueue | ( | std::vector< storm::storage::sparse::state_type > const & | states | ) |
Definition at line 166 of file stateelimination.cpp.
std::shared_ptr< StatePriorityQueue > storm::utility::stateelimination::createStatePriorityQueue | ( | storm::storage::BitVector const & | states | ) |
Definition at line 161 of file stateelimination.cpp.
bool storm::utility::stateelimination::eliminationOrderIsPenaltyBased | ( | storm::settings::modules::EliminationSettings::EliminationOrder const & | order | ) |
Definition at line 41 of file stateelimination.cpp.
bool storm::utility::stateelimination::eliminationOrderIsStatic | ( | storm::settings::modules::EliminationSettings::EliminationOrder const & | order | ) |
Definition at line 47 of file stateelimination.cpp.
bool storm::utility::stateelimination::eliminationOrderNeedsDistances | ( | storm::settings::modules::EliminationSettings::EliminationOrder const & | order | ) |
Definition at line 24 of file stateelimination.cpp.
bool storm::utility::stateelimination::eliminationOrderNeedsForwardDistances | ( | storm::settings::modules::EliminationSettings::EliminationOrder const & | order | ) |
Definition at line 31 of file stateelimination.cpp.
bool storm::utility::stateelimination::eliminationOrderNeedsReversedDistances | ( | storm::settings::modules::EliminationSettings::EliminationOrder const & | order | ) |
Definition at line 36 of file stateelimination.cpp.
template uint_fast64_t storm::utility::stateelimination::estimateComplexity | ( | double const & | value | ) |
uint_fast64_t storm::utility::stateelimination::estimateComplexity | ( | ValueType const & | ) |
Definition at line 52 of file stateelimination.cpp.
template std::vector< uint_fast64_t > storm::utility::stateelimination::getDistanceBasedPriorities | ( | storm::storage::SparseMatrix< double > const & | transitionMatrix, |
storm::storage::SparseMatrix< double > const & | transitionMatrixTransposed, | ||
storm::storage::BitVector const & | initialStates, | ||
std::vector< double > const & | oneStepProbabilities, | ||
bool | forward, | ||
bool | reverse | ||
) |
std::vector< uint_fast64_t > storm::utility::stateelimination::getDistanceBasedPriorities | ( | storm::storage::SparseMatrix< ValueType > const & | transitionMatrix, |
storm::storage::SparseMatrix< ValueType > const & | transitionMatrixTransposed, | ||
storm::storage::BitVector const & | initialStates, | ||
std::vector< ValueType > const & | oneStepProbabilities, | ||
bool | forward, | ||
bool | reverse | ||
) |
Definition at line 171 of file stateelimination.cpp.
template std::vector< uint_fast64_t > storm::utility::stateelimination::getStateDistances | ( | storm::storage::SparseMatrix< double > const & | transitionMatrix, |
storm::storage::SparseMatrix< double > const & | transitionMatrixTransposed, | ||
storm::storage::BitVector const & | initialStates, | ||
std::vector< double > const & | oneStepProbabilities, | ||
bool | forward | ||
) |
std::vector< uint_fast64_t > storm::utility::stateelimination::getStateDistances | ( | storm::storage::SparseMatrix< ValueType > const & | transitionMatrix, |
storm::storage::SparseMatrix< ValueType > const & | transitionMatrixTransposed, | ||
storm::storage::BitVector const & | initialStates, | ||
std::vector< ValueType > const & | oneStepProbabilities, | ||
bool | forward | ||
) |
Definition at line 211 of file stateelimination.cpp.