MaximalEndComponent.h

Go to the documentation of this file.

#pragma once
 
#include <unordered_map>
 
#include "storm/storage/BoostTypes.h"
#include "storm/storage/sparse/StateType.h"
 
namespace storm {
namespace storage {
// fwd
class BitVector;

class MaximalEndComponent {
   public:
    typedef storm::storage::FlatSet<sparse::state_type> set_type;
    typedef std::unordered_map<uint_fast64_t, set_type> map_type;
    typedef map_type::iterator iterator;
    typedef map_type::const_iterator const_iterator;

    MaximalEndComponent();

    MaximalEndComponent(MaximalEndComponent const& other);

    MaximalEndComponent& operator=(MaximalEndComponent const& other);

    MaximalEndComponent(MaximalEndComponent&& other);

    MaximalEndComponent& operator=(MaximalEndComponent&& other);

    bool operator==(MaximalEndComponent const& other) const;

    bool operator!=(MaximalEndComponent const& other) const;

    void addState(uint_fast64_t state, set_type const& choices);

    void addState(uint_fast64_t state, set_type&& choices);

    std::size_t size() const;

    set_type const& getChoicesForState(uint_fast64_t state) const;

    set_type& getChoicesForState(uint_fast64_t state);

    void removeState(uint_fast64_t state);

    bool containsState(uint_fast64_t state) const;

    bool containsAnyState(storm::storage::BitVector stateSet) const;

    bool containsChoice(uint_fast64_t state, uint_fast64_t choice) const;

    set_type getStateSet() const;

    iterator begin();

    iterator end();

    const_iterator begin() const;

    const_iterator end() const;
 
    // Declare the streaming operator as a friend function.
    friend std::ostream& operator<<(std::ostream& out, MaximalEndComponent const& component);
 
   private:
    // This stores the mapping from states contained in the MEC to the choices in this MEC.
    map_type stateToChoicesMapping;
};
}  // namespace storage
}  // namespace storm