mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
mcrl2::data::representative_generator Class Reference

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 search_for_lexicographically_minimal_symbol (function_symbol &f_result, const sort_expression &sort, const std::vector< function_symbol > &function_symbols)
 
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.
 

Detailed Description

Components for generating an arbitrary element of a sort.

This component delivers a term based on a lexicographic ordering of function symbols. It delivers 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 simple. Use of constructors is preferred above mappings and constructors or mappings representing constants are preferred over those that have non-empty 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.

Constructor & Destructor Documentation

◆ representative_generator()

mcrl2::data::representative_generator::representative_generator ( const data_specification &  specification)
inline

Constructor with data specification as context.

Definition at line 263 of file representative_generator.h.

Member Function Documentation

◆ find_representative() [1/2]

bool mcrl2::data::representative_generator::find_representative ( const function_symbol &  symbol,
std::set< sort_expression > &  visited_sorts,
data_expression &  result 
)
inlineprotected

Finds a representative of the form f(t1,...,tn) where f is the function symbol.

Parameters
[in]symbolThe function symbol f using which the representative is constructed.
[in]visited_sortsA set of sorts for which no representative can be constructed. This is used to prevent
[out]resultThe representative of the shape f(t1,...,tn). This is only set if this function yields true.
Returns
a boolean indicating whether a representative has successfully been found.
Precondition
symbol.sort() is of type function_sort

Definition at line 81 of file representative_generator.h.

◆ find_representative() [2/2]

bool mcrl2::data::representative_generator::find_representative ( const sort_expression &  sort,
std::set< sort_expression > &  visited_sorts,
data_expression &  result 
)
inlineprotected

Finds a representative element for an arbitrary sort expression.

Parameters
[in]sortthe sort for which to find the representative
[in]visited_sortsA set of sorts for which no representative can be constructed. This is used to prevent
[out]resultThe representative of the shape f(t1,...,tn). This is only set if this function yields true.
Returns
a boolean indicating whether a representative has successfully been found.

Definition at line 141 of file representative_generator.h.

◆ operator()()

data_expression mcrl2::data::representative_generator::operator() ( const sort_expression &  sort)
inline

Returns a representative of a sort.

Parameters
[in]sortsort of which to find a representatitive

Definition at line 269 of file representative_generator.h.

◆ search_for_lexicographically_minimal_symbol()

bool mcrl2::data::representative_generator::search_for_lexicographically_minimal_symbol ( function_symbol &  f_result,
const sort_expression &  sort,
const std::vector< function_symbol > &  function_symbols 
)
inlineprotected

Definition at line 109 of file representative_generator.h.

◆ set_representative()

void mcrl2::data::representative_generator::set_representative ( const sort_expression &  sort,
const data_expression &  representative 
)
inlineprotected

Sets a data expression as representative of the sort.

Parameters
[in]sortthe sort of which to set the representative
[in]representativethe data expression that serves as representative

Definition at line 68 of file representative_generator.h.

Member Data Documentation

◆ m_representatives_cache

std::map< sort_expression, data_expression > mcrl2::data::representative_generator::m_representatives_cache
protected

Serves as a cache for later find operations.

Definition at line 61 of file representative_generator.h.

◆ m_specification

const data_specification& mcrl2::data::representative_generator::m_specification
protected

Data specification context.

Definition at line 58 of file representative_generator.h.

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