mcrl2::data::identifier_generator< Generator > Class Template Reference

Abstract base class for identifier generators. Identifier generators generate fresh names that do not appear in a given context. A context is maintained containing already used identifiers. Using the operator()() and operator()(std::string) fresh identifiers are generated that do not appear in the context. More...

#include <identifier_generator.h>

Inheritance diagram for mcrl2::data::identifier_generator< Generator >:

Public Member Functions
	identifier_generator ()=default
	Constructor.
virtual	~identifier_generator ()=default
	Destructor.
virtual void	clear_context ()=0
	Clears the context.
virtual void	add_identifier (const core::identifier_string &s)=0
	Adds the identifier s to the context.
virtual void	remove_identifier (const core::identifier_string &s)=0
	Removes the identifier s from the context.
void	add_identifiers (const std::set< core::identifier_string > &ids)
	Add a set of identifiers to the context.
void	remove_identifiers (const std::set< core::identifier_string > &ids)
	Remove a set of identifiers from the context.
virtual bool	has_identifier (const core::identifier_string &s) const =0
	Returns true if the identifier s appears in the context.
virtual core::identifier_string	operator() (const std::string &hint, bool add_to_context=true)
	Returns a fresh identifier, with the given hint as prefix. The returned identifier is added to the context.

Protected Attributes
Generator	m_generator

Detailed Description

template<typename Generator = utilities::number_postfix_generator>
class mcrl2::data::identifier_generator< Generator >

Abstract base class for identifier generators. Identifier generators generate fresh names that do not appear in a given context. A context is maintained containing already used identifiers. Using the operator()() and operator()(std::string) fresh identifiers are generated that do not appear in the context.

Definition at line 30 of file identifier_generator.h.

Constructor & Destructor Documentation

identifier_generator()

template<typename Generator = utilities::number_postfix_generator>

mcrl2::data::identifier_generator< Generator >::identifier_generator ( )

default

Constructor.

~identifier_generator()

template<typename Generator = utilities::number_postfix_generator>

virtual mcrl2::data::identifier_generator< Generator >::~identifier_generator ( )

virtualdefault

Destructor.

Member Function Documentation

add_identifier()

template<typename Generator = utilities::number_postfix_generator>

virtual void mcrl2::data::identifier_generator< Generator >::add_identifier ( const core::identifier_string &  s )

pure virtual

Adds the identifier s to the context.

Parameters

s	An identifier.

Implemented in mcrl2::data::set_identifier_generator, and mcrl2::data::multiset_identifier_generator.

add_identifiers()

template<typename Generator = utilities::number_postfix_generator>

void mcrl2::data::identifier_generator< Generator >::add_identifiers ( const std::set< core::identifier_string > &  ids )

inline

Add a set of identifiers to the context.

Definition at line 57 of file identifier_generator.h.

clear_context()

template<typename Generator = utilities::number_postfix_generator>

virtual void mcrl2::data::identifier_generator< Generator >::clear_context ( )

pure virtual

Clears the context.

Implemented in mcrl2::data::set_identifier_generator, and mcrl2::data::multiset_identifier_generator.

has_identifier()

template<typename Generator = utilities::number_postfix_generator>

virtual bool mcrl2::data::identifier_generator< Generator >::has_identifier ( const core::identifier_string &  s ) const

pure virtual

Returns true if the identifier s appears in the context.

Parameters

s	An identifier.

Returns

True if the identifier appears in the context.

Implemented in mcrl2::data::set_identifier_generator, and mcrl2::data::multiset_identifier_generator.

operator()()

template<typename Generator = utilities::number_postfix_generator>

virtual core::identifier_string mcrl2::data::identifier_generator< Generator >::operator() ( const std::string &  hint, bool  add_to_context = true  )

inlinevirtual

Returns a fresh identifier, with the given hint as prefix. The returned identifier is added to the context.

Parameters

hint	A string
add_to_context	If true, the freshly generated identifier is added to the context to make sure no duplicates are generated.

Returns

A fresh identifier.

Reimplemented in mcrl2::data::xyz_identifier_generator.

Definition at line 87 of file identifier_generator.h.

remove_identifier()

template<typename Generator = utilities::number_postfix_generator>

virtual void mcrl2::data::identifier_generator< Generator >::remove_identifier ( const core::identifier_string &  s )

pure virtual

Removes the identifier s from the context.

Parameters

s	An identifier.

Implemented in mcrl2::data::set_identifier_generator, and mcrl2::data::multiset_identifier_generator.

remove_identifiers()

template<typename Generator = utilities::number_postfix_generator>

void mcrl2::data::identifier_generator< Generator >::remove_identifiers ( const std::set< core::identifier_string > &  ids )

inline

Remove a set of identifiers from the context.

Definition at line 66 of file identifier_generator.h.

Member Data Documentation

m_generator

template<typename Generator = utilities::number_postfix_generator>

Generator mcrl2::data::identifier_generator< Generator >::m_generator

protected

Definition at line 33 of file identifier_generator.h.

---

The documentation for this class was generated from the following file:

• data/include/mcrl2/data/identifier_generator.h