mCRL2
Loading...
Searching...
No Matches
mcrl2::data::identifier_generator< Generator > Class Template Referenceabstract

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 >:
mcrl2::data::multiset_identifier_generator mcrl2::data::set_identifier_generator mcrl2::data::xyz_identifier_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 31 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
sAn 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 55 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

◆ 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
sAn 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
hintA string
add_to_contextIf 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 83 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
sAn 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 64 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 34 of file identifier_generator.h.


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