mcrl2::data::enumerator_queue

Include file:

#include "mcrl2/data/enumerator.h
class mcrl2::data::enumerator_queue

Contains the enumerator queue.

Public types

type size_type

typedef for std::deque< EnumeratorListElement >::size_type

type value_type

typedef for EnumeratorListElement

Protected attributes

std::deque<EnumeratorListElement> P

Public member functions

const EnumeratorListElement &back() const
EnumeratorListElement &back()
void clear()
bool empty() const
enumerator_queue() = default

Default constructor.

enumerator_queue(const EnumeratorListElement &value)

Initializes the enumerator queue with the given value.

const EnumeratorListElement &front() const
EnumeratorListElement &front()
void pop_back()
void pop_front()
void push_back(const EnumeratorListElement &x)
std::deque<EnumeratorListElement>::size_type size() const