From a212cce8c126bcaf7f16b9a7d8e7cbac22fe7db8 Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 24 Jul 2015 12:22:39 +0200 Subject: [PATCH] Added a method to get the number of choices for a specific state. Former-commit-id: 1ced589a95f7d182d46e3e2cfd62193ce144a6d9 --- src/models/sparse/NondeterministicModel.cpp | 6 ++++++ src/models/sparse/NondeterministicModel.h | 9 ++++++++- 2 files changed, 14 insertions(+), 1 deletion(-) 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;