Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NondeterministicModel.h
Go to the documentation of this file.
1#ifndef STORM_MODELS_SYMBOLIC_NONDETERMINISTICMODEL_H_
2#define STORM_MODELS_SYMBOLIC_NONDETERMINISTICMODEL_H_
3
5
6namespace storm {
7namespace models {
8namespace symbolic {
9
13template<storm::dd::DdType Type, typename ValueType = double>
14class NondeterministicModel : public Model<Type, ValueType> {
15 public:
17
20
23
42 NondeterministicModel(storm::models::ModelType const& modelType, std::shared_ptr<storm::dd::DdManager<Type>> manager, storm::dd::Bdd<Type> reachableStates,
44 std::set<storm::expressions::Variable> const& rowVariables,
45 std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
46 std::set<storm::expressions::Variable> const& columnVariables,
47 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
48 std::set<storm::expressions::Variable> const& nondeterminismVariables,
49 std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
50 std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
51
68 NondeterministicModel(storm::models::ModelType const& modelType, std::shared_ptr<storm::dd::DdManager<Type>> manager, storm::dd::Bdd<Type> reachableStates,
70 std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables,
71 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
72 std::set<storm::expressions::Variable> const& nondeterminismVariables,
73 std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap = std::map<std::string, storm::dd::Bdd<Type>>(),
74 std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
75
81 virtual uint_fast64_t getNumberOfChoices() const override;
82
88 virtual std::set<storm::expressions::Variable> const& getNondeterminismVariables() const override;
89
96
103
111 virtual storm::dd::Bdd<Type> getQualitativeTransitionMatrix(bool keepNondeterminism = true) const override;
112
113 virtual void printModelInformationToStream(std::ostream& out) const override;
114
115 virtual void reduceToStateBasedRewards() override;
116
117 protected:
118 virtual void printDdVariableInformationToStream(std::ostream& out) const override;
119
120 // A mask that characterizes all illegal nondeterministic choices.
122
123 private:
124 void createIllegalMask();
125
126 // The meta variables encoding the nondeterminism in the model.
127 std::set<storm::expressions::Variable> nondeterminismVariables;
128};
129
130} // namespace symbolic
131} // namespace models
132} // namespace storm
133
134#endif /* STORM_MODELS_SYMBOLIC_NONDETERMINISTICMODEL_H_ */
Base class for all symbolic models.
Definition Model.h:45
storm::dd::Add< Type, ValueType > transitionMatrix
Definition Model.h:410
Base class for all nondeterministic symbolic models.
NondeterministicModel(NondeterministicModel< Type, ValueType > &&other)=default
virtual uint_fast64_t getNumberOfChoices() const override
Retrieves the number of nondeterministic choices in the model.
virtual std::set< storm::expressions::Variable > const & getNondeterminismVariables() const override
Retrieves the meta variables used to encode the nondeterminism in the model.
virtual void printModelInformationToStream(std::ostream &out) const override
Prints information about the model to the specified stream.
Model< Type, ValueType >::RewardModelType RewardModelType
storm::dd::Bdd< Type > const & getIllegalMask() const
Retrieves a BDD characterizing all illegal nondeterminism encodings in the model.
storm::dd::Bdd< Type > getIllegalSuccessorMask() const
Retrieves a BDD characterizing the illegal successors for each choice.
NondeterministicModel & operator=(NondeterministicModel< Type, ValueType > const &other)=default
NondeterministicModel & operator=(NondeterministicModel< Type, ValueType > &&other)=default
virtual void reduceToStateBasedRewards() override
Converts the transition rewards of all reward models to state-based rewards.
virtual void printDdVariableInformationToStream(std::ostream &out) const override
Prints information about the DD variables to the specified stream.
NondeterministicModel(NondeterministicModel< Type, ValueType > const &other)=default
virtual storm::dd::Bdd< Type > getQualitativeTransitionMatrix(bool keepNondeterminism=true) const override
Retrieves the matrix qualitatively (i.e.
LabParser.cpp.