#ifndef STORM_MODELS_SPARSE_NONDETERMINISTICMODEL_H_ #define STORM_MODELS_SPARSE_NONDETERMINISTICMODEL_H_ #include "storm/models/sparse/Model.h" #include "storm/storage/StateActionPair.h" namespace storm { // Forward declare Scheduler class. namespace storage { template class Scheduler; } 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 this model * @param components The components for this model. */ NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents const& components); NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents&& components); /*! * 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; using Model::getNumberOfChoices; /*! * @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; /*! * For a state/action pair, get the choice index referring to the state-action pair. */ uint_fast64_t getChoiceIndex(storm::storage::StateActionPair const& stateactPair) const; /*! * Applies the given scheduler to this model. * @param scheduler the considered scheduler. * @param dropUnreachableStates if set, the resulting model only considers the states that are reachable from an initial state */ std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates = true) const; virtual void printModelInformationToStream(std::ostream& out) const override; virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, 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 override; }; } // namespace sparse } // namespace models } // namespace storm #endif /* STORM_MODELS_SPARSE_NONDETERMINISTICMODEL_H_ */