mCRL2
Loading...
Searching...
No Matches
pos1.h File Reference

Go to the source code of this file.

Namespaces

namespace  mcrl2
 A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
 
namespace  mcrl2::data
 Namespace for all data library functionality.
 
namespace  mcrl2::data::sort_pos
 Namespace for system defined sort pos.
 

Typedefs

typedef std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > mcrl2::data::sort_pos::implementation_map
 

Functions

const core::identifier_stringmcrl2::data::sort_pos::pos_name ()
 
const basic_sortmcrl2::data::sort_pos::pos ()
 Constructor for sort expression Pos.
 
bool mcrl2::data::sort_pos::is_pos (const sort_expression &e)
 Recogniser for sort expression Pos.
 
const core::identifier_stringmcrl2::data::sort_pos::c1_name ()
 Generate identifier @c1.
 
const function_symbolmcrl2::data::sort_pos::c1 ()
 Constructor for function symbol @c1.
 
bool mcrl2::data::sort_pos::is_c1_function_symbol (const atermpp::aterm &e)
 Recogniser for function @c1.
 
const core::identifier_stringmcrl2::data::sort_pos::cdub_name ()
 Generate identifier @cDub.
 
const function_symbolmcrl2::data::sort_pos::cdub ()
 Constructor for function symbol @cDub.
 
bool mcrl2::data::sort_pos::is_cdub_function_symbol (const atermpp::aterm &e)
 Recogniser for function @cDub.
 
application mcrl2::data::sort_pos::cdub (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @cDub.
 
void mcrl2::data::sort_pos::make_cdub (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @cDub.
 
bool mcrl2::data::sort_pos::is_cdub_application (const atermpp::aterm &e)
 Recogniser for application of @cDub.
 
function_symbol_vector mcrl2::data::sort_pos::pos_generate_constructors_code ()
 Give all system defined constructors for pos.
 
function_symbol_vector mcrl2::data::sort_pos::pos_mCRL2_usable_constructors ()
 Give all defined constructors which can be used in mCRL2 specs for pos.
 
implementation_map mcrl2::data::sort_pos::pos_cpp_implementable_constructors ()
 Give all system defined constructors which have an implementation in C++ and not in rewrite rules for pos.
 
const core::identifier_stringmcrl2::data::sort_pos::maximum_name ()
 Generate identifier max.
 
const function_symbolmcrl2::data::sort_pos::maximum ()
 Constructor for function symbol max.
 
bool mcrl2::data::sort_pos::is_maximum_function_symbol (const atermpp::aterm &e)
 Recogniser for function max.
 
application mcrl2::data::sort_pos::maximum (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol max.
 
void mcrl2::data::sort_pos::make_maximum (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol max.
 
bool mcrl2::data::sort_pos::is_maximum_application (const atermpp::aterm &e)
 Recogniser for application of max.
 
const core::identifier_stringmcrl2::data::sort_pos::minimum_name ()
 Generate identifier min.
 
const function_symbolmcrl2::data::sort_pos::minimum ()
 Constructor for function symbol min.
 
bool mcrl2::data::sort_pos::is_minimum_function_symbol (const atermpp::aterm &e)
 Recogniser for function min.
 
application mcrl2::data::sort_pos::minimum (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol min.
 
void mcrl2::data::sort_pos::make_minimum (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol min.
 
bool mcrl2::data::sort_pos::is_minimum_application (const atermpp::aterm &e)
 Recogniser for application of min.
 
const core::identifier_stringmcrl2::data::sort_pos::succ_name ()
 Generate identifier succ.
 
const function_symbolmcrl2::data::sort_pos::succ ()
 Constructor for function symbol succ.
 
bool mcrl2::data::sort_pos::is_succ_function_symbol (const atermpp::aterm &e)
 Recogniser for function succ.
 
application mcrl2::data::sort_pos::succ (const data_expression &arg0)
 Application of function symbol succ.
 
void mcrl2::data::sort_pos::make_succ (data_expression &result, const data_expression &arg0)
 Make an application of function symbol succ.
 
bool mcrl2::data::sort_pos::is_succ_application (const atermpp::aterm &e)
 Recogniser for application of succ.
 
const core::identifier_stringmcrl2::data::sort_pos::pos_predecessor_name ()
 Generate identifier @pospred.
 
const function_symbolmcrl2::data::sort_pos::pos_predecessor ()
 Constructor for function symbol @pospred.
 
bool mcrl2::data::sort_pos::is_pos_predecessor_function_symbol (const atermpp::aterm &e)
 Recogniser for function @pospred.
 
application mcrl2::data::sort_pos::pos_predecessor (const data_expression &arg0)
 Application of function symbol @pospred.
 
void mcrl2::data::sort_pos::make_pos_predecessor (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @pospred.
 
bool mcrl2::data::sort_pos::is_pos_predecessor_application (const atermpp::aterm &e)
 Recogniser for application of @pospred.
 
const core::identifier_stringmcrl2::data::sort_pos::plus_name ()
 Generate identifier +.
 
const function_symbolmcrl2::data::sort_pos::plus ()
 Constructor for function symbol +.
 
bool mcrl2::data::sort_pos::is_plus_function_symbol (const atermpp::aterm &e)
 Recogniser for function +.
 
application mcrl2::data::sort_pos::plus (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol +.
 
void mcrl2::data::sort_pos::make_plus (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol +.
 
bool mcrl2::data::sort_pos::is_plus_application (const atermpp::aterm &e)
 Recogniser for application of +.
 
const core::identifier_stringmcrl2::data::sort_pos::add_with_carry_name ()
 Generate identifier @addc.
 
const function_symbolmcrl2::data::sort_pos::add_with_carry ()
 Constructor for function symbol @addc.
 
bool mcrl2::data::sort_pos::is_add_with_carry_function_symbol (const atermpp::aterm &e)
 Recogniser for function @addc.
 
application mcrl2::data::sort_pos::add_with_carry (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @addc.
 
void mcrl2::data::sort_pos::make_add_with_carry (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @addc.
 
bool mcrl2::data::sort_pos::is_add_with_carry_application (const atermpp::aterm &e)
 Recogniser for application of @addc.
 
const core::identifier_stringmcrl2::data::sort_pos::times_name ()
 Generate identifier *.
 
const function_symbolmcrl2::data::sort_pos::times ()
 Constructor for function symbol *.
 
bool mcrl2::data::sort_pos::is_times_function_symbol (const atermpp::aterm &e)
 Recogniser for function *.
 
application mcrl2::data::sort_pos::times (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol *.
 
void mcrl2::data::sort_pos::make_times (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol *.
 
bool mcrl2::data::sort_pos::is_times_application (const atermpp::aterm &e)
 Recogniser for application of *.
 
const core::identifier_stringmcrl2::data::sort_pos::powerlog2_pos_name ()
 Generate identifier @powerlog2.
 
const function_symbolmcrl2::data::sort_pos::powerlog2_pos ()
 Constructor for function symbol @powerlog2.
 
bool mcrl2::data::sort_pos::is_powerlog2_pos_function_symbol (const atermpp::aterm &e)
 Recogniser for function @powerlog2.
 
application mcrl2::data::sort_pos::powerlog2_pos (const data_expression &arg0)
 Application of function symbol @powerlog2.
 
void mcrl2::data::sort_pos::make_powerlog2_pos (data_expression &result, const data_expression &arg0)
 Make an application of function symbol @powerlog2.
 
bool mcrl2::data::sort_pos::is_powerlog2_pos_application (const atermpp::aterm &e)
 Recogniser for application of @powerlog2.
 
function_symbol_vector mcrl2::data::sort_pos::pos_generate_functions_code ()
 Give all system defined mappings for pos.
 
function_symbol_vector mcrl2::data::sort_pos::pos_generate_constructors_and_functions_code ()
 Give all system defined mappings and constructors for pos.
 
function_symbol_vector mcrl2::data::sort_pos::pos_mCRL2_usable_mappings ()
 Give all system defined mappings that can be used in mCRL2 specs for pos.
 
implementation_map mcrl2::data::sort_pos::pos_cpp_implementable_mappings ()
 Give all system defined mappings that are to be implemented in C++ code for pos.
 
const data_expressionmcrl2::data::sort_pos::left (const data_expression &e)
 Function for projecting out argument. left from an application.
 
const data_expressionmcrl2::data::sort_pos::right (const data_expression &e)
 Function for projecting out argument. right from an application.
 
const data_expressionmcrl2::data::sort_pos::arg (const data_expression &e)
 Function for projecting out argument. arg from an application.
 
const data_expressionmcrl2::data::sort_pos::arg1 (const data_expression &e)
 Function for projecting out argument. arg1 from an application.
 
const data_expressionmcrl2::data::sort_pos::arg2 (const data_expression &e)
 Function for projecting out argument. arg2 from an application.
 
const data_expressionmcrl2::data::sort_pos::arg3 (const data_expression &e)
 Function for projecting out argument. arg3 from an application.
 
data_equation_vector mcrl2::data::sort_pos::pos_generate_equations_code ()
 Give all system defined equations for pos.