Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseDeterministicVisitingTimesHelper.h
Go to the documentation of this file.
1#pragma once
2#include <vector>
3
9
10namespace storm {
11class Environment;
12
13namespace modelchecker {
14namespace helper {
15
21template<typename ValueType>
22class SparseDeterministicVisitingTimesHelper : public SingleValueModelCheckerHelper<ValueType, storm::models::ModelRepresentation::Sparse> {
23 public:
27 typedef std::function<ValueType(uint64_t)> ValueGetter;
28
33
37 SparseDeterministicVisitingTimesHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates);
38
45
56
64 std::vector<ValueType> computeExpectedVisitingTimes(Environment const& env, storm::storage::BitVector const& initialStates);
65
71 std::vector<ValueType> computeExpectedVisitingTimes(Environment const& env, uint64_t initialState);
72
78 std::vector<ValueType> computeExpectedVisitingTimes(Environment const& env, ValueGetter const& initialStateValueGetter);
79
86 void computeExpectedVisitingTimes(Environment const& env, std::vector<ValueType>& stateValues);
87
101 std::vector<ValueType> computeExpectedVisitingTimes(Environment const& env, storm::storage::BitVector const& subsystem,
102 std::vector<ValueType> const& initialValues) const;
103
104 private:
108 bool isContinuousTime() const;
109
113 void createBackwardTransitions();
114
118 void createDecomposition(Environment const& env);
119
123 void createNonBsccStateVector();
124
131 std::vector<ValueType> computeUpperBounds(storm::storage::BitVector const& stateSetAsBitVector) const;
132
139 storm::Environment getEnvironmentForSolver(storm::Environment const& env, bool topological = false) const;
140
144 storm::Environment getEnvironmentForTopologicalSolver(storm::Environment const& env) const;
145
149 void processSingletonScc(uint64_t sccState, std::vector<ValueType>& stateValues) const;
150
155 std::vector<ValueType> computeValueForStateSet(storm::Environment const& env, storm::storage::BitVector const& stateSetAsBitVector,
156 std::vector<ValueType> const& stateValues) const;
157
158 storm::storage::SparseMatrix<ValueType> const& transitionMatrix;
160
162 std::unique_ptr<storm::storage::SparseMatrix<ValueType>> computedBackwardTransitions;
163
165 std::unique_ptr<storm::storage::StronglyConnectedComponentDecomposition<ValueType>> computedSccDecomposition;
166
167 storm::storage::BitVector nonBsccStates;
168};
169
170} // namespace helper
171} // namespace modelchecker
172} // namespace storm
Helper class that optionally holds a reference to an object of type T.
Definition OptionalRef.h:48
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.
Definition BitVector.h:18
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...
LabParser.cpp.
Definition cli.cpp:18