diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 817295346..084b5fe7a 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -137,8 +137,8 @@ namespace storm { // Construct new state as copy from original one DFTStatePointer newState = std::make_shared>(*state); - std::pair>, bool> nextBEPair = newState->letNextBEFail(smallest++); - std::shared_ptr> nextBE = nextBEPair.first; + std::pair const>, bool> nextBEPair = newState->letNextBEFail(smallest++); + std::shared_ptr 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()); diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index 6125b6fa1..67dec3dc4 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -20,6 +20,7 @@ namespace storm { class ExplicitDFTModelBuilder { using DFTElementPointer = std::shared_ptr>; + using DFTElementCPointer = std::shared_ptr const>; using DFTGatePointer = std::shared_ptr>; using DFTStatePointer = std::shared_ptr>; diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 319a08925..b3f0dce7a 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -148,11 +148,10 @@ namespace storm { } template - bool DFT::rootOfClosedSubDFT(size_t index) const { - //boost::container::flat_set marked; - //DFTElementPointer elem = getElement(index); - - + std::vector DFT::getIndependentSubDftRoots(size_t index) const { + auto elem = getElement(index); + auto ISD = elem->independentSubDft(); + return ISD; } // Explicitly instantiate the class. diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 92f1c0531..ecea467e4 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -9,7 +9,6 @@ #include -#include "DFTIsomorphism.h" #include "DFTElements.h" #include "../BitVector.h" @@ -37,6 +36,7 @@ namespace storm { class DFT { using DFTElementPointer = std::shared_ptr>; + using DFTElementCPointer = std::shared_ptr const>; using DFTElementVector = std::vector; using DFTGatePointer = std::shared_ptr>; using DFTGateVector = std::vector; @@ -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> getBasicElement(size_t index) const { - assert(index < nrElements()); - assert(mElements[index]->isBasicElement()); - return std::static_pointer_cast>(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 const> getGate(size_t index) const { +// return +// } + + std::shared_ptr const> getBasicElement(size_t index) const { + assert(isBasicElement(index)); + return std::static_pointer_cast const>(mElements[index]); + } + + std::shared_ptr const> getGate(size_t index) const { + assert(isGate(index)); + return std::static_pointer_cast const>(mElements[index]); + } + + std::shared_ptr const> getDependency(size_t index) const { + assert(isDependency(index)); + return std::static_pointer_cast const>(mElements[index]); } std::vector>> 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 getIndependentSubDftRoots(size_t index) const; private: bool elementIndicesCorrect() const { for(size_t i = 0; i < mElements.size(); ++i) { diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 17bb4aee8..672ca14a7 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -82,7 +82,7 @@ namespace storm { bool DFTState::updateFailableDependencies(size_t id) { assert(hasFailed(id)); for (size_t i = 0; i < mDft.getDependencies().size(); ++i) { - std::shared_ptr> dependency = std::static_pointer_cast>(mDft.getElement(mDft.getDependencies()[i])); + std::shared_ptr 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 - std::pair>, bool> DFTState::letNextBEFail(size_t index) + std::pair const>, bool> DFTState::letNextBEFail(size_t index) { STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); if (nrFailableDependencies() > 0) { // Consider failure due to dependency assert(index < nrFailableDependencies()); - std::shared_ptr> dependency = std::static_pointer_cast>(mDft.getElement(mFailableDependencies[index])); - std::pair>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true); + std::shared_ptr const> dependency = mDft.getDependency(mFailableDependencies[index]); + std::pair 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>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false); + std::pair const>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false); mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index); setFailed(res.first->id()); return res; diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index a1bab2583..17a9c2d3b 100644 --- a/src/storage/dft/DFTState.h +++ b/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>, bool> letNextBEFail(size_t smallestIndex = 0); + std::pair const>, bool> letNextBEFail(size_t smallestIndex = 0); std::string getCurrentlyFailableString() const { std::stringstream stream;