From 6e2f5602e1406bc81d0a731a87c27eec320f0561 Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 18 Dec 2015 14:00:02 +0100 Subject: [PATCH] Finished templating Former-commit-id: 7225717fdbc78fcdad9dbc3b7d4ff1fc14a6b318 --- src/builder/ExplicitDFTModelBuilder.cpp | 22 +- src/builder/ExplicitDFTModelBuilder.h | 7 +- src/storage/dft/DFT.cpp | 10 +- src/storage/dft/DFT.h | 42 +- src/storage/dft/DFTBuilder.cpp | 35 +- src/storage/dft/DFTBuilder.h | 20 +- src/storage/dft/DFTElements.cpp | 33 +- src/storage/dft/DFTElements.h | 438 +++++++++--------- src/storage/dft/DFTState.cpp | 96 ++-- src/storage/dft/DFTState.h | 17 +- .../dft/DFTStateSpaceGenerationQueues.h | 49 +- src/storage/dft/OrderDFTElementsById.cpp | 25 +- src/storage/dft/OrderDFTElementsById.h | 16 +- 13 files changed, 453 insertions(+), 357 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index fb1c5cd33..e039b389f 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -13,10 +13,10 @@ namespace storm { template std::shared_ptr> ExplicitDFTModelBuilder::buildCTMC() { // Initialize - storm::storage::DFTState state(mDft, newIndex++); + storm::storage::DFTState state(mDft, newIndex++); mStates.insert(state); - std::queue stateQueue; + std::queue> stateQueue; stateQueue.push(state); bool deterministicModel = true; @@ -46,7 +46,7 @@ namespace storm { modelComponents.stateLabeling.addLabel(elem->name() + "_fail"); } - for (storm::storage::DFTState state : mStates) { + for (storm::storage::DFTState state : mStates) { if (mDft.hasFailed(state)) { modelComponents.stateLabeling.addLabelToState("failed", state.getId()); } @@ -72,7 +72,7 @@ namespace storm { } template - void ExplicitDFTModelBuilder::exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder) { + void ExplicitDFTModelBuilder::exploreStates(std::queue>& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder) { std::vector> outgoingTransitions; @@ -82,7 +82,7 @@ namespace storm { ValueType sum = 0; // Consider next state - storm::storage::DFTState state = stateQueue.front(); + storm::storage::DFTState state = stateQueue.front(); stateQueue.pop(); size_t smallest = 0; @@ -99,7 +99,7 @@ namespace storm { while (smallest < state.nrFailableBEs()) { STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state)); - storm::storage::DFTState newState(state); + storm::storage::DFTState newState(state); std::pair>, bool> nextBE = newState.letNextBEFail(smallest++); if (nextBE.first == nullptr) { std::cout << "break" << std::endl; @@ -108,26 +108,26 @@ namespace storm { } STORM_LOG_TRACE("with the failure of: " << nextBE.first->name() << " [" << nextBE.first->id() << "]"); - storm::storage::DFTStateSpaceGenerationQueues queues; + storm::storage::DFTStateSpaceGenerationQueues queues; - for (std::shared_ptr parent : nextBE.first->parents()) { + for (DFTGatePointer parent : nextBE.first->parents()) { if (newState.isOperational(parent->id())) { queues.propagateFailure(parent); } } while (!queues.failurePropagationDone()) { - std::shared_ptr next = queues.nextFailurePropagation(); + DFTGatePointer next = queues.nextFailurePropagation(); next->checkFails(newState, queues); } while (!queues.failsafePropagationDone()) { - std::shared_ptr next = queues.nextFailsafePropagation(); + DFTGatePointer next = queues.nextFailsafePropagation(); next->checkFailsafe(newState, queues); } while (!queues.dontCarePropagationDone()) { - std::shared_ptr next = queues.nextDontCarePropagation(); + DFTElementPointer next = queues.nextDontCarePropagation(); next->checkDontCareAnymore(newState, queues); } diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index de3a94293..8148559c3 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -18,6 +18,9 @@ namespace storm { template, typename IndexType = uint32_t> class ExplicitDFTModelBuilder { + using DFTElementPointer = std::shared_ptr>; + using DFTGatePointer = std::shared_ptr>; + // A structure holding the individual components of a model. struct ModelComponents { ModelComponents(); @@ -36,7 +39,7 @@ namespace storm { }; storm::storage::DFT const &mDft; - std::unordered_set mStates; + std::unordered_set> mStates; size_t newIndex = 0; public: @@ -47,7 +50,7 @@ namespace storm { std::shared_ptr> buildCTMC(); private: - void exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder); + void exploreStates(std::queue>& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder); }; } diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 719c59e26..0b8c99685 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -4,7 +4,7 @@ namespace storm { namespace storage { template - DFT::DFT(std::vector> const& elements, std::shared_ptr const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0) + DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0) { assert(elementIndicesCorrect()); @@ -19,7 +19,7 @@ namespace storm { } else if(elem->isSpareGate()) { ++mNrOfSpares; - for(auto const& spareReprs : std::static_pointer_cast(elem)->children()) { + for(auto const& spareReprs : std::static_pointer_cast>(elem)->children()) { if(mActivationIndex.count(spareReprs->id()) == 0) { mActivationIndex[spareReprs->id()] = stateIndex++; } @@ -34,7 +34,7 @@ namespace storm { mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes)); } - std::static_pointer_cast(elem)->setUseIndex(stateIndex); + std::static_pointer_cast>(elem)->setUseIndex(stateIndex); mUsageIndex.insert(std::make_pair(elem->id(), stateIndex)); stateIndex += mUsageInfoBits; @@ -108,7 +108,7 @@ namespace storm { } template - std::string DFT::getElementsWithStateString(DFTState const& state) const{ + std::string DFT::getElementsWithStateString(DFTState const& state) const{ std::stringstream stream; for (auto const& elem : mElements) { stream << "[" << elem->id() << "]"; @@ -126,7 +126,7 @@ namespace storm { } template - std::string DFT::getStateString(DFTState const& state) const{ + std::string DFT::getStateString(DFTState const& state) const{ std::stringstream stream; stream << "(" << state.getId() << ") "; for (auto const& elem : mElements) { diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 068ea4ef1..0f39e3ddc 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -17,8 +17,9 @@ namespace storm { namespace storage { + template struct DFTElementSort { - bool operator()(std::shared_ptr const& a, std::shared_ptr const& b) const { + bool operator()(std::shared_ptr> const& a, std::shared_ptr> const& b) const { if (a->rank() == 0 && b->rank() == 0) { return a->isConstant(); } else { @@ -27,11 +28,18 @@ namespace storm { } }; + + template class DFT { + using DFTElementPointer = std::shared_ptr>; + using DFTElementVector = std::vector; + using DFTGatePointer = std::shared_ptr>; + using DFTGateVector = std::vector; + private: - std::vector> mElements; + DFTElementVector mElements; size_t mNrOfBEs; size_t mNrOfSpares; size_t mTopLevelIndex; @@ -44,9 +52,8 @@ namespace storm { std::map mUsageIndex; public: - DFT(std::vector> const& elements, std::shared_ptr const& tle); - - + DFT(DFTElementVector const& elements, DFTElementPointer const& tle); + size_t stateSize() const { return mStateSize; } @@ -72,15 +79,15 @@ namespace storm { return mIdToFailureIndex[id]; } - void initializeUses(DFTState& state) const { + void initializeUses(DFTState& state) const { for(auto const& elem : mElements) { if(elem->isSpareGate()) { - std::static_pointer_cast(elem)->initializeUses(state); + std::static_pointer_cast>(elem)->initializeUses(state); } } } - void initializeActivation(DFTState& state) const { + void initializeActivation(DFTState& state) const { state.activate(mTopLevelIndex); for(auto const& elem : mTopModule) { if(mElements[elem]->isSpareGate()) { @@ -108,8 +115,7 @@ namespace storm { } } - - void propagateActivation(DFTState& state, size_t representativeId) const { + void propagateActivation(DFTState& state, size_t representativeId) const { state.activate(representativeId); for(size_t id : module(representativeId)) { if(mElements[id]->isSpareGate()) { @@ -120,15 +126,15 @@ namespace storm { std::vector nonColdBEs() const { std::vector result; - for(std::shared_ptr elem : mElements) { + for(DFTElementPointer elem : mElements) { if(elem->isBasicElement() && !elem->isColdBasicElement()) { result.push_back(elem->id()); } } return result; } - - std::shared_ptr const& getElement(size_t index) const { + + DFTElementPointer const& getElement(size_t index) const { assert(index < nrElements()); return mElements[index]; } @@ -140,7 +146,7 @@ namespace storm { std::vector>> getBasicElements() const { std::vector>> elements; - for (std::shared_ptr elem : mElements) { + for (DFTElementPointer elem : mElements) { if (elem->isBasicElement()) { elements.push_back(std::static_pointer_cast>(elem)); } @@ -149,11 +155,11 @@ namespace storm { } - bool hasFailed(DFTState const& state) const { + bool hasFailed(DFTState const& state) const { return state.hasFailed(mTopLevelIndex); } - bool isFailsafe(DFTState const& state) const { + bool isFailsafe(DFTState const& state) const { return state.isFailsafe(mTopLevelIndex); } @@ -163,9 +169,9 @@ namespace storm { std::string getSpareModulesString() const; - std::string getElementsWithStateString(DFTState const& state) const; + std::string getElementsWithStateString(DFTState const& state) const; - std::string getStateString(DFTState const& state) const; + std::string getStateString(DFTState const& state) const; private: bool elementIndicesCorrect() const { diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index ee7676449..870b7f8bf 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -17,7 +17,7 @@ namespace storm { DFT DFTBuilder::build() { for(auto& elem : mChildNames) { for(auto const& child : elem.second) { - std::shared_ptr gate = std::static_pointer_cast(elem.first); + DFTGatePointer gate = std::static_pointer_cast>(elem.first); gate->pushBackChild(mElements[child]); mElements[child]->addParent(gate); } @@ -30,25 +30,25 @@ namespace storm { computeRank(elem.second); } - std::vector> elems = topoSort(); + DFTElementVector elems = topoSort(); size_t id = 0; - for(std::shared_ptr e : elems) { + for(DFTElementPointer e : elems) { e->setId(id++); } return DFT(elems, mElements[topLevelIdentifier]); } template - unsigned DFTBuilder::computeRank(std::shared_ptr const& elem) { + unsigned DFTBuilder::computeRank(DFTElementPointer const& elem) { if(elem->rank() == -1) { if(elem->nrChildren() == 0) { elem->setRank(0); } else { - std::shared_ptr gate = std::static_pointer_cast(elem); + DFTGatePointer gate = std::static_pointer_cast>(elem); unsigned maxrnk = 0; unsigned newrnk = 0; - for (std::shared_ptr const &child : gate->children()) { + for (DFTElementPointer const &child : gate->children()) { newrnk = computeRank(child); if (newrnk > maxrnk) { maxrnk = newrnk; @@ -68,22 +68,22 @@ namespace storm { // Element with that name already exists. return false; } - std::shared_ptr element; + DFTElementPointer element; switch(tp) { case DFTElementTypes::AND: - element = std::make_shared(mNextId++, name); + element = std::make_shared>(mNextId++, name); break; case DFTElementTypes::OR: - element = std::make_shared(mNextId++, name); + element = std::make_shared>(mNextId++, name); break; case DFTElementTypes::PAND: - element = std::make_shared(mNextId++, name); + element = std::make_shared>(mNextId++, name); break; case DFTElementTypes::POR: - element = std::make_shared(mNextId++, name); + element = std::make_shared>(mNextId++, name); break; case DFTElementTypes::SPARE: - element = std::make_shared(mNextId++, name); + element = std::make_shared>(mNextId++, name); break; case DFTElementTypes::BE: case DFTElementTypes::VOT: @@ -102,13 +102,13 @@ namespace storm { } template - void DFTBuilder::topoVisit(std::shared_ptr const& n, std::map, topoSortColour>& visited, std::vector>& 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(std::shared_ptr const& c : std::static_pointer_cast(n)->children()) { + for(DFTElementPointer const& c : std::static_pointer_cast>(n)->children()) { topoVisit(c, visited, L); } } @@ -117,14 +117,15 @@ namespace storm { } } + // TODO Matthias: use typedefs template - std::vector> DFTBuilder::topoSort() { - std::map, topoSortColour> visited; + std::vector>> DFTBuilder::topoSort() { + std::map>, topoSortColour> visited; for(auto const& e : mElements) { visited.insert(std::make_pair(e.second, topoSortColour::WHITE)); } - std::vector> L; + std::vector>> L; for(auto const& e : visited) { topoVisit(e.first, visited, L); } diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index f129afc0b..88fdc6ef0 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -14,11 +14,17 @@ namespace storm { template class DFTBuilder { - + + using DFTElementPointer = std::shared_ptr>; + using DFTElementVector = std::vector; + using DFTGatePointer = std::shared_ptr>; + using DFTGateVector = std::vector; + + private: std::size_t mNextId = 0; std::string topLevelIdentifier; - std::unordered_map> mElements; - std::unordered_map, std::vector> mChildNames; + std::unordered_map mElements; + std::unordered_map> mChildNames; public: DFTBuilder() { @@ -64,7 +70,7 @@ namespace storm { std::cerr << "Voting gates with threshold higher than the number of children is not supported." << std::endl; return false; } - std::shared_ptr element = std::make_shared(mNextId++, name, threshold); + DFTElementPointer element = std::make_shared>(mNextId++, name, threshold); mElements[name] = element; mChildNames[element] = children; @@ -96,15 +102,15 @@ namespace storm { private: - unsigned computeRank(std::shared_ptr const& elem); + unsigned computeRank(DFTElementPointer const& elem); bool addStandardGate(std::string const& name, std::vector const& children, DFTElementTypes tp); enum class topoSortColour {WHITE, BLACK, GREY}; - void topoVisit(std::shared_ptr const& n, std::map, topoSortColour>& visited, std::vector>& L); + void topoVisit(DFTElementPointer const& n, std::map& visited, DFTElementVector& L); - std::vector> topoSort(); + DFTElementVector topoSort(); }; } diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index a9040eab0..0c18e3be6 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -1,11 +1,15 @@ +#include +#include #include "DFTElements.h" namespace storm { namespace storage { - bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + + template + bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { if(!state.dontCare(mId)) { - for(std::shared_ptr const& parent : mParents) { + for(DFTGatePointer const& parent : mParents) { if(state.isOperational(parent->id())) { return false; } @@ -16,8 +20,9 @@ namespace storm { } return false; } - - void DFTElement::extendSpareModule(std::set& elementsInModule) const { + + template + void DFTElement::extendSpareModule(std::set& elementsInModule) const { for(auto const& parent : mParents) { if(elementsInModule.count(parent->id()) == 0 && !parent->isSpareGate()) { elementsInModule.insert(parent->id()); @@ -25,8 +30,9 @@ namespace storm { } } } - - void DFTElement::extendUnit(std::set& unit) const { + + template + void DFTElement::extendUnit(std::set& unit) const { unit.insert(mId); for(auto const& parent : mParents) { if(unit.count(parent->id()) != 0) { @@ -34,20 +40,23 @@ namespace storm { } } } - - void DFTElement::checkForSymmetricChildren() const { - + + 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 { - if(DFTElement::checkDontCareAnymore(state, queues)) { - state.beNoLongerFailable(mId); + bool DFTBE::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + if(DFTElement::checkDontCareAnymore(state, queues)) { + state.beNoLongerFailable(this->mId); return true; } return false; } + // Explicitly instantiate the class. template class DFTBE; diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 7d3c6110c..6296a176f 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -16,21 +16,28 @@ using std::size_t; namespace storm { namespace storage { + + template class DFTGate; - + + template class DFTElement { + + using DFTGatePointer = std::shared_ptr>; + using DFTGateVector = std::vector; + + protected: size_t mId; std::string mName; size_t mRank = -1; - std::vector> mParents; - - - + DFTGateVector mParents; public: - DFTElement(size_t id, std::string const& name) : mId(id), mName(name) + DFTElement(size_t id, std::string const& name) : + mId(id), mName(name) {} + virtual ~DFTElement() {} @@ -74,7 +81,7 @@ namespace storm { return mName; } - bool addParent(std::shared_ptr const& e) { + bool addParent(DFTGatePointer const& e) { if(std::find(mParents.begin(), mParents.end(), e) != mParents.end()) { return false; } @@ -89,20 +96,21 @@ namespace storm { return !mParents.empty(); } - std::vector> const& parents() const { + DFTGateVector const& parents() const { return mParents; } virtual void extendSpareModule(std::set& elementsInModule) const; virtual size_t nrChildren() const = 0; + virtual std::string toString() const = 0; - virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; + virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; virtual std::vector independentUnit() const = 0; - virtual void extendUnit(std::set& unit) const; + virtual void extendUnit(std::set& unit) const; void checkForSymmetricChildren() const; }; @@ -130,26 +138,34 @@ namespace storm { assert(false); } } - - class DFTGate : public DFTElement { + + + + template + class DFTGate : public DFTElement { + + using DFTElementPointer = std::shared_ptr>; + using DFTElementVector = std::vector; + protected: - std::vector> mChildren; + DFTElementVector mChildren; + public: - DFTGate(size_t id, std::string const& name, std::vector> const& children) : - DFTElement(id, name), mChildren(children) + DFTGate(size_t id, std::string const& name, DFTElementVector const& children) : + DFTElement(id, name), mChildren(children) {} virtual ~DFTGate() {} - void pushBackChild(std::shared_ptr elem) { + void pushBackChild(DFTElementPointer elem) { return mChildren.push_back(elem); } size_t nrChildren() const override { return mChildren.size(); } - - std::vector> const& children() const { + + DFTElementVector const& children() const { return mChildren; } @@ -159,11 +175,13 @@ namespace storm { virtual std::string typestring() const = 0; - virtual void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; - virtual void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; + + virtual void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; + + virtual void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; virtual void extendSpareModule(std::set& elementsInSpareModule) const override { - DFTElement::extendSpareModule(elementsInSpareModule); + DFTElement::extendSpareModule(elementsInSpareModule); for(auto const& child : mChildren) { if(elementsInSpareModule.count(child->id()) == 0) { elementsInSpareModule.insert(child->id()); @@ -173,24 +191,22 @@ namespace storm { } virtual std::vector independentUnit() const override { - std::set unit = {mId}; + std::set unit = {this->mId}; for(auto const& child : mChildren) { child->extendUnit(unit); } - for(auto const& parent : mParents) { + for(auto const& parent : this->mParents) { if(unit.count(parent->id()) != 0) { return {}; } } - return std::vector(unit.begin(), unit.end()); - } - - + return std::vector(unit.begin(), unit.end()); + } virtual std::string toString() const override { std::stringstream stream; - stream << "{" << name() << "} " << typestring() << "( "; - std::vector>::const_iterator it = mChildren.begin(); + stream << "{" << this->name() << "} " << typestring() << "( "; + typename DFTElementVector::const_iterator it = mChildren.begin(); stream << (*it)->name(); ++it; while(it != mChildren.end()) { @@ -199,10 +215,10 @@ namespace storm { } stream << ")"; return stream.str(); - } - - virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - if(DFTElement::checkDontCareAnymore(state, queues)) { + } + + virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + if(DFTElement::checkDontCareAnymore(state, queues)) { childrenDontCare(state, queues); return true; } @@ -210,37 +226,37 @@ namespace storm { } virtual void extendUnit(std::set& unit) const override { - DFTElement::extendUnit(unit); + DFTElement::extendUnit(unit); for(auto const& child : mChildren) { child->extendUnit(unit); } } protected: - - void fail(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - for(std::shared_ptr parent : mParents) { + + void fail(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + for(std::shared_ptr parent : this->mParents) { if(state.isOperational(parent->id())) { queues.propagateFailure(parent); } } - state.setFailed(mId); + state.setFailed(this->mId); } - - void failsafe(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - for(std::shared_ptr parent : mParents) { + + void failsafe(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + for(std::shared_ptr parent : this->mParents) { if(state.isOperational(parent->id())) { queues.propagateFailsafe(parent); } } - state.setFailsafe(mId); + state.setFailsafe(this->mId); } - - void childrenDontCare(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + + void childrenDontCare(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { queues.propagateDontCare(mChildren); } - - bool hasFailsafeChild(DFTState& state) const { + + bool hasFailsafeChild(DFTState& state) const { for(auto const& child : mChildren) { if(state.isFailsafe(child->id())) { @@ -249,9 +265,8 @@ namespace storm { } return false; } - - - bool hasFailedChild(DFTState& state) const { + + bool hasFailedChild(DFTState& state) const { for(auto const& child : mChildren) { if(state.hasFailed(child->id())) { return true; @@ -265,17 +280,15 @@ namespace storm { template - class DFTBE : public DFTElement { - + class DFTBE : public DFTElement { ValueType mActiveFailureRate; ValueType mPassiveFailureRate; + public: DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) : - DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate) - { - - } + DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate) + {} virtual size_t nrChildren() const { return 0; @@ -304,9 +317,10 @@ namespace storm { } virtual std::vector independentUnit() const { - return {mId}; + return {this->mId}; } - virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; + + virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; }; template @@ -314,16 +328,17 @@ namespace storm { return os << "{" << be.name() << "} BE(" << be.activeFailureRate() << ", " << be.passiveFailureRate() << ")"; } - - - class DFTConst : public DFTElement { + + template + class DFTConst : public DFTElement { + bool mFailed; + public: - DFTConst(size_t id, std::string const& name, bool failed) : DFTElement(id, name), mFailed(failed) - { - - } + DFTConst(size_t id, std::string const& name, bool failed) : + DFTElement(id, name), mFailed(failed) + {} bool failed() const { return mFailed; @@ -339,96 +354,96 @@ namespace storm { }; - class DFTAnd : public DFTGate { + + + template + class DFTAnd : public DFTGate { public: - DFTAnd(size_t id, std::string const& name, std::vector> const& children = {}) : - DFTGate(id, name, children) + DFTAnd(size_t id, std::string const& name, std::vector>> const& children = {}) : + DFTGate(id, name, children) {} - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - - if(state.isOperational(mId)) { - for(auto const& child : mChildren) + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + if(state.isOperational(this->mId)) { + for(auto const& child : this->mChildren) { if(!state.hasFailed(child->id())) { - return;// false; + return; } } - fail(state, queues); - //return true; - } - //return false; + this->fail(state, queues); + } } - - void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ - assert(hasFailsafeChild(state)); - if(state.isOperational(mId)) { - failsafe(state, queues); - childrenDontCare(state, queues); - //return true; + + void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ + assert(this->hasFailsafeChild(state)); + if(state.isOperational(this->mId)) { + this->failsafe(state, queues); + this->childrenDontCare(state, queues); } - //return false; } std::string typestring() const { return "AND"; } }; - - inline std::ostream& operator<<(std::ostream& os, DFTAnd const& gate) { + + template + inline std::ostream& operator<<(std::ostream& os, DFTAnd const& gate) { return os << gate.toString(); } - + - class DFTOr : public DFTGate { + template + class DFTOr : public DFTGate { + public: - DFTOr(size_t id, std::string const& name, std::vector> const& children = {}) : - DFTGate(id, name, children) + DFTOr(size_t id, std::string const& name, std::vector>> const& children = {}) : + DFTGate(id, name, children) {} - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - assert(hasFailedChild(state)); - if(state.isOperational(mId)) { - fail(state, queues); - //return true; - } - // return false; + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + assert(this->hasFailedChild(state)); + if(state.isOperational(this->mId)) { + this->fail(state, queues); + } } - - void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ - for(auto const& child : mChildren) { + + void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ + for(auto const& child : this->mChildren) { if(!state.isFailsafe(child->id())) { - return;// false; + return; } } - failsafe(state, queues); - //return true; + this->failsafe(state, queues); } std::string typestring() const { return "OR"; } - private: - //static const std::string typestring = "or"; }; - - inline std::ostream& operator<<(std::ostream& os, DFTOr const& gate) { + + template + inline std::ostream& operator<<(std::ostream& os, DFTOr const& gate) { return os << gate.toString(); } - class DFTSeqAnd : public DFTGate { + + + template + class DFTSeqAnd : public DFTGate { + public: - DFTSeqAnd(size_t id, std::string const& name, std::vector> const& children = {}) : - DFTGate(id, name, children) + DFTSeqAnd(size_t id, std::string const& name, std::vector>> const& children = {}) : + DFTGate(id, name, children) {} - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - - if(!state.hasFailed(mId)) { + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + if(!state.hasFailed(this->mId)) { bool childOperationalBefore = false; - for(auto const& child : mChildren) + for(auto const& child : this->mChildren) { if(!state.hasFailed(child->id())) { childOperationalBefore = true; @@ -436,22 +451,20 @@ namespace storm { else { if(childOperationalBefore) { state.markAsInvalid(); - return; //false; + return; } } } if(!childOperationalBefore) { fail(state, queues); - //return true; } } - //return false; } - - void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ + + void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ assert(hasFailsafeChild(state)); - if(state.isOperational(mId)) { + if(state.isOperational(this->mId)) { failsafe(state, queues); //return true; } @@ -461,71 +474,74 @@ namespace storm { std::string typestring() const { return "SEQAND"; } - private: - //static const std::string typestring = "seqand"; }; - - inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd const& gate) { + + template + inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd const& gate) { return os << gate.toString(); } - - class DFTPand : public DFTGate { + + + + template + class DFTPand : public DFTGate { + public: - DFTPand(size_t id, std::string const& name, std::vector> const& children = {}) : - DFTGate(id, name, children) + DFTPand(size_t id, std::string const& name, std::vector>> const& children = {}) : + DFTGate(id, name, children) {} - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - if(state.isOperational(mId)) { + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + if(state.isOperational(this->mId)) { bool childOperationalBefore = false; - for(auto const& child : mChildren) + for(auto const& child : this->mChildren) { if(!state.hasFailed(child->id())) { childOperationalBefore = true; } else if(childOperationalBefore && state.hasFailed(child->id())){ - failsafe(state, queues); - childrenDontCare(state, queues); - return; //false; + this->failsafe(state, queues); + this->childrenDontCare(state, queues); + return; } } if(!childOperationalBefore) { - fail(state, queues); - //return true; + this->fail(state, queues); } } - // return false; } - - void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ - assert(hasFailsafeChild(state)); - if(state.isOperational(mId)) { - failsafe(state, queues); - childrenDontCare(state, queues); - //return true; + + void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ + assert(this->hasFailsafeChild(state)); + if(state.isOperational(this->mId)) { + this->failsafe(state, queues); + this->childrenDontCare(state, queues); } - //return false; - } + } std::string typestring() const { return "PAND"; } }; - inline std::ostream& operator<<(std::ostream& os, DFTPand const& gate) { + template + inline std::ostream& operator<<(std::ostream& os, DFTPand const& gate) { return os << gate.toString(); } - - class DFTPor : public DFTGate { + + + + template + class DFTPor : public DFTGate { public: - DFTPor(size_t id, std::string const& name, std::vector> const& children = {}) : - DFTGate(id, name, children) + DFTPor(size_t id, std::string const& name, std::vector>> const& children = {}) : + DFTGate(id, name, children) {} - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { assert(false); } - - void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ + + void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ assert(false); } @@ -533,58 +549,60 @@ namespace storm { return "POR"; } }; - - inline std::ostream& operator<<(std::ostream& os, DFTPor const& gate) { + + template + inline std::ostream& operator<<(std::ostream& os, DFTPor const& gate) { return os << gate.toString(); } - class DFTVot : public DFTGate { + + + template + class DFTVot : public DFTGate { + private: unsigned mThreshold; + public: - DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector> const& children = {}) : - DFTGate(id, name, children), mThreshold(threshold) + DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector>> const& children = {}) : + DFTGate(id, name, children), mThreshold(threshold) {} - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - - if(state.isOperational(mId)) { + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + if(state.isOperational(this->mId)) { unsigned nrFailedChildren = 0; - for(auto const& child : mChildren) + for(auto const& child : this->mChildren) { if(state.hasFailed(child->id())) { ++nrFailedChildren; if(nrFailedChildren >= mThreshold) { - fail(state, queues); - return;// true; + this->fail(state, queues); + return; } } } } - // return false; - } - - void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ - assert(hasFailsafeChild(state)); - if(state.isOperational(mId)) { + + void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ + assert(this->hasFailsafeChild(state)); + if(state.isOperational(this->mId)) { unsigned nrFailsafeChildren = 0; - for(auto const& child : mChildren) + for(auto const& child : this->mChildren) { if(state.isFailsafe(child->id())) { ++nrFailsafeChildren; - if(nrFailsafeChildren > nrChildren() - mThreshold) + if(nrFailsafeChildren > this->nrChildren() - mThreshold) { - failsafe(state, queues); - childrenDontCare(state, queues); - return;// true; + this->failsafe(state, queues); + this->childrenDontCare(state, queues); + return; } } } } - //return false; } std::string typestring() const { @@ -593,21 +611,24 @@ namespace storm { }; - inline std::ostream& operator<<(std::ostream& os, DFTVot const& gate) { + template + inline std::ostream& operator<<(std::ostream& os, DFTVot const& gate) { return os << gate.toString(); - } - - class DFTSpare : public DFTGate { + } + + + + template + class DFTSpare : public DFTGate { + + private: size_t mUseIndex; size_t mActiveIndex; public: - DFTSpare(size_t id, std::string const& name, std::vector> const& children = {}) : - DFTGate(id, name, children) - { - - } - + DFTSpare(size_t id, std::string const& name, std::vector>> const& children = {}) : + DFTGate(id, name, children) + {} std::string typestring() const { return "SPARE"; @@ -624,39 +645,40 @@ namespace storm { void setActiveIndex(size_t activeIndex) { mActiveIndex = activeIndex; } - - void initializeUses(storm::storage::DFTState& state) { - assert(mChildren.size() > 0); - state.setUsesAtPosition(mUseIndex, mChildren[0]->id()); + + void initializeUses(storm::storage::DFTState& state) { + assert(this->mChildren.size() > 0); + state.setUsesAtPosition(mUseIndex, this->mChildren[0]->id()); } - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - if(state.isOperational(mId)) { + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + if(state.isOperational(this->mId)) { size_t uses = state.extractUses(mUseIndex); if(!state.isOperational(uses)) { // TODO compute children ids before. std::vector childrenIds; - for(auto const& child : mChildren) { + for(auto const& child : this->mChildren) { childrenIds.push_back(child->id()); } - bool claimingSuccessful = state.claimNew(mId, mUseIndex, uses, childrenIds); + bool claimingSuccessful = state.claimNew(this->mId, mUseIndex, uses, childrenIds); if(!claimingSuccessful) { - fail(state, queues); + this->fail(state, queues); } } } } - - void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - if(state.isOperational(mId)) { + + void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + if(state.isOperational(this->mId)) { if(state.isFailsafe(state.extractUses((mUseIndex)))) { - failsafe(state, queues); - childrenDontCare(state, queues); + this->failsafe(state, queues); + this->childrenDontCare(state, queues); } } } }; + } } diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 87838b9a2..98cada93a 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -5,8 +5,8 @@ namespace storm { namespace storage { - // TODO Matthias: template - DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft) { + template + DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft) { mInactiveSpares = dft.getSpareIndices(); dft.initializeUses(*this); dft.initializeActivation(*this); @@ -14,70 +14,83 @@ namespace storm { mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); } - - DFTElementState DFTState::getElementState(size_t id) const { + + template + DFTElementState DFTState::getElementState(size_t id) const { return static_cast(getElementStateInt(id)); } - int DFTState::getElementStateInt(size_t id) const { + template + int DFTState::getElementStateInt(size_t id) const { return mStatus.getAsInt(mDft.failureIndex(id), 2); } - size_t DFTState::getId() const { + template + size_t DFTState::getId() const { return mId; } - void DFTState::setId(size_t id) { + template + void DFTState::setId(size_t id) { mId = id; } - bool DFTState::isOperational(size_t id) const { + template + bool DFTState::isOperational(size_t id) const { return getElementState(id) == DFTElementState::Operational; } - bool DFTState::hasFailed(size_t id) const { + template + bool DFTState::hasFailed(size_t id) const { return mStatus[mDft.failureIndex(id)]; } - bool DFTState::isFailsafe(size_t id) const { + template + bool DFTState::isFailsafe(size_t id) const { return mStatus[mDft.failureIndex(id)+1]; } - bool DFTState::dontCare(size_t id) const { + template + bool DFTState::dontCare(size_t id) const { return getElementState(id) == DFTElementState::DontCare; } - void DFTState::setFailed(size_t id) { + template + void DFTState::setFailed(size_t id) { mStatus.set(mDft.failureIndex(id)); } - void DFTState::setFailsafe(size_t id) { + template + void DFTState::setFailsafe(size_t id) { mStatus.set(mDft.failureIndex(id)+1); } - void DFTState::setDontCare(size_t id) { + template + void DFTState::setDontCare(size_t id) { mStatus.setFromInt(mDft.failureIndex(id), 2, static_cast(DFTElementState::DontCare) ); } - - void DFTState::beNoLongerFailable(size_t id) { + + template + void DFTState::beNoLongerFailable(size_t id) { auto it = std::find(mIsCurrentlyFailableBE.begin(), mIsCurrentlyFailableBE.end(), id); if(it != mIsCurrentlyFailableBE.end()) { mIsCurrentlyFailableBE.erase(it); } } - // TODO Matthias: template - std::pair>, bool> DFTState::letNextBEFail(size_t index) + template + std::pair>, bool> DFTState::letNextBEFail(size_t index) { assert(index < mIsCurrentlyFailableBE.size()); STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); - std::pair>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false); + std::pair>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false); mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index); setFailed(res.first->id()); return res; } - - void DFTState::activate(size_t repr) { + + template + void DFTState::activate(size_t repr) { std::vector const& module = mDft.module(repr); for(size_t elem : module) { if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) { @@ -89,33 +102,37 @@ namespace storm { } } } - - - bool DFTState::isActiveSpare(size_t id) const { + + template + bool DFTState::isActiveSpare(size_t id) const { assert(mDft.getElement(id)->isSpareGate()); return (std::find(mInactiveSpares.begin(), mInactiveSpares.end(), id) == mInactiveSpares.end()); } - - uint_fast64_t DFTState::uses(size_t id) const { + + template + uint_fast64_t DFTState::uses(size_t id) const { return extractUses(mDft.usageIndex(id)); } - - uint_fast64_t DFTState::extractUses(size_t from) const { + + template + uint_fast64_t DFTState::extractUses(size_t from) const { assert(mDft.usageInfoBits() < 64); return mStatus.getAsInt(from, mDft.usageInfoBits()); } - - bool DFTState::isUsed(size_t child) { + + template + bool DFTState::isUsed(size_t child) { return (std::find(mUsedRepresentants.begin(), mUsedRepresentants.end(), child) != mUsedRepresentants.end()); - } - - void DFTState::setUsesAtPosition(size_t usageIndex, size_t child) { + + template + void DFTState::setUsesAtPosition(size_t usageIndex, size_t child) { mStatus.setFromInt(usageIndex, mDft.usageInfoBits(), child); mUsedRepresentants.push_back(child); } - - bool DFTState::claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector const& childIds) { + + template + bool DFTState::claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector const& childIds) { auto it = find(childIds.begin(), childIds.end(), currentlyUses); assert(it != childIds.end()); ++it; @@ -132,5 +149,12 @@ namespace storm { return false; } + // Explicitly instantiate the class. + template class DFTState; + +#ifdef STORM_HAVE_CARL + template class DFTState; +#endif + } -} +} \ No newline at end of file diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 1e8f8cb01..4f25550b0 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -14,7 +14,7 @@ namespace storm { template class DFTBE; - + template class DFTState { friend struct std::hash; private: @@ -24,12 +24,10 @@ namespace storm { std::vector mIsCurrentlyFailableBE; std::vector mUsedRepresentants; bool mValid = true; - // TODO Matthias: template - const DFT& mDft; + const DFT& mDft; public: - // TODO Matthias: template - DFTState(DFT const& dft, size_t id); + DFTState(DFT const& dft, size_t id); DFTElementState getElementState(size_t id) const; @@ -109,8 +107,7 @@ namespace storm { return mIsCurrentlyFailableBE.size(); } - // TODO Matthias: template - std::pair>, bool> letNextBEFail(size_t smallestIndex = 0); + std::pair>, bool> letNextBEFail(size_t smallestIndex = 0); std::string getCurrentlyFailableString() { std::stringstream stream; @@ -137,9 +134,9 @@ namespace storm { } namespace std { - template<> - struct hash { - size_t operator()(storm::storage::DFTState const& s) const { + template + struct hash> { + size_t operator()(storm::storage::DFTState const& s) const { return hash()(s.mStatus); } }; diff --git a/src/storage/dft/DFTStateSpaceGenerationQueues.h b/src/storage/dft/DFTStateSpaceGenerationQueues.h index ec0879d52..b881a220b 100644 --- a/src/storage/dft/DFTStateSpaceGenerationQueues.h +++ b/src/storage/dft/DFTStateSpaceGenerationQueues.h @@ -10,19 +10,28 @@ namespace storm { namespace storage { + + template class DFTGate; + template class DFTElement; - - - + + + template class DFTStateSpaceGenerationQueues { - std::priority_queue, std::vector>, OrderElementsByRank> failurePropagation; - std::vector> failsafePropagation; - std::vector> dontcarePropagation; - std::vector> activatePropagation; + + using DFTElementPointer = std::shared_ptr>; + using DFTElementVector = std::vector; + using DFTGatePointer = std::shared_ptr>; + using DFTGateVector = std::vector; + + std::priority_queue> failurePropagation; + DFTGateVector failsafePropagation; + DFTElementVector dontcarePropagation; + DFTElementVector activatePropagation; public: - void propagateFailure(std::shared_ptr const& elem) { + void propagateFailure(DFTGatePointer const& elem) { failurePropagation.push(elem); } @@ -30,8 +39,8 @@ namespace storm { return failurePropagation.empty(); } - std::shared_ptr nextFailurePropagation() { - std::shared_ptr next = failurePropagation.top(); + DFTGatePointer nextFailurePropagation() { + DFTGatePointer next = failurePropagation.top(); failurePropagation.pop(); return next; } @@ -40,12 +49,12 @@ namespace storm { return failsafePropagation.empty(); } - void propagateFailsafe(std::shared_ptr const& gate) { + void propagateFailsafe(DFTGatePointer const& gate) { failsafePropagation.push_back(gate); } - - std::shared_ptr nextFailsafePropagation() { - std::shared_ptr next = failsafePropagation.back(); + + DFTGatePointer nextFailsafePropagation() { + DFTGatePointer next = failsafePropagation.back(); failsafePropagation.pop_back(); return next; } @@ -54,25 +63,23 @@ namespace storm { return dontcarePropagation.empty(); } - void propagateDontCare(std::shared_ptr const& elem) { + void propagateDontCare(DFTElementPointer const& elem) { dontcarePropagation.push_back(elem); } - void propagateDontCare(std::vector> const& elems) { + void propagateDontCare(DFTElementVector const& elems) { dontcarePropagation.insert(dontcarePropagation.end(), elems.begin(), elems.end()); } - std::shared_ptr nextDontCarePropagation() { - std::shared_ptr next = dontcarePropagation.back(); + DFTElementPointer nextDontCarePropagation() { + DFTElementPointer next = dontcarePropagation.back(); dontcarePropagation.pop_back(); return next; } }; + } - } - - #endif /* DFTSTATESPACEGENERATIONQUEUES_H */ diff --git a/src/storage/dft/OrderDFTElementsById.cpp b/src/storage/dft/OrderDFTElementsById.cpp index 017969848..6c9493bee 100644 --- a/src/storage/dft/OrderDFTElementsById.cpp +++ b/src/storage/dft/OrderDFTElementsById.cpp @@ -3,16 +3,31 @@ namespace storm { namespace storage { - bool OrderElementsById::operator()(std::shared_ptr const& a , std::shared_ptr const& b) const { + + template + bool OrderElementsById::operator()(std::shared_ptr> const& a , std::shared_ptr> const& b) const { return a->id() < b->id(); } - bool OrderElementsById::operator ()(const std::shared_ptr& a, const std::shared_ptr& b) const { + + template + bool OrderElementsById::operator ()(const std::shared_ptr>& a, const std::shared_ptr>& b) const { return a->id() < b->id(); } - - - bool OrderElementsByRank::operator ()(const std::shared_ptr& a, const std::shared_ptr& b) const { + + + template + bool OrderElementsByRank::operator ()(const std::shared_ptr>& a, const std::shared_ptr>& b) const { return a->rank() < b->rank(); } + + + // Explicitly instantiate the class. + template class OrderElementsById; + template class OrderElementsByRank; + +#ifdef STORM_HAVE_CARL + template class OrderElementsById; + template class OrderElementsByRank; +#endif } } diff --git a/src/storage/dft/OrderDFTElementsById.h b/src/storage/dft/OrderDFTElementsById.h index 8dfc22da0..821a2de45 100644 --- a/src/storage/dft/OrderDFTElementsById.h +++ b/src/storage/dft/OrderDFTElementsById.h @@ -5,16 +5,22 @@ namespace storm { namespace storage { + + template class DFTGate; + template class DFTElement; - + + template struct OrderElementsById { - bool operator()(std::shared_ptr const& a , std::shared_ptr const& b) const; - bool operator()(std::shared_ptr const& a, std::shared_ptr const& b) const; + bool operator()(std::shared_ptr> const& a , std::shared_ptr> const& b) const; + + bool operator()(std::shared_ptr> const& a, std::shared_ptr> const& b) const; }; - + + template struct OrderElementsByRank { - bool operator()(std::shared_ptr const& a, std::shared_ptr const& b) const; + bool operator()(std::shared_ptr> const& a, std::shared_ptr> const& b) const; }; }