diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 48428d7cc..3aa121a0a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -37,13 +37,13 @@ file(GLOB STORM_SOLVER_STATEELIMINATION_FILES ${PROJECT_SOURCE_DIR}/src/solver/s file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp) file(GLOB STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) +file(GLOB STORM_STORAGE_DFT_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/*.h ${PROJECT_SOURCE_DIR}/src/storage/dft/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_CUDD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_SYLVAN_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.cpp) file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp) file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) -file(GLOB_RECURSE STORM_STORAGE_DFT_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp) # Additional include files like the storm-config.h diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index 67dec3dc4..0b80608cf 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -49,7 +49,7 @@ namespace storm { size_t newIndex = 0; public: - ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft), mStates(((mDft.stateSize() / 64) + 1) * 64, std::pow(2, mDft.nrBasicElements())) { + ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, std::pow(2, mDft.nrBasicElements())) { // stateSize is bound for size of bitvector // 2^nrBE is upper bound for state space } diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 5735af2a7..9506b29a5 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -10,13 +10,12 @@ namespace storm { namespace storage { template - DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0) + DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mTopLevelIndex(tle->id()), mNrOfBEs(0), mNrOfSpares(0) { assert(elementIndicesCorrect()); - - size_t stateIndex = 0; mUsageInfoBits = storm::utility::math::uint64_log2(mElements.size()-1)+1; - + size_t stateIndex = 0; + for (auto& elem : mElements) { mIdToFailureIndex.push_back(stateIndex); stateIndex += 2; @@ -25,6 +24,7 @@ namespace storm { } else if (elem->isSpareGate()) { ++mNrOfSpares; + bool firstChild = true; for(auto const& spareReprs : std::static_pointer_cast>(elem)->children()) { if(mActivationIndex.count(spareReprs->id()) == 0) { mActivationIndex[spareReprs->id()] = stateIndex++; @@ -32,11 +32,9 @@ namespace storm { std::set module = {spareReprs->id()}; spareReprs->extendSpareModule(module); std::vector sparesAndBes; - bool secondSpare = false; - for(auto const& modelem : module) { - if (mElements[modelem]->isSpareGate()) { - STORM_LOG_THROW(!secondSpare, storm::exceptions::NotSupportedException, "Module for '" << spareReprs->name() << "' contains more than one spare."); - secondSpare = true; + for(size_t modelem : module) { + if (spareReprs->id() != modelem && (isRepresentative(modelem) || (!firstChild && mTopLevelIndex == modelem))) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Module for '" << spareReprs->name() << "' contains more than one representative."); } if(mElements[modelem]->isSpareGate() || mElements[modelem]->isBasicElement()) { sparesAndBes.push_back(modelem); @@ -44,7 +42,7 @@ namespace storm { } } mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes)); - + firstChild = false; } std::static_pointer_cast>(elem)->setUseIndex(stateIndex); mUsageIndex.insert(std::make_pair(elem->id(), stateIndex)); @@ -71,8 +69,8 @@ namespace storm { } mTopModule = std::vector(topModuleSet.begin(), topModuleSet.end()); - mStateSize = stateIndex; - mTopLevelIndex = tle->id(); + mStateVectorSize = stateIndex; + } } diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index f2036e7d7..ca860d074 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -53,7 +53,7 @@ namespace storm { size_t mNrOfSpares; size_t mTopLevelIndex; size_t mUsageInfoBits; - size_t mStateSize; + size_t mStateVectorSize; std::map mActivationIndex; std::map> mSpareModules; std::vector mDependencies; @@ -65,8 +65,8 @@ namespace storm { public: DFT(DFTElementVector const& elements, DFTElementPointer const& tle); - size_t stateSize() const { - return mStateSize; + size_t stateVectorSize() const { + return mStateVectorSize; } size_t nrElements() const { @@ -198,6 +198,15 @@ namespace storm { } return elements; } + + bool isRepresentative(size_t id) const { + for (auto const& parent : getElement(id)->parents()) { + if (parent->isSpareGate()) { + return true; + } + } + return false; + } bool hasRepresentant(size_t id) const { return mRepresentants.find(id) != mRepresentants.end(); diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 9916bbe0e..7e8429fdd 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -6,13 +6,12 @@ namespace storm { namespace storage { template - DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft) { + DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft) { mInactiveSpares = dft.getSpareIndices(); dft.initializeUses(*this); dft.initializeActivation(*this); std::vector alwaysActiveBEs = dft.nonColdBEs(); mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); - } template