#ifndef STORM_MODELS_SPARSE_NONDETERMINISTICMODEL_H_ #define STORM_MODELS_SPARSE_NONDETERMINISTICMODEL_H_ #include "src/models/sparse/Model.h" #include "src/utility/OsDetection.h" namespace storm { namespace models { namespace sparse { /*! * The base class of sparse nondeterministic models. */ template> class NondeterministicModel: public Model { public: /*! * Constructs a model from the given data. * * @param modelType The type of the model. * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling of the states. * @param rewardModels A mapping of reward model names to reward models. * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ NondeterministicModel(storm::models::ModelType const& modelType, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels = std::unordered_map(), boost::optional> const& optionalChoiceLabeling = boost::optional>()); /*! * Constructs a model by moving the given data. * * @param modelType The type of the model. * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling of the states. * @param rewardModels A mapping of reward model names to reward models. * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ NondeterministicModel(storm::models::ModelType const& modelType, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels = std::unordered_map(), boost::optional>&& optionalChoiceLabeling = boost::optional>()); NondeterministicModel(NondeterministicModel const& other) = default; NondeterministicModel& operator=(NondeterministicModel const& other) = default; #ifndef WINDOWS NondeterministicModel(NondeterministicModel&& other) = default; NondeterministicModel& operator=(NondeterministicModel&& other) = default; #endif /*! * Retrieves the number of (nondeterministic) choices in the model. * * @return The number of (nondeterministic) choices in the model. */ uint_fast64_t getNumberOfChoices() const; /*! * Retrieves the vector indicating which matrix rows represent non-deterministic choices of a certain state. * * @return The vector indicating which matrix rows represent non-deterministic choices of a certain state. */ std::vector const& getNondeterministicChoiceIndices() const; /*! * @param state State for which we want to know how many choices it has * * @return The number of non-deterministic choices for the given state */ uint_fast64_t getNumberOfChoices(uint_fast64_t state) const; virtual void reduceToStateBasedRewards() override; virtual void printModelInformationToStream(std::ostream& out) const; virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const; }; } // namespace sparse } // namespace models } // namespace storm #endif /* STORM_MODELS_SPARSE_NONDETERMINISTICMODEL_H_ */