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:
symbol The function symbol f using which the representative is constructed.
visited_sorts A set of sorts for which no representative can be constructed. This is used to prevent
result The 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.
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:
sort the sort for which to find the representative
visited_sorts A set of sorts for which no representative can be constructed. This is used to prevent
result The 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.
set_representative
(const sort_expression &sort, const data_expression &representative)¶Sets a data expression as representative of the sort.
Parameters:
sort the sort of which to set the representative
representative the data expression that serves as representative
operator()
(const sort_expression &sort)Returns a representative of a sort.
Parameters:
sort sort of which to find a representatitive
representative_generator
(const data_specification &specification)¶Constructor with data specification as context.