Storm
A Modern Probabilistic Model Checker
|
Classes | |
class | GSVIBackend |
class | IIBackend |
struct | IIData |
class | IntervalIterationHelper |
Implements interval iteration. More... | |
class | OptimisticValueIterationHelper |
Implements Optimistic value iteration. More... | |
class | OVIBackend |
class | RationalSearchHelper |
Implements rational search. More... | |
class | RSBackend |
class | SchedulerTrackingBackend |
class | SchedulerTrackingHelper |
Helper class to extract optimal scheduler choices from a MinMax equation system solution. More... | |
class | SoundValueIterationHelper |
Implements sound value iteration. More... | |
class | SVIBackend |
class | ValueIterationHelper |
class | ValueIterationOperator |
This class represents the Value Iteration Operator (also known as Bellman operator). More... | |
class | VIOperatorBackend |
Enumerations | |
enum class | RSResult { InProgress , Converged , PrecisionExceeded } |
enum class | SVIStage { Initial , y_less_1 , b_eq_d } |
Functions | |
template<typename ValueType > | |
boost::optional< std::vector< uint64_t > > | computeTopologicalGroupOrdering (storm::storage::SparseMatrix< ValueType > const &matrix) |
Returns a reordering of the matrix row(groups) and columns such that we can solve the (minmax or linear) equation system in one go. | |
template<typename ValueType > | |
storm::storage::SparseMatrix< ValueType > | createReorderedMatrix (storm::storage::SparseMatrix< ValueType > const &matrix, std::vector< uint64_t > const &newToOrigIndexMap, std::vector< std::pair< uint64_t, ValueType > > &bFactors) |
reorders the row group such that the i'th row of the new matrix corresponds to the order[i]'th row of the source matrix. | |
template<typename ValueType > | |
bool | checkConvergence (std::pair< std::vector< ValueType >, std::vector< ValueType > > const &xy, uint64_t &convergenceCheckState, std::function< void()> const &getNextConvergenceCheckState, bool relative, ValueType const &precision) |
template<bool Relative, typename ValueType > | |
static ValueType | diff (ValueType const &oldValue, ValueType const &newValue) |
template<bool Relative, typename ValueType > | |
void | guessCandidate (std::pair< std::vector< ValueType >, std::vector< ValueType > > &vu, ValueType const &guessValue, std::optional< ValueType > const &lowerBound, std::optional< ValueType > const &upperBound) |
|
strong |
Enumerator | |
---|---|
InProgress | |
Converged | |
PrecisionExceeded |
Definition at line 16 of file RationalSearchHelper.h.
|
strong |
Enumerator | |
---|---|
Initial | |
y_less_1 | |
b_eq_d |
Definition at line 29 of file SoundValueIterationHelper.cpp.
bool storm::solver::helper::checkConvergence | ( | std::pair< std::vector< ValueType >, std::vector< ValueType > > const & | xy, |
uint64_t & | convergenceCheckState, | ||
std::function< void()> const & | getNextConvergenceCheckState, | ||
bool | relative, | ||
ValueType const & | precision | ||
) |
Definition at line 57 of file IntervalterationHelper.cpp.
boost::optional< std::vector< uint64_t > > storm::solver::helper::computeTopologicalGroupOrdering | ( | storm::storage::SparseMatrix< ValueType > const & | matrix | ) |
Returns a reordering of the matrix row(groups) and columns such that we can solve the (minmax or linear) equation system in one go.
More precisely, let x be the result and i an arbitrary rowgroup index. Solving for rowgroup x[i] only requires knowledge of the result at rowgroups x[i+1], x[i+2], ...
Definition at line 20 of file AcyclicSolverHelper.h.
storm::storage::SparseMatrix< ValueType > storm::solver::helper::createReorderedMatrix | ( | storm::storage::SparseMatrix< ValueType > const & | matrix, |
std::vector< uint64_t > const & | newToOrigIndexMap, | ||
std::vector< std::pair< uint64_t, ValueType > > & | bFactors | ||
) |
reorders the row group such that the i'th row of the new matrix corresponds to the order[i]'th row of the source matrix.
Also eliminates selfloops p>0 and inserts 1/p into the bFactors
Definition at line 77 of file AcyclicSolverHelper.h.
|
static |
Definition at line 15 of file OptimisticValueIterationHelper.cpp.
void storm::solver::helper::guessCandidate | ( | std::pair< std::vector< ValueType >, std::vector< ValueType > > & | vu, |
ValueType const & | guessValue, | ||
std::optional< ValueType > const & | lowerBound, | ||
std::optional< ValueType > const & | upperBound | ||
) |
Definition at line 86 of file OptimisticValueIterationHelper.cpp.