Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Model.h
Go to the documentation of this file.
1#pragma once
2
3#include <optional>
4#include <unordered_map>
5#include <vector>
6
16
17namespace storm {
18namespace storage {
19class BitVector;
20}
21
22namespace models {
23namespace sparse {
24
25template<typename ValueType>
26class StandardRewardModel;
27
31template<class CValueType, class CRewardModelType = StandardRewardModel<CValueType>>
32class Model : public storm::models::Model<CValueType> {
33 public:
34 typedef CValueType ValueType;
35 typedef CRewardModelType RewardModelType;
37
40
49
50 virtual ~Model() = default;
51
59
67
73 virtual uint_fast64_t getNumberOfStates() const override;
74
80 virtual uint_fast64_t getNumberOfTransitions() const override;
81
87 virtual uint_fast64_t getNumberOfChoices() const override;
88
95
102
109 storm::storage::BitVector const& getStates(std::string const& label) const;
110
117 bool hasLabel(std::string const& label) const;
118
125
132
138 std::unordered_map<std::string, RewardModelType> const& getRewardModels() const;
139
145 std::unordered_map<std::string, RewardModelType>& getRewardModels();
146
152 virtual bool hasRewardModel(std::string const& rewardModelName) const override;
153
159 RewardModelType const& getRewardModel(std::string const& rewardModelName) const;
160
166 RewardModelType& getRewardModel(std::string const& rewardModelName);
167
174
181
187 virtual bool hasUniqueRewardModel() const override;
188
194 virtual std::string const& getUniqueRewardModelName() const override;
195
201 bool hasRewardModel() const;
202
208 uint_fast64_t getNumberOfRewardModels() const;
209
215 void addRewardModel(std::string const& rewardModelName, RewardModelType const& rewModel);
216
221 bool removeRewardModel(std::string const& rewardModelName);
222
226 void restrictRewardModels(std::set<std::string> const& keptRewardModels);
227
234
241
247 bool hasChoiceLabeling() const;
248
256
262 std::optional<storm::models::sparse::ChoiceLabeling> const& getOptionalChoiceLabeling() const;
263
269 std::optional<storm::models::sparse::ChoiceLabeling>& getOptionalChoiceLabeling();
270
276 bool hasStateValuations() const;
277
285
291 std::optional<storm::storage::sparse::StateValuations> const& getOptionalStateValuations() const;
292
298 std::optional<storm::storage::sparse::StateValuations>& getOptionalStateValuations();
299
305 bool hasChoiceOrigins() const;
306
313 std::shared_ptr<storm::storage::sparse::ChoiceOrigins> const& getChoiceOrigins() const;
314
320 std::optional<std::shared_ptr<storm::storage::sparse::ChoiceOrigins>> const& getOptionalChoiceOrigins() const;
321
327 std::optional<std::shared_ptr<storm::storage::sparse::ChoiceOrigins>>& getOptionalChoiceOrigins();
328
334 virtual void printModelInformationToStream(std::ostream& out) const override;
335
336 bool isSinkState(uint64_t sink) const;
337
352 virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, bool includeLabeling = true,
353 storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr,
354 std::vector<ValueType> const* secondValue = nullptr, std::vector<uint64_t> const* stateColoring = nullptr,
355 std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr,
356 bool finalizeOutput = true) const;
357
361 virtual void writeJsonToStream(std::ostream& outStream) const;
362
369 std::set<std::string> getLabelsOfState(storm::storage::sparse::state_type state) const;
370
371 virtual bool isSparseModel() const override;
372
373 virtual bool supportsParameters() const override;
374
381 virtual bool hasParameters() const override;
382
383 virtual bool isExact() const override;
384
391 virtual bool supportsUncertainty() const override;
392
400 virtual bool hasUncertainty() const;
401
402 virtual std::size_t hash() const;
403
404 protected:
405 RewardModelType& rewardModel(std::string const& rewardModelName);
412
419
425 void printModelInformationHeaderToStream(std::ostream& out) const;
426
433 void printModelInformationFooterToStream(std::ostream& out) const;
434
440 void printRewardModelsInformationToStream(std::ostream& out) const;
441
447 virtual std::string additionalDotStateInfo(uint64_t state) const;
448
449 private:
450 // Upon construction of a model, this function asserts that the specified components are valid
451 void assertValidityOfComponents(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components) const;
452
453 // A matrix representing transition relation.
455
456 // The labeling of the states.
458
459 // The reward models of the model.
460 std::unordered_map<std::string, RewardModelType> rewardModels;
461
462 // If set, a vector representing the labels of choices.
463 std::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling;
464
465 // if set, retrieves for each state the variable valuation that this state represents
466 std::optional<storm::storage::sparse::StateValuations> stateValuations;
467
468 // if set, gives information about where each choice originates w.r.t. the input model description
469 std::optional<std::shared_ptr<storm::storage::sparse::ChoiceOrigins>> choiceOrigins;
470};
471
477std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model);
478
484std::set<storm::RationalFunctionVariable> getRewardParameters(Model<storm::RationalFunction> const& model);
485
491std::set<storm::RationalFunctionVariable> getRateParameters(Model<storm::RationalFunction> const& model);
492
498std::set<storm::RationalFunctionVariable> getAllParameters(Model<storm::RationalFunction> const& model);
499} // namespace sparse
500} // namespace models
501} // namespace storm
This class manages the labeling of the choice space with a number of (atomic) labels.
Base class for all sparse models.
Definition Model.h:32
storm::models::sparse::ChoiceLabeling const & getChoiceLabeling() const
Retrieves the labels for the choices of the model.
Definition Model.cpp:334
RewardModelType const & getUniqueRewardModel() const
Retrieves the unique reward model, if there exists exactly one.
Definition Model.cpp:303
bool hasRewardModel() const
Retrieves whether the model has at least one reward model.
Definition Model.cpp:298
storm::storage::SparseMatrix< ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:197
virtual std::size_t hash() const
Definition Model.cpp:395
virtual bool hasUncertainty() const
Checks whether the model actually is uncertain, i.e., whether there is a non-singleton transition rel...
Definition Model.cpp:674
Model(Model< ValueType, RewardModelType > const &other)=default
void setInitialStates(storm::storage::BitVector const &states)
Overwrites the initial states of the model.
Definition Model.cpp:182
virtual bool supportsUncertainty() const override
Does it support uncertainty (e.g., via interval-valued entries).
Definition Model.cpp:654
void setTransitionMatrix(storm::storage::SparseMatrix< ValueType > const &transitionMatrix)
Sets the transition matrix of the model.
Definition Model.cpp:621
void printModelInformationFooterToStream(std::ostream &out) const
Prints the information footer (reward models, labels and size in memory) of the model to the specifie...
Definition Model.cpp:423
virtual void printModelInformationToStream(std::ostream &out) const override
Prints information about the model to the specified stream.
Definition Model.cpp:389
Model & operator=(Model< ValueType, RewardModelType > const &other)=default
std::unordered_map< std::string, RewardModelType > const & getRewardModels() const
Retrieves the reward models.
Definition Model.cpp:699
void restrictRewardModels(std::set< std::string > const &keptRewardModels)
Removes all reward models whose name is not in the given set.
Definition Model.cpp:274
bool hasStateValuations() const
Retrieves whether this model was build with state valuations.
Definition Model.cpp:349
storm::storage::BitVector const & getStates(std::string const &label) const
Returns the sets of states labeled with the given label.
Definition Model.cpp:187
bool removeRewardModel(std::string const &rewardModelName)
Removes the reward model with the given name from the model.
Definition Model.cpp:264
void printRewardModelsInformationToStream(std::ostream &out) const
Prints information about the reward models to the specified stream.
Definition Model.cpp:437
std::set< std::string > getLabelsOfState(storm::storage::sparse::state_type state) const
Retrieves the set of labels attached to the given state.
Definition Model.cpp:616
std::optional< std::shared_ptr< storm::storage::sparse::ChoiceOrigins > > const & getOptionalChoiceOrigins() const
Retrieves an optional value that contains the choice origins if there are some.
Definition Model.cpp:379
RewardModelType & rewardModel(std::string const &rewardModelName)
Definition Model.cpp:212
virtual uint_fast64_t getNumberOfChoices() const override
Returns the number of choices ine the model.
Definition Model.cpp:172
storm::storage::sparse::StateValuations const & getStateValuations() const
Retrieves the valuations of the states of the model.
Definition Model.cpp:354
virtual bool isSparseModel() const override
Checks whether the model is a sparse model.
Definition Model.cpp:644
void addRewardModel(std::string const &rewardModelName, RewardModelType const &rewModel)
Adds a reward model to the model.
Definition Model.cpp:254
virtual storm::storage::SparseMatrix< ValueType >::const_rows getRows(storm::storage::sparse::state_type state) const
Returns an object representing the matrix rows associated with the given state.
Definition Model.cpp:157
std::shared_ptr< storm::storage::sparse::ChoiceOrigins > const & getChoiceOrigins() const
Retrieves the origins of the choices of the model.
Definition Model.cpp:374
storm::storage::SparseMatrix< ValueType > getBackwardTransitions() const
Retrieves the backward transition relation of the model, i.e.
Definition Model.cpp:152
bool isSinkState(uint64_t sink) const
Definition Model.cpp:631
bool hasChoiceLabeling() const
Retrieves whether this model has a labeling of the choices.
Definition Model.cpp:329
uint_fast64_t getNumberOfRewardModels() const
Retrieves the number of reward models associated with this model.
Definition Model.cpp:315
virtual ~Model()=default
storm::models::sparse::StateLabeling const & getStateLabeling() const
Returns the state labeling associated with this model.
Definition Model.cpp:319
static const storm::models::ModelRepresentation Representation
Definition Model.h:36
virtual void writeJsonToStream(std::ostream &outStream) const
Writes a JSON representation of the model to the given stream.
Definition Model.cpp:523
void printModelInformationHeaderToStream(std::ostream &out) const
Prints the information header (number of states and transitions) of the model to the specified stream...
Definition Model.cpp:415
std::optional< storm::models::sparse::ChoiceLabeling > const & getOptionalChoiceLabeling() const
Retrieves an optional value that contains the choice labeling if there is one.
Definition Model.cpp:339
CRewardModelType RewardModelType
Definition Model.h:35
virtual bool supportsParameters() const override
Checks whether the model supports parameters.
Definition Model.cpp:649
virtual bool hasUniqueRewardModel() const override
Retrieves whether the model has a unique reward model.
Definition Model.cpp:287
virtual void writeDotToStream(std::ostream &outStream, size_t maxWidthLabel=30, bool includeLabeling=true, storm::storage::BitVector const *subsystem=nullptr, std::vector< ValueType > const *firstValue=nullptr, std::vector< ValueType > const *secondValue=nullptr, std::vector< uint64_t > const *stateColoring=nullptr, std::vector< std::string > const *colors=nullptr, std::vector< uint_fast64_t > *scheduler=nullptr, bool finalizeOutput=true) const
Exports the model to the dot-format and prints the result to the given stream.
virtual std::string additionalDotStateInfo(uint64_t state) const
Return a string that is additonally added to the state information in the dot stream.
Definition Model.cpp:611
std::optional< storm::storage::sparse::StateValuations > const & getOptionalStateValuations() const
Retrieves an optional value that contains the state valuations if there are some.
Definition Model.cpp:359
virtual uint_fast64_t getNumberOfTransitions() const override
Returns the number of (non-zero) transitions of the model.
Definition Model.cpp:167
virtual bool isExact() const override
Checks whether the model is exact.
Definition Model.cpp:689
bool hasChoiceOrigins() const
Retrieves whether this model was build with choice origins.
Definition Model.cpp:369
virtual bool hasParameters() const override
Checks whether the model has parameters.
Definition Model.cpp:659
virtual uint_fast64_t getNumberOfStates() const override
Returns the number of states of the model.
Definition Model.cpp:162
bool hasLabel(std::string const &label) const
Retrieves whether the given label is a valid label in this model.
Definition Model.cpp:192
RewardModelType const & getRewardModel(std::string const &rewardModelName) const
Retrieves the reward model with the given name, if one exists.
Definition Model.cpp:218
virtual std::string const & getUniqueRewardModelName() const override
Retrieves the name of the unique reward model, if there exists exactly one.
Definition Model.cpp:292
storm::storage::BitVector const & getInitialStates() const
Retrieves the initial states of the model.
Definition Model.cpp:177
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
This class represents a number of consecutive rows of the matrix.
A class that holds a possibly non-square matrix in the compressed row storage format.
std::set< storm::RationalFunctionVariable > getRateParameters(Model< storm::RationalFunction > const &model)
Get all parameters occurring in rates.
Definition Model.cpp:716
std::set< storm::RationalFunctionVariable > getRewardParameters(Model< storm::RationalFunction > const &model)
Get all parameters occurring in rewards.
Definition Model.cpp:707
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
Definition Model.cpp:703
std::set< storm::RationalFunctionVariable > getAllParameters(Model< storm::RationalFunction > const &model)
Get all parameters (probability, rewards, and rates) occurring in the model.
Definition Model.cpp:728
storage::BitVector BitVector
LabParser.cpp.