diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index b8e2c54a2..d1d6f320f 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -5,6 +5,8 @@ #include "DFT.h" #include #include "OrderDFTElementsById.h" +#include +#include #include "../../exceptions/WrongFormatException.h" @@ -86,6 +88,16 @@ namespace storm { case DFTElementTypes::SPARE: element = std::make_shared(mNextId++, name); break; + case DFTElementTypes::BE: + case DFTElementTypes::VOT: + // Handled separately + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type handled separately."); + case DFTElementTypes::CONSTF: + case DFTElementTypes::CONSTS: + case DFTElementTypes::FDEP: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported."); + default: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known."); } mElements[name] = element; mChildNames[element] = children; diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index d6245a606..d223387e8 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -145,7 +145,7 @@ namespace storm { return mChildren.push_back(elem); } - size_t nrChildren() const { + size_t nrChildren() const override { return mChildren.size(); } @@ -153,7 +153,7 @@ namespace storm { return mChildren; } - virtual bool isGate() const { + virtual bool isGate() const override { return true; } @@ -172,7 +172,7 @@ namespace storm { } } - virtual std::vector independentUnit() const { + virtual std::vector independentUnit() const override { std::set unit = {mId}; for(auto const& child : mChildren) { child->extendUnit(unit); @@ -187,7 +187,7 @@ namespace storm { - virtual void print(std::ostream& os = std::cout) const { + virtual void print(std::ostream& os = std::cout) const override { os << "{" << name() << "} " << typestring() << "( "; std::vector>::const_iterator it = mChildren.begin(); os << (*it)->name(); @@ -199,7 +199,7 @@ namespace storm { os << ")"; } - virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { if(DFTElement::checkDontCareAnymore(state, queues)) { childrenDontCare(state, queues); return true; @@ -207,7 +207,7 @@ namespace storm { return false; } - virtual void extendUnit(std::set& unit) const { + virtual void extendUnit(std::set& unit) const override { DFTElement::extendUnit(unit); for(auto const& child : mChildren) { child->extendUnit(unit); diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 01534342b..e7756cbbd 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -5,7 +5,7 @@ namespace storm { namespace storage { - DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateSize()), mDft(dft), mId(id) { + DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft) { mInactiveSpares = dft.getSpareIndices(); dft.initializeUses(*this); dft.initializeActivation(*this);