DFTSeq.h

Go to the documentation of this file.

#pragma once
 
#include "DFTRestriction.h"
 
namespace storm::dft {
namespace storage {
namespace elements {
 
template<typename ValueType>
class DFTSeq : public DFTRestriction<ValueType> {
   public:
    DFTSeq(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {})
        : DFTRestriction<ValueType>(id, name, children) {
        // Intentionally left empty.
    }
 
    std::shared_ptr<DFTElement<ValueType>> clone() const override {
        return std::shared_ptr<DFTElement<ValueType>>(new DFTSeq<ValueType>(this->id(), this->name(), {}));
    }
 
    storm::dft::storage::elements::DFTElementType type() const override {
        return storm::dft::storage::elements::DFTElementType::SEQ;
    }
 
    bool isSeqEnforcer() const override {
        return true;
    }
 
    void checkFails(storm::dft::storage::DFTState<ValueType>& state, storm::dft::storage::DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
        STORM_LOG_ASSERT(queues.failurePropagationDone(), "Failure propagation not finished.");
        bool childOperationalBefore = false;
        for (auto const& child : this->children()) {
            if (!state.hasFailed(child->id())) {
                childOperationalBefore = true;
            } else if (childOperationalBefore && state.hasFailed(child->id())) {
                // Child has failed before left sibling.
                this->fail(state, queues);
                return;
            }
        }
    }
 
    void checkFailsafe(storm::dft::storage::DFTState<ValueType>&, storm::dft::storage::DFTStateSpaceGenerationQueues<ValueType>&) const override {}
 
    bool checkDontCareAnymore(storm::dft::storage::DFTState<ValueType>&, storm::dft::storage::DFTStateSpaceGenerationQueues<ValueType>&) const override {
        return false;
    }
};
 
}  // namespace elements
}  // namespace storage
}  // namespace storm::dft