Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::modelchecker::internal Namespace Reference

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)
 

Enumeration Type Documentation

◆ BisectionMethodBounds

Enumerator
Simple 
Advanced 

Definition at line 535 of file ConditionalHelper.cpp.

Function Documentation

◆ computeReachabilityProbabilities()

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

Note
This code is optimized for cases where not all states are reachable from the initial states.

Definition at line 112 of file ConditionalHelper.cpp.

◆ computeViaBisection()

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

◆ computeViaPolicyIteration()

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

◆ computeViaRestartMethod()

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

See also
doi.org/10.1007/978-3-642-54862-8_43

Definition at line 226 of file ConditionalHelper.cpp.

◆ eliminateEndComponents()

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

◆ handleTrivialCases()

template<typename ValueType , typename SolutionType = ValueType>
std::optional< SolutionType > storm::modelchecker::internal::handleTrivialCases ( uint64_t const  initialState,
NormalFormData< ValueType > const &  normalForm 
)

Definition at line 670 of file ConditionalHelper.cpp.

◆ obtainNormalForm()

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

◆ solveMinMaxEquationSystem()

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