FailableElements.h

Go to the documentation of this file.

#pragma once
 
#include <list>
#include <memory>
 
#include "storm/storage/BitVector.h"
 
namespace storm::dft {
namespace storage {
 
// Forward declarations
template<typename ValueType>
class DFT;
 
namespace elements {
 
template<typename ValueType>
class DFTBE;
template<typename ValueType>
class DFTDependency;
 
}  // namespace elements
 
class FailableElements {
   public:
    class const_iterator {
       public:
        // Define iterator
        using iterator_category = std::input_iterator_tag;
        using value_type = size_t;
        using difference_type = std::ptrdiff_t;
        using pointer = size_t*;
        using reference = size_t&;
 
        const_iterator(bool dependency, bool conflicting, storm::storage::BitVector::const_iterator const& iterBE,
                       std::list<size_t>::const_iterator const& iterDependency, std::list<size_t>::const_iterator nonConflictEnd,
                       std::list<size_t>::const_iterator conflictBegin);
 
        const_iterator(const_iterator const& other) = default;
 
        const_iterator& operator=(const_iterator const& other) = default;
 
        const_iterator& operator++();
 
        uint_fast64_t operator*() const;
 
        bool operator!=(const_iterator const& other) const;
 
        bool operator==(const_iterator const& other) const;
 
        bool isFailureDueToDependency() const;
 
        bool isConflictingDependency() const;
 
        template<typename ValueType>
        std::shared_ptr<storm::dft::storage::elements::DFTBE<ValueType> const> asBE(storm::dft::storage::DFT<ValueType> const& dft) const;
 
        template<typename ValueType>
        std::shared_ptr<storm::dft::storage::elements::DFTDependency<ValueType> const> asDependency(storm::dft::storage::DFT<ValueType> const& dft) const;
 
       private:
        // Whether dependencies are currently considered.
        bool dependency;
        // Whether the iterator currently points to a conflicting dependency.
        bool conflicting;
        // Iterators for underlying data structures
        storm::storage::BitVector::const_iterator itBE;
        std::list<size_t>::const_iterator itDep;
 
        // Pointers marking end of non-conflict list and beginning of conflict list
        // Used for sequential iteration over all dependencies
        std::list<size_t>::const_iterator nonConflictEnd;
        std::list<size_t>::const_iterator conflictBegin;
    };
 
    FailableElements(size_t maxBEId) : currentlyFailableBE(maxBEId) {}
 
    void addBE(size_t id);
 
    void addDependency(size_t id, bool isConflicting);
 
    void removeBE(size_t id);
 
    void removeDependency(size_t id);
 
    void clear();
 
    FailableElements::const_iterator begin(bool forceBE = false) const;
 
    FailableElements::const_iterator end(bool forceBE = false) const;
 
    bool hasDependencies() const;
 
    bool hasBEs() const;
 
    std::string getCurrentlyFailableString(bool forceBE = false) const;
 
   private:
    // We use a BitVector for BEs but a list for dependencies, because usually only a few dependencies are failable at the same time.
    // In contrast, usually most BEs are failable.
    // The lists of failable elements are sorted by increasing id.
    storm::storage::BitVector currentlyFailableBE;
    std::list<size_t> failableConflictingDependencies;
    std::list<size_t> failableNonconflictingDependencies;
};
 
}  // namespace storage
}  // namespace storm::dft