mcrl2::data::representative_generator

Include file:

#include "mcrl2/data/representative_generator.h
class mcrl2::data::representative_generator

Components for generating an arbitrary element of a sort.

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.

Protected attributes

std::map<sort_expression, data_expression> m_representatives_cache

Serves as a cache for later find operations.

const data_specification &m_specification

Data specification context.

Protected member functions

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.

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

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.

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.

void 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

Public member functions

data_expression 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.