From ed7efc0268b46b31f4fe1ce06b76bab6878847b9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 16 Feb 2018 18:15:19 +0100 Subject: [PATCH] Moved DFTBuilder to builder dir --- .../{storage/dft => builder}/DFTBuilder.cpp | 118 +++++++++--------- .../{storage/dft => builder}/DFTBuilder.h | 50 ++++---- src/storm-dft/parser/DFTGalileoParser.cpp | 4 +- src/storm-dft/parser/DFTGalileoParser.h | 4 +- src/storm-dft/parser/DFTJsonParser.h | 4 +- src/storm-dft/storage/dft/DFT.cpp | 6 +- src/storm-dft/storage/dft/DFT.h | 12 +- 7 files changed, 101 insertions(+), 97 deletions(-) rename src/storm-dft/{storage/dft => builder}/DFTBuilder.cpp (73%) rename src/storm-dft/{storage/dft => builder}/DFTBuilder.h (81%) diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp similarity index 73% rename from src/storm-dft/storage/dft/DFTBuilder.cpp rename to src/storm-dft/builder/DFTBuilder.cpp index 88abc9665..a333c3cd6 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -11,15 +11,15 @@ namespace storm { - namespace storage { + namespace builder { template std::size_t DFTBuilder::mUniqueOffset = 0; template - DFT DFTBuilder::build() { + storm::storage::DFT DFTBuilder::build() { for(auto& elem : mChildNames) { - DFTGatePointer gate = std::static_pointer_cast>(elem.first); + DFTGatePointer gate = std::static_pointer_cast>(elem.first); for(auto const& child : elem.second) { auto itFind = mElements.find(child); if (itFind != mElements.end()) { @@ -54,16 +54,16 @@ namespace storm { for(auto& elem : mDependencyChildNames) { bool first = true; - std::vector>> dependencies; + std::vector>> dependencies; for(auto const& childName : elem.second) { auto itFind = mElements.find(childName); 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."); - dependencies.push_back(std::static_pointer_cast>(childElement)); + dependencies.push_back(std::static_pointer_cast>(childElement)); } else { - elem.first->setTriggerElement(std::static_pointer_cast>(childElement)); + elem.first->setTriggerElement(std::static_pointer_cast>(childElement)); childElement->addOutgoingDependency(elem.first); } first = false; @@ -92,7 +92,7 @@ namespace storm { } STORM_LOG_ASSERT(!mTopLevelIdentifier.empty(), "No top level element."); - DFT dft(elems, mElements[mTopLevelIdentifier]); + storm::storage::DFT dft(elems, mElements[mTopLevelIdentifier]); // Set layout info for (auto& elem : mElements) { @@ -113,7 +113,7 @@ namespace storm { if(elem->nrChildren() == 0 || elem->isDependency()) { elem->setRank(0); } else { - DFTGatePointer gate = std::static_pointer_cast>(elem); + DFTGatePointer gate = std::static_pointer_cast>(elem); unsigned maxrnk = 0; unsigned newrnk = 0; @@ -131,7 +131,7 @@ namespace storm { } template - bool DFTBuilder::addRestriction(std::string const& name, std::vector const& children, DFTElementType tp) { + bool DFTBuilder::addRestriction(std::string const& name, std::vector const& children, storm::storage::DFTElementType tp) { if (children.size() <= 1) { STORM_LOG_ERROR("Sequence enforcers require at least two children"); } @@ -140,10 +140,10 @@ namespace storm { } DFTRestrictionPointer restr; switch (tp) { - case DFTElementType::SEQ: - restr = std::make_shared>(mNextId++, name); + case storm::storage::DFTElementType::SEQ: + restr = std::make_shared>(mNextId++, name); break; - case DFTElementType::MUTEX: + case storm::storage::DFTElementType::MUTEX: // TODO notice that mutex state generation support is lacking anyway, as DONT CARE propagation would be broken for this. STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported."); break; @@ -159,7 +159,7 @@ namespace storm { } template - bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, DFTElementType tp) { + bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, storm::storage::DFTElementType tp) { STORM_LOG_ASSERT(children.size() > 0, "No child for " << name); if(mElements.count(name) != 0) { // Element with that name already exists. @@ -167,28 +167,28 @@ namespace storm { } DFTElementPointer element; switch(tp) { - case DFTElementType::AND: - element = std::make_shared>(mNextId++, name); + case storm::storage::DFTElementType::AND: + element = std::make_shared>(mNextId++, name); break; - case DFTElementType::OR: - element = std::make_shared>(mNextId++, name); + case storm::storage::DFTElementType::OR: + element = std::make_shared>(mNextId++, name); break; - case DFTElementType::PAND: - element = std::make_shared>(mNextId++, name, pandDefaultInclusive); + case storm::storage::DFTElementType::PAND: + element = std::make_shared>(mNextId++, name, pandDefaultInclusive); break; - case DFTElementType::POR: - element = std::make_shared>(mNextId++, name, porDefaultInclusive); + case storm::storage::DFTElementType::POR: + element = std::make_shared>(mNextId++, name, porDefaultInclusive); break; - case DFTElementType::SPARE: - element = std::make_shared>(mNextId++, name); + case storm::storage::DFTElementType::SPARE: + element = std::make_shared>(mNextId++, name); break; - case DFTElementType::BE: - case DFTElementType::VOT: - case DFTElementType::PDEP: + case storm::storage::DFTElementType::BE: + case storm::storage::DFTElementType::VOT: + case storm::storage::DFTElementType::PDEP: // Handled separately STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type handled separately."); - case DFTElementType::CONSTF: - case DFTElementType::CONSTS: + case storm::storage::DFTElementType::CONSTF: + case storm::storage::DFTElementType::CONSTS: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported."); default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known."); @@ -199,29 +199,29 @@ namespace storm { } template - void DFTBuilder::topoVisit(DFTElementPointer const& n, std::map>& visited, DFTElementVector& L) { + 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) { if(n->isGate()) { visited[n] = topoSortColour::GREY; - for (DFTElementPointer const& c : std::static_pointer_cast>(n)->children()) { + for (DFTElementPointer const& c : std::static_pointer_cast>(n)->children()) { topoVisit(c, visited, L); } } // TODO restrictions and dependencies have no parents, so this can be done more efficiently. if(n->isRestriction()) { visited[n] = topoSortColour::GREY; - for (DFTElementPointer const& c : std::static_pointer_cast>(n)->children()) { + for (DFTElementPointer const& c : std::static_pointer_cast>(n)->children()) { topoVisit(c, visited, L); } } if(n->isDependency()) { visited[n] = topoSortColour::GREY; - for (DFTElementPointer const& c : std::static_pointer_cast>(n)->dependentEvents()) { + for (DFTElementPointer const& c : std::static_pointer_cast>(n)->dependentEvents()) { topoVisit(c, visited, L); } - topoVisit(std::static_pointer_cast>(n)->triggerEvent(), visited, L); + topoVisit(std::static_pointer_cast>(n)->triggerEvent(), visited, L); } visited[n] = topoSortColour::BLACK; L.push_back(n); @@ -229,8 +229,8 @@ namespace storm { } template - std::vector>> DFTBuilder::topoSort() { - std::map> visited; + std::vector>> DFTBuilder::topoSort() { + std::map> visited; for(auto const& e : mElements) { visited.insert(std::make_pair(e.second, topoSortColour::WHITE)); } @@ -252,22 +252,22 @@ namespace storm { void DFTBuilder::copyElement(DFTElementPointer element) { std::vector children; switch (element->type()) { - case DFTElementType::AND: - case DFTElementType::OR: - case DFTElementType::PAND: - case DFTElementType::POR: - case DFTElementType::SPARE: - case DFTElementType::VOT: + case storm::storage::DFTElementType::AND: + case storm::storage::DFTElementType::OR: + case storm::storage::DFTElementType::PAND: + case storm::storage::DFTElementType::POR: + case storm::storage::DFTElementType::SPARE: + case storm::storage::DFTElementType::VOT: { - for (DFTElementPointer const& elem : std::static_pointer_cast>(element)->children()) { + for (DFTElementPointer const& elem : std::static_pointer_cast>(element)->children()) { children.push_back(elem->name()); } - copyGate(std::static_pointer_cast>(element), children); + copyGate(std::static_pointer_cast>(element), children); break; } - case DFTElementType::BE: + case storm::storage::DFTElementType::BE: { - std::shared_ptr> be = std::static_pointer_cast>(element); + std::shared_ptr> be = std::static_pointer_cast>(element); ValueType dormancyFactor = storm::utility::zero(); if (be->canFail()) { dormancyFactor = be->passiveFailureRate() / be->activeFailureRate(); @@ -275,14 +275,14 @@ namespace storm { addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor, be->isTransient()); break; } - case DFTElementType::CONSTF: - case DFTElementType::CONSTS: + case storm::storage::DFTElementType::CONSTF: + case storm::storage::DFTElementType::CONSTS: // TODO STORM_LOG_ASSERT(false, "Const elements not supported."); break; - case DFTElementType::PDEP: + case storm::storage::DFTElementType::PDEP: { - DFTDependencyPointer dependency = std::static_pointer_cast>(element); + DFTDependencyPointer dependency = std::static_pointer_cast>(element); children.push_back(dependency->triggerEvent()->name()); for(auto const& depEv : dependency->dependentEvents()) { children.push_back(depEv->name()); @@ -290,10 +290,10 @@ namespace storm { addDepElement(element->name(), children, dependency->probability()); break; } - case DFTElementType::SEQ: - case DFTElementType::MUTEX: + case storm::storage::DFTElementType::SEQ: + case storm::storage::DFTElementType::MUTEX: { - for (DFTElementPointer const& elem : std::static_pointer_cast>(element)->children()) { + for (DFTElementPointer const& elem : std::static_pointer_cast>(element)->children()) { children.push_back(elem->name()); } addRestriction(element->name(), children, element->type()); @@ -308,15 +308,15 @@ namespace storm { template void DFTBuilder::copyGate(DFTGatePointer gate, std::vector const& children) { switch (gate->type()) { - case DFTElementType::AND: - case DFTElementType::OR: - case DFTElementType::PAND: - case DFTElementType::POR: - case DFTElementType::SPARE: + case storm::storage::DFTElementType::AND: + case storm::storage::DFTElementType::OR: + case storm::storage::DFTElementType::PAND: + case storm::storage::DFTElementType::POR: + case storm::storage::DFTElementType::SPARE: addStandardGate(gate->name(), children, gate->type()); break; - case DFTElementType::VOT: - addVotElement(gate->name(), std::static_pointer_cast>(gate)->threshold(), children); + case storm::storage::DFTElementType::VOT: + addVotElement(gate->name(), std::static_pointer_cast>(gate)->threshold(), children); break; default: STORM_LOG_ASSERT(false, "Dft type not known."); diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h similarity index 81% rename from src/storm-dft/storage/dft/DFTBuilder.h rename to src/storm-dft/builder/DFTBuilder.h index 42713e601..625355371 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.h +++ b/src/storm-dft/builder/DFTBuilder.h @@ -11,18 +11,22 @@ namespace storm { namespace storage { + // Forward declaration template class DFT; + } + + namespace builder { template class DFTBuilder { - using DFTElementPointer = std::shared_ptr>; + using DFTElementPointer = std::shared_ptr>; using DFTElementVector = std::vector; - using DFTGatePointer = std::shared_ptr>; + using DFTGatePointer = std::shared_ptr>; using DFTGateVector = std::vector; - using DFTDependencyPointer = std::shared_ptr>; - using DFTRestrictionPointer = std::shared_ptr>; + using DFTDependencyPointer = std::shared_ptr>; + using DFTRestrictionPointer = std::shared_ptr>; private: std::size_t mNextId = 0; @@ -34,7 +38,7 @@ namespace storm { std::unordered_map> mDependencyChildNames; std::vector mDependencies; std::vector mRestrictions; - std::unordered_map mLayoutInfo; + std::unordered_map mLayoutInfo; public: DFTBuilder(bool defaultInclusive = true, bool binaryDependencies = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive), binaryDependencies(binaryDependencies) { @@ -42,47 +46,47 @@ namespace storm { } bool addAndElement(std::string const& name, std::vector const& children) { - return addStandardGate(name, children, DFTElementType::AND); + return addStandardGate(name, children, storm::storage::DFTElementType::AND); } bool addOrElement(std::string const& name, std::vector const& children) { - return addStandardGate(name, children, DFTElementType::OR); + return addStandardGate(name, children, storm::storage::DFTElementType::OR); } bool addPandElement(std::string const& name, std::vector const& children) { - return addStandardGate(name, children, DFTElementType::PAND); + return addStandardGate(name, children, storm::storage::DFTElementType::PAND); } bool addPandElement(std::string const& name, std::vector const& children, bool inclusive) { bool tmpDefault = pandDefaultInclusive; pandDefaultInclusive = inclusive; - bool result = addStandardGate(name, children, DFTElementType::PAND); + bool result = addStandardGate(name, children, storm::storage::DFTElementType::PAND); pandDefaultInclusive = tmpDefault; return result; } bool addPorElement(std::string const& name, std::vector const& children) { - return addStandardGate(name, children, DFTElementType::POR); + return addStandardGate(name, children, storm::storage::DFTElementType::POR); } bool addPorElement(std::string const& name, std::vector const& children, bool inclusive) { bool tmpDefault = porDefaultInclusive; porDefaultInclusive = inclusive; - bool result = addStandardGate(name, children, DFTElementType::POR); + bool result = addStandardGate(name, children, storm::storage::DFTElementType::POR); pandDefaultInclusive = tmpDefault; return result; } bool addSpareElement(std::string const& name, std::vector const& children) { - return addStandardGate(name, children, DFTElementType::SPARE); + return addStandardGate(name, children, storm::storage::DFTElementType::SPARE); } bool addSequenceEnforcer(std::string const& name, std::vector const& children) { - return addRestriction(name, children, DFTElementType::SEQ); + return addRestriction(name, children, storm::storage::DFTElementType::SEQ); } bool addMutex(std::string const& name, std::vector const& children) { - return addRestriction(name, children, DFTElementType::MUTEX); + return addRestriction(name, children, storm::storage::DFTElementType::MUTEX); } bool addDepElement(std::string const& name, std::vector const& children, ValueType probability) { @@ -125,15 +129,13 @@ namespace storm { } STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, "PDep with multiple children supported."); - DFTDependencyPointer element = std::make_shared>(mNextId++, - nameDep, - probability); + DFTDependencyPointer element = std::make_shared>(mNextId++, nameDep, probability); mElements[element->name()] = element; mDependencyChildNames[element] = {trigger, children[i]}; mDependencies.push_back(element); } } else { - DFTDependencyPointer element = std::make_shared>(mNextId++, name, probability); + DFTDependencyPointer element = std::make_shared>(mNextId++, name, probability); mElements[element->name()] = element; mDependencyChildNames[element] = children; mDependencies.push_back(element); @@ -161,7 +163,7 @@ namespace storm { STORM_LOG_ERROR("Voting gates with threshold higher than the number of children is not supported."); return false; } - DFTElementPointer element = std::make_shared>(mNextId++, name, threshold); + DFTElementPointer element = std::make_shared>(mNextId++, name, threshold); mElements[name] = element; mChildNames[element] = children; @@ -173,7 +175,7 @@ namespace storm { //failureRate > 0 //0 <= dormancyFactor <= 1 - mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor, transient); + mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor, transient); return true; } @@ -189,7 +191,7 @@ namespace storm { std::string getUniqueName(std::string name); - DFT build(); + storm::storage::DFT build(); /** * Copy element and insert it again in the builder. @@ -211,13 +213,13 @@ namespace storm { unsigned computeRank(DFTElementPointer const& elem); - bool addStandardGate(std::string const& name, std::vector const& children, DFTElementType tp); + bool addStandardGate(std::string const& name, std::vector const& children, storm::storage::DFTElementType tp); - bool addRestriction(std::string const& name, std::vector const& children, DFTElementType tp); + bool addRestriction(std::string const& name, std::vector const& children, storm::storage::DFTElementType tp); enum class topoSortColour {WHITE, BLACK, GREY}; - void topoVisit(DFTElementPointer const& n, std::map>& visited, DFTElementVector& L); + void topoVisit(DFTElementPointer const& n, std::map>& visited, DFTElementVector& L); DFTElementVector topoSort(); diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index ca56f25da..94ef80c67 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -33,7 +33,7 @@ namespace storm { template storm::storage::DFT DFTGalileoParser::parseDFT(const std::string& filename, bool defaultInclusive, bool binaryDependencies) { - storm::storage::DFTBuilder builder(defaultInclusive, binaryDependencies); + storm::builder::DFTBuilder builder(defaultInclusive, binaryDependencies); ValueParser valueParser; // Regular expression to detect comments // taken from: https://stackoverflow.com/questions/9449887/removing-c-c-style-comments-using-boostregex @@ -166,7 +166,7 @@ namespace storm { } template - bool DFTGalileoParser::parseBasicElement(std::vector const& tokens, storm::storage::DFTBuilder& builder, ValueParser& valueParser) { + bool DFTGalileoParser::parseBasicElement(std::vector const& tokens, storm::builder::DFTBuilder& builder, ValueParser& valueParser) { // Default values Distribution distribution = Distribution::None; ValueType firstValDistribution = storm::utility::zero(); diff --git a/src/storm-dft/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h index e8e78244f..c56540edd 100644 --- a/src/storm-dft/parser/DFTGalileoParser.h +++ b/src/storm-dft/parser/DFTGalileoParser.h @@ -7,7 +7,7 @@ #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm-dft/storage/dft/DFT.h" -#include "storm-dft/storage/dft/DFTBuilder.h" +#include "storm-dft/builder/DFTBuilder.h" #include "storm/parser/ValueParser.h" @@ -51,7 +51,7 @@ namespace storm { * * @return True iff the parsing and creation was successful. */ - static bool parseBasicElement(std::vector const& tokens, storm::storage::DFTBuilder& builder, ValueParser& valueParser); + static bool parseBasicElement(std::vector const& tokens, storm::builder::DFTBuilder& builder, ValueParser& valueParser); enum Distribution { None, Constant, Exponential, Weibull, LogNormal }; }; diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h index d23baf58e..5517d85e1 100644 --- a/src/storm-dft/parser/DFTJsonParser.h +++ b/src/storm-dft/parser/DFTJsonParser.h @@ -7,7 +7,7 @@ #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm-dft/storage/dft/DFT.h" -#include "storm-dft/storage/dft/DFTBuilder.h" +#include "storm-dft/builder/DFTBuilder.h" // JSON parser #include "json.hpp" @@ -19,7 +19,7 @@ namespace storm { template class DFTJsonParser { - storm::storage::DFTBuilder builder; + storm::builder::DFTBuilder builder; std::shared_ptr manager; diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 6f5db6a44..81784ea96 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -7,7 +7,7 @@ #include "storm/utility/iota_n.h" #include "storm/utility/vector.h" -#include "storm-dft/storage/dft/DFTBuilder.h" +#include "storm-dft/builder/DFTBuilder.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" @@ -271,7 +271,7 @@ namespace storm { std::vector> res; for(auto const& subdft : subdfts) { - DFTBuilder builder; + storm::builder::DFTBuilder builder; for(size_t id : subdft.second) { builder.copyElement(mElements[id]); @@ -307,7 +307,7 @@ namespace storm { std::vector> rewriteIds; rewriteIds.push_back(modIdea); - DFTBuilder builder; + storm::builder::DFTBuilder builder; // Accumulate elements which must be rewritten std::set rewriteSet; diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 20c42fdb8..c373c8199 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -18,6 +18,11 @@ #include "storm-dft/storage/dft/DFTLayoutInfo.h" namespace storm { + namespace builder { + // Forward declaration + template class DFTBuilder; + } + namespace storage { template @@ -32,11 +37,8 @@ namespace storm { }; - // Forward declarations + // Forward declaration template class DFTColouring; - - template class DFTBuilder; - /** * Represents a Dynamic Fault Tree @@ -76,7 +78,7 @@ namespace storm { DFT optimize() const; - void copyElements(std::vector elements, DFTBuilder builder) const; + void copyElements(std::vector elements, storm::builder::DFTBuilder builder) const; size_t stateVectorSize() const { return mStateVectorSize;