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

Go to the source code of this file.

Namespaces

namespace  storm
 LabParser.cpp.
 
namespace  storm::modelchecker
 
namespace  storm::modelchecker::helper
 

Functions

template<typename ValueType >
void storm::modelchecker::helper::addSspMatrixChoice (uint64_t const &inputMatrixChoice, storm::storage::SparseMatrix< ValueType > const &inputTransitionMatrix, std::vector< uint64_t > const &inputToSspStateMap, uint64_t const &numberOfNonComponentStates, uint64_t const &currentSspChoice, storm::storage::SparseMatrixBuilder< ValueType > &sspMatrixBuilder)
 Auxiliary function that adds the entries of the Ssp Matrix for a single choice (i.e., row) Transitions that lead to a Component state will be redirected to a new auxiliary state (there is one aux.