diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index bbfe99dd6..c8825fff1 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -60,10 +60,23 @@ namespace storm { //size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); //size_t currentFailable = 0; state->getFailableElements().init(exploreDependencies); + + // Check whether operational relevant event remains + bool remainingRelevantEvent = true; + if (mDft.hasFailed(state)) { + remainingRelevantEvent = false; + // Toplevel has failed already -> check for possible other relevant events + for (auto const& event : mDft.getRelevantEvents()) { + if (state->isOperational(event)) { + remainingRelevantEvent = true; + break; + } + } + } // Check for absorbing state: // - either no relevant event remains (i.e., all relevant events have failed already), or // - no BE can fail - if (!state->getFailableElements().hasRemainingRelevantEvent() || state->getFailableElements().isEnd()) { + if (!remainingRelevantEvent || state->getFailableElements().isEnd()) { Choice choice(0, true); // Add self loop choice.addProbability(state->getId(), storm::utility::one()); @@ -122,8 +135,6 @@ namespace storm { newState->updateFailableInRestrictions(next->id()); } - newState->updateRemainingRelevantEvents(); - bool transient = false; if (nextBE->type() == storm::storage::DFTElementType::BE_EXP) { auto beExp = std::static_pointer_cast const>(nextBE); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 927343ebc..5132813d8 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -17,7 +17,8 @@ namespace storm { namespace storage { template - DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mNrRepresentatives(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) { + DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mNrRepresentatives(0), + mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) { // Check that ids correspond to indices in the element vector STORM_LOG_ASSERT(elementIndicesCorrect(), "Ids incorrect."); @@ -25,19 +26,20 @@ namespace storm { if (isRepresentative(elem->id())) { ++mNrRepresentatives; } - if(elem->isBasicElement()) { + if (elem->isBasicElement()) { ++mNrOfBEs; } else if (elem->isSpareGate()) { // Build spare modules by setting representatives and representants ++mNrOfSpares; mMaxSpareChildCount = std::max(mMaxSpareChildCount, std::static_pointer_cast>(elem)->children().size()); - for(auto const& spareReprs : std::static_pointer_cast>(elem)->children()) { - STORM_LOG_THROW(spareReprs->isGate() || spareReprs->isBasicElement(), storm::exceptions::WrongFormatException, "Child '" << spareReprs->name() << "' of spare '" << elem->name() << "' must be gate or BE."); + for (auto const& spareReprs : std::static_pointer_cast>(elem)->children()) { + STORM_LOG_THROW(spareReprs->isGate() || spareReprs->isBasicElement(), storm::exceptions::WrongFormatException, + "Child '" << spareReprs->name() << "' of spare '" << elem->name() << "' must be gate or BE."); std::set module = {spareReprs->id()}; spareReprs->extendSpareModule(module); std::vector sparesAndBes; - for(size_t modelem : module) { - if(mElements[modelem]->isSpareGate() || mElements[modelem]->isBasicElement()) { + for (size_t modelem : module) { + if (mElements[modelem]->isSpareGate() || mElements[modelem]->isBasicElement()) { sparesAndBes.push_back(modelem); mRepresentants.insert(std::make_pair(modelem, spareReprs->id())); } @@ -52,14 +54,14 @@ namespace storm { // For the top module, we assume, contrary to [Jun15], that we have all spare gates and basic elements which are not in another module. std::set topModuleSet; // Initialize with all ids. - for(auto const& elem : mElements) { + for (auto const& elem : mElements) { if (elem->isBasicElement() || elem->isSpareGate()) { topModuleSet.insert(elem->id()); } } // Erase spare modules - for(auto const& module : mSpareModules) { - for(auto const& index : module.second) { + for (auto const& module : mSpareModules) { + for (auto const& index : module.second) { topModuleSet.erase(index); } } @@ -72,7 +74,8 @@ namespace storm { if (!mTopModule.empty()) { for (auto& module : mSpareModules) { if (std::find(module.second.begin(), module.second.end(), mTopModule.front()) != module.second.end()) { - STORM_LOG_WARN("Elements of spare module '" << getElement(module.first)->name() << "' also contained in top module. All elements of this spare module will be activated from the beginning on."); + STORM_LOG_WARN("Elements of spare module '" << getElement(module.first)->name() + << "' also contained in top module. All elements of this spare module will be activated from the beginning on."); module.second.clear(); } } @@ -86,10 +89,10 @@ namespace storm { template DFTStateGenerationInfo DFT::buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const { DFTStateGenerationInfo generationInfo(nrElements(), mNrOfSpares, mNrRepresentatives, mMaxSpareChildCount); - + // Generate Pre and Post info for restrictions, and mutexes - for(auto const& elem : mElements) { - if(!elem->isDependency() && !elem->isRestriction()) { + for (auto const& elem : mElements) { + if (!elem->isDependency() && !elem->isRestriction()) { generationInfo.setRestrictionPreElements(elem->id(), elem->seqRestrictionPres()); generationInfo.setRestrictionPostElements(elem->id(), elem->seqRestrictionPosts()); generationInfo.setMutexElements(elem->id(), elem->mutexRestrictionElements()); @@ -121,7 +124,7 @@ namespace storm { } } size_t offset = stateIndex - groupIndex; - + // Mirror symmetries size_t noSymmetricElements = symmetryGroup.front().size(); STORM_LOG_ASSERT(noSymmetricElements > 1, "No symmetry available."); @@ -141,7 +144,7 @@ namespace storm { size_t index = generationInfo.getStateIndex(originalElement); size_t activationIndex = isRepresentative(originalElement) ? generationInfo.getSpareActivationIndex(originalElement) : 0; size_t usageIndex = mElements[originalElement]->isSpareGate() ? generationInfo.getSpareUsageIndex(originalElement) : 0; - + // Mirror symmetry for each element for (size_t i = 1; i < symmetricElements.size(); ++i) { size_t symmetricElement = symmetricElements[i]; @@ -179,7 +182,8 @@ namespace storm { std::shared_ptr const> dependency = getDependency(idDependency); visitQueue.push(dependency->id()); visitQueue.push(dependency->triggerEvent()->id()); - STORM_LOG_THROW(dependency->dependentEvents().size() == 1, storm::exceptions::NotSupportedException, "Direct state generation does not support n-ary dependencies. Consider rewriting them by setting the binary dependency flag."); + STORM_LOG_THROW(dependency->dependentEvents().size() == 1, storm::exceptions::NotSupportedException, + "Direct state generation does not support n-ary dependencies. Consider rewriting them by setting the binary dependency flag."); visitQueue.push(dependency->dependentEvents()[0]->id()); } stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); @@ -191,7 +195,7 @@ namespace storm { stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); } } - + generationInfo.generateSymmetries(symmetries); STORM_LOG_TRACE(generationInfo); @@ -201,31 +205,32 @@ namespace storm { return generationInfo; } - + template size_t DFT::generateStateInfo(DFTStateGenerationInfo& generationInfo, size_t id, storm::storage::BitVector& visited, size_t stateIndex) const { STORM_LOG_ASSERT(!visited[id], "Element already visited."); visited.set(id); - + // Reserve bits for element generationInfo.addStateIndex(id, stateIndex); stateIndex += 2; - + if (isRepresentative(id)) { generationInfo.addSpareActivationIndex(id, stateIndex); ++stateIndex; } - + if (mElements[id]->isSpareGate()) { generationInfo.addSpareUsageIndex(id, stateIndex); stateIndex += generationInfo.usageInfoBits(); } - + return stateIndex; } - + template - size_t DFT::performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue& visitQueue, storm::storage::BitVector& visited, size_t stateIndex) const { + size_t DFT::performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue& visitQueue, storm::storage::BitVector& visited, + size_t stateIndex) const { while (!visitQueue.empty()) { size_t id = visitQueue.front(); visitQueue.pop(); @@ -234,7 +239,7 @@ namespace storm { continue; } stateIndex = generateStateInfo(generationInfo, id, visited, stateIndex); - + // Insert children if (mElements[id]->isGate()) { for (auto const& child : std::static_pointer_cast>(mElements[id])->children()) { @@ -244,15 +249,15 @@ namespace storm { } return stateIndex; } - + template - std::vector> DFT::topModularisation() const { + std::vector> DFT::topModularisation() const { STORM_LOG_ASSERT(isGate(mTopLevelIndex), "Top level element is no gate."); auto const& children = getGate(mTopLevelIndex)->children(); std::map> subdfts; - for(auto const& child : children) { + for (auto const& child : children) { std::vector isubdft; - if(child->nrParents() > 1 || child->hasOutgoingDependencies() || child->hasRestrictions()) { + if (child->nrParents() > 1 || child->hasOutgoingDependencies() || child->hasRestrictions()) { STORM_LOG_TRACE("child " << child->name() << " does not allow modularisation."); return {*this}; } @@ -260,40 +265,40 @@ namespace storm { isubdft = getGate(child->id())->independentSubDft(false); } else { STORM_LOG_ASSERT(isBasicElement(child->id()), "Child is no BE."); - if(getBasicElement(child->id())->hasIngoingDependencies()) { + if (getBasicElement(child->id())->hasIngoingDependencies()) { STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); return {*this}; } else { isubdft = {child->id()}; } - + } - if(isubdft.empty()) { + if (isubdft.empty()) { return {*this}; } else { subdfts[child->id()] = isubdft; } } - + std::vector> res; - for(auto const& subdft : subdfts) { + for (auto const& subdft : subdfts) { storm::builder::DFTBuilder builder; - - for(size_t id : subdft.second) { + + for (size_t id : subdft.second) { builder.copyElement(mElements[id]); } builder.setTopLevel(mElements[subdft.first]->name()); res.push_back(builder.build()); } return res; - + } - + template uint64_t DFT::maxRank() const { uint64_t max = 0; for (auto const& e : mElements) { - if(e->rank() > max) { + if (e->rank() > max) { max = e->rank(); } } @@ -338,7 +343,8 @@ namespace storm { // Accumulate children names std::vector childrenNames; for (size_t i = 1; i < rewrites.size(); ++i) { - STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), "Children have not the same father for rewrite " << mElements[rewrites[i]]->name()); + STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), + "Children have not the same father for rewrite " << mElements[rewrites[i]]->name()); childrenNames.push_back(mElements[rewrites[i]]->name()); } @@ -369,7 +375,7 @@ namespace storm { childrenNames.clear(); childrenNames.push_back(newParentName); for (auto const& child : originalParent->children()) { - if (std::find(rewrites.begin()+1, rewrites.end(), child->id()) == rewrites.end()) { + if (std::find(rewrites.begin() + 1, rewrites.end(), child->id()) == rewrites.end()) { // Child was not rewritten and must be kept childrenNames.push_back(child->name()); } @@ -466,21 +472,21 @@ namespace storm { STORM_LOG_ASSERT(it != mTopModule.end(), "Element not found."); stream << mElements[(*it)]->name(); ++it; - while(it != mTopModule.end()) { - stream << ", " << mElements[(*it)]->name(); + while (it != mTopModule.end()) { + stream << ", " << mElements[(*it)]->name(); ++it; } stream << "}" << std::endl; - for(auto const& spareModule : mSpareModules) { + for (auto const& spareModule : mSpareModules) { stream << "[" << mElements[spareModule.first]->name() << "] = {"; if (!spareModule.second.empty()) { std::vector::const_iterator it = spareModule.second.begin(); STORM_LOG_ASSERT(it != spareModule.second.end(), "Element not found."); stream << mElements[(*it)]->name(); ++it; - while(it != spareModule.second.end()) { - stream << ", " << mElements[(*it)]->name(); + while (it != spareModule.second.end()) { + stream << ", " << mElements[(*it)]->name(); ++it; } } @@ -490,7 +496,7 @@ namespace storm { } template - std::string DFT::getElementsWithStateString(DFTStatePointer const& state) const{ + std::string DFT::getElementsWithStateString(DFTStatePointer const& state) const { std::stringstream stream; for (auto const& elem : mElements) { stream << "[" << elem->id() << "]"; @@ -499,9 +505,9 @@ namespace storm { stream << "\t** " << storm::storage::toChar(state->getDependencyState(elem->id())) << "[dep]"; } else { stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id())); - if(elem->isSpareGate()) { + if (elem->isSpareGate()) { size_t useId = state->uses(elem->id()); - if(useId == elem->id() || state->isActive(useId)) { + if (useId == elem->id() || state->isActive(useId)) { stream << "actively "; } stream << "using " << useId; @@ -511,7 +517,7 @@ namespace storm { } return stream.str(); } - + template std::string DFT::getStateString(DFTStatePointer const& state) const { std::stringstream stream; @@ -521,10 +527,10 @@ namespace storm { stream << storm::storage::toChar(state->getDependencyState(elem->id())) << "[dep]"; } else { stream << storm::storage::toChar(state->getElementState(elem->id())); - if(elem->isSpareGate()) { + if (elem->isSpareGate()) { stream << "["; size_t useId = state->uses(elem->id()); - if(useId == elem->id() || state->isActive(useId)) { + if (useId == elem->id() || state->isActive(useId)) { stream << "actively "; } stream << "using " << useId << "]"; @@ -532,7 +538,7 @@ namespace storm { } } return stream.str(); - } + } template std::string DFT::getStateString(storm::storage::BitVector const& status, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) const { @@ -543,7 +549,7 @@ namespace storm { stream << storm::storage::toChar(DFTState::getDependencyState(status, stateGenerationInfo, elem->id())) << "[dep]"; } else { stream << storm::storage::toChar(DFTState::getElementState(status, stateGenerationInfo, elem->id())); - if(elem->isSpareGate()) { + if (elem->isSpareGate()) { stream << "["; size_t nrUsedChild = status.getAsInt(stateGenerationInfo.getSpareUsageIndex(elem->id()), stateGenerationInfo.usageInfoBits()); size_t useId; @@ -552,7 +558,7 @@ namespace storm { } else { useId = getChild(elem->id(), nrUsedChild); } - if(useId == elem->id() || status[stateGenerationInfo.getSpareActivationIndex(useId)]) { + if (useId == elem->id() || status[stateGenerationInfo.getSpareActivationIndex(useId)]) { stream << "actively "; } stream << "using " << useId << "]"; @@ -561,13 +567,13 @@ namespace storm { } return stream.str(); } - + template size_t DFT::getChild(size_t spareId, size_t nrUsedChild) const { STORM_LOG_ASSERT(mElements[spareId]->isSpareGate(), "Element is no spare."); return getGate(spareId)->children()[nrUsedChild]->id(); } - + template size_t DFT::getNrChild(size_t spareId, size_t childId) const { STORM_LOG_ASSERT(mElements[spareId]->isSpareGate(), "Element is no spare."); @@ -580,8 +586,8 @@ namespace storm { STORM_LOG_ASSERT(false, "Child not found."); return 0; } - - template + + template std::vector DFT::getIndependentSubDftRoots(size_t index) const { auto elem = getElement(index); auto ISD = elem->independentSubDft(false); @@ -608,7 +614,7 @@ namespace storm { bool wellformed = true; // Check independence of spare modules // TODO: comparing one element of each spare module sufficient? - for (auto module1 = mSpareModules.begin() ; module1 != mSpareModules.end() ; ++module1) { + for (auto module1 = mSpareModules.begin(); module1 != mSpareModules.end(); ++module1) { size_t firstElement = module1->second.front(); for (auto module2 = std::next(module1); module2 != mSpareModules.end(); ++module2) { if (std::find(module2->second.begin(), module2->second.end(), firstElement) != module2->second.end()) { @@ -621,6 +627,7 @@ namespace storm { } } // TODO check VOT gates + // TODO check only one constant failed event return wellformed; } @@ -634,7 +641,7 @@ namespace storm { STORM_LOG_TRACE("Considering ids " << index1 << ", " << index2 << " for isomorphism."); bool sharedSpareMode = false; std::map bijection; - + if (isBasicElement(index1)) { if (!isBasicElement(index2)) { return {}; @@ -646,18 +653,18 @@ namespace storm { return {}; } } - + STORM_LOG_ASSERT(isGate(index1), "Element is no gate."); STORM_LOG_ASSERT(isGate(index2), "Element is no gate."); std::vector isubdft1 = getGate(index1)->independentSubDft(false); std::vector isubdft2 = getGate(index2)->independentSubDft(false); - if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) { + if (isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) { if (isubdft1.empty() && isubdft2.empty() && sparesAsLeaves) { // Check again for shared spares sharedSpareMode = true; isubdft1 = getGate(index1)->independentSubDft(false, true); isubdft2 = getGate(index2)->independentSubDft(false, true); - if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) { + if (isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) { return {}; } } else { @@ -668,7 +675,7 @@ namespace storm { auto LHS = colouring.colourSubdft(isubdft1); auto RHS = colouring.colourSubdft(isubdft2); auto IsoCheck = DFTIsomorphismCheck(LHS, RHS, *this); - + while (IsoCheck.findNextIsomorphism()) { bijection = IsoCheck.getIsomorphism(); if (sharedSpareMode) { @@ -677,7 +684,7 @@ namespace storm { if (getElement(elementId)->isSpareGate()) { std::shared_ptr> spareLeft = std::static_pointer_cast>(mElements[elementId]); std::shared_ptr> spareRight = std::static_pointer_cast>(mElements[bijection.at(elementId)]); - + if (spareLeft->nrChildren() != spareRight->nrChildren()) { bijectionSpareCompatible = false; break; @@ -692,13 +699,13 @@ namespace storm { // Ignore shared child continue; } - + // TODO generalize for more than one parent if (spareLeft->children().at(i)->nrParents() != 1 || spareRight->children().at(i)->nrParents() != 1) { bijectionSpareCompatible = false; break; } - + std::map tmpBijection = findBijection(childLeftId, childRightId, colouring, false); if (!tmpBijection.empty()) { bijection.insert(tmpBijection.begin(), tmpBijection.end()); @@ -731,12 +738,12 @@ namespace storm { std::map>> res; // Find symmetries for gates - for(auto const& colourClass : completeCategories.gateCandidates) { + for (auto const& colourClass : completeCategories.gateCandidates) { findSymmetriesHelper(colourClass.second, colouring, res); } // Find symmetries for BEs - for(auto const& colourClass : completeCategories.beCandidates) { + for (auto const& colourClass : completeCategories.beCandidates) { findSymmetriesHelper(colourClass.second, colouring, res); } @@ -744,41 +751,42 @@ namespace storm { } template - void DFT::findSymmetriesHelper(std::vector const& candidates, DFTColouring const& colouring, std::map>>& result) const { - if(candidates.size() <= 0) { + void DFT::findSymmetriesHelper(std::vector const& candidates, DFTColouring const& colouring, + std::map>>& result) const { + if (candidates.size() <= 0) { return; } std::set foundEqClassFor; - for(auto it1 = candidates.cbegin(); it1 != candidates.cend(); ++it1) { + for (auto it1 = candidates.cbegin(); it1 != candidates.cend(); ++it1) { std::vector> symClass; - if(foundEqClassFor.count(*it1) > 0) { + if (foundEqClassFor.count(*it1) > 0) { // This item is already in a class. continue; } - if(!getElement(*it1)->hasOnlyStaticParents()) { + if (!getElement(*it1)->hasOnlyStaticParents()) { continue; } std::tuple, std::vector, std::vector> influencedElem1Ids = getSortedParentAndDependencyIds(*it1); auto it2 = it1; - for(++it2; it2 != candidates.cend(); ++it2) { - if(!getElement(*it2)->hasOnlyStaticParents()) { + for (++it2; it2 != candidates.cend(); ++it2) { + if (!getElement(*it2)->hasOnlyStaticParents()) { continue; } - if(influencedElem1Ids == getSortedParentAndDependencyIds(*it2)) { + if (influencedElem1Ids == getSortedParentAndDependencyIds(*it2)) { std::map bijection = findBijection(*it1, *it2, colouring, true); if (!bijection.empty()) { STORM_LOG_TRACE("Subdfts are symmetric"); foundEqClassFor.insert(*it2); - if(symClass.empty()) { - for(auto const& i : bijection) { + if (symClass.empty()) { + for (auto const& i : bijection) { symClass.push_back(std::vector({i.first})); } } auto symClassIt = symClass.begin(); - for(auto const& i : bijection) { + for (auto const& i : bijection) { symClassIt->emplace_back(i.second); ++symClassIt; @@ -787,7 +795,7 @@ namespace storm { } } - if(!symClass.empty()) { + if (!symClass.empty()) { result.emplace(*it1, symClass); } } @@ -795,31 +803,32 @@ namespace storm { template std::vector DFT::findModularisationRewrite() const { - for(auto const& e : mElements) { - if(e->isGate() && (e->type() == DFTElementType::AND || e->type() == DFTElementType::OR) ) { - // suitable parent gate! - Lets check the independent submodules of the children - auto const& children = std::static_pointer_cast>(e)->children(); - for(auto const& child : children) { - - auto ISD = std::static_pointer_cast>(child)->independentSubDft(true); - // In the ISD, check for other children: - - std::vector rewrite = {e->id(), child->id()}; - for(size_t isdElemId : ISD) { - if(isdElemId == child->id()) continue; - if(std::find_if(children.begin(), children.end(), [&isdElemId](std::shared_ptr> const& e) { return e->id() == isdElemId; } ) != children.end()) { - // element in subtree is also child - rewrite.push_back(isdElemId); - } - } - if(rewrite.size() > 2 && rewrite.size() < children.size() - 1) { - return rewrite; - } + for (auto const& e : mElements) { + if (e->isGate() && (e->type() == DFTElementType::AND || e->type() == DFTElementType::OR)) { + // suitable parent gate! - Lets check the independent submodules of the children + auto const& children = std::static_pointer_cast>(e)->children(); + for (auto const& child : children) { + + auto ISD = std::static_pointer_cast>(child)->independentSubDft(true); + // In the ISD, check for other children: + + std::vector rewrite = {e->id(), child->id()}; + for (size_t isdElemId : ISD) { + if (isdElemId == child->id()) continue; + if (std::find_if(children.begin(), children.end(), [&isdElemId](std::shared_ptr> const& e) { return e->id() == isdElemId; }) != + children.end()) { + // element in subtree is also child + rewrite.push_back(isdElemId); + } + } + if (rewrite.size() > 2 && rewrite.size() < children.size() - 1) { + return rewrite; + } - } - } - } - return {}; + } + } + } + return {}; } @@ -831,14 +840,14 @@ namespace storm { // Ingoing dependencies std::vector ingoingDeps; if (isBasicElement(index)) { - for(auto const& dep : getBasicElement(index)->ingoingDependencies()) { + for (auto const& dep : getBasicElement(index)->ingoingDependencies()) { ingoingDeps.push_back(dep->id()); } std::sort(ingoingDeps.begin(), ingoingDeps.end()); } // Outgoing dependencies std::vector outgoingDeps; - for(auto const& dep : getElement(index)->outgoingDependencies()) { + for (auto const& dep : getElement(index)->outgoingDependencies()) { outgoingDeps.push_back(dep->id()); } std::sort(outgoingDeps.begin(), outgoingDeps.end()); @@ -863,10 +872,12 @@ namespace storm { template void DFT::setRelevantEvents(std::set const& relevantEvents, bool allowDCForRelevantEvents) const { + mRelevantEvents.clear(); for (auto const& elem : mElements) { if (relevantEvents.find(elem->id()) != relevantEvents.end()) { elem->setRelevance(true); elem->setAllowDC(allowDCForRelevantEvents); + mRelevantEvents.insert(elem->id()); } else { elem->setRelevance(false); elem->setAllowDC(true); @@ -876,29 +887,20 @@ namespace storm { template std::set DFT::getRelevantEvents() const { - std::set relevantEvents; - for (auto const& elem : mElements) { - if (elem->isRelevant()) { - relevantEvents.insert(elem->id()); - } - } - return relevantEvents; + return mRelevantEvents; } - template std::string DFT::getRelevantEventsString() const { std::stringstream stream; bool first = true; - for (auto const& elem : mElements) { - if (elem->isRelevant()) { - if (first) { - first = false; - } else { - stream << ", "; - } - stream << elem->name() << " [" << elem->id() << "]"; + for (size_t relevant_id : getRelevantEvents()) { + if (first) { + first = false; + } else { + stream << ", "; } + stream << getElement(relevant_id)->name() << " [" << relevant_id << "]"; } return stream.str(); } @@ -998,12 +1000,16 @@ namespace storm { } stream << "=========================================" << std::endl; } - + // Explicitly instantiate the class. - template class DFT; + template + class DFT; #ifdef STORM_HAVE_CARL - template class DFT; + + template + class DFT; + #endif } diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 53f901408..831795cce 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -68,6 +68,7 @@ namespace storm { std::map mRepresentants; // id element -> id representative std::vector> mSymmetries; std::map mLayoutInfo; + mutable std::set mRelevantEvents; public: DFT(DFTElementVector const& elements, DFTElementPointer const& tle); @@ -327,7 +328,7 @@ namespace storm { /*! * Set the relevance flag for all elements according to the given relevant events. - * @param relevantEvents All elements which should be to relevant. All elements not occuring are set to irrelevant. + * @param relevantEvents All elements which should be to relevant. All elements not occurring are set to irrelevant. * @param allowDCForRelevantEvents Flag whether Don't Care propagation is allowed even for relevant events. */ void setRelevantEvents(std::set const& relevantEvents, bool allowDCForRelevantEvents) const; diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index 86cd79400..d528035d3 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -7,7 +7,7 @@ namespace storm { namespace storage { template - DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateBitVectorSize()), mId(id), failableElements(dft.nrElements(), dft.getRelevantEvents()), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { + DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateBitVectorSize()), mId(id), failableElements(dft.nrElements()), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { // TODO: use construct() // Initialize uses @@ -33,7 +33,7 @@ namespace storm { } template - DFTState::DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), failableElements(dft.nrElements(), dft.getRelevantEvents()), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { + DFTState::DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), failableElements(dft.nrElements()), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { // Intentionally left empty } @@ -87,10 +87,6 @@ namespace storm { } } - // Initialize remaining relevant events - failableElements.remainingRelevantEvents = mDft.getRelevantEvents(); - this->updateRemainingRelevantEvents(); - mPseudoState = false; } @@ -316,18 +312,6 @@ namespace storm { } } - template - void DFTState::updateRemainingRelevantEvents() { - for (auto it = failableElements.remainingRelevantEvents.begin(); it != failableElements.remainingRelevantEvents.end(); ) { - if (isOperational(*it)) { - ++it; - } else { - // Element is not relevant anymore - it = failableElements.remainingRelevantEvents.erase(it); - } - } - } - template ValueType DFTState::getBERate(size_t id) const { STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE."); diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index fd911b355..3718e7627 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -25,7 +25,7 @@ namespace storm { struct FailableElements { - FailableElements(size_t nrElements, std::set relevantEvents) : currentlyFailableBE(nrElements), remainingRelevantEvents(relevantEvents), it(currentlyFailableBE.begin()) { + FailableElements(size_t nrElements) : currentlyFailableBE(nrElements), it(currentlyFailableBE.begin()) { // Intentionally left empty } @@ -103,19 +103,10 @@ namespace storm { return !currentlyFailableBE.empty(); } - /*! - * Check whether at least one relevant event has not failed yet. - * @return True iff one relevant event is still operational. - */ - bool hasRemainingRelevantEvent() const { - return !remainingRelevantEvents.empty(); - } - mutable bool dependency; storm::storage::BitVector currentlyFailableBE; std::vector mFailableDependencies; - std::set remainingRelevantEvents; mutable storm::storage::BitVector::const_iterator it; mutable std::vector::const_iterator itDep; @@ -312,11 +303,6 @@ namespace storm { */ void updateDontCareDependencies(size_t id); - /*! - * Update remaining relevant events. - */ - void updateRemainingRelevantEvents(); - /** * Sets the next BE as failed * @param index Index in currentlyFailableBE of BE to fail