MaximalEndComponent.h

Go to the documentation of this file.

#ifndef STORM_STORAGE_MAXIMALENDCOMPONENT_H_
#define STORM_STORAGE_MAXIMALENDCOMPONENT_H_
 
#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);
 
    bool operator!=(MaximalEndComponent const& other);
 
    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
 
#endif /* STORM_STORAGE_MAXIMALENDCOMPONENT_H_ */