DFTElement.h

Go to the documentation of this file.

#pragma once
 
#include <cstdlib>
#include <functional>
#include <iostream>
#include <map>
#include <memory>
#include <set>
#include <string>
#include <vector>
 
#include "storm-dft/storage/DFTState.h"
#include "storm-dft/storage/DFTStateSpaceGenerationQueues.h"
#include "storm-dft/storage/elements/DFTElementType.h"
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/utility/constants.h"
 
namespace storm::dft {
namespace storage {
namespace elements {
 
using std::size_t;
 
// Forward declarations
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>;
 
   public:
    DFTElement(size_t id, std::string const& name) : mId(id), mName(name), mRank(-1), mRelevant(false), mAllowDC(true) {
        // Intentionally left empty.
    }
 
    virtual std::shared_ptr<DFTElement<ValueType>> clone() const = 0;
 
    virtual ~DFTElement() = default;
 
    virtual size_t id() const {
        return mId;
    }
 
    virtual void setId(size_t id) {
        this->mId = id;
    }
 
    virtual std::string const& name() const {
        return mName;
    }
 
    virtual storm::dft::storage::elements::DFTElementType type() const = 0;
 
    virtual std::string typestring() const {
        return storm::dft::storage::elements::toString(this->type());
    }
 
    virtual size_t rank() const {
        return mRank;
    }
 
    virtual void setRank(size_t rank) {
        this->mRank = rank;
    }
 
    virtual bool isRelevant() const {
        return mRelevant;
    }
 
    virtual void setRelevance(bool relevant) const {
        this->mRelevant = relevant;
    }
 
    virtual void setAllowDC(bool allowDC) const {
        this->mAllowDC = allowDC;
    }
 
    virtual bool isBasicElement() const {
        return false;
    }
 
    virtual bool isGate() const {
        return false;
    }
 
    virtual bool isStaticElement() const {
        return false;
    }
 
    virtual bool isSpareGate() const {
        return false;
    }
 
    virtual bool isDependency() const {
        return false;
    }
 
    virtual bool isRestriction() const {
        return false;
    }
 
    virtual std::size_t nrChildren() const = 0;
 
    bool hasParents() const {
        return !mParents.empty();
    }
 
    size_t nrParents() const {
        return mParents.size();
    }
 
    DFTGateVector const& parents() const {
        return mParents;
    }
 
    void addParent(DFTGatePointer const& parent) {
        if (std::find(this->parents().begin(), this->parents().end(), parent) == this->parents().end()) {
            // Parent does not exist yet
            mParents.push_back(parent);
        }
    }
 
    std::vector<size_t> parentIds() const {
        std::vector<size_t> ids;
        for (auto parent : this->parents()) {
            ids.push_back(parent->id());
        }
        return ids;
    }
 
    bool hasOnlyStaticParents() const {
        for (auto const& parent : this->parents()) {
            if (!parent->isStaticElement()) {
                return false;
            }
        }
        return true;
    }
 
    bool hasRestrictions() const {
        return !mRestrictions.empty();
    }
 
    size_t nrRestrictions() const {
        return mRestrictions.size();
    }
 
    DFTRestrictionVector const& restrictions() const {
        return mRestrictions;
    }
 
    void addRestriction(DFTRestrictionPointer const& restriction) {
        if (std::find(this->restrictions().begin(), this->restrictions().end(), restriction) == this->restrictions().end()) {
            // Restriction does not exist yet
            mRestrictions.push_back(restriction);
        }
    }
 
    bool hasOutgoingDependencies() const {
        return !mOutgoingDependencies.empty();
    }
 
    size_t nrOutgoingDependencies() const {
        return mOutgoingDependencies.size();
    }
 
    DFTDependencyVector const& outgoingDependencies() const {
        return mOutgoingDependencies;
    }
 
    void addOutgoingDependency(DFTDependencyPointer const& outgoingDependency) {
        STORM_LOG_ASSERT(outgoingDependency->triggerEvent()->id() == this->id(), "Ids do not match.");
        if (std::find(this->outgoingDependencies().begin(), this->outgoingDependencies().end(), outgoingDependency) == this->outgoingDependencies().end()) {
            // Outgoing dependency does not exist yet
            mOutgoingDependencies.push_back(outgoingDependency);
        }
    }
 
    virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
 
    virtual bool checkDontCareAnymore(storm::dft::storage::DFTState<ValueType>& state,
                                      storm::dft::storage::DFTStateSpaceGenerationQueues<ValueType>& queues) const;
 
    virtual std::vector<size_t> independentUnit() const;
 
    virtual void extendUnit(std::set<size_t>& unit) const;
 
    virtual std::vector<size_t> independentSubDft(bool blockParents, bool sparesAsLeaves = false) const;
 
    virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const;
 
    virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const {
        return type() == other.type();
    }
 
    virtual std::string toString() const = 0;
 
   protected:
    std::size_t mId;
    std::string mName;
    std::size_t mRank;
    DFTGateVector mParents;
    DFTDependencyVector mOutgoingDependencies;
    DFTRestrictionVector mRestrictions;
    mutable bool mRelevant;  // Must be mutable to allow changes later on. TODO: avoid mutable
    mutable bool mAllowDC;   // Must be mutable to allow changes later on. TODO: avoid mutable
};
 
template<typename ValueType>
inline std::ostream& operator<<(std::ostream& os, DFTElement<ValueType> const& element) {
    return os << element.toString();
}
 
}  // namespace elements
}  // namespace storage
}  // namespace storm::dft