DFTState.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
 
#include "storm/storage/BitVector.h"
 
#include "storm-dft/builder/DftExplorationHeuristic.h"
#include "storm-dft/storage/DFTElementState.h"
#include "storm-dft/storage/FailableElements.h"
 
namespace storm::dft {
namespace storage {
 
// Forward declarations
namespace elements {
 
template<typename ValueType>
class DFTBE;
template<typename ValueType>
class DFTDependency;
template<typename ValueType>
class DFTElement;
 
}  // namespace elements
 
template<typename ValueType>
class DFT;
class DFTStateGenerationInfo;
 
template<typename ValueType>
class DFTState {
    friend struct std::hash<DFTState>;
 
   private:
    // Status is bitvector where each element has two bits with the meaning according to DFTElementState
    storm::storage::BitVector mStatus;
    size_t mId;
    storm::dft::storage::FailableElements failableElements;
    std::vector<size_t> mUsedRepresentants;
    size_t indexRelevant;
    bool mPseudoState;
    bool mValid = true;
    bool mTransient = false;
    const DFT<ValueType>& mDft;
    const DFTStateGenerationInfo& mStateGenerationInfo;
 
   public:
    DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id);
 
    DFTState(storm::storage::BitVector const& status, DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id);
 
    void construct();
 
    std::shared_ptr<DFTState<ValueType>> copy() const;
 
    DFTElementState getElementState(size_t id) const;
 
    static DFTElementState getElementState(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id);
 
    DFTDependencyState getDependencyState(size_t id) const;
 
    static DFTDependencyState getDependencyState(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id);
 
    size_t getId() const;
 
    void setId(size_t id);
 
    bool isOperational(size_t id) const;
 
    bool hasFailed(size_t id) const;
 
    static bool hasFailed(storm::storage::BitVector const& state, size_t indexId);
 
    bool isFailsafe(size_t id) const;
 
    static bool isFailsafe(storm::storage::BitVector const& state, size_t indexId);
 
    bool dontCare(size_t id) const;
 
    bool dependencyTriggered(size_t id) const;
 
    bool dependencySuccessful(size_t id) const;
 
    bool dependencyUnsuccessful(size_t id) const;
 
    void setFailed(size_t id);
 
    void setFailsafe(size_t id);
 
    void setDontCare(size_t id);
 
    void setDependencySuccessful(size_t id);
 
    void setDependencyUnsuccessful(size_t id);
 
    void setDependencyDontCare(size_t id);
 
    void beNoLongerFailable(size_t id);
 
    void activate(size_t repr);
 
    bool isActive(size_t id) const;
 
    void markAsInvalid() {
        mValid = false;
    }
 
    bool isInvalid() const {
        return !mValid;
    }
 
    void markAsTransient() {
        mTransient = true;
    }
 
    bool isTransient() const {
        return mTransient;
    }
 
    bool isPseudoState() const {
        return mPseudoState;
    }
 
    storm::storage::BitVector const& status() const {
        return mStatus;
    }
 
    storm::dft::storage::FailableElements& getFailableElements() {
        return failableElements;
    }
 
    uint_fast64_t uses(size_t id) const;
 
    static uint_fast64_t usesIndex(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id);
 
    uint_fast64_t extractUses(size_t from) const;
 
    bool isUsed(size_t child) const;
 
    void setUses(size_t spareId, size_t child);
 
    void finalizeUses(size_t spareId);
 
    bool claimNew(size_t spareId, size_t currentlyUses, std::vector<std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType>>> const& children);
 
    ValueType getFailableBERate(size_t index) const;
 
    ValueType getBERate(size_t id) const;
 
    bool updateFailableDependencies(size_t id);
 
    bool updateFailableInRestrictions(size_t id);
 
    void updateDontCareDependencies(size_t id);
 
    void letBEFail(std::shared_ptr<storm::dft::storage::elements::DFTBE<ValueType> const> be);
 
    void letDependencyTrigger(std::shared_ptr<storm::dft::storage::elements::DFTDependency<ValueType> const> dependency, bool successful = true);
 
    bool orderBySymmetry();
 
    bool isEventDisabledViaRestriction(size_t id) const;
 
    bool isEventRelevantInRestriction(size_t id) const;
 
    bool hasOperationalRelevantEvent();
 
    friend bool operator==(DFTState const& a, DFTState const& b) {
        return a.mStatus == b.mStatus;
    }
 
   private:
    void propagateActivation(size_t representativeId);
 
    int getElementStateInt(size_t id) const;
 
    static int getElementStateInt(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id);
};
 
}  // namespace storage
}  // namespace storm::dft
 
namespace std {
template<typename ValueType>
struct hash<storm::dft::storage::DFTState<ValueType>> {
    size_t operator()(storm::dft::storage::DFTState<ValueType> const& s) const {
        return hash<storm::storage::BitVector>()(s.mStatus);
    }
};
}  // namespace std