1#ifndef STORM_MODELS_SYMBOLIC_MODEL_H_
2#define STORM_MODELS_SYMBOLIC_MODEL_H_
6#include <unordered_map>
16#include "storm-config.h"
22template<storm::dd::DdType Type>
25template<storm::dd::DdType Type>
31template<storm::dd::DdType Type,
typename ValueType>
32class AddExpressionAdapter;
38template<storm::dd::DdType Type,
typename ValueType>
39class StandardRewardModel;
44template<storm::dd::DdType Type,
typename CValueType =
double>
79 std::set<storm::expressions::Variable>
const& rowVariables,
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>());
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,
106 std::unordered_map<std::string, RewardModelType>
const& rewardModels = std::unordered_map<std::string, RewardModelType>());
177 virtual bool hasLabel(std::string
const& label)
const;
256 virtual bool hasRewardModel(std::string
const& rewardModelName)
const override;
301 std::unordered_map<std::string, RewardModelType>
const&
getRewardModels()
const;
314 virtual std::optional<storm::dd::DdType>
getDdType()
const override;
316 virtual bool isExact()
const override;
328 std::vector<std::string>
getLabels()
const;
330 void addParameters(std::set<storm::RationalFunctionVariable>
const& parameters);
332 std::set<storm::RationalFunctionVariable>
const&
getParameters()
const;
334 template<
typename NewValueType>
335 typename std::enable_if<!std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type
toValueType()
const;
337 template<
typename NewValueType>
338 typename std::enable_if<std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type
toValueType()
const;
362 std::map<std::string, storm::dd::Bdd<Type>>
const&
getLabelToBddMap()
const;
399 std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>>
const&
getRowExpressionAdapter()
const;
403 std::shared_ptr<storm::dd::DdManager<Type>> manager;
414 std::set<storm::expressions::Variable> rowVariables;
417 std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter;
420 std::set<storm::expressions::Variable> columnVariables;
424 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
427 std::map<std::string, storm::expressions::Expression> labelToExpressionMap;
430 std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap;
433 std::unordered_map<std::string, RewardModelType> rewardModels;
436 std::set<storm::RationalFunctionVariable> parameters;
439 std::set<storm::expressions::Variable> emptyVariableSet;
Base class for all symbolic models.
virtual bool hasParameters() const override
Checks whether the model has parameters.
storm::dd::DdManager< Type > & getManager() const
Retrieves the manager responsible for the DDs that represent this model.
RewardModelType const & getRewardModel(std::string const &rewardModelName) const
Retrieves the reward model with the given name, if one exists.
void addParameters(std::set< storm::RationalFunctionVariable > const ¶meters)
storm::dd::Add< Type, ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
storm::dd::Bdd< Type > const & getDeadlockStates() const
virtual void printModelInformationToStream(std::ostream &out) const override
Prints information about the model to the specified stream.
virtual storm::expressions::Expression getExpression(std::string const &label) const
Returns the expression for the given label.
std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > > const & getRowExpressionAdapter() const
Retrieves the expression adapter of this model.
void writeDotToFile(std::string const &filename) const
Model & operator=(Model< Type, ValueType > &&other)=default
RewardModelType const & getUniqueRewardModel() const
Retrieves the unique reward model, if there exists exactly one.
virtual bool isSymbolicModel() const override
Checks whether the model is a symbolic model.
virtual void printDdVariableInformationToStream(std::ostream &out) const
Prints information about the DD variables to the specified stream.
virtual std::string const & getUniqueRewardModelName() const override
Retrieves the name of the unique reward model, if there exists exactly one.
virtual storm::dd::Bdd< Type > getQualitativeTransitionMatrix(bool keepNondeterminism=true) const
Retrieves the matrix qualitatively (i.e.
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...
std::shared_ptr< storm::dd::DdManager< Type > > const & getManagerAsSharedPointer() const
Retrieves the manager responsible for the DDs that represent this model.
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
std::vector< std::string > getLabels() const
storm::dd::Add< Type, ValueType > getRowColumnIdentity() const
Retrieves an ADD that represents the diagonal of the transition matrix.
static const storm::models::ModelRepresentation Representation
void printRewardModelsInformationToStream(std::ostream &out) const
Prints information about the reward models to the specified stream.
virtual bool isExact() const override
Checks whether the model is exact.
virtual bool supportsParameters() const override
Checks whether the model supports parameters.
std::map< std::string, storm::dd::Bdd< Type > > const & getLabelToBddMap() const
Retrieves the mapping of labels to their defining expressions.
std::set< storm::RationalFunctionVariable > const & getParameters() const
storm::dd::Bdd< Type > const & getInitialStates() const
Retrieves the initial states of the model.
storm::dd::Add< Type, ValueType > transitionMatrix
virtual std::set< storm::expressions::Variable > const & getNondeterminismVariables() const
Retrieves all meta variables used to encode the nondeterminism.
void printModelInformationFooterToStream(std::ostream &out) const
Prints the information footer (reward models, labels) of the model to the specified stream.
std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const & getRowColumnMetaVariablePairs() const
Retrieves the pairs of row and column meta variables.
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.
static const storm::dd::DdType DdType
virtual bool hasLabel(std::string const &label) const
Retrieves whether the given label is a valid label in this model.
std::map< std::string, storm::expressions::Expression > const & getLabelToExpressionMap() const
Retrieves the mapping of labels to their defining expressions.
void printModelInformationHeaderToStream(std::ostream &out) const
Prints the information header (number of states and transitions) of the model to the specified stream...
std::unordered_map< std::string, RewardModelType > & getRewardModels()
virtual uint_fast64_t getNumberOfChoices() const override
Returns the number of choices ine the model.
std::set< storm::expressions::Variable > getRowAndNondeterminismVariables() const
Retrieves all meta variables used to encode rows and nondetermism.
void setTransitionMatrix(storm::dd::Add< Type, ValueType > const &transitionMatrix)
Sets the transition matrix of the model.
std::set< storm::expressions::Variable > getColumnAndNondeterminismVariables() const
Retrieves all meta variables used to encode columns and nondetermism.
virtual storm::dd::Bdd< Type > getStates(std::string const &label) const
Returns the sets of states labeled with the given label.
virtual uint_fast64_t getNumberOfTransitions() const override
Returns the number of (non-zero) transitions of the model.
std::enable_if< std::is_same< ValueType, NewValueType >::value, std::shared_ptr< Model< Type, NewValueType > > >::type toValueType() const
StandardRewardModel< Type, ValueType > RewardModelType
bool hasRewardModel() const
Retrieves whether the model has at least one reward model.
virtual bool hasUniqueRewardModel() const override
Retrieves whether the model has a unique reward model.
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
virtual uint_fast64_t getNumberOfStates() const override
Returns the number of states of the model.
virtual std::optional< storm::dd::DdType > getDdType() const override