#ifndef STORM_MODELS_SYMBOLIC_DETERMINISTICMODEL_H_ #define STORM_MODELS_SYMBOLIC_DETERMINISTICMODEL_H_ #include "src/models/symbolic/Model.h" #include "src/utility/OsDetection.h" namespace storm { namespace models { namespace symbolic { /*! * Base class for all deterministic symbolic models. */ template class DeterministicModel : public Model { public: DeterministicModel(DeterministicModel const& other) = default; DeterministicModel& operator=(DeterministicModel const& other) = default; #ifndef WINDOWS DeterministicModel(DeterministicModel&& other) = default; DeterministicModel& operator=(DeterministicModel&& other) = default; #endif /*! * Constructs a model from the given data. * * @param modelType The type of the model. * @param manager The manager responsible for the decision diagrams. * @param reachableStates A DD representing the reachable states. * @param initialStates A DD representing the initial states of the model. * @param transitionMatrix The matrix representing the transitions in the model. * @param rowVariables The set of row meta variables used in the DDs. * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row * meta variables. * @param columVariables The set of column meta variables used in the DDs. * @param columnExpressionAdapter An object that can be used to translate expressions in terms of the * column meta variables. * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. * @param labelToExpressionMap A mapping from label names to their defining expressions. * @param optionalStateRewardVector The reward values associated with the states. * @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. */ DeterministicModel(storm::models::ModelType const& modelType, std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), boost::optional> const& optionalStateRewardVector = boost::optional>(), boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); }; } // namespace symbolic } // namespace models } // namespace storm #endif /* STORM_MODELS_SYMBOLIC_DETERMINISTICMODEL_H_ */