Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MarkovAutomaton.h
Go to the documentation of this file.
1#ifndef STORM_MODELS_SPARSE_MARKOVAUTOMATON_H_
2#define STORM_MODELS_SPARSE_MARKOVAUTOMATON_H_
3
6
7namespace storm {
8namespace models {
9namespace sparse {
10
14template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
15class MarkovAutomaton : public NondeterministicModel<ValueType, RewardModelType> {
16 public:
30 storm::storage::BitVector const& markovianStates,
31 std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
32
46 storm::storage::BitVector&& markovianStates,
47 std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>());
48
56
59
62
68 bool isClosed() const;
69
76 bool containsZenoCycle() const;
77
85
93
101
107 std::vector<ValueType> const& getExitRates() const;
108
114 std::vector<ValueType>& getExitRates();
115
123
130
137
141 void close();
142
146 bool isConvertibleToCtmc() const;
147
148 bool hasOnlyTrivialNondeterminism() const;
149
155 std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> convertToCtmc() const;
156
157 virtual void printModelInformationToStream(std::ostream& out) const override;
158
159 private:
166 void turnRatesToProbabilities();
167
171 bool checkIsClosed() const;
172
178 bool checkContainsZenoCycle() const;
179
180 // A bit vector representing the set of Markovian states.
181 storm::storage::BitVector markovianStates;
182
183 // A vector storing the exit rates of all states of the model.
184 std::vector<ValueType> exitRates;
185
186 // A flag indicating whether the Markov automaton has been closed, which is typically a prerequisite for model checking.
187 bool closed;
188
189 // A flag indicating whether the Markov automaton contains Zeno cycles.
190 mutable boost::optional<bool> hasZenoCycle;
191};
192
193} // namespace sparse
194} // namespace models
195} // namespace storm
196
197#endif /* STORM_MODELS_SPARSE_MARKOVAUTOMATON_H_ */
This class represents a Markov automaton.
void close()
Closes the Markov automaton.
bool containsZenoCycle() const
Retrieves whether the Markov automaton contains Zeno cycles.
bool isClosed() const
Retrieves whether the Markov automaton is closed.
std::shared_ptr< storm::models::sparse::Ctmc< ValueType, RewardModelType > > convertToCtmc() const
Convert the MA to a CTMC.
MarkovAutomaton & operator=(MarkovAutomaton< ValueType, RewardModelType > &&other)=default
bool isProbabilisticState(storm::storage::sparse::state_type state) const
Retrieves whether the given state is a probabilistic state.
MarkovAutomaton & operator=(MarkovAutomaton< ValueType, RewardModelType > const &other)=default
bool isMarkovianState(storm::storage::sparse::state_type state) const
Retrieves whether the given state is a Markovian state.
bool isConvertibleToCtmc() const
Determines whether the Markov automaton can be converted to a CTMC without changing any measures.
virtual void printModelInformationToStream(std::ostream &out) const override
Prints information about the model to the specified stream.
std::vector< ValueType > const & getExitRates() const
Retrieves the vector representing the exit rates of the states.
storm::storage::BitVector const & getMarkovianStates() const
Retrieves the set of Markovian states of the model.
ValueType const & getExitRate(storm::storage::sparse::state_type state) const
Retrieves the exit rate of the given state.
ValueType getMaximalExitRate() const
Retrieves the maximal exit rate over all states of the model.
MarkovAutomaton(MarkovAutomaton< ValueType, RewardModelType > const &other)=default
MarkovAutomaton(MarkovAutomaton< ValueType, RewardModelType > &&other)=default
bool isHybridState(storm::storage::sparse::state_type state) const
Retrieves whether the given state is a hybrid state, i.e.
The base class of sparse nondeterministic models.
This class manages the labeling of the state space with a number of (atomic) labels.
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
A class that holds a possibly non-square matrix in the compressed row storage format.
LabParser.cpp.