diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index 408a7a535..9762def61 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -15,6 +15,7 @@
#include "SymmetricUnits.h"
#include "../../utility/math.h"
#include "src/utility/macros.h"
+#include "DFTStateGenerationInfo.h"
namespace storm {
namespace storage {
@@ -35,96 +36,6 @@ namespace storm {
template<typename T> class DFTColouring;
- class DFTStateGenerationInfo {
- private:
- const size_t mUsageInfoBits;
- std::map<size_t, size_t> mSpareUsageIndex; // id spare -> index first bit in state
- std::map<size_t, size_t> mSpareActivationIndex; // id spare representative -> index in state
- std::vector<size_t> mIdToStateIndex; // id -> index first bit in state
- std::map<size_t, size_t> mRestrictedItems;
- std::vector<std::pair<size_t, std::vector<size_t>>> mSymmetries; // pair (lenght of symmetry group, vector indicating the starting points of the symmetry groups)
-
- public:
-
- DFTStateGenerationInfo(size_t nrElements, size_t maxSpareChildCount) : mUsageInfoBits(storm::utility::math::uint64_log2(maxSpareChildCount) + 1), mIdToStateIndex(nrElements) {
- assert(maxSpareChildCount < pow(2, mUsageInfoBits));
- }
-
- size_t usageInfoBits() const {
- return mUsageInfoBits;
- }
-
- void addStateIndex(size_t id, size_t index) {
- assert(id < mIdToStateIndex.size());
- mIdToStateIndex[id] = index;
- }
-
- void addSpareActivationIndex(size_t id, size_t index) {
- mSpareActivationIndex[id] = index;
- }
-
- void addSpareUsageIndex(size_t id, size_t index) {
- mSpareUsageIndex[id] = index;
- }
-
- size_t getStateIndex(size_t id) const {
- assert(id < mIdToStateIndex.size());
- return mIdToStateIndex[id];
- }
-
- size_t getSpareUsageIndex(size_t id) const {
- assert(mSpareUsageIndex.count(id) > 0);
- return mSpareUsageIndex.at(id);
- }
-
- size_t getSpareActivationIndex(size_t id) const {
- assert(mSpareActivationIndex.count(id) > 0);
- return mSpareActivationIndex.at(id);
- }
-
- void addSymmetry(size_t length, std::vector<size_t>& startingIndices) {
- mSymmetries.push_back(std::make_pair(length, startingIndices));
- }
-
- size_t getSymmetrySize() const {
- return mSymmetries.size();
- }
-
- size_t getSymmetryLength(size_t pos) const {
- assert(pos < mSymmetries.size());
- return mSymmetries[pos].first;
- }
-
- std::vector<size_t> const& getSymmetryIndices(size_t pos) const {
- assert(pos < mSymmetries.size());
- return mSymmetries[pos].second;
- }
-
- friend std::ostream& operator<<(std::ostream& os, DFTStateGenerationInfo const& info) {
- os << "Id to state index:" << std::endl;
- for (size_t id = 0; id < info.mIdToStateIndex.size(); ++id) {
- os << id << " -> " << info.getStateIndex(id) << std::endl;
- }
- os << "Spare usage index with usage InfoBits of size " << info.mUsageInfoBits << ":" << std::endl;
- for (auto pair : info.mSpareUsageIndex) {
- os << pair.first << " -> " << pair.second << std::endl;
- }
- os << "Spare activation index:" << std::endl;
- for (auto pair : info.mSpareActivationIndex) {
- os << pair.first << " -> " << pair.second << std::endl;
- }
- os << "Symmetries:" << std::endl;
- for (auto pair : info.mSymmetries) {
- os << "Length: " << pair.first << ", starting indices: ";
- for (size_t index : pair.second) {
- os << index << ", ";
- }
- os << std::endl;
- }
- return os;
- }
-
- };
/**
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index dc07505bd..49bc5cc53 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -1,1024 +1,12 @@
-#ifndef DFTELEMENTS_H
-#define DFTELEMENTS_H
-
-#include <set>
-#include <vector>
-#include <memory>
-#include <string>
-#include <cassert>
-#include <cstdlib>
-#include <iostream>
-#include <functional>
-
-#include "DFTElementType.h"
-#include "DFTState.h"
-#include "DFTStateSpaceGenerationQueues.h"
-#include "src/utility/constants.h"
-#include "src/adapters/CarlAdapter.h"
-
-using std::size_t;
-
-namespace storm {
- namespace storage {
-
- template<typename ValueType>
- class DFTGate;
-
- template<typename ValueType>
- class DFTDependency;
- template<typename ValueType>
- class DFTRestriction;
-
- template<typename ValueType>
- class DFTElement {
-
- using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
- using DFTGateVector = std::vector<DFTGatePointer>;
- using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
- using DFTDependencyVector = std::vector<DFTDependencyPointer>;
- using DFTRestrictionPointer = std::shared_ptr<DFTRestriction<ValueType>>;
- using DFTRestrictionVector = std::vector<DFTRestrictionPointer>;
-
-
- protected:
- size_t mId;
- std::string mName;
- size_t mRank = -1;
- DFTGateVector mParents;
- DFTDependencyVector mOutgoingDependencies;
- DFTRestrictionVector mRestrictions;
-
-
- public:
- DFTElement(size_t id, std::string const& name) :
- mId(id), mName(name)
- {}
-
- virtual ~DFTElement() {}
-
- /**
- * Returns the id
- */
- virtual size_t id() const {
- return mId;
- }
-
- virtual DFTElementType type() const = 0;
-
- virtual void setRank(size_t rank) {
- mRank = rank;
- }
-
- virtual size_t rank() const {
- return mRank;
- }
-
- virtual bool isConstant() const {
- return false;
- }
-
- virtual bool isGate() const {
- return false;
- }
-
- /**
- * Returns true if the element is a BE
- */
- virtual bool isBasicElement() const {
- return false;
- }
-
- virtual bool isColdBasicElement() const {
- return false;
- }
-
- /**
- * Returns true if the element is a spare gate
- */
- virtual bool isSpareGate() const {
- return false;
- }
-
- virtual bool isDependency() const {
- return false;
- }
-
- virtual bool isRestriction() const {
- return false;
- }
-
- virtual void setId(size_t newId) {
- mId = newId;
- }
-
- /**
- * Returns the name
- */
- virtual std::string const& name() const {
- return mName;
- }
-
- bool addParent(DFTGatePointer const& e) {
- if(std::find(mParents.begin(), mParents.end(), e) != mParents.end()) {
- return false;
- }
- else
- {
- mParents.push_back(e);
- return true;
- }
- }
-
- bool addRestriction(DFTRestrictionPointer const& e) {
- if (std::find(mRestrictions.begin(), mRestrictions.end(), e) != mRestrictions.end()) {
- return false;
- } else {
- mRestrictions.push_back(e);
- return true;
- }
- }
-
- bool hasOnlyStaticParents() const {
- for(auto const& parent : mParents) {
- if(!isStaticGateType(parent->type())) {
- return false;
- }
- }
- return true;
- }
-
-
- bool hasParents() const {
- return !mParents.empty();
- }
-
- size_t nrParents() const {
- return mParents.size();
- }
-
- DFTGateVector const& parents() const {
- return mParents;
- }
-
- bool hasRestrictions() const {
- return !mRestrictions.empty();
- }
-
- size_t nrRestrictions() const {
- return mRestrictions.size();
- }
-
- DFTRestrictionVector const& restrictions() const {
- return mRestrictions;
- }
-
- std::vector<size_t> parentIds() const {
- std::vector<size_t> res;
- for(auto parent : parents()) {
- res.push_back(parent->id());
- }
- return res;
- }
-
- bool addOutgoingDependency(DFTDependencyPointer const& e) {
- assert(e->triggerEvent()->id() == this->id());
- if(std::find(mOutgoingDependencies.begin(), mOutgoingDependencies.end(), e) != mOutgoingDependencies.end()) {
- return false;
- }
- else
- {
- mOutgoingDependencies.push_back(e);
- return true;
- }
- }
-
- bool hasOutgoingDependencies() const {
- return !mOutgoingDependencies.empty();
- }
-
- size_t nrOutgoingDependencies() const {
- return mOutgoingDependencies.size();
- }
-
- std::set<DFTElement<ValueType>> restrictedItems() const {
- std::set<DFTElement<ValueType>> result;
- for(auto const& restr : mRestrictions) {
- bool foundThis = false;
- for(auto const& child : restr->children()) {
- if(!foundThis) {
- if(child->id() == mId) {
- foundThis = true;
- }
- } else if(result.count(child) == 0) {
- result.insert(child);
- }
- }
- }
- }
-
- std::set<DFTElement<ValueType>> restrictedItemsTC() const {
- std::set<DFTElement<ValueType>> result;
- for(auto const& restr : mRestrictions) {
- bool foundThis = false;
- for(auto const& child : restr->children()) {
- if(!foundThis) {
- if(child->id() == mId) {
- foundThis = true;
- }
- } else if(result.count(child) == 0) {
- result.insert(child);
- std::set<DFTElement<ValueType>> tmpRes = child->restrictedItemsTC();
- result.insert(tmpRes.begin(), tmpRes.end());
- }
- }
- }
- }
-
- DFTDependencyVector const& outgoingDependencies() const {
- return mOutgoingDependencies;
- }
-
- virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
-
- // virtual void extendImmediateFailureCausePathEvents(std::set<size_t>& ) const;
-
- virtual size_t nrChildren() const = 0;
-
- virtual std::string toString() const = 0;
-
- virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const;
-
- /**
- * Computes the independent unit of this element, that is, all elements which are direct or indirect successors of an element.
- */
- virtual std::vector<size_t> independentUnit() const;
-
- /**
- * Helper to independent unit computation
- * @see independentUnit
- */
- virtual void extendUnit(std::set<size_t>& unit) const;
-
- /**
- * Computes independent subtrees starting with this element (this), that is, all elements (x) which are connected to either
- * - one of the children of the element,
- * - a probabilistic dependency
- * such that there exists a path from x to a child of this does not go through this.
- */
- virtual std::vector<size_t> independentSubDft(bool blockParents) const;
- /**
- * Helper to the independent subtree computation
- * @see independentSubDft
- */
- virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const;
-
- virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const {
- return type() == other.type();
- }
-
-
- protected:
- // virtual bool checkIsomorphicSubDftHelper(DFTElement const& otherElem, std::vector<std::pair<DFTElement const&, DFTElement const&>>& mapping, std::vector<DFTElement const&> const& order ) const = 0;
-
- };
-
-
-
-
- template<typename ValueType>
- class DFTGate : public DFTElement<ValueType> {
-
- using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
- using DFTElementVector = std::vector<DFTElementPointer>;
-
- protected:
- DFTElementVector mChildren;
-
- public:
- DFTGate(size_t id, std::string const& name, DFTElementVector const& children) :
- DFTElement<ValueType>(id, name), mChildren(children)
- {}
-
- virtual ~DFTGate() {}
-
- void pushBackChild(DFTElementPointer elem) {
- return mChildren.push_back(elem);
- }
-
- size_t nrChildren() const override {
- return mChildren.size();
- }
-
- DFTElementVector const& children() const {
- return mChildren;
- }
-
- virtual bool isGate() const override {
- return true;
- }
-
-
- virtual std::string typestring() const = 0;
-
- virtual void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
-
- virtual void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
-
- virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
- if (!this->isSpareGate()) {
- DFTElement<ValueType>::extendSpareModule(elementsInSpareModule);
- for( auto const& child : mChildren) {
- if(elementsInSpareModule.count(child->id()) == 0) {
- elementsInSpareModule.insert(child->id());
- child->extendSpareModule(elementsInSpareModule);
- }
- }
- }
- }
-
- virtual std::vector<size_t> independentUnit() const override {
- std::set<size_t> unit = {this->mId};
- for(auto const& child : mChildren) {
- child->extendUnit(unit);
- }
- return std::vector<size_t>(unit.begin(), unit.end());
- }
-
- virtual void extendUnit(std::set<size_t>& unit) const override {
- DFTElement<ValueType>::extendUnit(unit);
- for(auto const& child : mChildren) {
- child->extendUnit(unit);
- }
- }
-
- virtual std::vector<size_t> independentSubDft(bool blockParents) const override {
- auto prelRes = DFTElement<ValueType>::independentSubDft(blockParents);
- if(prelRes.empty()) {
- // No elements (especially not this->id) in the prelimanry result, so we know already that it is not a subdft.
- return prelRes;
- }
- std::set<size_t> unit(prelRes.begin(), prelRes.end());
- std::vector<size_t> pids = this->parentIds();
- for(auto const& child : mChildren) {
- child->extendSubDft(unit, pids, blockParents);
- if(unit.empty()) {
- // Parent in the subdft, ie it is *not* a subdft
- break;
- }
- }
- return std::vector<size_t>(unit.begin(), unit.end());
- }
-
- virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
- if(elemsInSubtree.count(this->id()) > 0) return;
- DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
- if(elemsInSubtree.empty()) {
- // Parent in the subdft, ie it is *not* a subdft
- return;
- }
- for(auto const& child : mChildren) {
- child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
- if(elemsInSubtree.empty()) {
- // Parent in the subdft, ie it is *not* a subdft
- return;
- }
- }
- }
-
-
- virtual std::string toString() const override {
- std::stringstream stream;
- stream << "{" << this->name() << "} " << typestring() << "( ";
- typename DFTElementVector::const_iterator it = mChildren.begin();
- stream << (*it)->name();
- ++it;
- while(it != mChildren.end()) {
- stream << ", " << (*it)->name();
- ++it;
- }
- stream << ")";
- return stream.str();
- }
-
- virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- if(DFTElement<ValueType>::checkDontCareAnymore(state, queues)) {
- childrenDontCare(state, queues);
- return true;
- }
- return false;
- }
-
-
- protected:
-
- void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
- for(std::shared_ptr<DFTGate> parent : this->mParents) {
- if(state.isOperational(parent->id())) {
- queues.propagateFailure(parent);
- }
- }
- for(std::shared_ptr<DFTRestriction<ValueType>> restr : this->mRestrictions) {
- queues.checkRestrictionLater(restr);
- }
- state.setFailed(this->mId);
- this->childrenDontCare(state, queues);
- }
-
- void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
- for(std::shared_ptr<DFTGate> parent : this->mParents) {
- if(state.isOperational(parent->id())) {
- queues.propagateFailsafe(parent);
- }
- }
- state.setFailsafe(this->mId);
- this->childrenDontCare(state, queues);
- }
-
- void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
- queues.propagateDontCare(mChildren);
- }
-
- bool hasFailsafeChild(DFTState<ValueType>& state) const {
- for(auto const& child : mChildren) {
- if(state.isFailsafe(child->id()))
- {
- return true;
- }
- }
- return false;
- }
-
- bool hasFailedChild(DFTState<ValueType>& state) const {
- for(auto const& child : mChildren) {
- if(state.hasFailed(child->id())) {
- return true;
- }
- }
- return false;
- }
-
- };
-
-
-
- template<typename ValueType>
- class DFTBE : public DFTElement<ValueType> {
-
- using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
- using DFTDependencyVector = std::vector<DFTDependencyPointer>;
-
- protected:
- ValueType mActiveFailureRate;
- ValueType mPassiveFailureRate;
- DFTDependencyVector mIngoingDependencies;
-
- public:
- DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) :
- DFTElement<ValueType>(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate)
- {}
-
- DFTElementType type() const override {
- return DFTElementType::BE;
- }
-
- virtual size_t nrChildren() const override {
- return 0;
- }
-
- ValueType const& activeFailureRate() const {
- return mActiveFailureRate;
- }
-
- ValueType const& passiveFailureRate() const {
- return mPassiveFailureRate;
- }
-
- bool addIngoingDependency(DFTDependencyPointer const& e) {
- assert(e->dependentEvent()->id() == this->id());
- if(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), e) != mIngoingDependencies.end()) {
- return false;
- }
- else
- {
- mIngoingDependencies.push_back(e);
- return true;
- }
- }
-
- bool hasIngoingDependencies() const {
- return !mIngoingDependencies.empty();
- }
-
- size_t nrIngoingDependencies() const {
- return mIngoingDependencies.size();
- }
-
- DFTDependencyVector const& ingoingDependencies() const {
- return mIngoingDependencies;
- }
-
- std::string toString() const override {
- std::stringstream stream;
- stream << *this;
- return stream.str();
- }
-
- bool isBasicElement() const override{
- return true;
- }
-
- bool isColdBasicElement() const override{
- return storm::utility::isZero(mPassiveFailureRate);
- }
-
- virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
- if(elemsInSubtree.count(this->id())) return;
- DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
- if(elemsInSubtree.empty()) {
- // Parent in the subdft, ie it is *not* a subdft
- return;
- }
- for(auto const& incDep : mIngoingDependencies) {
- incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
- if(elemsInSubtree.empty()) {
- // Parent in the subdft, ie it is *not* a subdft
- return;
- }
- }
- }
-
- bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
- if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
- DFTBE<ValueType> const& otherBE = static_cast<DFTBE<ValueType> const&>(other);
- return (mActiveFailureRate == otherBE.mActiveFailureRate) && (mPassiveFailureRate == otherBE.mPassiveFailureRate);
- }
-
- virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override;
- };
-
- template<typename ValueType>
- inline std::ostream& operator<<(std::ostream& os, DFTBE<ValueType> const& be) {
- return os << "{" << be.name() << "} BE(" << be.activeFailureRate() << ", " << be.passiveFailureRate() << ")";
- }
-
-
-
- template<typename ValueType>
- class DFTConst : public DFTElement<ValueType> {
-
- bool mFailed;
-
- public:
- DFTConst(size_t id, std::string const& name, bool failed) :
- DFTElement<ValueType>(id, name), mFailed(failed)
- {}
-
- DFTElementType type() const override {
- if(mFailed) {
- return DFTElementType::CONSTF;
- } else {
- return DFTElementType::CONSTS;
- }
- }
-
-
- bool failed() const {
- return mFailed;
- }
-
- virtual bool isConstant() const {
- return true;
- }
-
- virtual size_t nrChildren() const override {
- return 0;
- }
-
-
-
- bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
- if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
- DFTConst<ValueType> const& otherCNST = static_cast<DFTConst<ValueType> const&>(other);
- return (mFailed == otherCNST.mFailed);
- }
-
- };
-
-
- template<typename ValueType>
- class DFTDependency : public DFTElement<ValueType> {
-
- using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
- using DFTBEPointer = std::shared_ptr<DFTBE<ValueType>>;
-
- protected:
- std::string mNameTrigger;
- std::string mNameDependent;
- ValueType mProbability;
- DFTGatePointer mTriggerEvent;
- DFTBEPointer mDependentEvent;
-
- public:
- DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent, ValueType probability) :
- DFTElement<ValueType>(id, name), mNameTrigger(trigger), mNameDependent(dependent), mProbability(probability)
- {
- }
-
- virtual ~DFTDependency() {}
-
- void initialize(DFTGatePointer triggerEvent, DFTBEPointer dependentEvent) {
- assert(triggerEvent->name() == mNameTrigger);
- assert(dependentEvent->name() == mNameDependent);
- mTriggerEvent = triggerEvent;
- mDependentEvent = dependentEvent;
- }
-
- std::string nameTrigger() const {
- return mNameTrigger;
- }
-
- std::string nameDependent() const {
- return mNameDependent;
- }
-
- ValueType const& probability() const {
- return mProbability;
- }
-
- DFTGatePointer const& triggerEvent() const {
- assert(mTriggerEvent);
- return mTriggerEvent;
- }
-
- DFTBEPointer const& dependentEvent() const {
- assert(mDependentEvent);
- return mDependentEvent;
- }
-
- DFTElementType type() const override {
- return DFTElementType::PDEP;
- }
-
- virtual size_t nrChildren() const override {
- return 1;
- }
-
- virtual bool isDependency() const override {
- return true;
- }
-
- virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
- if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
- DFTDependency<ValueType> const& otherDEP= static_cast<DFTDependency<ValueType> const&>(other);
- return (mProbability == otherDEP.mProbability);
- }
-
-
- virtual std::vector<size_t> independentUnit() const override {
- std::set<size_t> unit = {this->mId};
- mDependentEvent->extendUnit(unit);
- if(unit.count(mTriggerEvent->id()) != 0) {
- return {};
- }
- return std::vector<size_t>(unit.begin(), unit.end());
- }
-
- virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
- if(elemsInSubtree.count(this->id())) return;
- DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
- if(elemsInSubtree.empty()) {
- // Parent in the subdft, ie it is *not* a subdft
- return;
- }
- mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
- if(elemsInSubtree.empty()) {
- // Parent in the subdft, ie it is *not* a subdft
- return;
- }
- mTriggerEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
-
-
- }
-
- virtual std::string toString() const override {
- std::stringstream stream;
- bool fdep = storm::utility::isOne(mProbability);
- stream << "{" << this->name() << "} " << (fdep ? "FDEP" : "PDEP") << "(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")";
- if (!fdep) {
- stream << " with probability " << mProbability;
- }
- return stream.str();
- }
-
- protected:
-
- };
-
-
- template<typename ValueType>
- class DFTAnd : public DFTGate<ValueType> {
-
- public:
- DFTAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children)
- {}
-
- void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- if(state.isOperational(this->mId)) {
- for(auto const& child : this->mChildren)
- {
- if(!state.hasFailed(child->id())) {
- return;
- }
- }
- this->fail(state, queues);
- }
- }
-
- void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- assert(this->hasFailsafeChild(state));
- if(state.isOperational(this->mId)) {
- this->failsafe(state, queues);
- this->childrenDontCare(state, queues);
- }
- }
-
- virtual DFTElementType type() const override {
- return DFTElementType::AND;
- }
-
- std::string typestring() const override {
- return "AND";
- }
- };
-
- template<typename ValueType>
- inline std::ostream& operator<<(std::ostream& os, DFTAnd<ValueType> const& gate) {
- return os << gate.toString();
- }
-
-
-
- template<typename ValueType>
- class DFTOr : public DFTGate<ValueType> {
-
- public:
- DFTOr(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children)
- {}
-
- void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- assert(this->hasFailedChild(state));
- if(state.isOperational(this->mId)) {
- this->fail(state, queues);
- }
- }
-
- void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- for(auto const& child : this->mChildren) {
- if(!state.isFailsafe(child->id())) {
- return;
- }
- }
- this->failsafe(state, queues);
- }
-
- virtual DFTElementType type() const override {
- return DFTElementType::OR;
- }
-
- std::string typestring() const override {
- return "OR";
- }
- };
-
- template<typename ValueType>
- inline std::ostream& operator<<(std::ostream& os, DFTOr<ValueType> const& gate) {
- return os << gate.toString();
- }
-
- template<typename ValueType>
- class DFTPand : public DFTGate<ValueType> {
-
- public:
- DFTPand(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children)
- {}
-
- void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- if(state.isOperational(this->mId)) {
- bool childOperationalBefore = false;
- for(auto const& child : this->mChildren)
- {
- if(!state.hasFailed(child->id())) {
- childOperationalBefore = true;
- } else if(childOperationalBefore && state.hasFailed(child->id())){
- this->failsafe(state, queues);
- this->childrenDontCare(state, queues);
- return;
- }
- }
- if(!childOperationalBefore) {
- this->fail(state, queues);
- }
- }
- }
-
- void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- assert(this->hasFailsafeChild(state));
- if(state.isOperational(this->mId)) {
- this->failsafe(state, queues);
- this->childrenDontCare(state, queues);
- }
- }
-
- virtual DFTElementType type() const override {
- return DFTElementType::PAND;
- }
-
- std::string typestring() const override {
- return "PAND";
- }
- };
-
- template<typename ValueType>
- inline std::ostream& operator<<(std::ostream& os, DFTPand<ValueType> const& gate) {
- return os << gate.toString();
- }
-
-
-
- template<typename ValueType>
- class DFTPor : public DFTGate<ValueType> {
- public:
- DFTPor(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children)
- {}
-
- void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- assert(false);
- }
-
- void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- assert(false);
- }
-
- virtual DFTElementType type() const override {
- return DFTElementType::POR;
- }
-
- std::string typestring() const override {
- return "POR";
- }
- };
-
- template<typename ValueType>
- inline std::ostream& operator<<(std::ostream& os, DFTPor<ValueType> const& gate) {
- return os << gate.toString();
- }
-
-
-
- template<typename ValueType>
- class DFTVot : public DFTGate<ValueType> {
-
- private:
- unsigned mThreshold;
-
- public:
- DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children), mThreshold(threshold)
- {}
-
- void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- if(state.isOperational(this->mId)) {
- unsigned nrFailedChildren = 0;
- for(auto const& child : this->mChildren)
- {
- if(state.hasFailed(child->id())) {
- ++nrFailedChildren;
- if(nrFailedChildren >= mThreshold)
- {
- this->fail(state, queues);
- return;
- }
- }
- }
-
- }
- }
-
- void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- assert(this->hasFailsafeChild(state));
- if(state.isOperational(this->mId)) {
- unsigned nrFailsafeChildren = 0;
- for(auto const& child : this->mChildren)
- {
- if(state.isFailsafe(child->id())) {
- ++nrFailsafeChildren;
- if(nrFailsafeChildren > this->nrChildren() - mThreshold)
- {
- this->failsafe(state, queues);
- this->childrenDontCare(state, queues);
- return;
- }
- }
- }
- }
- }
-
- virtual DFTElementType type() const override {
- return DFTElementType::VOT;
- }
-
- std::string typestring() const override{
- return "VOT (" + std::to_string(mThreshold) + ")";
- }
-
- virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
- if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
- DFTVot<ValueType> const& otherVOT = static_cast<DFTVot<ValueType> const&>(other);
- return (mThreshold == otherVOT.mThreshold);
- }
- };
-
- template<typename ValueType>
- inline std::ostream& operator<<(std::ostream& os, DFTVot<ValueType> const& gate) {
- return os << gate.toString();
- }
-
-
-
- template<typename ValueType>
- class DFTSpare : public DFTGate<ValueType> {
-
- public:
- DFTSpare(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children)
- {}
-
- std::string typestring() const override {
- return "SPARE";
- }
-
- virtual DFTElementType type() const override {
- return DFTElementType::SPARE;
- }
-
- bool isSpareGate() const override {
- return true;
- }
-
- void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
- DFTGate<ValueType>::fail(state, queues);
- state.finalizeUses(this->mId);
- }
-
- void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
- DFTGate<ValueType>::failsafe(state, queues);
- state.finalizeUses(this->mId);
- }
-
- bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- if (DFTGate<ValueType>::checkDontCareAnymore(state, queues)) {
- state.finalizeUses(this->mId);
- return true;
- }
- return false;
- }
-
- void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- if(state.isOperational(this->mId)) {
- size_t uses = state.uses(this->mId);
- if(!state.isOperational(uses)) {
- bool claimingSuccessful = state.claimNew(this->mId, uses, this->mChildren);
- if(!claimingSuccessful) {
- this->fail(state, queues);
- }
- }
- }
- }
-
- void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- if(state.isOperational(this->mId)) {
- if(state.isFailsafe(state.uses(this->mId))) {
- this->failsafe(state, queues);
- this->childrenDontCare(state, queues);
- }
- }
- }
-
- };
-
- template<typename ValueType>
- bool equalType(DFTElement<ValueType> const& e1, DFTElement<ValueType> const& e2) {
- return e1.isTypeEqualTo(e2);
- }
-
- }
-}
-
-
-
-#endif /* DFTELEMENTS_H */
-
+#pragma once
+
+#include "elements/DFTAnd.h"
+#include "elements/DFTBE.h"
+#include "elements/DFTConst.h"
+#include "elements/DFTDependency.h"
+#include "elements/DFTOr.h"
+#include "elements/DFTPand.h"
+#include "elements/DFTPor.h"
+#include "elements/DFTRestriction.h"
+#include "elements/DFTSpare.h"
+#include "elements/DFTVot.h"
\ No newline at end of file
diff --git a/src/storage/dft/DFTStateGenerationInfo.h b/src/storage/dft/DFTStateGenerationInfo.h
new file mode 100644
index 000000000..f82d4e8af
--- /dev/null
+++ b/src/storage/dft/DFTStateGenerationInfo.h
@@ -0,0 +1,96 @@
+#pragma once
+
+namespace storm {
+ namespace storage {
+ class DFTStateGenerationInfo {
+ private:
+ const size_t mUsageInfoBits;
+ std::map<size_t, size_t> mSpareUsageIndex; // id spare -> index first bit in state
+ std::map<size_t, size_t> mSpareActivationIndex; // id spare representative -> index in state
+ std::vector<size_t> mIdToStateIndex; // id -> index first bit in state
+ std::map<size_t, size_t> mRestrictedItems;
+ std::vector<std::pair<size_t, std::vector<size_t>>> mSymmetries; // pair (lenght of symmetry group, vector indicating the starting points of the symmetry groups)
+
+ public:
+
+ DFTStateGenerationInfo(size_t nrElements, size_t maxSpareChildCount) : mUsageInfoBits(storm::utility::math::uint64_log2(maxSpareChildCount) + 1), mIdToStateIndex(nrElements) {
+ assert(maxSpareChildCount < pow(2, mUsageInfoBits));
+ }
+
+ size_t usageInfoBits() const {
+ return mUsageInfoBits;
+ }
+
+ void addStateIndex(size_t id, size_t index) {
+ assert(id < mIdToStateIndex.size());
+ mIdToStateIndex[id] = index;
+ }
+
+ void addSpareActivationIndex(size_t id, size_t index) {
+ mSpareActivationIndex[id] = index;
+ }
+
+ void addSpareUsageIndex(size_t id, size_t index) {
+ mSpareUsageIndex[id] = index;
+ }
+
+ size_t getStateIndex(size_t id) const {
+ assert(id < mIdToStateIndex.size());
+ return mIdToStateIndex[id];
+ }
+
+ size_t getSpareUsageIndex(size_t id) const {
+ assert(mSpareUsageIndex.count(id) > 0);
+ return mSpareUsageIndex.at(id);
+ }
+
+ size_t getSpareActivationIndex(size_t id) const {
+ assert(mSpareActivationIndex.count(id) > 0);
+ return mSpareActivationIndex.at(id);
+ }
+
+ void addSymmetry(size_t length, std::vector<size_t>& startingIndices) {
+ mSymmetries.push_back(std::make_pair(length, startingIndices));
+ }
+
+ size_t getSymmetrySize() const {
+ return mSymmetries.size();
+ }
+
+ size_t getSymmetryLength(size_t pos) const {
+ assert(pos < mSymmetries.size());
+ return mSymmetries[pos].first;
+ }
+
+ std::vector<size_t> const& getSymmetryIndices(size_t pos) const {
+ assert(pos < mSymmetries.size());
+ return mSymmetries[pos].second;
+ }
+
+ friend std::ostream& operator<<(std::ostream& os, DFTStateGenerationInfo const& info) {
+ os << "Id to state index:" << std::endl;
+ for (size_t id = 0; id < info.mIdToStateIndex.size(); ++id) {
+ os << id << " -> " << info.getStateIndex(id) << std::endl;
+ }
+ os << "Spare usage index with usage InfoBits of size " << info.mUsageInfoBits << ":" << std::endl;
+ for (auto pair : info.mSpareUsageIndex) {
+ os << pair.first << " -> " << pair.second << std::endl;
+ }
+ os << "Spare activation index:" << std::endl;
+ for (auto pair : info.mSpareActivationIndex) {
+ os << pair.first << " -> " << pair.second << std::endl;
+ }
+ os << "Symmetries:" << std::endl;
+ for (auto pair : info.mSymmetries) {
+ os << "Length: " << pair.first << ", starting indices: ";
+ for (size_t index : pair.second) {
+ os << index << ", ";
+ }
+ os << std::endl;
+ }
+ return os;
+ }
+
+ };
+ }
+}
\ No newline at end of file
diff --git a/src/storage/dft/elements/DFTAnd.h b/src/storage/dft/elements/DFTAnd.h
new file mode 100644
index 000000000..5a5763166
--- /dev/null
+++ b/src/storage/dft/elements/DFTAnd.h
@@ -0,0 +1,50 @@
+#pragma once
+#include "DFTGate.h"
+
+namespace storm {
+ namespace storage {
+ template<typename ValueType>
+ class DFTAnd : public DFTGate<ValueType> {
+
+ public:
+ DFTAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+ DFTGate<ValueType>(id, name, children)
+ {}
+
+ void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ if(state.isOperational(this->mId)) {
+ for(auto const& child : this->mChildren)
+ {
+ if(!state.hasFailed(child->id())) {
+ return;
+ }
+ }
+ this->fail(state, queues);
+ }
+ }
+
+ void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ assert(this->hasFailsafeChild(state));
+ if(state.isOperational(this->mId)) {
+ this->failsafe(state, queues);
+ this->childrenDontCare(state, queues);
+ }
+ }
+
+ virtual DFTElementType type() const override {
+ return DFTElementType::AND;
+ }
+
+ std::string typestring() const override {
+ return "AND";
+ }
+ };
+
+ template<typename ValueType>
+ inline std::ostream& operator<<(std::ostream& os, DFTAnd<ValueType> const& gate) {
+ return os << gate.toString();
+ }
+
+
+ }
+}
diff --git a/src/storage/dft/elements/DFTBE.h b/src/storage/dft/elements/DFTBE.h
new file mode 100644
index 000000000..5e09e965e
--- /dev/null
+++ b/src/storage/dft/elements/DFTBE.h
@@ -0,0 +1,104 @@
+#pragma once
+namespace storm {
+ namespace storage {
+ template<typename ValueType>
+ class DFTBE : public DFTElement<ValueType> {
+
+ using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
+ using DFTDependencyVector = std::vector<DFTDependencyPointer>;
+
+ protected:
+ ValueType mActiveFailureRate;
+ ValueType mPassiveFailureRate;
+ DFTDependencyVector mIngoingDependencies;
+
+ public:
+ DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) :
+ DFTElement<ValueType>(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate)
+ {}
+
+ DFTElementType type() const override {
+ return DFTElementType::BE;
+ }
+
+ virtual size_t nrChildren() const override {
+ return 0;
+ }
+
+ ValueType const& activeFailureRate() const {
+ return mActiveFailureRate;
+ }
+
+ ValueType const& passiveFailureRate() const {
+ return mPassiveFailureRate;
+ }
+
+ bool addIngoingDependency(DFTDependencyPointer const& e) {
+ assert(e->dependentEvent()->id() == this->id());
+ if(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), e) != mIngoingDependencies.end()) {
+ return false;
+ }
+ else
+ {
+ mIngoingDependencies.push_back(e);
+ return true;
+ }
+ }
+
+ bool hasIngoingDependencies() const {
+ return !mIngoingDependencies.empty();
+ }
+
+ size_t nrIngoingDependencies() const {
+ return mIngoingDependencies.size();
+ }
+
+ DFTDependencyVector const& ingoingDependencies() const {
+ return mIngoingDependencies;
+ }
+
+ std::string toString() const override {
+ std::stringstream stream;
+ stream << *this;
+ return stream.str();
+ }
+
+ bool isBasicElement() const override{
+ return true;
+ }
+
+ bool isColdBasicElement() const override{
+ return storm::utility::isZero(mPassiveFailureRate);
+ }
+
+ virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
+ if(elemsInSubtree.count(this->id())) return;
+ DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+ if(elemsInSubtree.empty()) {
+ // Parent in the subdft, ie it is *not* a subdft
+ return;
+ }
+ for(auto const& incDep : mIngoingDependencies) {
+ incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+ if(elemsInSubtree.empty()) {
+ // Parent in the subdft, ie it is *not* a subdft
+ return;
+ }
+ }
+ }
+
+ bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+ if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+ DFTBE<ValueType> const& otherBE = static_cast<DFTBE<ValueType> const&>(other);
+ return (mActiveFailureRate == otherBE.mActiveFailureRate) && (mPassiveFailureRate == otherBE.mPassiveFailureRate);
+ }
+
+ virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override;
+ };
+
+ template<typename ValueType>
+ inline std::ostream& operator<<(std::ostream& os, DFTBE<ValueType> const& be) {
+ return os << "{" << be.name() << "} BE(" << be.activeFailureRate() << ", " << be.passiveFailureRate() << ")";
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/dft/elements/DFTConst.h b/src/storage/dft/elements/DFTConst.h
new file mode 100644
index 000000000..e827e173c
--- /dev/null
+++ b/src/storage/dft/elements/DFTConst.h
@@ -0,0 +1,47 @@
+#pragma once
+
+
+#include "DFTElement.h"
+namespace storm {
+ namespace storage {
+ template<typename ValueType>
+ class DFTConst : public DFTElement<ValueType> {
+
+ bool mFailed;
+
+ public:
+ DFTConst(size_t id, std::string const& name, bool failed) :
+ DFTElement<ValueType>(id, name), mFailed(failed)
+ {}
+
+ DFTElementType type() const override {
+ if(mFailed) {
+ return DFTElementType::CONSTF;
+ } else {
+ return DFTElementType::CONSTS;
+ }
+ }
+
+
+ bool failed() const {
+ return mFailed;
+ }
+
+ virtual bool isConstant() const {
+ return true;
+ }
+
+ virtual size_t nrChildren() const override {
+ return 0;
+ }
+
+
+ bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+ if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+ DFTConst<ValueType> const& otherCNST = static_cast<DFTConst<ValueType> const&>(other);
+ return (mFailed == otherCNST.mFailed);
+ }
+
+ };
+ }
+}
\ No newline at end of file
diff --git a/src/storage/dft/elements/DFTDependency.h b/src/storage/dft/elements/DFTDependency.h
new file mode 100644
index 000000000..c7f3f6bfd
--- /dev/null
+++ b/src/storage/dft/elements/DFTDependency.h
@@ -0,0 +1,118 @@
+#pragma once
+
+
+#include "DFTElement.h"
+namespace storm {
+ namespace storage {
+
+ template<typename ValueType>
+ class DFTDependency : public DFTElement<ValueType> {
+
+ using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
+ using DFTBEPointer = std::shared_ptr<DFTBE<ValueType>>;
+
+ protected:
+ std::string mNameTrigger;
+ std::string mNameDependent;
+ ValueType mProbability;
+ DFTGatePointer mTriggerEvent;
+ DFTBEPointer mDependentEvent;
+
+ public:
+ DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent, ValueType probability) :
+ DFTElement<ValueType>(id, name), mNameTrigger(trigger), mNameDependent(dependent), mProbability(probability)
+ {
+ }
+
+ virtual ~DFTDependency() {}
+
+ void initialize(DFTGatePointer triggerEvent, DFTBEPointer dependentEvent) {
+ assert(triggerEvent->name() == mNameTrigger);
+ assert(dependentEvent->name() == mNameDependent);
+ mTriggerEvent = triggerEvent;
+ mDependentEvent = dependentEvent;
+ }
+
+ std::string nameTrigger() const {
+ return mNameTrigger;
+ }
+
+ std::string nameDependent() const {
+ return mNameDependent;
+ }
+
+ ValueType const& probability() const {
+ return mProbability;
+ }
+
+ DFTGatePointer const& triggerEvent() const {
+ assert(mTriggerEvent);
+ return mTriggerEvent;
+ }
+
+ DFTBEPointer const& dependentEvent() const {
+ assert(mDependentEvent);
+ return mDependentEvent;
+ }
+
+ DFTElementType type() const override {
+ return DFTElementType::PDEP;
+ }
+
+ virtual size_t nrChildren() const override {
+ return 1;
+ }
+
+ virtual bool isDependency() const override {
+ return true;
+ }
+
+ virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+ if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+ DFTDependency<ValueType> const& otherDEP= static_cast<DFTDependency<ValueType> const&>(other);
+ return (mProbability == otherDEP.mProbability);
+ }
+
+
+ virtual std::vector<size_t> independentUnit() const override {
+ std::set<size_t> unit = {this->mId};
+ mDependentEvent->extendUnit(unit);
+ if(unit.count(mTriggerEvent->id()) != 0) {
+ return {};
+ }
+ return std::vector<size_t>(unit.begin(), unit.end());
+ }
+
+ virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
+ if(elemsInSubtree.count(this->id())) return;
+ DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+ if(elemsInSubtree.empty()) {
+ // Parent in the subdft, ie it is *not* a subdft
+ return;
+ }
+ mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+ if(elemsInSubtree.empty()) {
+ // Parent in the subdft, ie it is *not* a subdft
+ return;
+ }
+ mTriggerEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+
+
+ }
+
+ virtual std::string toString() const override {
+ std::stringstream stream;
+ bool fdep = storm::utility::isOne(mProbability);
+ stream << "{" << this->name() << "} " << (fdep ? "FDEP" : "PDEP") << "(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")";
+ if (!fdep) {
+ stream << " with probability " << mProbability;
+ }
+ return stream.str();
+ }
+
+ protected:
+
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/dft/elements/DFTElement.h b/src/storage/dft/elements/DFTElement.h
new file mode 100644
index 000000000..d6840132a
--- /dev/null
+++ b/src/storage/dft/elements/DFTElement.h
@@ -0,0 +1,297 @@
+#pragma once
+
+#include <string>
+#include <cassert>
+#include <cstdlib>
+#include <iostream>
+#include <functional>
+#include <set>
+#include <vector>
+#include <memory>
+
+
+
+#include "../DFTElementType.h"
+#include "../DFTState.h"
+#include "../DFTStateSpaceGenerationQueues.h"
+#include "src/utility/constants.h"
+#include "src/adapters/CarlAdapter.h"
+
+
+
+
+namespace storm {
+ namespace storage {
+
+ using std::size_t;
+ template<typename ValueType>
+ class DFTGate;
+
+ template<typename ValueType>
+ class DFTDependency;
+ template<typename ValueType>
+ class DFTRestriction;
+
+
+ template<typename ValueType>
+ class DFTElement {
+
+ using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
+ using DFTGateVector = std::vector<DFTGatePointer>;
+ using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
+ using DFTDependencyVector = std::vector<DFTDependencyPointer>;
+ using DFTRestrictionPointer = std::shared_ptr<DFTRestriction<ValueType>>;
+ using DFTRestrictionVector = std::vector<DFTRestrictionPointer>;
+
+
+ protected:
+ std::size_t mId;
+ std::string mName;
+ std::size_t mRank = -1;
+ DFTGateVector mParents;
+ DFTDependencyVector mOutgoingDependencies;
+ DFTRestrictionVector mRestrictions;
+
+
+ public:
+ DFTElement(size_t id, std::string const& name) :
+ mId(id), mName(name)
+ {}
+
+ virtual ~DFTElement() {}
+
+ /**
+ * Returns the id
+ */
+ virtual size_t id() const {
+ return mId;
+ }
+
+ virtual DFTElementType type() const = 0;
+
+ virtual void setRank(size_t rank) {
+ mRank = rank;
+ }
+
+ virtual size_t rank() const {
+ return mRank;
+ }
+
+ virtual bool isConstant() const {
+ return false;
+ }
+
+ virtual bool isGate() const {
+ return false;
+ }
+
+ /**
+ * Returns true if the element is a BE
+ */
+ virtual bool isBasicElement() const {
+ return false;
+ }
+
+ virtual bool isColdBasicElement() const {
+ return false;
+ }
+
+ /**
+ * Returns true if the element is a spare gate
+ */
+ virtual bool isSpareGate() const {
+ return false;
+ }
+
+ virtual bool isDependency() const {
+ return false;
+ }
+
+ virtual bool isRestriction() const {
+ return false;
+ }
+
+ virtual void setId(size_t newId) {
+ mId = newId;
+ }
+
+ /**
+ * Returns the name
+ */
+ virtual std::string const& name() const {
+ return mName;
+ }
+
+ bool addParent(DFTGatePointer const& e) {
+ if(std::find(mParents.begin(), mParents.end(), e) != mParents.end()) {
+ return false;
+ }
+ else
+ {
+ mParents.push_back(e);
+ return true;
+ }
+ }
+
+ bool addRestriction(DFTRestrictionPointer const& e) {
+ if (std::find(mRestrictions.begin(), mRestrictions.end(), e) != mRestrictions.end()) {
+ return false;
+ } else {
+ mRestrictions.push_back(e);
+ return true;
+ }
+ }
+
+ bool hasOnlyStaticParents() const {
+ for(auto const& parent : mParents) {
+ if(!isStaticGateType(parent->type())) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+
+ bool hasParents() const {
+ return !mParents.empty();
+ }
+
+ size_t nrParents() const {
+ return mParents.size();
+ }
+
+ DFTGateVector const& parents() const {
+ return mParents;
+ }
+
+ bool hasRestrictions() const {
+ return !mRestrictions.empty();
+ }
+
+ size_t nrRestrictions() const {
+ return mRestrictions.size();
+ }
+
+ DFTRestrictionVector const& restrictions() const {
+ return mRestrictions;
+ }
+
+ std::vector<size_t> parentIds() const {
+ std::vector<size_t> res;
+ for(auto parent : parents()) {
+ res.push_back(parent->id());
+ }
+ return res;
+ }
+
+ bool addOutgoingDependency(DFTDependencyPointer const& e) {
+ assert(e->triggerEvent()->id() == this->id());
+ if(std::find(mOutgoingDependencies.begin(), mOutgoingDependencies.end(), e) != mOutgoingDependencies.end()) {
+ return false;
+ }
+ else
+ {
+ mOutgoingDependencies.push_back(e);
+ return true;
+ }
+ }
+
+ bool hasOutgoingDependencies() const {
+ return !mOutgoingDependencies.empty();
+ }
+
+ size_t nrOutgoingDependencies() const {
+ return mOutgoingDependencies.size();
+ }
+
+ std::set<DFTElement<ValueType>> restrictedItems() const {
+ std::set<DFTElement<ValueType>> result;
+ for(auto const& restr : mRestrictions) {
+ bool foundThis = false;
+ for(auto const& child : restr->children()) {
+ if(!foundThis) {
+ if(child->id() == mId) {
+ foundThis = true;
+ }
+ } else if(result.count(child) == 0) {
+ result.insert(child);
+ }
+ }
+ }
+ }
+
+ std::set<DFTElement<ValueType>> restrictedItemsTC() const {
+ std::set<DFTElement<ValueType>> result;
+ for(auto const& restr : mRestrictions) {
+ bool foundThis = false;
+ for(auto const& child : restr->children()) {
+ if(!foundThis) {
+ if(child->id() == mId) {
+ foundThis = true;
+ }
+ } else if(result.count(child) == 0) {
+ result.insert(child);
+ std::set<DFTElement<ValueType>> tmpRes = child->restrictedItemsTC();
+ result.insert(tmpRes.begin(), tmpRes.end());
+ }
+ }
+ }
+ }
+
+ DFTDependencyVector const& outgoingDependencies() const {
+ return mOutgoingDependencies;
+ }
+
+ virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
+
+ // virtual void extendImmediateFailureCausePathEvents(std::set<size_t>& ) const;
+
+ virtual std::size_t nrChildren() const = 0;
+
+ virtual std::string toString() const = 0;
+
+ virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const;
+
+ /**
+ * Computes the independent unit of this element, that is, all elements which are direct or indirect successors of an element.
+ */
+ virtual std::vector<size_t> independentUnit() const;
+
+ /**
+ * Helper to independent unit computation
+ * @see independentUnit
+ */
+ virtual void extendUnit(std::set<size_t>& unit) const;
+
+ /**
+ * Computes independent subtrees starting with this element (this), that is, all elements (x) which are connected to either
+ * - one of the children of the element,
+ * - a probabilistic dependency
+ * such that there exists a path from x to a child of this does not go through this.
+ */
+ virtual std::vector<size_t> independentSubDft(bool blockParents) const;
+ /**
+ * Helper to the independent subtree computation
+ * @see independentSubDft
+ */
+ virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const;
+
+ virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const {
+ return type() == other.type();
+ }
+
+
+ protected:
+ // virtual bool checkIsomorphicSubDftHelper(DFTElement const& otherElem, std::vector<std::pair<DFTElement const&, DFTElement const&>>& mapping, std::vector<DFTElement const&> const& order ) const = 0;
+
+ };
+
+
+
+
+ template<typename ValueType>
+ bool equalType(DFTElement<ValueType> const& e1, DFTElement<ValueType> const& e2) {
+ return e1.isTypeEqualTo(e2);
+ }
+ }
+}
diff --git a/src/storage/dft/elements/DFTGate.h b/src/storage/dft/elements/DFTGate.h
new file mode 100644
index 000000000..52f9bcd43
--- /dev/null
+++ b/src/storage/dft/elements/DFTGate.h
@@ -0,0 +1,180 @@
+#pragma once
+
+#include "DFTElement.h"
+namespace storm {
+ namespace storage {
+ template<typename ValueType>
+ class DFTGate : public DFTElement<ValueType> {
+
+ using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
+ using DFTElementVector = std::vector<DFTElementPointer>;
+
+ protected:
+ DFTElementVector mChildren;
+
+ public:
+ DFTGate(size_t id, std::string const& name, DFTElementVector const& children) :
+ DFTElement<ValueType>(id, name), mChildren(children)
+ {}
+
+ virtual ~DFTGate() {}
+
+ void pushBackChild(DFTElementPointer elem) {
+ return mChildren.push_back(elem);
+ }
+
+ size_t nrChildren() const override {
+ return mChildren.size();
+ }
+
+ DFTElementVector const& children() const {
+ return mChildren;
+ }
+
+ virtual bool isGate() const override {
+ return true;
+ }
+
+
+ virtual std::string typestring() const = 0;
+
+ virtual void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
+
+ virtual void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
+
+ virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
+ if (!this->isSpareGate()) {
+ DFTElement<ValueType>::extendSpareModule(elementsInSpareModule);
+ for( auto const& child : mChildren) {
+ if(elementsInSpareModule.count(child->id()) == 0) {
+ elementsInSpareModule.insert(child->id());
+ child->extendSpareModule(elementsInSpareModule);
+ }
+ }
+ }
+ }
+
+ virtual std::vector<size_t> independentUnit() const override {
+ std::set<size_t> unit = {this->mId};
+ for(auto const& child : mChildren) {
+ child->extendUnit(unit);
+ }
+ return std::vector<size_t>(unit.begin(), unit.end());
+ }
+
+ virtual void extendUnit(std::set<size_t>& unit) const override {
+ DFTElement<ValueType>::extendUnit(unit);
+ for(auto const& child : mChildren) {
+ child->extendUnit(unit);
+ }
+ }
+
+ virtual std::vector<size_t> independentSubDft(bool blockParents) const override {
+ auto prelRes = DFTElement<ValueType>::independentSubDft(blockParents);
+ if(prelRes.empty()) {
+ // No elements (especially not this->id) in the prelimanry result, so we know already that it is not a subdft.
+ return prelRes;
+ }
+ std::set<size_t> unit(prelRes.begin(), prelRes.end());
+ std::vector<size_t> pids = this->parentIds();
+ for(auto const& child : mChildren) {
+ child->extendSubDft(unit, pids, blockParents);
+ if(unit.empty()) {
+ // Parent in the subdft, ie it is *not* a subdft
+ break;
+ }
+ }
+ return std::vector<size_t>(unit.begin(), unit.end());
+ }
+
+ virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
+ if(elemsInSubtree.count(this->id()) > 0) return;
+ DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+ if(elemsInSubtree.empty()) {
+ // Parent in the subdft, ie it is *not* a subdft
+ return;
+ }
+ for(auto const& child : mChildren) {
+ child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+ if(elemsInSubtree.empty()) {
+ // Parent in the subdft, ie it is *not* a subdft
+ return;
+ }
+ }
+ }
+
+
+ virtual std::string toString() const override {
+ std::stringstream stream;
+ stream << "{" << this->name() << "} " << typestring() << "( ";
+ typename DFTElementVector::const_iterator it = mChildren.begin();
+ stream << (*it)->name();
+ ++it;
+ while(it != mChildren.end()) {
+ stream << ", " << (*it)->name();
+ ++it;
+ }
+ stream << ")";
+ return stream.str();
+ }
+
+ virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ if(DFTElement<ValueType>::checkDontCareAnymore(state, queues)) {
+ childrenDontCare(state, queues);
+ return true;
+ }
+ return false;
+ }
+
+
+ protected:
+
+ void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+ for(std::shared_ptr<DFTGate> parent : this->mParents) {
+ if(state.isOperational(parent->id())) {
+ queues.propagateFailure(parent);
+ }
+ }
+ for(std::shared_ptr<DFTRestriction<ValueType>> restr : this->mRestrictions) {
+ queues.checkRestrictionLater(restr);
+ }
+ state.setFailed(this->mId);
+ this->childrenDontCare(state, queues);
+ }
+
+ void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+ for(std::shared_ptr<DFTGate> parent : this->mParents) {
+ if(state.isOperational(parent->id())) {
+ queues.propagateFailsafe(parent);
+ }
+ }
+ state.setFailsafe(this->mId);
+ this->childrenDontCare(state, queues);
+ }
+
+ void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+ queues.propagateDontCare(mChildren);
+ }
+
+ bool hasFailsafeChild(DFTState<ValueType>& state) const {
+ for(auto const& child : mChildren) {
+ if(state.isFailsafe(child->id()))
+ {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ bool hasFailedChild(DFTState<ValueType>& state) const {
+ for(auto const& child : mChildren) {
+ if(state.hasFailed(child->id())) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ };
+ }
+}
\ No newline at end of file
diff --git a/src/storage/dft/elements/DFTOr.h b/src/storage/dft/elements/DFTOr.h
new file mode 100644
index 000000000..93e481d35
--- /dev/null
+++ b/src/storage/dft/elements/DFTOr.h
@@ -0,0 +1,45 @@
+#pragma once
+
+#include "DFTGate.h"
+namespace storm {
+ namespace storage {
+ template<typename ValueType>
+ class DFTOr : public DFTGate<ValueType> {
+
+ public:
+ DFTOr(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+ DFTGate<ValueType>(id, name, children)
+ {}
+
+ void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ assert(this->hasFailedChild(state));
+ if(state.isOperational(this->mId)) {
+ this->fail(state, queues);
+ }
+ }
+
+ void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ for(auto const& child : this->mChildren) {
+ if(!state.isFailsafe(child->id())) {
+ return;
+ }
+ }
+ this->failsafe(state, queues);
+ }
+
+ virtual DFTElementType type() const override {
+ return DFTElementType::OR;
+ }
+
+ std::string typestring() const override {
+ return "OR";
+ }
+ };
+
+ template<typename ValueType>
+ inline std::ostream& operator<<(std::ostream& os, DFTOr<ValueType> const& gate) {
+ return os << gate.toString();
+ }
+ }
+}
+
\ No newline at end of file
diff --git a/src/storage/dft/elements/DFTPand.h b/src/storage/dft/elements/DFTPand.h
new file mode 100644
index 000000000..86472d76f
--- /dev/null
+++ b/src/storage/dft/elements/DFTPand.h
@@ -0,0 +1,56 @@
+#pragma once
+
+#include "DFTGate.h"
+namespace storm {
+ namespace storage {
+ template<typename ValueType>
+ class DFTPand : public DFTGate<ValueType> {
+
+ public:
+ DFTPand(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+ DFTGate<ValueType>(id, name, children)
+ {}
+
+ void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ if(state.isOperational(this->mId)) {
+ bool childOperationalBefore = false;
+ for(auto const& child : this->mChildren)
+ {
+ if(!state.hasFailed(child->id())) {
+ childOperationalBefore = true;
+ } else if(childOperationalBefore && state.hasFailed(child->id())){
+ this->failsafe(state, queues);
+ this->childrenDontCare(state, queues);
+ return;
+ }
+ }
+ if(!childOperationalBefore) {
+ this->fail(state, queues);
+ }
+ }
+ }
+
+ void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ assert(this->hasFailsafeChild(state));
+ if(state.isOperational(this->mId)) {
+ this->failsafe(state, queues);
+ this->childrenDontCare(state, queues);
+ }
+ }
+
+ virtual DFTElementType type() const override {
+ return DFTElementType::PAND;
+ }
+
+ std::string typestring() const override {
+ return "PAND";
+ }
+ };
+
+ template<typename ValueType>
+ inline std::ostream& operator<<(std::ostream& os, DFTPand<ValueType> const& gate) {
+ return os << gate.toString();
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/dft/elements/DFTPor.h b/src/storage/dft/elements/DFTPor.h
new file mode 100644
index 000000000..1aaa943b0
--- /dev/null
+++ b/src/storage/dft/elements/DFTPor.h
@@ -0,0 +1,36 @@
+#pragma once
+
+#include "DFTGate.h"
+namespace storm {
+ namespace storage {
+ template<typename ValueType>
+ class DFTPor : public DFTGate<ValueType> {
+ public:
+ DFTPor(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+ DFTGate<ValueType>(id, name, children)
+ {}
+
+ void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ assert(false);
+ }
+
+ void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ assert(false);
+ }
+
+ virtual DFTElementType type() const override {
+ return DFTElementType::POR;
+ }
+
+ std::string typestring() const override {
+ return "POR";
+ }
+ };
+
+ template<typename ValueType>
+ inline std::ostream& operator<<(std::ostream& os, DFTPor<ValueType> const& gate) {
+ return os << gate.toString();
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/dft/elements/DFTRestriction.h b/src/storage/dft/elements/DFTRestriction.h
index 70163a6e6..f0fef5845 100644
--- a/src/storage/dft/elements/DFTRestriction.h
+++ b/src/storage/dft/elements/DFTRestriction.h
@@ -1,7 +1,6 @@
#pragma once
-#include "../DFTElements.h"
-
+#include "DFTElement.h"
namespace storm {
namespace storage {
template<typename ValueType>
diff --git a/src/storage/dft/elements/DFTSpare.h b/src/storage/dft/elements/DFTSpare.h
new file mode 100644
index 000000000..dd3689311
--- /dev/null
+++ b/src/storage/dft/elements/DFTSpare.h
@@ -0,0 +1,70 @@
+#pragma once
+
+
+#include "DFTGate.h"
+namespace storm {
+ namespace storage {
+
+
+ template<typename ValueType>
+ class DFTSpare : public DFTGate<ValueType> {
+
+ public:
+ DFTSpare(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+ DFTGate<ValueType>(id, name, children)
+ {}
+
+ std::string typestring() const override {
+ return "SPARE";
+ }
+
+ virtual DFTElementType type() const override {
+ return DFTElementType::SPARE;
+ }
+
+ bool isSpareGate() const override {
+ return true;
+ }
+
+ void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+ DFTGate<ValueType>::fail(state, queues);
+ state.finalizeUses(this->mId);
+ }
+
+ void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+ DFTGate<ValueType>::failsafe(state, queues);
+ state.finalizeUses(this->mId);
+ }
+
+ bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ if (DFTGate<ValueType>::checkDontCareAnymore(state, queues)) {
+ state.finalizeUses(this->mId);
+ return true;
+ }
+ return false;
+ }
+
+ void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ if(state.isOperational(this->mId)) {
+ size_t uses = state.uses(this->mId);
+ if(!state.isOperational(uses)) {
+ bool claimingSuccessful = state.claimNew(this->mId, uses, this->mChildren);
+ if(!claimingSuccessful) {
+ this->fail(state, queues);
+ }
+ }
+ }
+ }
+
+ void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ if(state.isOperational(this->mId)) {
+ if(state.isFailsafe(state.uses(this->mId))) {
+ this->failsafe(state, queues);
+ this->childrenDontCare(state, queues);
+ }
+ }
+ }
+
+ };
+ }
+}
\ No newline at end of file
diff --git a/src/storage/dft/elements/DFTVot.h b/src/storage/dft/elements/DFTVot.h
new file mode 100644
index 000000000..3a3e818d2
--- /dev/null
+++ b/src/storage/dft/elements/DFTVot.h
@@ -0,0 +1,75 @@
+#pragma once
+namespace storm {
+ namespace storage {
+
+
+ template<typename ValueType>
+ class DFTVot : public DFTGate<ValueType> {
+
+ private:
+ unsigned mThreshold;
+
+ public:
+ DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+ DFTGate<ValueType>(id, name, children), mThreshold(threshold)
+ {}
+
+ void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ if(state.isOperational(this->mId)) {
+ unsigned nrFailedChildren = 0;
+ for(auto const& child : this->mChildren)
+ {
+ if(state.hasFailed(child->id())) {
+ ++nrFailedChildren;
+ if(nrFailedChildren >= mThreshold)
+ {
+ this->fail(state, queues);
+ return;
+ }
+ }
+ }
+
+ }
+ }
+
+ void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ assert(this->hasFailsafeChild(state));
+ if(state.isOperational(this->mId)) {
+ unsigned nrFailsafeChildren = 0;
+ for(auto const& child : this->mChildren)
+ {
+ if(state.isFailsafe(child->id())) {
+ ++nrFailsafeChildren;
+ if(nrFailsafeChildren > this->nrChildren() - mThreshold)
+ {
+ this->failsafe(state, queues);
+ this->childrenDontCare(state, queues);
+ return;
+ }
+ }
+ }
+ }
+ }
+
+ virtual DFTElementType type() const override {
+ return DFTElementType::VOT;
+ }
+
+ std::string typestring() const override{
+ return "VOT (" + std::to_string(mThreshold) + ")";
+ }
+
+ virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+ if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+ DFTVot<ValueType> const& otherVOT = static_cast<DFTVot<ValueType> const&>(other);
+ return (mThreshold == otherVOT.mThreshold);
+ }
+ };
+
+ template<typename ValueType>
+ inline std::ostream& operator<<(std::ostream& os, DFTVot<ValueType> const& gate) {
+ return os << gate.toString();
+ }
+
+ }
+}
\ No newline at end of file