mCRL2

Components for generating an arbitrary element of a sort. More...
#include <representative_generator.h>
Public Member Functions  
representative_generator (const data_specification &specification)  
Constructor with data specification as context.  
data_expression  operator() (const sort_expression &sort) 
Returns a representative of a sort.  
Protected Member Functions  
void  set_representative (const sort_expression &sort, const data_expression &representative) 
Sets a data expression as representative of the sort.  
bool  find_representative (const function_symbol &symbol, std::set< sort_expression > &visited_sorts, data_expression &result) 
Finds a representative of the form f(t1,...,tn) where f is the function symbol.  
bool  find_representative (const sort_expression &sort, std::set< sort_expression > &visited_sorts, data_expression &result) 
Finds a representative element for an arbitrary sort expression.  
Protected Attributes  
const data_specification &  m_specification 
Data specification context.  
std::map< sort_expression, data_expression >  m_representatives_cache 
Serves as a cache for later find operations.  
Components for generating an arbitrary element of a sort.
This component is not deterministic. So, it is not guaranteed to deliver the same element each time it is run.
A representative is an arbitrary element of a given sort. This component takes a specification and generates representatives for sorts defined by the specification. An important property is that for the same sort the same representative is returned. For this it assumes that the context constructors and mappings for the sort remain unchanged.
The general aim is to keep the representative expression as simple. Use of constructors is preferred above mappings and constructors or mappings representing constants are preferred over those that have nonempty domain.
Constructors and functions that have arrows in their target sorts (e.g. f:A>(B>C)) are not used to construct default terms. Once an element is generated it is kept for later requests, which is done for performance when used frequently on the same specification. At some point a sufficiently advanced enumerator may be used to replace the current implementation.
This component will evolve through time, in the sense that more complex expressions will be generated over time to act as representative a certain sort, for instance containing function symbols with complex target sorts, containing explicit function constructors (lambda's). So, no reliance is possible on the particular shape of the terms that are generated.
Definition at line 52 of file representative_generator.h.

inline 
Constructor with data specification as context.
Definition at line 239 of file representative_generator.h.

inlineprotected 
Finds a representative of the form f(t1,...,tn) where f is the function symbol.
[in]  symbol  The function symbol f using which the representative is constructed. 
[in]  visited_sorts  A set of sorts for which no representative can be constructed. This is used to prevent 
[out]  result  The representative of the shape f(t1,...,tn). This is only set if this function yields true. 
Definition at line 81 of file representative_generator.h.

inlineprotected 
Finds a representative element for an arbitrary sort expression.
[in]  sort  the sort for which to find the representative 
[in]  visited_sorts  A set of sorts for which no representative can be constructed. This is used to prevent 
[out]  result  The representative of the shape f(t1,...,tn). This is only set if this function yields true. 
Definition at line 115 of file representative_generator.h.

inline 
Returns a representative of a sort.
[in]  sort  sort of which to find a representatitive 
Definition at line 245 of file representative_generator.h.

inlineprotected 
Sets a data expression as representative of the sort.
[in]  sort  the sort of which to set the representative 
[in]  representative  the data expression that serves as representative 
Definition at line 68 of file representative_generator.h.

protected 
Serves as a cache for later find operations.
Definition at line 61 of file representative_generator.h.

protected 
Data specification context.
Definition at line 58 of file representative_generator.h.