DFTRestriction.h

Go to the documentation of this file.

#pragma once
 
#include "DFTChildren.h"
 
namespace storm::dft {
namespace storage {
namespace elements {
 
template<typename ValueType>
class DFTRestriction : public DFTChildren<ValueType> {
    using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
    using DFTElementVector = std::vector<DFTElementPointer>;
 
   public:
    DFTRestriction(size_t id, std::string const& name, DFTElementVector const& children) : DFTChildren<ValueType>(id, name, children) {
        // Intentionally left empty.
    }
 
    virtual ~DFTRestriction() = default;
 
    bool isRestriction() const override {
        return true;
    }
 
    virtual bool isSeqEnforcer() const {
        return false;
    }
 
    virtual bool isMutex() const {
        return false;
    }
 
    bool allChildrenBEs() const {
        for (auto const& elem : this->children()) {
            if (!elem->isBasicElement()) {
                return false;
            }
        }
        return true;
    }
 
    void extendSpareModule(std::set<size_t>&) const override {
        // Do nothing
    }
 
    bool checkDontCareAnymore(storm::dft::storage::DFTState<ValueType>&, storm::dft::storage::DFTStateSpaceGenerationQueues<ValueType>&) const override {
        return false;
    }
 
   protected:
    void fail(storm::dft::storage::DFTState<ValueType>& state, storm::dft::storage::DFTStateSpaceGenerationQueues<ValueType>&) const override {
        state.markAsInvalid();
    }
 
    void failsafe(storm::dft::storage::DFTState<ValueType>&, storm::dft::storage::DFTStateSpaceGenerationQueues<ValueType>&) const override {
        // Do nothing
    }
};
 
}  // namespace elements
}  // namespace storage
}  // namespace storm::dft