diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index d49bfd067..f6fff39ff 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -61,7 +61,7 @@ namespace storm { } template - bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, DFTElementTypes tp) { + bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, DFTElementType tp) { assert(children.size() > 0); if(mElements.count(name) != 0) { // Element with that name already exists. @@ -69,28 +69,28 @@ namespace storm { } DFTElementPointer element; switch(tp) { - case DFTElementTypes::AND: + case DFTElementType::AND: element = std::make_shared>(mNextId++, name); break; - case DFTElementTypes::OR: + case DFTElementType::OR: element = std::make_shared>(mNextId++, name); break; - case DFTElementTypes::PAND: + case DFTElementType::PAND: element = std::make_shared>(mNextId++, name); break; - case DFTElementTypes::POR: + case DFTElementType::POR: element = std::make_shared>(mNextId++, name); break; - case DFTElementTypes::SPARE: + case DFTElementType::SPARE: element = std::make_shared>(mNextId++, name); break; - case DFTElementTypes::BE: - case DFTElementTypes::VOT: + case DFTElementType::BE: + case DFTElementType::VOT: // Handled separately STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type handled separately."); - case DFTElementTypes::CONSTF: - case DFTElementTypes::CONSTS: - case DFTElementTypes::FDEP: + case DFTElementType::CONSTF: + case DFTElementType::CONSTS: + case DFTElementType::FDEP: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported."); default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known."); diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index 12d5e88c3..0cb0efab5 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -32,23 +32,23 @@ namespace storm { } bool addAndElement(std::string const& name, std::vector const& children) { - return addStandardGate(name, children, DFTElementTypes::AND); + return addStandardGate(name, children, DFTElementType::AND); } bool addOrElement(std::string const& name, std::vector const& children) { - return addStandardGate(name, children, DFTElementTypes::OR); + return addStandardGate(name, children, DFTElementType::OR); } bool addPandElement(std::string const& name, std::vector const& children) { - return addStandardGate(name, children, DFTElementTypes::PAND); + return addStandardGate(name, children, DFTElementType::PAND); } bool addPorElement(std::string const& name, std::vector const& children) { - return addStandardGate(name, children, DFTElementTypes::POR); + return addStandardGate(name, children, DFTElementType::POR); } bool addSpareElement(std::string const& name, std::vector const& children) { - return addStandardGate(name, children, DFTElementTypes::SPARE); + return addStandardGate(name, children, DFTElementType::SPARE); } bool addVotElement(std::string const& name, unsigned threshold, std::vector const& children) { @@ -98,7 +98,7 @@ namespace storm { unsigned computeRank(DFTElementPointer const& elem); - bool addStandardGate(std::string const& name, std::vector const& children, DFTElementTypes tp); + bool addStandardGate(std::string const& name, std::vector const& children, DFTElementType tp); enum class topoSortColour {WHITE, BLACK, GREY}; diff --git a/src/storage/dft/DFTElementType.h b/src/storage/dft/DFTElementType.h new file mode 100644 index 000000000..9aba9fa54 --- /dev/null +++ b/src/storage/dft/DFTElementType.h @@ -0,0 +1,32 @@ +#pragma once + +#include +namespace storm { + namespace storage { + + enum class DFTElementType : int {AND = 0, COUNTING = 1, OR = 2, VOT = 3, BE = 4, CONSTF = 5, CONSTS = 6, PAND = 7, SPARE = 8, POR = 9, FDEP = 10, SEQAND = 11}; + + inline bool isGateType(DFTElementType const& tp) { + switch(tp) { + case DFTElementType::AND: + case DFTElementType::COUNTING: + case DFTElementType::OR: + case DFTElementType::VOT: + case DFTElementType::PAND: + case DFTElementType::SPARE: + case DFTElementType::POR: + case DFTElementType::SEQAND: + return true; + case DFTElementType::BE: + case DFTElementType::CONSTF: + case DFTElementType::CONSTS: + case DFTElementType::FDEP: + return false; + default: + assert(false); + } + } + + } +} + diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index 761975762..d5b089c84 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -31,6 +31,14 @@ namespace storm { } } + template + std::vector DFTElement::independentUnit() const { + std::vector res; + res.push_back(this->id()); + // Extend for pdeps. + return res; + } + template void DFTElement::extendUnit(std::set& unit) const { unit.insert(mId); @@ -62,11 +70,6 @@ namespace storm { } } - template - void DFTElement::checkForSymmetricChildren() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not implemented."); - assert(false); - } template bool DFTBE::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index b047ddbd1..663c5b230 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -8,7 +8,9 @@ #include #include #include +#include +#include "DFTElementType.h" #include "DFTState.h" #include "DFTStateSpaceGenerationQueues.h" #include "src/utility/constants.h" @@ -132,7 +134,7 @@ namespace storm { /** * Computes the independent unit of this element, that is, all elements which are direct or indirect successors of an element. */ - virtual std::vector independentUnit() const = 0; + virtual std::vector independentUnit() const; /** * Helper to independent unit computation @@ -153,33 +155,15 @@ namespace storm { */ virtual void extendSubDft(std::set elemsInSubtree, std::vector const& parentsOfSubRoot) const; - void checkForSymmetricChildren() const; - }; - enum class DFTElementTypes {AND, COUNTING, OR, VOT, BE, CONSTF, CONSTS, PAND, SPARE, POR, FDEP, SEQAND}; - inline bool isGateType(DFTElementTypes const& tp) { - switch(tp) { - case DFTElementTypes::AND: - case DFTElementTypes::COUNTING: - case DFTElementTypes::OR: - case DFTElementTypes::VOT: - case DFTElementTypes::PAND: - case DFTElementTypes::SPARE: - case DFTElementTypes::POR: - case DFTElementTypes::SEQAND: - return true; - case DFTElementTypes::BE: - case DFTElementTypes::CONSTF: - case DFTElementTypes::CONSTS: - case DFTElementTypes::FDEP: - return false; - default: - assert(false); - } - } + protected: + // virtual bool checkIsomorphicSubDftHelper(DFTElement const& otherElem, std::vector>& mapping, std::vector const& order ) const = 0; + + }; + @@ -281,7 +265,6 @@ namespace storm { } - virtual std::string toString() const override { std::stringstream stream; stream << "{" << this->name() << "} " << typestring() << "( "; @@ -304,7 +287,7 @@ namespace storm { return false; } - + protected: void fail(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { @@ -388,12 +371,6 @@ namespace storm { bool isColdBasicElement() const { return storm::utility::isZero(mPassiveFailureRate); } - - virtual std::vector independentUnit() const override { - return {this->mId}; - } - - virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; };