Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Model.h
Go to the documentation of this file.
1#ifndef STORM_MODELS_SYMBOLIC_MODEL_H_
2#define STORM_MODELS_SYMBOLIC_MODEL_H_
3
4#include <memory>
5#include <set>
6#include <unordered_map>
7
15
16#include "storm-config.h"
18
19namespace storm {
20namespace dd {
21
22template<storm::dd::DdType Type>
23class Dd;
24
25template<storm::dd::DdType Type>
26class DdManager;
27
28} // namespace dd
29
30namespace adapters {
31template<storm::dd::DdType Type, typename ValueType>
32class AddExpressionAdapter;
33}
34
35namespace models {
36namespace symbolic {
37
38template<storm::dd::DdType Type, typename ValueType>
39class StandardRewardModel;
40
44template<storm::dd::DdType Type, typename CValueType = double>
45class Model : public storm::models::Model<CValueType> {
46 public:
47 typedef CValueType ValueType;
48
49 static const storm::dd::DdType DdType = Type;
51
53
54 Model(Model<Type, ValueType> const& other) = default;
55 Model& operator=(Model<Type, ValueType> const& other) = default;
56
57 Model(Model<Type, ValueType>&& other) = default;
59
77 Model(storm::models::ModelType const& modelType, std::shared_ptr<storm::dd::DdManager<Type>> manager, storm::dd::Bdd<Type> reachableStates,
79 std::set<storm::expressions::Variable> const& rowVariables,
80 std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
81 std::set<storm::expressions::Variable> const& columnVariables,
82 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
83 std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
84 std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
85
101 Model(storm::models::ModelType const& modelType, std::shared_ptr<storm::dd::DdManager<Type>> manager, storm::dd::Bdd<Type> reachableStates,
103 std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables,
104 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
105 std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap = std::map<std::string, storm::dd::Bdd<Type>>(),
106 std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
107
108 virtual uint_fast64_t getNumberOfStates() const override;
109
110 virtual uint_fast64_t getNumberOfTransitions() const override;
111
112 virtual uint_fast64_t getNumberOfChoices() const override;
113
120
126 std::shared_ptr<storm::dd::DdManager<Type>> const& getManagerAsSharedPointer() const;
127
134
141
142 /*
143 * Retrieves the deadlock states of the model.
144 */
146
153 virtual storm::dd::Bdd<Type> getStates(std::string const& label) const;
154
161 virtual storm::expressions::Expression getExpression(std::string const& label) const;
162
169 virtual storm::dd::Bdd<Type> getStates(storm::expressions::Expression const& expression) const;
170
177 virtual bool hasLabel(std::string const& label) const;
178
185
192
200 virtual storm::dd::Bdd<Type> getQualitativeTransitionMatrix(bool keepNondeterminism = true) const;
201
207 std::set<storm::expressions::Variable> const& getRowVariables() const;
208
214 std::set<storm::expressions::Variable> const& getColumnVariables() const;
215
221 std::set<storm::expressions::Variable> getRowAndNondeterminismVariables() const;
222
228 std::set<storm::expressions::Variable> getColumnAndNondeterminismVariables() const;
229
235 virtual std::set<storm::expressions::Variable> const& getNondeterminismVariables() const;
236
242 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& getRowColumnMetaVariablePairs() const;
243
250
256 virtual bool hasRewardModel(std::string const& rewardModelName) const override;
257
263 RewardModelType const& getRewardModel(std::string const& rewardModelName) const;
264
271
277 virtual std::string const& getUniqueRewardModelName() const override;
278
285
291 virtual bool hasUniqueRewardModel() const override;
292
298 bool hasRewardModel() const;
299
300 std::unordered_map<std::string, RewardModelType>& getRewardModels();
301 std::unordered_map<std::string, RewardModelType> const& getRewardModels() const;
302
308 uint_fast64_t getNumberOfRewardModels() const;
309
310 virtual void printModelInformationToStream(std::ostream& out) const override;
311
312 virtual bool isSymbolicModel() const override;
313
314 virtual std::optional<storm::dd::DdType> getDdType() const override;
315
316 virtual bool isExact() const override;
317
318 virtual bool supportsParameters() const override;
319
326 virtual bool hasParameters() const override;
327
328 std::vector<std::string> getLabels() const;
329
330 void addParameters(std::set<storm::RationalFunctionVariable> const& parameters);
331
332 std::set<storm::RationalFunctionVariable> const& getParameters() const;
333
334 template<typename NewValueType>
335 typename std::enable_if<!std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type toValueType() const;
336
337 template<typename NewValueType>
338 typename std::enable_if<std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type toValueType() const;
339
340 void writeDotToFile(std::string const& filename) const;
341
342 protected:
349
355 std::map<std::string, storm::expressions::Expression> const& getLabelToExpressionMap() const;
356
362 std::map<std::string, storm::dd::Bdd<Type>> const& getLabelToBddMap() const;
363
369 void printModelInformationHeaderToStream(std::ostream& out) const;
370
377 void printModelInformationFooterToStream(std::ostream& out) const;
378
384 void printRewardModelsInformationToStream(std::ostream& out) const;
385
391 virtual void printDdVariableInformationToStream(std::ostream& out) const;
392
393 protected:
399 std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> const& getRowExpressionAdapter() const;
400
401 private:
402 // The manager responsible for the decision diagrams.
403 std::shared_ptr<storm::dd::DdManager<Type>> manager;
404
405 // A vector representing the reachable states of the model.
406 storm::dd::Bdd<Type> reachableStates;
407
408 protected:
409 // A matrix representing transition relation.
411
412 private:
413 // The meta variables used to encode the rows of the transition matrix.
414 std::set<storm::expressions::Variable> rowVariables;
415
416 // An adapter that can translate expressions to DDs over the row meta variables.
417 std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter;
418
419 // The meta variables used to encode the columns of the transition matrix.
420 std::set<storm::expressions::Variable> columnVariables;
421
422 // A vector holding all pairs of row and column meta variable pairs. This is used to swap the variables
423 // in the DDs from row to column variables and vice versa.
424 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
425
426 // A mapping from labels to expressions defining them.
427 std::map<std::string, storm::expressions::Expression> labelToExpressionMap;
428
429 // A mapping from labels to BDDs characterizing the labeled states.
430 std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap;
431
432 // The reward models associated with the model.
433 std::unordered_map<std::string, RewardModelType> rewardModels;
434
435 // The parameters. Only meaningful for models over rational functions.
436 std::set<storm::RationalFunctionVariable> parameters;
437
438 // An empty variable set that can be used when references to non-existing sets need to be returned.
439 std::set<storm::expressions::Variable> emptyVariableSet;
440};
441
442} // namespace symbolic
443} // namespace models
444} // namespace storm
445
446#endif /* STORM_MODELS_SYMBOLIC_MODEL_H_ */
Definition DdTest.cpp:25
Base class for all symbolic models.
Definition Model.h:45
virtual bool hasParameters() const override
Checks whether the model has parameters.
Definition Model.cpp:417
storm::dd::DdManager< Type > & getManager() const
Retrieves the manager responsible for the DDs that represent this model.
Definition Model.cpp:92
RewardModelType const & getRewardModel(std::string const &rewardModelName) const
Retrieves the reward model with the given name, if one exists.
Definition Model.cpp:254
void addParameters(std::set< storm::RationalFunctionVariable > const &parameters)
Definition Model.cpp:432
storm::dd::Add< Type, ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:177
storm::dd::Bdd< Type > const & getDeadlockStates() const
Definition Model.cpp:112
virtual void printModelInformationToStream(std::ostream &out) const override
Prints information about the model to the specified stream.
Definition Model.cpp:313
virtual storm::expressions::Expression getExpression(std::string const &label) const
Returns the expression for the given label.
Definition Model.cpp:132
std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > > const & getRowExpressionAdapter() const
Retrieves the expression adapter of this model.
Definition Model.cpp:383
void writeDotToFile(std::string const &filename) const
Definition Model.cpp:408
Model & operator=(Model< Type, ValueType > &&other)=default
RewardModelType const & getUniqueRewardModel() const
Retrieves the unique reward model, if there exists exactly one.
Definition Model.cpp:272
virtual bool isSymbolicModel() const override
Checks whether the model is a symbolic model.
Definition Model.cpp:388
virtual void printDdVariableInformationToStream(std::ostream &out) const
Prints information about the DD variables to the specified stream.
Definition Model.cpp:368
virtual std::string const & getUniqueRewardModelName() const override
Retrieves the name of the unique reward model, if there exists exactly one.
Definition Model.cpp:279
virtual storm::dd::Bdd< Type > getQualitativeTransitionMatrix(bool keepNondeterminism=true) const
Retrieves the matrix qualitatively (i.e.
Definition Model.cpp:187
std::set< storm::expressions::Variable > const & getColumnVariables() const
Retrieves the meta variables used to encode the columns of the transition matrix and the vector indic...
Definition Model.cpp:197
std::shared_ptr< storm::dd::DdManager< Type > > const & getManagerAsSharedPointer() const
Retrieves the manager responsible for the DDs that represent this model.
Definition Model.cpp:97
Model(Model< Type, ValueType > &&other)=default
Model & operator=(Model< Type, ValueType > const &other)=default
uint_fast64_t getNumberOfRewardModels() const
Retrieves the number of reward models associated with this model.
Model(Model< Type, ValueType > const &other)=default
std::enable_if<!std::is_same< ValueType, NewValueType >::value, std::shared_ptr< Model< Type, NewValueType > > >::type toValueType() const
Definition Model.cpp:453
std::vector< std::string > getLabels() const
Definition Model.cpp:319
storm::dd::Add< Type, ValueType > getRowColumnIdentity() const
Retrieves an ADD that represents the diagonal of the transition matrix.
Definition Model.cpp:243
static const storm::models::ModelRepresentation Representation
Definition Model.h:52
void printRewardModelsInformationToStream(std::ostream &out) const
Prints information about the reward models to the specified stream.
Definition Model.cpp:350
virtual bool isExact() const override
Checks whether the model is exact.
Definition Model.cpp:398
virtual bool supportsParameters() const override
Checks whether the model supports parameters.
Definition Model.cpp:403
std::map< std::string, storm::dd::Bdd< Type > > const & getLabelToBddMap() const
Retrieves the mapping of labels to their defining expressions.
Definition Model.cpp:238
std::set< storm::RationalFunctionVariable > const & getParameters() const
Definition Model.cpp:437
storm::dd::Bdd< Type > const & getInitialStates() const
Retrieves the initial states of the model.
Definition Model.cpp:107
storm::dd::Add< Type, ValueType > transitionMatrix
Definition Model.h:410
virtual std::set< storm::expressions::Variable > const & getNondeterminismVariables() const
Retrieves all meta variables used to encode the nondeterminism.
Definition Model.cpp:218
void printModelInformationFooterToStream(std::ostream &out) const
Prints the information footer (reward models, labels) of the model to the specified stream.
Definition Model.cpp:336
std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const & getRowColumnMetaVariablePairs() const
Retrieves the pairs of row and column meta variables.
Definition Model.cpp:223
std::set< storm::expressions::Variable > const & getRowVariables() const
Retrieves the meta variables used to encode the rows of the transition matrix and the vector indices.
Definition Model.cpp:192
static const storm::dd::DdType DdType
Definition Model.h:49
virtual bool hasLabel(std::string const &label) const
Retrieves whether the given label is a valid label in this model.
Definition Model.cpp:162
std::map< std::string, storm::expressions::Expression > const & getLabelToExpressionMap() const
Retrieves the mapping of labels to their defining expressions.
Definition Model.cpp:233
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:328
std::unordered_map< std::string, RewardModelType > & getRewardModels()
Definition Model.cpp:303
virtual uint_fast64_t getNumberOfChoices() const override
Returns the number of choices ine the model.
Definition Model.cpp:87
std::set< storm::expressions::Variable > getRowAndNondeterminismVariables() const
Retrieves all meta variables used to encode rows and nondetermism.
Definition Model.cpp:202
void setTransitionMatrix(storm::dd::Add< Type, ValueType > const &transitionMatrix)
Sets the transition matrix of the model.
Definition Model.cpp:228
std::set< storm::expressions::Variable > getColumnAndNondeterminismVariables() const
Retrieves all meta variables used to encode columns and nondetermism.
Definition Model.cpp:210
virtual storm::dd::Bdd< Type > getStates(std::string const &label) const
Returns the sets of states labeled with the given label.
Definition Model.cpp:117
virtual uint_fast64_t getNumberOfTransitions() const override
Returns the number of (non-zero) transitions of the model.
Definition Model.cpp:82
std::enable_if< std::is_same< ValueType, NewValueType >::value, std::shared_ptr< Model< Type, NewValueType > > >::type toValueType() const
StandardRewardModel< Type, ValueType > RewardModelType
Definition Model.h:50
bool hasRewardModel() const
Retrieves whether the model has at least one reward model.
Definition Model.cpp:298
virtual bool hasUniqueRewardModel() const override
Retrieves whether the model has a unique reward model.
Definition Model.cpp:293
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
Definition Model.cpp:102
virtual uint_fast64_t getNumberOfStates() const override
Returns the number of states of the model.
Definition Model.cpp:77
virtual std::optional< storm::dd::DdType > getDdType() const override
Definition Model.cpp:393
LabParser.cpp.