diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index 747075ef3..d3e635636 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -18,6 +18,7 @@ namespace storm { template storm::storage::DFT DFTBuilder::build() { + // Build parent/child connections between elements for(auto& elem : mChildNames) { DFTGatePointer gate = std::static_pointer_cast>(elem.first); for(auto const& child : elem.second) { @@ -25,10 +26,11 @@ namespace storm { if (itFind != mElements.end()) { // Child found DFTElementPointer childElement = itFind->second; - STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name()); if(!childElement->isDependency()) { gate->pushBackChild(childElement); childElement->addParent(gate); + } else { + STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name()); } } else { // Child not found -> find first dependent event to assure that child is dependency @@ -40,18 +42,20 @@ namespace storm { } } } - + + // Build connections for restrictions for(auto& elem : mRestrictionChildNames) { for(auto const& childName : elem.second) { auto itFind = mElements.find(childName); STORM_LOG_ASSERT(itFind != mElements.end(), "Child not found."); DFTElementPointer childElement = itFind->second; - STORM_LOG_ASSERT(!childElement->isDependency() && !childElement->isRestriction(), "Child '" << childElement->name() << "' has invalid type."); + STORM_LOG_THROW(childElement->isGate() || childElement->isBasicElement(), storm::exceptions::WrongFormatException, "Child '" << childElement->name() << "' of restriction '" << elem.first->name() << "' must be gate or BE."); elem.first->pushBackChild(childElement); childElement->addRestriction(elem.first); } } + // Build connections for dependencies for(auto& elem : mDependencyChildNames) { bool first = true; std::vector>> dependencies; @@ -60,16 +64,17 @@ namespace storm { STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << childName << "' not found"); DFTElementPointer childElement = itFind->second; if (!first) { - STORM_LOG_ASSERT(childElement->isBasicElement(), "Child '" << childName << "' of dependency '" << elem.first->name() << "' must be BE."); + STORM_LOG_THROW(childElement->isBasicElement(), storm::exceptions::WrongFormatException, "Child '" << childName << "' of dependency '" << elem.first->name() << "' must be BE."); dependencies.push_back(std::static_pointer_cast>(childElement)); } else { + first = false; + STORM_LOG_THROW(childElement->isGate() || childElement->isBasicElement(), storm::exceptions::WrongFormatException, "Child '" << childName << "' of dependency '" << elem.first->name() << "' must be gate or BE."); elem.first->setTriggerElement(std::static_pointer_cast>(childElement)); childElement->addOutgoingDependency(elem.first); } - first = false; } if (binaryDependencies) { - assert(dependencies.size() == 1); + STORM_LOG_ASSERT(dependencies.size() == 1, "Dependency '" << elem.first->name() << "' should only have one dependent element."); } elem.first->setDependentEvents(dependencies); for (auto& dependency : dependencies) { @@ -84,14 +89,14 @@ namespace storm { for (auto& elem : mElements) { computeRank(elem.second); } - DFTElementVector elems = topoSort(); + // Set ids size_t id = 0; for(DFTElementPointer e : elems) { e->setId(id++); } - STORM_LOG_ASSERT(!mTopLevelIdentifier.empty(), "No top level element."); + STORM_LOG_THROW(!mTopLevelIdentifier.empty(), storm::exceptions::WrongFormatException, "No top level element defined."); storm::storage::DFT dft(elems, mElements[mTopLevelIdentifier]); // Set layout info @@ -110,7 +115,7 @@ namespace storm { template unsigned DFTBuilder::computeRank(DFTElementPointer const& elem) { if(elem->rank() == static_castrank())>(-1)) { - if(elem->nrChildren() == 0 || elem->isDependency()) { + if(elem->nrChildren() == 0 || elem->isDependency() || elem->isRestriction()) { elem->setRank(0); } else { DFTGatePointer gate = std::static_pointer_cast>(elem); @@ -200,9 +205,8 @@ namespace storm { template void DFTBuilder::topoVisit(DFTElementPointer const& n, std::map>& visited, DFTElementVector& L) { - if(visited[n] == topoSortColour::GREY) { - throw storm::exceptions::WrongFormatException("DFT is cyclic"); - } else if(visited[n] == topoSortColour::WHITE) { + STORM_LOG_THROW(visited[n] != topoSortColour::GREY, storm::exceptions::WrongFormatException, "DFT is cyclic"); + if(visited[n] == topoSortColour::WHITE) { if(n->isGate()) { visited[n] = topoSortColour::GREY; for (DFTElementPointer const& c : std::static_pointer_cast>(n)->children()) { @@ -210,13 +214,13 @@ namespace storm { } } // TODO restrictions and dependencies have no parents, so this can be done more efficiently. - if(n->isRestriction()) { + else if(n->isRestriction()) { visited[n] = topoSortColour::GREY; for (DFTElementPointer const& c : std::static_pointer_cast>(n)->children()) { topoVisit(c, visited, L); } } - if(n->isDependency()) { + else if(n->isDependency()) { visited[n] = topoSortColour::GREY; for (DFTElementPointer const& c : std::static_pointer_cast>(n)->dependentEvents()) { topoVisit(c, visited, L); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index e758f209b..753f1d23a 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -4,6 +4,7 @@ #include #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/WrongFormatException.h" #include "storm/utility/iota_n.h" #include "storm/utility/vector.h" @@ -25,11 +26,12 @@ namespace storm { } if(elem->isBasicElement()) { ++mNrOfBEs; - } - else if (elem->isSpareGate()) { + } 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."); std::set module = {spareReprs->id()}; spareReprs->extendSpareModule(module); std::vector sparesAndBes; @@ -41,12 +43,22 @@ namespace storm { } mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes)); } - } else if (elem->isDependency()) { mDependencies.push_back(elem->id()); } } - + + // Check independence of spare modules + // TODO: comparing one element of each spare module sufficient? + 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()) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Spare modules of '" << getElement(module1->first)->name() << "' and '" << getElement(module2->first)->name() << "' should not overlap."); + } + } + } + // 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. @@ -64,10 +76,13 @@ namespace storm { // Extend top module and insert those elements which are part of the top module and a spare module mElements[mTopLevelIndex]->extendSpareModule(topModuleSet); mTopModule = std::vector(topModuleSet.begin(), topModuleSet.end()); - // Clear all spare modules where at least one element is also in the top module + + // Clear all spare modules where at least one element is also in the top module. + // These spare modules will be activated from the beginning. 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."); module.second.clear(); } }