work towards const correctness and additional methods

Former-commit-id: 2c4667412c

src/builder/ExplicitDFTModelBuilder.cpp

@@ -137,8 +137,8 @@ namespace storm {
 
                     // Construct new state as copy from original one
                     DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
-                    std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType>>, bool> nextBEPair = newState->letNextBEFail(smallest++);
-                    std::shared_ptr<storm::storage::DFTBE<ValueType>> nextBE = nextBEPair.first;
+                    std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(smallest++);
+                    std::shared_ptr<storm::storage::DFTBE<ValueType> const>& nextBE = nextBEPair.first;
                     assert(nextBE);
                     assert(nextBEPair.second == hasDependencies);
                     STORM_LOG_TRACE("with the failure of: " << nextBE->name() << " [" << nextBE->id() << "]");
@@ -192,7 +192,7 @@ namespace storm {
                         // Set failure rate according to usage
                         bool isUsed = true;
                         if (mDft.hasRepresentant(nextBE->id())) {
-                            DFTElementPointer representant = mDft.getRepresentant(nextBE->id());
+                            DFTElementCPointer representant = mDft.getRepresentant(nextBE->id());
                             // Used must be checked for the state we are coming from as this state is responsible for the
                             // rate and not the new state we are going to
                             isUsed = state->isUsed(representant->id());

src/builder/ExplicitDFTModelBuilder.h

@@ -20,6 +20,7 @@ namespace storm {
         class ExplicitDFTModelBuilder {
 
             using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
+            using DFTElementCPointer = std::shared_ptr<storm::storage::DFTElement<ValueType> const>;
             using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
             using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
 

src/storage/dft/DFT.cpp

@@ -148,11 +148,10 @@ namespace storm {
         }
 
         template <typename ValueType>
-        bool DFT<ValueType>::rootOfClosedSubDFT(size_t index) const {
-            //boost::container::flat_set<size_t> marked;
-            //DFTElementPointer elem = getElement(index);
-
-
+        std::vector<size_t> DFT<ValueType>::getIndependentSubDftRoots(size_t index) const {
+            auto elem = getElement(index);
+            auto ISD = elem->independentSubDft();
+            return ISD;
         }
 
         // Explicitly instantiate the class.

src/storage/dft/DFT.h

@@ -9,7 +9,6 @@
 
 #include <boost/iterator/counting_iterator.hpp>
 
-#include "DFTIsomorphism.h"
 #include "DFTElements.h"
 #include "../BitVector.h"
 
@@ -37,6 +36,7 @@ namespace storm {
         class DFT {
 
             using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
+            using DFTElementCPointer = std::shared_ptr<DFTElement<ValueType> const>;
             using DFTElementVector = std::vector<DFTElementPointer>;
             using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
             using DFTGateVector = std::vector<DFTGatePointer>;
@@ -148,15 +148,40 @@ namespace storm {
              *  Get a pointer to an element in the DFT
              *  @param index The id of the element
              */
-            DFTElementPointer const& getElement(size_t index) const {
+            DFTElementCPointer getElement(size_t index) const {
                 assert(index < nrElements());
                 return mElements[index];
             }
 
-            std::shared_ptr<DFTBE<ValueType>> getBasicElement(size_t index) const {
-                assert(index < nrElements());
-                assert(mElements[index]->isBasicElement());
-                return std::static_pointer_cast<DFTBE<ValueType>>(mElements[index]);
+            bool isBasicElement(size_t index) const {
+                return getElement(index)->isBasicElement();
+            }
+
+            bool isGate(size_t index) const {
+                return getElement(index)->isGate();
+            }
+
+            bool isDependency(size_t index) const {
+                return getElement(index)->isDependency();
+            }
+
+//            std::shared_ptr<DFTGate<ValueType> const> getGate(size_t index) const {
+//                return
+//            }
+
+            std::shared_ptr<DFTBE<ValueType> const> getBasicElement(size_t index) const {
+                assert(isBasicElement(index));
+                return std::static_pointer_cast<DFTBE<ValueType> const>(mElements[index]);
+            }
+
+            std::shared_ptr<DFTGate<ValueType> const> getGate(size_t index) const {
+                assert(isGate(index));
+                return std::static_pointer_cast<DFTGate<ValueType> const>(mElements[index]);
+            }
+
+            std::shared_ptr<DFTDependency<ValueType> const> getDependency(size_t index) const {
+                assert(isDependency(index));
+                return std::static_pointer_cast<DFTDependency<ValueType> const>(mElements[index]);
             }
 
             std::vector<std::shared_ptr<DFTBE<ValueType>>> getBasicElements() const {
@@ -173,7 +198,7 @@ namespace storm {
                 return mRepresentants.find(id) != mRepresentants.end();
             }
 
-            DFTElementPointer getRepresentant(size_t id) const {
+            DFTElementCPointer getRepresentant(size_t id) const {
                 assert(hasRepresentant(id));
                 return getElement(mRepresentants.find(id)->second);
             }
@@ -196,7 +221,7 @@ namespace storm {
 
             std::string getStateString(DFTStatePointer const& state) const;
 
-            bool rootOfClosedSubDFT(size_t id) const;
+            std::vector<size_t> getIndependentSubDftRoots(size_t index) const;
         private:
             bool elementIndicesCorrect() const {
                 for(size_t i = 0; i < mElements.size(); ++i) {

src/storage/dft/DFTState.cpp

@@ -82,7 +82,7 @@ namespace storm {
         bool DFTState<ValueType>::updateFailableDependencies(size_t id) {
             assert(hasFailed(id));
             for (size_t i = 0; i < mDft.getDependencies().size(); ++i) {
-                std::shared_ptr<DFTDependency<ValueType>> dependency = std::static_pointer_cast<DFTDependency<ValueType>>(mDft.getElement(mDft.getDependencies()[i]));
+                std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(mDft.getDependencies()[i]);
                 if (dependency->triggerEvent()->id() == id) {
                     if (!hasFailed(dependency->dependentEvent()->id())) {
                         mFailableDependencies.push_back(dependency->id());
@@ -94,21 +94,21 @@ namespace storm {
         }
 
         template<typename ValueType>
-        std::pair<std::shared_ptr<DFTBE<ValueType>>, bool> DFTState<ValueType>::letNextBEFail(size_t index)
+        std::pair<std::shared_ptr<DFTBE<ValueType> const>, bool> DFTState<ValueType>::letNextBEFail(size_t index)
         {
             STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString());
             if (nrFailableDependencies() > 0) {
                 // Consider failure due to dependency
                 assert(index < nrFailableDependencies());
-                std::shared_ptr<DFTDependency<ValueType>> dependency = std::static_pointer_cast<DFTDependency<ValueType>>(mDft.getElement(mFailableDependencies[index]));
-                std::pair<std::shared_ptr<DFTBE<ValueType>>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true);
+                std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(mFailableDependencies[index]);
+                std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true);
                 mFailableDependencies.erase(mFailableDependencies.begin() + index);
                 setFailed(res.first->id());
                 return res;
             } else {
                 // Consider "normal" failure
                 assert(index < nrFailableBEs());
-                std::pair<std::shared_ptr<DFTBE<ValueType>>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
+                std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
                 mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
                 setFailed(res.first->id());
                 return res;

src/storage/dft/DFTState.h

@@ -127,7 +127,7 @@ namespace storm {
              * @param smallestIndex Index in currentlyFailableBE of BE to fail
              * @return Pair of BE which fails and flag indicating if the failure was due to functional dependencies
              */
-            std::pair<std::shared_ptr<DFTBE<ValueType>>, bool> letNextBEFail(size_t smallestIndex = 0);
+            std::pair<std::shared_ptr<DFTBE<ValueType> const>, bool> letNextBEFail(size_t smallestIndex = 0);
             
             std::string getCurrentlyFailableString() const {
                 std::stringstream stream;