Include file:
#include "mcrl2/data/representative_generator.h
mcrl2::data::
representative_generator
¶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 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.
mcrl2::data::representative_generator::
m_representatives_cache
¶Serves as a cache for later find operations.
mcrl2::data::representative_generator::
m_specification
¶Data specification context.
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.
Parameters:
Returns: a boolean indicating whether a representative has successfully been found.
Pre: symbol.sort() is of type function_sort
find_representative
(const sort_expression &sort, std::set<sort_expression> &visited_sorts, data_expression &result)¶Finds a representative element for an arbitrary sort expression.
Parameters:
Returns: a boolean indicating whether a representative has successfully been found.
set_representative
(const sort_expression &sort, const data_expression &representative)¶Sets a data expression as representative of the sort.
Parameters:
operator()
(const sort_expression &sort)Returns a representative of a sort.
Parameters:
representative_generator
(const data_specification &specification)¶Constructor with data specification as context.