Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
storm::solver::helper Namespace Reference

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)
 

Enumeration Type Documentation

◆ RSResult

Enumerator
InProgress 
Converged 
PrecisionExceeded 

Definition at line 16 of file RationalSearchHelper.h.

◆ SVIStage

Enumerator
Initial 
y_less_1 
b_eq_d 

Definition at line 29 of file SoundValueIterationHelper.cpp.

Function Documentation

◆ checkConvergence()

template<typename ValueType >
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.

◆ computeTopologicalGroupOrdering()

template<typename ValueType >
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.

◆ createReorderedMatrix()

template<typename ValueType >
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.

◆ diff()

template<bool Relative, typename ValueType >
static ValueType storm::solver::helper::diff ( ValueType const &  oldValue,
ValueType const &  newValue 
)
static

Definition at line 15 of file OptimisticValueIterationHelper.cpp.

◆ guessCandidate()

template<bool Relative, typename ValueType >
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.