Include file:

#include "mcrl2/data/set_identifier_generator.h
class mcrl2::data::multiset_identifier_generator

Identifier generator that stores the identifiers of the context in a multiset. If an identifier occurs multiple times, multiple calls to remove_from_context are required to remove it. Using the operator()() and operator()(std::string) fresh identifiers can be generated that do not appear in the context.

Protected attributes

std::multiset<core::identifier_string> mcrl2::data::multiset_identifier_generator::m_identifiers

The context of the identifier generator.

Public member functions

void add_identifier(const core::identifier_string &s) override

Adds the identifier s to the context.


  • s A
void clear_context() override

Clears the context.

const std::multiset<core::identifier_string> &context() const

Returns the context.

Returns: The context.

bool has_identifier(const core::identifier_string &s) const override

Returns true if the identifier s appears in the context.


  • s A

Returns: True if the identifier s appears in the context.

multiset_identifier_generator() = default


void remove_identifier(const core::identifier_string &s) override

Removes one occurrence of the identifier s from the context.


  • s A