Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ConditionalHelper.cpp File Reference
Include dependency graph for ConditionalHelper.cpp:

Go to the source code of this file.

Classes

struct  storm::modelchecker::internal::NormalFormData< ValueType >
 
class  storm::modelchecker::internal::WeightedReachabilityHelper< ValueType, SolutionType >
 A helper class that computes (weighted) reachability probabilities for a given MDP in normal form. More...
 

Namespaces

namespace  storm
 LabParser.cpp.
 
namespace  storm::modelchecker
 
namespace  storm::modelchecker::internal
 

Enumerations

enum class  storm::modelchecker::internal::BisectionMethodBounds { storm::modelchecker::internal::Simple , storm::modelchecker::internal::Advanced }
 

Functions

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={})
 
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)
 
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.
 
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)
 
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.
 
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)
 
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)
 
template<typename ValueType , typename SolutionType = ValueType>
std::optional< SolutionType > storm::modelchecker::internal::handleTrivialCases (uint64_t const initialState, NormalFormData< ValueType > const &normalForm)
 
template<typename ValueType , typename SolutionType >
std::unique_ptr< CheckResultstorm::modelchecker::computeConditionalProbabilities (Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)
 
template std::unique_ptr< CheckResultstorm::modelchecker::computeConditionalProbabilities (Environment const &env, storm::solver::SolveGoal< double > &&goal, storm::storage::SparseMatrix< double > const &transitionMatrix, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)
 
template std::unique_ptr< CheckResultstorm::modelchecker::computeConditionalProbabilities (Environment const &env, storm::solver::SolveGoal< storm::RationalNumber > &&goal, storm::storage::SparseMatrix< storm::RationalNumber > const &transitionMatrix, storm::storage::SparseMatrix< storm::RationalNumber > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)