13namespace modelchecker {
21template<
typename ValueType>
102 std::vector<ValueType>
const& initialValues)
const;
108 bool isContinuousTime()
const;
113 void createBackwardTransitions();
123 void createNonBsccStateVector();
149 void processSingletonScc(uint64_t sccState, std::vector<ValueType>& stateValues)
const;
156 std::vector<ValueType>
const& stateValues)
const;
162 std::unique_ptr<storm::storage::SparseMatrix<ValueType>> computedBackwardTransitions;
165 std::unique_ptr<storm::storage::StronglyConnectedComponentDecomposition<ValueType>> computedSccDecomposition;
Helper class that optionally holds a reference to an object of type T.
Helper for model checking queries where we are interested in (optimizing) a single value per state.
Helper class for computing for each state the expected number of times to visit that state assuming a...
std::vector< ValueType > computeExpectedVisitingTimes(Environment const &env, storm::storage::BitVector const &initialStates)
Computes for each state the expected number of times we are visiting that state assuming the given in...
void provideSCCDecomposition(storm::storage::StronglyConnectedComponentDecomposition< ValueType > const &decomposition)
Provides the decomposition into SCCs that can be used during the computation.
void provideBackwardTransitions(storm::storage::SparseMatrix< ValueType > const &backwardTransitions)
Provides the backward transitions that can be used during the computation.
std::function< ValueType(uint64_t)> ValueGetter
Function mapping from indices to values.
A bit vector that is internally represented as a vector of 64-bit values.
A class that holds a possibly non-square matrix in the compressed row storage format.
This class represents the decomposition of a graph-like structure into its strongly connected compone...