diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index 31dbaf699..1810ffdec 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -39,6 +39,12 @@ namespace storm { return this->getTransitionMatrix().getRowGroupIndices(); } + template + uint_fast64_t getNumberOfChoices(uint_fast64_t state) const { + auto indices = this->getNondetermininisticChoiceIndices(); + return indices[state+1] - indices[state]; + } + template void NondeterministicModel::printModelInformationToStream(std::ostream& out) const { out << "-------------------------------------------------------------- " << std::endl; diff --git a/src/models/sparse/NondeterministicModel.h b/src/models/sparse/NondeterministicModel.h index 87d77111b..9151c2145 100644 --- a/src/models/sparse/NondeterministicModel.h +++ b/src/models/sparse/NondeterministicModel.h @@ -66,10 +66,17 @@ namespace storm { /*! * Retrieves the vector indicating which matrix rows represent non-deterministic choices of a certain state. * - * @param 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 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;