From c099183063d14a38f727aa9e44b554c8f3f988cc Mon Sep 17 00:00:00 2001
From: Joachim Klein <joachim.klein@automata.tools>
Date: Mon, 24 Aug 2020 22:25:14 +0200
Subject: [PATCH] (MDP-LTL) MaximalEndComponent: containsAnyState

 Conflicts:
	src/storm/storage/MaximalEndComponent.cpp
---
 src/storm/storage/MaximalEndComponent.cpp | 11 +++++++++++
 src/storm/storage/MaximalEndComponent.h   | 10 ++++++++++
 2 files changed, 21 insertions(+)

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.
              *