diff --git a/src/storm/storage/MaximalEndComponent.cpp b/src/storm/storage/MaximalEndComponent.cpp index 58683a3df..aa7453277 100644 --- a/src/storm/storage/MaximalEndComponent.cpp +++ b/src/storm/storage/MaximalEndComponent.cpp @@ -1,4 +1,5 @@ #include "storm/storage/MaximalEndComponent.h" +#include "storm/storage/BitVector.h" #include "storm/exceptions/InvalidStateException.h" namespace storm { @@ -69,6 +70,16 @@ namespace storm { return true; } + bool MaximalEndComponent::containsAnyState(storm::storage::BitVector stateSet) const { + // TODO: iteration over unordered_map is potentially inefficient? + for (auto const& stateChoicesPair : stateToChoicesMapping) { + if (stateSet.get(stateChoicesPair.first)) { + return true; + } + } + return false; + } + void MaximalEndComponent::removeState(uint_fast64_t state) { auto stateChoicePair = stateToChoicesMapping.find(state); diff --git a/src/storm/storage/MaximalEndComponent.h b/src/storm/storage/MaximalEndComponent.h index b40da6455..a1d5b37c2 100644 --- a/src/storm/storage/MaximalEndComponent.h +++ b/src/storm/storage/MaximalEndComponent.h @@ -8,6 +8,8 @@ namespace storm { namespace storage { + // fwd + class BitVector; /*! * This class represents a maximal end-component of a nondeterministic model. @@ -106,6 +108,14 @@ namespace storm { */ bool containsState(uint_fast64_t state) const; + /*! + * Retrieves whether at least one of the given states is contained in this MEC. + * + * @param stateSet The states for which to query membership in the MEC. + * @return True if any of the given states is contained in the MEC. + */ + bool containsAnyState(storm::storage::BitVector stateSet) const; + /*! * Retrieves whether the given choice for the given state is contained in the MEC. *