mcrl2::process::detail Namespace Reference

Classes
struct	action_actions
class	action_context
struct	add_capture_avoiding_replacement
struct	add_capture_avoiding_replacement_with_an_identifier_generator
struct	alphabet_bounded_traverser
	Traverser that computes the alphabet of process expressions. More...
struct	alphabet_efficient_traverser
	Traverser that computes the alphabet of process expressions. This version should be more efficient than the default one. More...
struct	alphabet_intersection_traverser
struct	alphabet_new_traverser
	Traverser that computes the alphabet of process expressions. More...
struct	alphabet_node
struct	alphabet_pcrl_traverser
	Traverser that computes the alphabet of pCRL process expressions. More...
struct	alphabet_traverser
	Traverser that computes the alphabet of process expressions. More...
struct	anonymize_builder
struct	anonymize_builder_instance
struct	apply_alphabet_efficient_traverser
struct	apply_alphabet_intersection_traverser
struct	apply_alphabet_traverser
struct	apply_push_allow_traverser
struct	apply_push_block_builder
struct	balance_summands_builder
struct	communicating_lpe_traverser
	Checks if a process expression is 'communicating LPE'. More...
struct	duplicate_equation_removal
struct	expand_process_instance_assignments_builder
struct	find_process_identifiers_traverser
struct	find_subterm_traverser
struct	is_guarded_traverser
struct	is_stochastic_traverser
struct	linear_process_conversion_traverser
	Converts a process expression into linear process format. Use the convert member functions for this. More...
struct	linear_process_expression_traverser
	Checks if a process equation is linear. Use the is_linear() member function for this. More...
struct	position_count_traverser
struct	printer
struct	process_actions
struct	process_command
class	process_context
struct	process_instance_replace_builder
struct	process_rewriter_command
	Process command that uses a rewrite strategy. More...
struct	process_traversal_algorithm
struct	process_variable_dependency_graph_traverser
	Creates a dependency graph of process variables. More...
struct	process_variable_dependency_traverser
	Computes dependencies of a process expression. More...
struct	process_variable_scc_algorithm
struct	push_allow_cache
struct	push_allow_node
struct	push_allow_traverser
struct	push_block_builder
struct	push_block_printer
struct	remove_data_parameters_builder
struct	replace_capture_avoiding_variables__with_an_identifier_generator_builder
struct	replace_subterm_builder
struct	stochastic_linear_process_conversion_traverser
	Converts a process expression into linear process format. Use the convert member functions for this. More...
struct	sync_multi_action_name_traverser
class	tarjan_scc_algorithm
struct	typecheck_builder

Functions
std::ostream &	operator<< (std::ostream &out, const alphabet_node &x)
alphabet_node	alphabet (const process_expression &x, const std::vector< process_equation > &equations, std::set< process_identifier > &W)
multi_action_name_set	alphabet_bounded (const process_expression &x, const allow_set &A, const std::vector< process_equation > &equations, const std::map< process_identifier, multi_action_name_set > &cache)
alphabet_node	alphabet_efficient (const process_expression &x, const std::vector< process_equation > &equations, std::set< process_identifier > &W)
alphabet_node	alphabet_intersection (const process_expression &x, const std::vector< process_equation > &equations, std::set< process_identifier > &W, const multi_action_name_set &A)
multi_action_name_set	alphabet_intersection (const process_expression &x, const std::vector< process_equation > &equations, const multi_action_name_set &A)
std::string	remove_braces (const std::string &text)
std::pair< std::string, bool >	remove_trailing_at_symbol (const std::string &text)
std::vector< std::string >	set_elements (const std::string &text)
std::pair< std::string, std::string >	split_arrow (const std::string &text)
std::vector< std::string >	split_bar (const std::string &text)
std::vector< std::string >	split_characters (const std::string &text)
core::identifier_string_list	make_identifier_string_list (const std::vector< std::string > &words)
multi_action_name	make_multi_action (const std::vector< std::string > &words)
multi_action_name	parse_multi_action_name (const std::string &text)
multi_action_name_set	parse_multi_action_name_set (const std::string &text)
multi_action_name	parse_simple_multi_action_name (const std::string &text)
std::pair< multi_action_name_set, bool >	parse_simple_multi_action_name_set (const std::string &text)
action_name_multiset_list	parse_allow_set (const std::string &text)
core::identifier_string_list	parse_block_set (const std::string &text)
communication_expression_list	parse_comm_set (const std::string &text)
rename_expression_list	parse_rename_set (const std::string &text)
process_expression	construct_allow (const multi_action_name_set &A, const process_expression &x, bool allow_required)
std::ostream &	operator<< (std::ostream &out, const push_allow_cache::alphabet_key &x)
char	print_alphabet_status (push_allow_cache::alphabet_status status)
std::ostream &	operator<< (std::ostream &out, const push_allow_cache::alphabet_value &x)
std::ostream &	operator<< (std::ostream &out, const push_allow_cache::unfinished_value &x)
std::ostream &	operator<< (std::ostream &out, const push_allow_cache &W)
std::ostream &	operator<< (std::ostream &out, const push_allow_node &x)
push_allow_node	push_allow (const process_expression &x, const allow_set &A, std::vector< process_equation > &equations, push_allow_cache &W, bool generate_missing_equations=false)
std::string	print_B (const std::set< core::identifier_string > &B)
process_expression	push_block (const std::set< core::identifier_string > &B, const process_expression &x, std::vector< process_equation > &equations, push_block_cache &W, data::set_identifier_generator &id_generator)
std::tuple< bool, data::data_expression_vector, std::string >	match_action_parameters (const data::data_expression_list &parameters, const data::sort_expression_list &expected_sorts, const data::detail::variable_context &variable_context, data::data_type_checker &typechecker)
std::pair< data::data_expression_list, data::sort_expression_list >	match_action_parameters (const data::data_expression_list &parameters, const data::sorts_list &possible_parameter_sorts, const data::detail::variable_context &variable_context, const core::identifier_string &name, const std::string &msg, data::data_type_checker &typechecker)
std::map< process_identifier, multi_action_name_set >	compute_pcrl_equation_cache (const std::vector< process_equation > &equations)
std::map< process_identifier, multi_action_name_set >	compute_pcrl_equation_cache (const std::vector< process_equation > &equations, const process_expression &init)
std::vector< std::size_t >	position_counts (const process_specification &x)
process_specification	parse_process_specification (const std::string &input_filename)
	Loads a process specification from input_filename, or from stdin if filename equals "".
data::data_expression_list	make_data_expression_list (const data::variable_list &x)
	Convert data::variable_list to data::expression_list.
process_instance	make_process_instance (const process_instance_assignment &x)
	Convert a process instance assignment to a process instance.
process_instance	make_process_instance (const process_expression &x)
	Precondition: x is a process instance or a process instance assignment.
data::mutable_map_substitution	make_process_instance_substitution (const process_instance &x)
	Given P(2, 3) it returns the substitution [x := 2, y := 3] for process identifier P(x, y).
process_instance	apply_substitution (const process_instance &x, data::mutable_map_substitution<> &sigma)
	Applies sigma to the arguments of x.
bool	is_guarded (const process_expression &x, const std::vector< process_equation > &equations, std::set< process_identifier > &W)
bool	check_process_instance_assignment (const process_equation &eq, const process_instance_assignment &inst)
	Returns true if the process instance assignment a matches with the process equation eq.
bool	check_process_instance (const process_equation &eq, const process_instance &init)
	Returns true if the process instance a matches with the process equation eq.
bool	is_process (const process_expression &x)
	Returns true if the argument is a process instance.
bool	is_stochastic_process (const process_expression &x)
	Returns true if the argument is a process instance, optionally wrapped in a stochastic distribution.
bool	is_timed_deadlock (const process_expression &x)
	Returns true if the argument is a deadlock.
bool	is_multiaction (const process_expression &x)
	Returns true if the argument is a multi-action.
bool	is_timed_multiaction (const process_expression &x)
	Returns true if the argument is a multi-action.
bool	is_action_prefix (const process_expression &x)
	Returns true if the argument is an action prefix.
bool	is_conditional_deadlock (const process_expression &x)
	Returns true if the argument is a conditional deadlock.
bool	is_conditional_action_prefix (const process_expression &x)
	Returns true if the argument is a conditional action prefix.
bool	is_alternative (const process_expression &x)
	Returns true if the argument is an alternative composition.
bool	is_linear_process_term (const process_expression &x)
	Returns true if the argument is a linear process.
process_expression	parse_process_expression_new (const std::string &text)
process_specification	parse_process_specification_new (const std::string &text)
void	complete_process_specification (process_specification &x, bool alpha_reduce=false)
std::set< process_identifier >	find_process_identifiers (const process_expression &x)
template<template< class > class Builder, template< template< class > class, class, class, class > class Binder, class Substitution , class IdentifierGenerator >
replace_capture_avoiding_variables__with_an_identifier_generator_builder< Builder, Binder, Substitution, IdentifierGenerator >	apply_replace_capture_avoiding_variables__with_an_identifier_generator_builder (Substitution &sigma, IdentifierGenerator &id_generator)
bool	equal_multi_actions (core::identifier_string_list a1, core::identifier_string_list a2)
bool	multi_actions_contains (const core::identifier_string_list &a, const action_name_multiset_list &A)
std::ostream &	operator<< (std::ostream &out, const std::pair< core::identifier_string, data::sort_expression_list > &x)
typecheck_builder	make_typecheck_builder (data::data_type_checker &data_typechecker, const data::detail::variable_context &variables, const detail::process_context &process_identifiers, const detail::action_context &action_context, const process_identifier *current_equation=nullptr)

Function Documentation

alphabet()

alphabet_node mcrl2::process::detail::alphabet ( const process_expression &  x, const std::vector< process_equation > &  equations, std::set< process_identifier > &  W  )

inline

Definition at line 262 of file alphabet.h.

alphabet_bounded()

multi_action_name_set mcrl2::process::detail::alphabet_bounded ( const process_expression &  x, const allow_set &  A, const std::vector< process_equation > &  equations, const std::map< process_identifier, multi_action_name_set > &  cache  )

inline

Definition at line 243 of file alphabet_bounded.h.

alphabet_efficient()

alphabet_node mcrl2::process::detail::alphabet_efficient ( const process_expression &  x, const std::vector< process_equation > &  equations, std::set< process_identifier > &  W  )

inline

Definition at line 118 of file alphabet_efficient.h.

alphabet_intersection() [1/2]

multi_action_name_set mcrl2::process::detail::alphabet_intersection ( const process_expression &  x, const std::vector< process_equation > &  equations, const multi_action_name_set &  A  )

inline

Definition at line 132 of file alphabet_intersection.h.

alphabet_intersection() [2/2]

alphabet_node mcrl2::process::detail::alphabet_intersection ( const process_expression &  x, const std::vector< process_equation > &  equations, std::set< process_identifier > &  W, const multi_action_name_set &  A  )

inline

Definition at line 124 of file alphabet_intersection.h.

apply_replace_capture_avoiding_variables__with_an_identifier_generator_builder()

template<template< class > class Builder, template< template< class > class, class, class, class > class Binder, class Substitution , class IdentifierGenerator >

replace_capture_avoiding_variables__with_an_identifier_generator_builder< Builder, Binder, Substitution, IdentifierGenerator > mcrl2::process::detail::apply_replace_capture_avoiding_variables__with_an_identifier_generator_builder	(	Substitution &	sigma,
		IdentifierGenerator &	id_generator
	)

Definition at line 121 of file replace_capture_avoiding_with_an_identifier_generator.h.

apply_substitution()

process_instance mcrl2::process::detail::apply_substitution ( const process_instance &  x, data::mutable_map_substitution<> &  sigma  )

inline

Applies sigma to the arguments of x.

Definition at line 88 of file eliminate_trivial_equations.h.

check_process_instance()

bool mcrl2::process::detail::check_process_instance ( const process_equation &  eq, const process_instance &  init  )

inline

Returns true if the process instance a matches with the process equation eq.

Definition at line 49 of file is_linear.h.

check_process_instance_assignment()

bool mcrl2::process::detail::check_process_instance_assignment ( const process_equation &  eq, const process_instance_assignment &  inst  )

inline

Returns true if the process instance assignment a matches with the process equation eq.

Definition at line 28 of file is_linear.h.

complete_process_specification()

void mcrl2::process::detail::complete_process_specification	(	process_specification &	x,
		bool	alpha_reduce = false
	)

Definition at line 151 of file process.cpp.

compute_pcrl_equation_cache() [1/2]

std::map< process_identifier, multi_action_name_set > mcrl2::process::detail::compute_pcrl_equation_cache ( const std::vector< process_equation > &  equations )

inline

Definition at line 27 of file pcrl_equation_cache.h.

compute_pcrl_equation_cache() [2/2]

std::map< process_identifier, multi_action_name_set > mcrl2::process::detail::compute_pcrl_equation_cache ( const std::vector< process_equation > &  equations, const process_expression &  init  )

inline

Definition at line 87 of file pcrl_equation_cache.h.

construct_allow()

process_expression mcrl2::process::detail::construct_allow ( const multi_action_name_set &  A, const process_expression &  x, bool  allow_required  )

inline

Definition at line 28 of file alphabet_push_allow.h.

equal_multi_actions()

bool mcrl2::process::detail::equal_multi_actions ( core::identifier_string_list  a1, core::identifier_string_list  a2  )

inline

Definition at line 92 of file typecheck.h.

find_process_identifiers()

std::set< process_identifier > mcrl2::process::detail::find_process_identifiers ( const process_expression &  x )

inline

Definition at line 169 of file process_variable_strongly_connected_components.h.

is_action_prefix()

bool mcrl2::process::detail::is_action_prefix ( const process_expression &  x )

inline

Returns true if the argument is an action prefix.

Definition at line 123 of file is_linear.h.

is_alternative()

bool mcrl2::process::detail::is_alternative ( const process_expression &  x )

inline

Returns true if the argument is an alternative composition.

Definition at line 147 of file is_linear.h.

is_conditional_action_prefix()

bool mcrl2::process::detail::is_conditional_action_prefix ( const process_expression &  x )

inline

Returns true if the argument is a conditional action prefix.

Definition at line 139 of file is_linear.h.

is_conditional_deadlock()

bool mcrl2::process::detail::is_conditional_deadlock ( const process_expression &  x )

inline

Returns true if the argument is a conditional deadlock.

Definition at line 131 of file is_linear.h.

is_guarded()

bool mcrl2::process::detail::is_guarded ( const process_expression &  x, const std::vector< process_equation > &  equations, std::set< process_identifier > &  W  )

inline

Definition at line 86 of file is_guarded.h.

is_linear_process_term()

bool mcrl2::process::detail::is_linear_process_term ( const process_expression &  x )

inline

Returns true if the argument is a linear process.

Definition at line 157 of file is_linear.h.

is_multiaction()

bool mcrl2::process::detail::is_multiaction ( const process_expression &  x )

inline

Returns true if the argument is a multi-action.

Definition at line 105 of file is_linear.h.

is_process()

bool mcrl2::process::detail::is_process ( const process_expression &  x )

inline

Returns true if the argument is a process instance.

Definition at line 71 of file is_linear.h.

is_stochastic_process()

bool mcrl2::process::detail::is_stochastic_process ( const process_expression &  x )

inline

Returns true if the argument is a process instance, optionally wrapped in a stochastic distribution.

Definition at line 81 of file is_linear.h.

is_timed_deadlock()

bool mcrl2::process::detail::is_timed_deadlock ( const process_expression &  x )

inline

Returns true if the argument is a deadlock.

Definition at line 96 of file is_linear.h.

is_timed_multiaction()

bool mcrl2::process::detail::is_timed_multiaction ( const process_expression &  x )

inline

Returns true if the argument is a multi-action.

Definition at line 115 of file is_linear.h.

make_data_expression_list()

data::data_expression_list mcrl2::process::detail::make_data_expression_list ( const data::variable_list &  x )

inline

Convert data::variable_list to data::expression_list.

Definition at line 27 of file eliminate_trivial_equations.h.

make_identifier_string_list()

core::identifier_string_list mcrl2::process::detail::make_identifier_string_list ( const std::vector< std::string > &  words )

inline

Definition at line 99 of file alphabet_parse.h.

make_multi_action()

multi_action_name mcrl2::process::detail::make_multi_action ( const std::vector< std::string > &  words )

inline

Definition at line 111 of file alphabet_parse.h.

make_process_instance() [1/2]

process_instance mcrl2::process::detail::make_process_instance ( const process_expression &  x )

inline

Precondition: x is a process instance or a process instance assignment.

Definition at line 55 of file eliminate_trivial_equations.h.

make_process_instance() [2/2]

process_instance mcrl2::process::detail::make_process_instance ( const process_instance_assignment &  x )

inline

Convert a process instance assignment to a process instance.

Definition at line 34 of file eliminate_trivial_equations.h.

make_process_instance_substitution()

data::mutable_map_substitution mcrl2::process::detail::make_process_instance_substitution ( const process_instance &  x )

inline

Given P(2, 3) it returns the substitution [x := 2, y := 3] for process identifier P(x, y).

Definition at line 69 of file eliminate_trivial_equations.h.

make_typecheck_builder()

typecheck_builder mcrl2::process::detail::make_typecheck_builder ( data::data_type_checker &  data_typechecker, const data::detail::variable_context &  variables, const detail::process_context &  process_identifiers, const detail::action_context &  action_context, const process_identifier *  current_equation = nullptr  )

inline

Definition at line 575 of file typecheck.h.

match_action_parameters() [1/2]

std::tuple< bool, data::data_expression_vector, std::string > mcrl2::process::detail::match_action_parameters ( const data::data_expression_list &  parameters, const data::sort_expression_list &  expected_sorts, const data::detail::variable_context &  variable_context, data::data_type_checker &  typechecker  )

inline

Definition at line 26 of file match_action_parameters.h.

match_action_parameters() [2/2]

std::pair< data::data_expression_list, data::sort_expression_list > mcrl2::process::detail::match_action_parameters ( const data::data_expression_list &  parameters, const data::sorts_list &  possible_parameter_sorts, const data::detail::variable_context &  variable_context, const core::identifier_string &  name, const std::string &  msg, data::data_type_checker &  typechecker  )

inline

Definition at line 50 of file match_action_parameters.h.

multi_actions_contains()

bool mcrl2::process::detail::multi_actions_contains ( const core::identifier_string_list &  a, const action_name_multiset_list &  A  )

inline

Definition at line 78 of file typecheck.h.

operator<<() [1/7]

std::ostream & mcrl2::process::detail::operator<< ( std::ostream &  out, const alphabet_node &  x  )

inline

Definition at line 37 of file alphabet.h.

operator<<() [2/7]

std::ostream & mcrl2::process::detail::operator<< ( std::ostream &  out, const push_allow_cache &  W  )

inline

Definition at line 238 of file alphabet_push_allow.h.

operator<<() [3/7]

std::ostream & mcrl2::process::detail::operator<< ( std::ostream &  out, const push_allow_cache::alphabet_key &  x  )

inline

Definition at line 208 of file alphabet_push_allow.h.

operator<<() [4/7]

std::ostream & mcrl2::process::detail::operator<< ( std::ostream &  out, const push_allow_cache::alphabet_value &  x  )

inline

Definition at line 226 of file alphabet_push_allow.h.

operator<<() [5/7]

std::ostream & mcrl2::process::detail::operator<< ( std::ostream &  out, const push_allow_cache::unfinished_value &  x  )

inline

Definition at line 232 of file alphabet_push_allow.h.

operator<<() [6/7]

std::ostream & mcrl2::process::detail::operator<< ( std::ostream &  out, const push_allow_node &  x  )

inline

Definition at line 274 of file alphabet_push_allow.h.

operator<<() [7/7]

std::ostream & mcrl2::process::detail::operator<< ( std::ostream &  out, const std::pair< core::identifier_string, data::sort_expression_list > &  x  )

inline

Definition at line 124 of file typecheck.h.

parse_allow_set()

action_name_multiset_list mcrl2::process::detail::parse_allow_set ( const std::string &  text )

inline

Definition at line 168 of file alphabet_parse.h.

parse_block_set()

core::identifier_string_list mcrl2::process::detail::parse_block_set ( const std::string &  text )

inline

Definition at line 179 of file alphabet_parse.h.

parse_comm_set()

communication_expression_list mcrl2::process::detail::parse_comm_set ( const std::string &  text )

inline

Definition at line 185 of file alphabet_parse.h.

parse_multi_action_name()

multi_action_name mcrl2::process::detail::parse_multi_action_name ( const std::string &  text )

inline

Definition at line 124 of file alphabet_parse.h.

parse_multi_action_name_set()

multi_action_name_set mcrl2::process::detail::parse_multi_action_name_set

(

const std::string &

text

)

Definition at line 131 of file alphabet_parse.h.

parse_process_expression_new()

process_expression mcrl2::process::detail::parse_process_expression_new

(

const std::string &

text

)

Definition at line 126 of file process.cpp.

parse_process_specification()

process_specification mcrl2::process::detail::parse_process_specification ( const std::string &  input_filename )

inline

Loads a process specification from input_filename, or from stdin if filename equals "".

Definition at line 25 of file process_io.h.

parse_process_specification_new()

process_specification mcrl2::process::detail::parse_process_specification_new

(

const std::string &

text

)

Definition at line 138 of file process.cpp.

parse_rename_set()

rename_expression_list mcrl2::process::detail::parse_rename_set ( const std::string &  text )

inline

Definition at line 197 of file alphabet_parse.h.

parse_simple_multi_action_name()

multi_action_name mcrl2::process::detail::parse_simple_multi_action_name ( const std::string &  text )

inline

Definition at line 144 of file alphabet_parse.h.

parse_simple_multi_action_name_set()

std::pair< multi_action_name_set, bool > mcrl2::process::detail::parse_simple_multi_action_name_set ( const std::string &  text )

inline

Definition at line 153 of file alphabet_parse.h.

position_counts()

std::vector< std::size_t > mcrl2::process::detail::position_counts ( const process_specification &  x )

inline

Definition at line 148 of file position_count_traverser.h.

print_alphabet_status()

char mcrl2::process::detail::print_alphabet_status ( push_allow_cache::alphabet_status  status )

inline

Definition at line 214 of file alphabet_push_allow.h.

print_B()

std::string mcrl2::process::detail::print_B ( const std::set< core::identifier_string > &  B )

inline

Definition at line 141 of file alphabet_push_block.h.

push_allow()

push_allow_node mcrl2::process::detail::push_allow ( const process_expression &  x, const allow_set &  A, std::vector< process_equation > &  equations, push_allow_cache &  W, bool  generate_missing_equations = false  )

inline

Definition at line 706 of file alphabet_push_allow.h.

push_block()

process_expression mcrl2::process::detail::push_block ( const std::set< core::identifier_string > &  B, const process_expression &  x, std::vector< process_equation > &  equations, push_block_cache &  W, data::set_identifier_generator &  id_generator  )

inline

Definition at line 347 of file alphabet_push_block.h.

remove_braces()

std::string mcrl2::process::detail::remove_braces ( const std::string &  text )

inline

Definition at line 26 of file alphabet_parse.h.

remove_trailing_at_symbol()

std::pair< std::string, bool > mcrl2::process::detail::remove_trailing_at_symbol ( const std::string &  text )

inline

Definition at line 40 of file alphabet_parse.h.

set_elements()

std::vector< std::string > mcrl2::process::detail::set_elements ( const std::string &  text )

inline

Definition at line 55 of file alphabet_parse.h.

split_arrow()

std::pair< std::string, std::string > mcrl2::process::detail::split_arrow ( const std::string &  text )

inline

Definition at line 64 of file alphabet_parse.h.

split_bar()

std::vector< std::string > mcrl2::process::detail::split_bar ( const std::string &  text )

inline

Definition at line 78 of file alphabet_parse.h.

split_characters()

std::vector< std::string > mcrl2::process::detail::split_characters ( const std::string &  text )

inline

Definition at line 86 of file alphabet_parse.h.