From dd17955a3e752f219a2d432d8f5d71b564ff29e0 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Mon, 1 Feb 2016 18:36:43 +0100
Subject: [PATCH] Added functionality to BitVectorHashMap

Former-commit-id: 0d1fa18d16f5a5c9459de99d7516e24a04654961
---
 src/storage/BitVectorHashMap.cpp | 5 +++++
 src/storage/BitVectorHashMap.h   | 8 ++++++++
 src/storage/dft/DFTState.cpp     | 2 +-
 src/storage/dft/DFTState.h       | 6 +++---
 4 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp
index c184b764b..9237dfde3 100644
--- a/src/storage/BitVectorHashMap.cpp
+++ b/src/storage/BitVectorHashMap.cpp
@@ -168,6 +168,11 @@ namespace storm {
             return values[flagBucketPair.second];
         }
         
+        template<class ValueType, class Hash1, class Hash2>
+        bool BitVectorHashMap<ValueType, Hash1, Hash2>::contains(storm::storage::BitVector const& key) const {
+            return findBucket(key).first;
+        }
+
         template<class ValueType, class Hash1, class Hash2>
         typename BitVectorHashMap<ValueType, Hash1, Hash2>::const_iterator BitVectorHashMap<ValueType, Hash1, Hash2>::begin() const {
             return const_iterator(*this, occupied.begin());
diff --git a/src/storage/BitVectorHashMap.h b/src/storage/BitVectorHashMap.h
index 3b0c7aa70..d50dac59e 100644
--- a/src/storage/BitVectorHashMap.h
+++ b/src/storage/BitVectorHashMap.h
@@ -95,6 +95,14 @@ namespace storm {
              */
             ValueType getValue(storm::storage::BitVector const& key) const;
             
+            /*!
+             * Checks if the given key is already contained in the map.
+             *
+             * @param key The key to search
+             * @return True if the key is already contained in the map
+             */
+            bool contains(storm::storage::BitVector const& key) const;
+
             /*!
              * Retrieves an iterator to the elements of the map.
              *
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index e6e410760..ebf3c770b 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -123,7 +123,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        bool DFTState<ValueType>::isUsed(size_t child) {
+        bool DFTState<ValueType>::isUsed(size_t child) const {
             return (std::find(mUsedRepresentants.begin(), mUsedRepresentants.end(), child) != mUsedRepresentants.end());
         }
 
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index b084e1a82..4ea11a991 100644
--- a/src/storage/dft/DFTState.h
+++ b/src/storage/dft/DFTState.h
@@ -61,7 +61,7 @@ namespace storm {
                 mValid = false;
             }
            
-            bool isInvalid() {
+            bool isInvalid() const {
                 return !mValid;
             }
             
@@ -88,7 +88,7 @@ namespace storm {
              * @param child The id of the child for which we want to know whether it is currently used.
              * @return true iff it is currently used by any of the spares.
              */
-            bool isUsed(size_t child);
+            bool isUsed(size_t child) const;
             
             /**
              * Sets to to the usageIndex which child is now used.
@@ -114,7 +114,7 @@ namespace storm {
              */
             std::pair<std::shared_ptr<DFTBE<ValueType>>, bool> letNextBEFail(size_t smallestIndex = 0);
             
-            std::string getCurrentlyFailableString() {
+            std::string getCurrentlyFailableString() const {
                 std::stringstream stream;
                 auto it = mIsCurrentlyFailableBE.begin();
                 stream << "{";