mcrl2/data/function_update.h

Include file:

#include "mcrl2/data/function_update.h"

The standard sort function_update.

This file was generated from the data sort specification mcrl2/data/build/function_update.spec.

Typedefs

type mcrl2::data::implementation_map

typedef for std::map< function_symbol, std::pair< std::function< data_expression(const data_expression &)>, std::string > >

Functions

const data_expression &mcrl2::data::arg1(const data_expression &e)

Function for projecting out argument. arg1 from an application.

Parameters:

  • e A data expression.

Pre: arg1 is defined for e.

Returns: The argument of e that corresponds to arg1.

const data_expression &mcrl2::data::arg2(const data_expression &e)

Function for projecting out argument. arg2 from an application.

Parameters:

  • e A data expression.

Pre: arg2 is defined for e.

Returns: The argument of e that corresponds to arg2.

const data_expression &mcrl2::data::arg3(const data_expression &e)

Function for projecting out argument. arg3 from an application.

Parameters:

  • e A data expression.

Pre: arg3 is defined for e.

Returns: The argument of e that corresponds to arg3.

function_symbol mcrl2::data::function_update(const sort_expression &s, const sort_expression &t)

Constructor for function symbol @func_update.

Parameters:

  • s A sort expression.
  • t A sort expression.

Returns: Function symbol function_update.

application mcrl2::data::function_update(const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Application of function symbol @func_update.

Parameters:

  • s A sort expression.
  • t A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
  • arg2 A data expression.

Returns: Application of @func_update to a number of arguments.

implementation_map mcrl2::data::function_update_cpp_implementable_constructors()

Give all system defined constructors which have an implementation in C++ and not in rewrite rules for function_update.

Returns: All system defined constructors that are to be implemented in C++ for function_update.

implementation_map mcrl2::data::function_update_cpp_implementable_mappings(const sort_expression &s, const sort_expression &t)

Give all system defined mappings that are to be implemented in C++ code for function_update.

Parameters:

  • s A sort expression
  • t A sort expression

Returns: A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for function_update

function_symbol_vector mcrl2::data::function_update_generate_constructors_and_functions_code(const sort_expression &s, const sort_expression &t)

Give all system defined mappings and constructors for function_update.

Parameters:

  • s A sort expression
  • t A sort expression

Returns: All system defined mappings for function_update

function_symbol_vector mcrl2::data::function_update_generate_constructors_code()

Give all system defined constructors for function_update.

Returns: All system defined constructors for function_update.

data_equation_vector mcrl2::data::function_update_generate_equations_code(const sort_expression &s, const sort_expression &t)

Give all system defined equations for function_update.

Parameters:

  • s A sort expression
  • t A sort expression

Returns: All system defined equations for sort function_update

function_symbol_vector mcrl2::data::function_update_generate_functions_code(const sort_expression &s, const sort_expression &t)

Give all system defined mappings for function_update.

Parameters:

  • s A sort expression
  • t A sort expression

Returns: All system defined mappings for function_update

function_symbol_vector mcrl2::data::function_update_mCRL2_usable_constructors()

Give all defined constructors which can be used in mCRL2 specs for function_update.

Returns: All system defined constructors that can be used in an mCRL2 specification for function_update.

function_symbol_vector mcrl2::data::function_update_mCRL2_usable_mappings(const sort_expression &s, const sort_expression &t)

Give all system defined mappings that can be used in mCRL2 specs for function_update.

Parameters:

  • s A sort expression
  • t A sort expression

Returns: All system defined mappings for that can be used in mCRL2 specificationis function_update

const core::identifier_string &mcrl2::data::function_update_name()

Generate identifier @func_update.

Returns: Identifier @func_update.

function_symbol mcrl2::data::function_update_stable(const sort_expression &s, const sort_expression &t)

Constructor for function symbol @func_update_stable.

Parameters:

  • s A sort expression.
  • t A sort expression.

Returns: Function symbol function_update_stable.

application mcrl2::data::function_update_stable(const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Application of function symbol @func_update_stable.

Parameters:

  • s A sort expression.
  • t A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
  • arg2 A data expression.

Returns: Application of @func_update_stable to a number of arguments.

const core::identifier_string &mcrl2::data::function_update_stable_name()

Generate identifier @func_update_stable.

Returns: Identifier @func_update_stable.

function_symbol mcrl2::data::if_always_else(const sort_expression &s, const sort_expression &t)

Constructor for function symbol @if_always_else.

Parameters:

  • s A sort expression.
  • t A sort expression.

Returns: Function symbol if_always_else.

application mcrl2::data::if_always_else(const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Application of function symbol @if_always_else.

Parameters:

  • s A sort expression.
  • t A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
  • arg2 A data expression.

Returns: Application of @if_always_else to a number of arguments.

data_expression mcrl2::data::if_always_else_application(const data_expression &a1)

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

data_expression mcrl2::data::if_always_else_manual_implementation(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

The data expression of an application of the function symbol @if_always_else.

This function is to be implemented manually.

Parameters:

  • arg0 A data expression.
  • arg1 A data expression.
  • arg2 A data expression.

Returns: The data expression corresponding to an application of @if_always_else to a number of arguments.

const core::identifier_string &mcrl2::data::if_always_else_name()

Generate identifier @if_always_else.

Returns: Identifier @if_always_else.

bool mcrl2::data::is_function_update_application(const atermpp::aterm_appl &e)

Recogniser for application of @func_update.

Parameters:

  • e A data expression.

Returns: true iff e is an application of function symbol function_update to a number of arguments.

bool mcrl2::data::is_function_update_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @func_update.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @func_update.

bool mcrl2::data::is_function_update_stable_application(const atermpp::aterm_appl &e)

Recogniser for application of @func_update_stable.

Parameters:

  • e A data expression.

Returns: true iff e is an application of function symbol function_update_stable to a number of arguments.

bool mcrl2::data::is_function_update_stable_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @func_update_stable.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @func_update_stable.

bool mcrl2::data::is_if_always_else_application(const atermpp::aterm_appl &e)

Recogniser for application of @if_always_else.

Parameters:

  • e A data expression.

Returns: true iff e is an application of function symbol if_always_else to a number of arguments.

bool mcrl2::data::is_if_always_else_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @if_always_else.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @if_always_else.

bool mcrl2::data::is_is_not_a_function_update_application(const atermpp::aterm_appl &e)

Recogniser for application of @is_not_an_update.

Parameters:

  • e A data expression.

Returns: true iff e is an application of function symbol is_not_a_function_update to a number of arguments.

bool mcrl2::data::is_is_not_a_function_update_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @is_not_an_update.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @is_not_an_update.

function_symbol mcrl2::data::is_not_a_function_update(const sort_expression &s, const sort_expression &t)

Constructor for function symbol @is_not_an_update.

Parameters:

  • s A sort expression.
  • t A sort expression.

Returns: Function symbol is_not_a_function_update.

application mcrl2::data::is_not_a_function_update(const sort_expression &s, const sort_expression &t, const data_expression &arg0)

Application of function symbol @is_not_an_update.

Parameters:

  • s A sort expression.
  • t A sort expression.
  • arg0 A data expression.

Returns: Application of @is_not_an_update to a number of arguments.

data_expression mcrl2::data::is_not_a_function_update_application(const data_expression &a1)

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

data_expression mcrl2::data::is_not_a_function_update_manual_implementation(const data_expression &arg0)

The data expression of an application of the function symbol @is_not_an_update.

This function is to be implemented manually.

Parameters:

  • arg0 A data expression.

Returns: The data expression corresponding to an application of @is_not_an_update to a number of arguments.

const core::identifier_string &mcrl2::data::is_not_a_function_update_name()

Generate identifier @is_not_an_update.

Returns: Identifier @is_not_an_update.

void mcrl2::data::make_function_update(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Make an application of function symbol @func_update.

Parameters:

  • result The data expression where the @func_update expression is put.
  • s A sort expression.
  • t A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
  • arg2 A data expression.
void mcrl2::data::make_function_update_stable(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Make an application of function symbol @func_update_stable.

Parameters:

  • result The data expression where the @func_update_stable expression is put.
  • s A sort expression.
  • t A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
  • arg2 A data expression.
void mcrl2::data::make_if_always_else(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Make an application of function symbol @if_always_else.

Parameters:

  • result The data expression where the @if_always_else expression is put.
  • s A sort expression.
  • t A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
  • arg2 A data expression.
void mcrl2::data::make_is_not_a_function_update(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0)

Make an application of function symbol @is_not_an_update.

Parameters:

  • result The data expression where the @is_not_an_update expression is put.
  • s A sort expression.
  • t A sort expression.
  • arg0 A data expression.