The main namespace for the Process library. More...

Namespaces
namespace	alphabet_operations

namespace	block_operations

namespace	detail

Classes
class	action
	\brief An action More...

class	action_label
	\brief An action label More...

struct	action_label_traverser
	\brief Traverser class More...

class	action_name_multiset
	\brief A multiset of action names More...

struct	add_data_expressions

struct	add_data_variable_binding
	Maintains a multiset of bound data variables during traversal. More...

struct	add_data_variable_builder_binding

struct	add_data_variable_traverser_binding

struct	add_process_expressions

struct	add_process_identifiers

struct	add_sort_expressions

struct	add_traverser_action_labels

struct	add_traverser_data_expressions

struct	add_traverser_identifier_strings

struct	add_traverser_process_expressions

struct	add_traverser_sort_expressions

struct	add_traverser_variables

struct	add_variables

class	allow
	\brief The allow operator More...

struct	allow_set
	Represents the set AI*. If the attribute A_includes_subsets is true, also subsets of the elements are included. An invariant of the allow_set is that elements of A do not contain elements of I. This invariant will be established during construction. More...

class	at
	\brief The at operator More...

class	block
	\brief The block operator More...

class	bounded_init
	\brief The bounded initialization More...

class	choice
	\brief The choice operator More...

class	comm
	\brief The communication operator More...

class	communication_expression
	\brief A communication expression More...

struct	data_expression_builder
	\brief Builder class More...

struct	data_expression_traverser
	\brief Traverser class More...

class	delta
	\brief The value delta More...

struct	eliminate_trivial_equations_algorithm

struct	eliminate_unused_equations_algorithm

class	hide
	\brief The hide operator More...

struct	identifier_string_traverser
	\brief Traverser class More...

class	if_then
	\brief The if-then operator More...

class	if_then_else
	\brief The if-then-else operator More...

class	left_merge
	\brief The left merge operator More...

class	merge
	\brief The merge operator More...

struct	multi_action_name
	Represents the name of a multi action. More...

class	process_equation
	\brief A process equation More...

class	process_expression
	\brief A process expression More...

struct	process_expression_builder
	\brief Builder class More...

struct	process_expression_traverser
	\brief Traverser class More...

class	process_identifier
	\brief A process identifier More...

struct	process_identifier_assignment

struct	process_identifier_builder
	\brief Builder class More...

class	process_instance
	\brief A process More...

class	process_instance_assignment
	\brief A process assignment More...

class	process_specification
	Process specification consisting of a data specification, action labels, a sequence of process equations and a process initialization. More...

class	process_type_checker

struct	push_block_cache

class	rename
	\brief The rename operator More...

class	rename_expression
	\brief A rename expression More...

class	seq
	\brief The sequential composition More...

struct	sort_expression_builder
	\brief Builder class More...

struct	sort_expression_traverser
	\brief Traverser class More...

class	stochastic_operator
	\brief The distribution operator More...

struct	stream_printer
	Prints the object x to a stream. More...

class	sum
	\brief The sum operator More...

class	sync
	\brief The synchronization operator More...

class	tau
	\brief The value tau More...

class	untyped_multi_action
	\brief An untyped multi action or data application More...

class	untyped_process_assignment
	\brief An untyped process assginment More...

struct	untyped_process_specification

struct	variable_builder
	\brief Builder class More...

struct	variable_traverser
	\brief Traverser class More...

Typedefs
typedef atermpp::term_list< action_label >	action_label_list
	\brief list of action_labels

typedef std::vector< action_label >	action_label_vector
	\brief vector of action_labels

typedef atermpp::term_list< action_name_multiset >	action_name_multiset_list
	\brief list of action_name_multisets

typedef std::vector< action_name_multiset >	action_name_multiset_vector
	\brief vector of action_name_multisets

typedef atermpp::term_list< communication_expression >	communication_expression_list
	\brief list of communication_expressions

typedef std::vector< communication_expression >	communication_expression_vector
	\brief vector of communication_expressions

typedef std::set< multi_action_name >	multi_action_name_set
	Represents a set of multi action names.

typedef atermpp::term_list< process_equation >	process_equation_list
	\brief list of process_equations

typedef std::vector< process_equation >	process_equation_vector
	\brief vector of process_equations

typedef atermpp::term_list< process_expression >	process_expression_list
	\brief list of process_expressions

typedef std::vector< process_expression >	process_expression_vector
	\brief vector of process_expressions

typedef atermpp::term_list< action >	action_list
	\brief list of actions

typedef std::vector< action >	action_vector
	\brief vector of actions

typedef atermpp::term_list< process_identifier >	process_identifier_list
	\brief list of process_identifiers

typedef std::vector< process_identifier >	process_identifier_vector
	\brief vector of process_identifiers

typedef atermpp::term_list< rename_expression >	rename_expression_list
	\brief list of rename_expressions

typedef std::vector< rename_expression >	rename_expression_vector
	\brief vector of rename_expressions

typedef atermpp::term_list< untyped_multi_action >	untyped_multi_action_list
	\brief list of untyped_multi_actions

typedef std::vector< untyped_multi_action >	untyped_multi_action_vector
	\brief vector of untyped_multi_actions

Functions
template<class... ARGUMENTS>
void	make_action_label (atermpp::aterm_appl &t, const ARGUMENTS &... args)

bool	is_action_label (const atermpp::aterm_appl &x)

std::string	pp (const action_label &x)

std::ostream &	operator<< (std::ostream &out, const action_label &x)

void	swap (action_label &t1, action_label &t2)
	\brief swap overload

std::string	pp (const action_label_list &x)

std::string	pp (const action_label_vector &x)

action_label_list	normalize_sorts (const action_label_list &x, const data::sort_specification &sortspec)

std::set< data::sort_expression >	find_sort_expressions (const process::action_label_list &x)

template<class... ARGUMENTS>
void	make_action_name_multiset (atermpp::aterm_appl &t, const ARGUMENTS &... args)

bool	is_action_name_multiset (const atermpp::aterm_appl &x)

std::string	pp (const action_name_multiset &x)

std::ostream &	operator<< (std::ostream &out, const action_name_multiset &x)

void	swap (action_name_multiset &t1, action_name_multiset &t2)
	\brief swap overload

std::ostream &	operator<< (std::ostream &out, const allow_set &x)

multi_action_name_set	alphabet (const process_expression &x, const std::vector< process_equation > &equations)

multi_action_name_set	alphabet_bounded (const process_expression &x, const multi_action_name_set &A, const std::vector< process_equation > &equations)

multi_action_name_set	alphabet_efficient (const process_expression &x, const std::vector< process_equation > &equations)

multi_action_name_set	alphabet_new (const process_expression &x, const std::vector< process_equation > &equations)

multi_action_name_set	alphabet_pcrl (const process_expression &x, const std::map< process_identifier, multi_action_name_set > &pcrl_equation_cache)
	Computes the alphabet of a pCRL expression x, using a pCRL equation cache.

void	alphabet_reduce (process_specification &procspec, std::size_t duplicate_equation_limit=(std::numeric_limits< size_t >::max)())
	Applies alphabet reduction to a process specification.

void	anonymize (process_specification &procspec)

template<typename T >
void	balance_summands (T &x, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Reduces the nesting depth of the choice operator.

template<typename T >
T	balance_summands (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Reduces the nesting depth of the choice operator.

template<class... ARGUMENTS>
void	make_communication_expression (atermpp::aterm_appl &t, const ARGUMENTS &... args)

bool	is_communication_expression (const atermpp::aterm_appl &x)

std::string	pp (const communication_expression &x)

std::ostream &	operator<< (std::ostream &out, const communication_expression &x)

void	swap (communication_expression &t1, communication_expression &t2)
	\brief swap overload

process_expression	push_allow (const process_expression &x, const action_name_multiset_list &V, std::vector< process_equation > &equations, data::set_identifier_generator &id_generator, std::map< process_identifier, multi_action_name_set > &pcrl_equation_cache)

process_expression	push_block (const core::identifier_string_list &B, const process_expression &x, std::vector< process_equation > &equations, data::set_identifier_generator &id_generator, std::map< process_identifier, multi_action_name_set > &pcrl_equation_cache)

process_expression	process_instance_replace (const process_expression &x, const std::map< process_identifier, process_instance > &substitutions)

void	process_instance_replace (process_specification &procspec, const std::map< process_identifier, process_instance > &substitutions)

void	eliminate_trivial_equations (process_specification &procspec)
	Eliminates trivial equations, that have a process instance as the right hand side.

void	eliminate_unused_equations (std::vector< process_equation > &equations, const process_expression &init)

process_expression	expand_process_instance_assignments (const process_expression &x, const std::vector< process_equation > &equations)
	Replaces embedded process instances by the right hand sides of the corresponding equations.

process_instance	expand_assignments (const process::process_instance_assignment &x, const std::vector< process_equation > &equations)

template<typename T , typename OutputIterator >
void	find_all_variables (const T &x, OutputIterator o)

template<typename T >
std::set< data::variable >	find_all_variables (const T &x)

template<typename T , typename OutputIterator >
void	find_free_variables (const T &x, OutputIterator o)

template<typename T , typename OutputIterator , typename VariableContainer >
void	find_free_variables_with_bound (const T &x, OutputIterator o, const VariableContainer &bound)

template<typename T >
std::set< data::variable >	find_free_variables (const T &x)

template<typename T , typename VariableContainer >
std::set< data::variable >	find_free_variables_with_bound (const T &x, VariableContainer const &bound)

template<typename T , typename OutputIterator >
void	find_identifiers (const T &x, OutputIterator o)

template<typename T >
std::set< core::identifier_string >	find_identifiers (const T &x)

template<typename T , typename OutputIterator >
void	find_sort_expressions (const T &x, OutputIterator o)

template<typename T >
std::set< data::sort_expression >	find_sort_expressions (const T &x)

template<typename T , typename OutputIterator >
void	find_function_symbols (const T &x, OutputIterator o)

template<typename T >
std::set< data::function_symbol >	find_function_symbols (const T &x)

template<typename T , typename OutputIterator >
void	find_action_labels (const T &x, OutputIterator o)
	Returns all action labels that occur in an object.

template<typename T >
std::set< process::action_label >	find_action_labels (const T &x)
	Returns all action labels that occur in an object.

template<typename T >
std::set< core::identifier_string >	find_action_names (const T &x)
	Returns all action names that occur in an object.

const process_equation &	find_equation (const std::vector< process_equation > &equations, const process_identifier &id)
	Finds an equation that corresponds to a process identifier.

bool	is_communicating_lpe (const process::process_expression &x)
	Returns true if x is in communicating LPE format.

bool	is_guarded (const process_expression &x, const std::vector< process_equation > &equations)
	Checks if a process expression is guarded.

bool	is_linear (const process_specification &p, bool verbose=false)
	Returns true if the process specification is linear.

bool	is_linear (const process_equation &eqn)
	Returns true if the process equation is linear.

bool	is_linear (const process_expression &x, const process_equation &eqn)
	Returns true if the process expression is linear.

bool	is_multi_action (const process_expression &x)
	Returns true if x is a multi action.

multi_action_name	sync_multi_action_name (const sync &x)
	Computes a multi action name corresponding to a sync (provided that the sync is a pCRL expression).

template<typename T >
bool	is_stochastic (const T &x)
	Returns true if the LPS object x contains a stochastic distribution in one of its attributes.

bool	is_well_typed (const process_specification &procspec)
	Returns true if the process specification is well typed. N.B. The check is very incomplete!

std::vector< process_expression >	split_summands (const process_expression &x)
	Splits a choice into a set of operands Given a process expression of the form p1 + p2 + .... + pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a + as main function symbol.

template<typename FwdIt >
process_expression	join_summands (FwdIt first, FwdIt last)
	Returns or applied to the sequence of process expressions [first, last).

action_label_list	merge_action_specifications (const action_label_list &actspec1, const action_label_list &actspec2)
	Merges two action specifications.

std::string	pp (const multi_action_name &x)
	Pretty print function for a multi action name.

std::ostream &	operator<< (std::ostream &out, const multi_action_name &alpha)

std::string	pp (const multi_action_name_set &A)
	Pretty print function for a set of multi action names.

std::ostream &	operator<< (std::ostream &out, const multi_action_name_set &A)

template<typename T >
void	normalize_sorts (T &x, const data::sort_specification &sortspec, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T >
T	normalize_sorts (const T &x, const data::sort_specification &sortspec, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

process::action_label_list	parse_action_declaration (const std::string &text, const data::data_specification &data_spec=data::detail::default_specification())
	Parses an action declaration from a string.

process_specification	parse_process_specification (std::istream &in)
	Parses a process specification from an input stream.

process_specification	parse_process_specification (const std::string &spec_string)
	Parses a process specification from a string.

process_identifier	parse_process_identifier (std::string text, const data::data_specification &dataspec)
	Parses a process identifier.

process_expression	parse_process_expression (const std::string &text, const std::string &data_decl, const std::string &proc_decl)
	Parses and type checks a process expression.

process_expression	parse_process_expression (const std::string &text, const std::string &procspec_text)
	Parses and type checks a process expression.

template<typename VariableContainer >
process_expression	parse_process_expression (const std::string &text, const VariableContainer &variables, const process_specification &procspec)
	Parses and type checks a process expression. N.B. Very inefficient!

template<typename VariableContainer , typename ActionLabelContainer , typename ProcessIdentifierContainer >
process_expression	parse_process_expression (const std::string &text, const VariableContainer &variables=VariableContainer(), const data::data_specification &dataspec=data::data_specification(), const ActionLabelContainer &action_labels=std::vector< action_label >(), const ProcessIdentifierContainer &process_identifiers=ProcessIdentifierContainer(), const process_identifier *current_equation=nullptr)

constexpr int	precedence (const choice &)

constexpr int	precedence (const sum &)

constexpr int	precedence (const stochastic_operator &)

constexpr int	precedence (const merge &)

constexpr int	precedence (const left_merge &)

constexpr int	precedence (const if_then &)

constexpr int	precedence (const if_then_else &)

constexpr int	precedence (const bounded_init &)

constexpr int	precedence (const seq &)

constexpr int	precedence (const at &)

constexpr int	precedence (const sync &)

int	precedence (const process_expression &x)

bool	is_left_associative (const choice &)

bool	is_left_associative (const merge &)

bool	is_left_associative (const left_merge &)

bool	is_left_associative (const bounded_init &)

bool	is_left_associative (const seq &)

bool	is_left_associative (const sync &)

bool	is_left_associative (const process_expression &x)

bool	is_right_associative (const choice &)

bool	is_right_associative (const merge &)

bool	is_right_associative (const left_merge &)

bool	is_right_associative (const bounded_init &)

bool	is_right_associative (const seq &)

bool	is_right_associative (const sync &)

bool	is_right_associative (const process_expression &x)

template<typename T >
std::string	pp (const T &x)
	Returns a string representation of the object x.

template<class... ARGUMENTS>
void	make_process_equation (atermpp::aterm_appl &t, const ARGUMENTS &... args)

bool	is_process_equation (const atermpp::aterm_appl &x)

std::string	pp (const process_equation &x)

std::ostream &	operator<< (std::ostream &out, const process_equation &x)

void	swap (process_equation &t1, process_equation &t2)
	\brief swap overload

std::string	pp (const process_equation_list &x)

std::string	pp (const process_equation_vector &x)

void	normalize_sorts (process_equation_vector &x, const data::sort_specification &sortspec)

std::set< data::sort_expression >	find_sort_expressions (const process::process_equation_vector &x)

bool	is_action (const atermpp::aterm_appl &x)

bool	is_process_instance (const atermpp::aterm_appl &x)

bool	is_process_instance_assignment (const atermpp::aterm_appl &x)

bool	is_delta (const atermpp::aterm_appl &x)

bool	is_tau (const atermpp::aterm_appl &x)

bool	is_sum (const atermpp::aterm_appl &x)

bool	is_block (const atermpp::aterm_appl &x)

bool	is_hide (const atermpp::aterm_appl &x)

bool	is_rename (const atermpp::aterm_appl &x)

bool	is_comm (const atermpp::aterm_appl &x)

bool	is_allow (const atermpp::aterm_appl &x)

bool	is_sync (const atermpp::aterm_appl &x)

bool	is_at (const atermpp::aterm_appl &x)

bool	is_seq (const atermpp::aterm_appl &x)

bool	is_if_then (const atermpp::aterm_appl &x)

bool	is_if_then_else (const atermpp::aterm_appl &x)

bool	is_bounded_init (const atermpp::aterm_appl &x)

bool	is_merge (const atermpp::aterm_appl &x)

bool	is_left_merge (const atermpp::aterm_appl &x)

bool	is_choice (const atermpp::aterm_appl &x)

bool	is_stochastic_operator (const atermpp::aterm_appl &x)

bool	is_untyped_process_assignment (const atermpp::aterm_appl &x)

bool	is_process_expression (const atermpp::aterm_appl &x)

std::string	pp (const process_expression &x)

std::ostream &	operator<< (std::ostream &out, const process_expression &x)

void	swap (process_expression &t1, process_expression &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_action (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const action &x)

std::ostream &	operator<< (std::ostream &out, const action &x)

void	swap (action &t1, action &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_process_instance (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const process_instance &x)

std::ostream &	operator<< (std::ostream &out, const process_instance &x)

void	swap (process_instance &t1, process_instance &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_process_instance_assignment (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const process_instance_assignment &x)

std::ostream &	operator<< (std::ostream &out, const process_instance_assignment &x)

void	swap (process_instance_assignment &t1, process_instance_assignment &t2)
	\brief swap overload

std::string	pp (const delta &x)

std::ostream &	operator<< (std::ostream &out, const delta &x)

void	swap (delta &t1, delta &t2)
	\brief swap overload

std::string	pp (const tau &x)

std::ostream &	operator<< (std::ostream &out, const tau &x)

void	swap (tau &t1, tau &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_sum (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const sum &x)

std::ostream &	operator<< (std::ostream &out, const sum &x)

void	swap (sum &t1, sum &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_block (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const block &x)

std::ostream &	operator<< (std::ostream &out, const block &x)

void	swap (block &t1, block &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_hide (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const hide &x)

std::ostream &	operator<< (std::ostream &out, const hide &x)

void	swap (hide &t1, hide &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_rename (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const rename &x)

std::ostream &	operator<< (std::ostream &out, const rename &x)

void	swap (rename &t1, rename &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_comm (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const comm &x)

std::ostream &	operator<< (std::ostream &out, const comm &x)

void	swap (comm &t1, comm &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_allow (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const allow &x)

std::ostream &	operator<< (std::ostream &out, const allow &x)

void	swap (allow &t1, allow &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_sync (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const sync &x)

std::ostream &	operator<< (std::ostream &out, const sync &x)

void	swap (sync &t1, sync &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_at (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const at &x)

std::ostream &	operator<< (std::ostream &out, const at &x)

void	swap (at &t1, at &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_seq (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const seq &x)

std::ostream &	operator<< (std::ostream &out, const seq &x)

void	swap (seq &t1, seq &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_if_then (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const if_then &x)

std::ostream &	operator<< (std::ostream &out, const if_then &x)

void	swap (if_then &t1, if_then &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_if_then_else (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const if_then_else &x)

std::ostream &	operator<< (std::ostream &out, const if_then_else &x)

void	swap (if_then_else &t1, if_then_else &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_bounded_init (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const bounded_init &x)

std::ostream &	operator<< (std::ostream &out, const bounded_init &x)

void	swap (bounded_init &t1, bounded_init &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_merge (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const merge &x)

std::ostream &	operator<< (std::ostream &out, const merge &x)

void	swap (merge &t1, merge &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_left_merge (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const left_merge &x)

std::ostream &	operator<< (std::ostream &out, const left_merge &x)

void	swap (left_merge &t1, left_merge &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_choice (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const choice &x)

std::ostream &	operator<< (std::ostream &out, const choice &x)

void	swap (choice &t1, choice &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_stochastic_operator (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const stochastic_operator &x)

std::ostream &	operator<< (std::ostream &out, const stochastic_operator &x)

void	swap (stochastic_operator &t1, stochastic_operator &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_untyped_process_assignment (atermpp::aterm_appl &t, const ARGUMENTS &... args)

std::string	pp (const untyped_process_assignment &x)

std::ostream &	operator<< (std::ostream &out, const untyped_process_assignment &x)

void	swap (untyped_process_assignment &t1, untyped_process_assignment &t2)
	\brief swap overload

std::string	pp (const process_expression_list &x)

std::string	pp (const process_expression_vector &x)

std::set< data::sort_expression >	find_sort_expressions (const process::process_expression &x)

std::string	pp (const action_list &x)

std::string	pp (const action_vector &x)

action	normalize_sorts (const action &x, const data::sort_specification &sortspec)

action	translate_user_notation (const action &x)

process::process_expression	translate_user_notation (const process::process_expression &x)

std::set< data::variable >	find_all_variables (const action &x)

std::set< data::variable >	find_free_variables (const action &x)

bool	equal_signatures (const action &a, const action &b)
	Compares the signatures of two actions.

template<class... ARGUMENTS>
void	make_process_identifier (atermpp::aterm_appl &t, const ARGUMENTS &... args)

bool	is_process_identifier (const atermpp::aterm_appl &x)

std::string	pp (const process_identifier &x)

std::ostream &	operator<< (std::ostream &out, const process_identifier &x)

void	swap (process_identifier &t1, process_identifier &t2)
	\brief swap overload

std::string	pp (const process_identifier_list &x)

std::string	pp (const process_identifier_vector &x)

void	normalize_sorts (process_identifier_vector &x, const data::sort_specification &sortspec)

void	process_info (const process_specification &procspec)
	Prints information about a process specification.

atermpp::aterm_appl	process_specification_to_aterm (const process_specification &spec)
	Conversion to aterm_appl.

void	complete_data_specification (process_specification &spec)
	Adds all sorts that appear in the process specification spec to the data specification of spec.

std::string	pp (const process_specification &x)

void	normalize_sorts (process_specification &x, const data::sort_specification &sortspec)

void	translate_user_notation (process::process_specification &x)

std::set< data::sort_expression >	find_sort_expressions (const process::process_specification &x)

std::set< core::identifier_string >	find_identifiers (const process::process_specification &x)

std::set< data::variable >	find_free_variables (const process::process_specification &x)

bool	is_process_specification (const atermpp::aterm_appl &x)
	Test for a process specification expression.

std::ostream &	operator<< (std::ostream &out, const process_specification &x)

bool	operator== (const process_specification &spec1, const process_specification &spec2)
	Equality operator.

bool	operator!= (const process_specification &spec1, const process_specification &spec2)
	Inequality operator.

std::vector< std::set< process_identifier > >	process_variable_strongly_connected_components (const std::vector< process_equation > &equations)
	Computes an SCC graph of the equations.

std::vector< std::set< process_identifier > >	process_variable_strongly_connected_components (const std::vector< process_equation > &equations, const process_expression &init)
	Compute an SCC graph of the equations reachable from init.

void	remove_data_parameters (process_specification &procspec)

void	remove_duplicate_equations (process_specification &procspec)
	Removes duplicate equations from a process specification, using a bisimulation algorithm.

template<class... ARGUMENTS>
void	make_rename_expression (atermpp::aterm_appl &t, const ARGUMENTS &... args)

bool	is_rename_expression (const atermpp::aterm_appl &x)

std::string	pp (const rename_expression &x)

std::ostream &	operator<< (std::ostream &out, const rename_expression &x)

void	swap (rename_expression &t1, rename_expression &t2)
	\brief swap overload

template<typename T , typename Substitution >
void	replace_sort_expressions (T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_sort_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_data_expressions (T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_data_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_all_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_all_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_free_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_free_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution , typename VariableContainer >
void	replace_free_variables (T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution , typename VariableContainer >
T	replace_free_variables (const T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_process_identifiers (T &x, const Substitution &sigma, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)

template<typename T , typename Substitution >
T	replace_process_identifiers (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution , typename IdentifierGenerator >
void	replace_variables_capture_avoiding_with_an_identifier_generator (T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution , typename IdentifierGenerator >
T	replace_variables_capture_avoiding_with_an_identifier_generator (const T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

process_expression	replace_subterm (const process_expression &expr, std::size_t x, std::size_t y, const process_expression &replacement)
	Replace the subterm at position (x, y) with a given term.

process_specification	replace_subterm (const process_specification &procspec, std::size_t x, std::size_t y, const process_expression &replacement)
	Replace the subterm at position (x, y) with a given term.

process_expression	find_subterm (const process_specification &procspec, std::size_t x, std::size_t y)

template<typename T , typename Rewriter >
void	rewrite (T &x, Rewriter R, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Rewriter >
T	rewrite (const T &x, Rewriter R, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Rewriter , typename Substitution >
void	rewrite (T &x, Rewriter R, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Rewriter , typename Substitution >
T	rewrite (const T &x, Rewriter R, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T >
void	translate_user_notation (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T >
T	translate_user_notation (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

action	typecheck_action (const core::identifier_string &name, const data::data_expression_list &parameters, data::data_type_checker &typechecker, const data::detail::variable_context &variable_context, const detail::action_context &action_context)

data::sorts_list	sorts_list_intersection (const data::sorts_list &sorts1, const data::sorts_list &sorts2)

std::ostream &	operator<< (std::ostream &out, const data::sorts_list &x)

void	typecheck_process_specification (process_specification &proc_spec)
	Type check a parsed mCRL2 process specification. Throws an exception if something went wrong.

template<typename VariableContainer , typename ActionLabelContainer , typename ProcessIdentifierContainer >
process_expression	typecheck_process_expression (const process_expression &x, const VariableContainer &variables=VariableContainer(), const data::data_specification &dataspec=data::data_specification(), const ActionLabelContainer &action_labels=ActionLabelContainer(), const ProcessIdentifierContainer &process_identifiers=ProcessIdentifierContainer(), const process_identifier *current_equation=nullptr)
	Typecheck a process expression.

template<class... ARGUMENTS>
void	make_untyped_multi_action (atermpp::aterm_appl &t, const ARGUMENTS &... args)

bool	is_untyped_multi_action (const atermpp::aterm_appl &x)

std::string	pp (const untyped_multi_action &x)

std::ostream &	operator<< (std::ostream &out, const untyped_multi_action &x)

void	swap (untyped_multi_action &t1, untyped_multi_action &t2)
	\brief swap overload

bool	is_pcrl (const process_expression &x)
	Returns true if x is a pCRL expression. N.B. This test depends on the assumption that in mCRL2 a top level pCRL expression may never contain a non-pCRL expression.

bool	contains_tau (const multi_action_name_set &A)

process_expression	make_sync (const process_expression &x, const process_expression &y)

process_expression	make_merge (const process_expression &x, const process_expression &y)

process_expression	make_left_merge (const process_expression &x, const process_expression &y)

process_expression	make_allow (const multi_action_name_set &A, const process_expression &x)

process_expression	make_comm (const communication_expression_list &C, const process_expression &x)

process_expression	make_hide (const core::identifier_string_list &I, const process_expression &x)

process_expression	make_block (const core::identifier_string_list &B, const process_expression &x)

Detailed Description

The main namespace for the Process library.

Typedef Documentation

◆ action_label_list

typedef atermpp::term_list<action_label> mcrl2::process::action_label_list

\brief list of action_labels

Definition at line 77 of file action_label.h.

◆ action_label_vector

typedef std::vector<action_label> mcrl2::process::action_label_vector

\brief vector of action_labels

Definition at line 80 of file action_label.h.

◆ action_list

typedef atermpp::term_list<action> mcrl2::process::action_list

\brief list of actions

Definition at line 187 of file process_expression.h.

◆ action_name_multiset_list

typedef atermpp::term_list<action_name_multiset> mcrl2::process::action_name_multiset_list

\brief list of action_name_multisets

Definition at line 67 of file action_name_multiset.h.

◆ action_name_multiset_vector

typedef std::vector<action_name_multiset> mcrl2::process::action_name_multiset_vector

\brief vector of action_name_multisets

Definition at line 70 of file action_name_multiset.h.

◆ action_vector

typedef std::vector<action> mcrl2::process::action_vector

\brief vector of actions

Definition at line 190 of file process_expression.h.

◆ communication_expression_list

typedef atermpp::term_list<communication_expression> mcrl2::process::communication_expression_list

\brief list of communication_expressions

Definition at line 77 of file communication_expression.h.

◆ communication_expression_vector

typedef std::vector<communication_expression> mcrl2::process::communication_expression_vector

\brief vector of communication_expressions

Definition at line 80 of file communication_expression.h.

◆ multi_action_name_set

typedef std::set<multi_action_name> mcrl2::process::multi_action_name_set

Represents a set of multi action names.

Definition at line 36 of file multi_action_name.h.

◆ process_equation_list

typedef atermpp::term_list<process_equation> mcrl2::process::process_equation_list

\brief list of process_equations

Definition at line 77 of file process_equation.h.

◆ process_equation_vector

typedef std::vector<process_equation> mcrl2::process::process_equation_vector

\brief vector of process_equations

Definition at line 80 of file process_equation.h.

◆ process_expression_list

typedef atermpp::term_list<process_expression> mcrl2::process::process_expression_list

\brief list of process_expressions

Definition at line 59 of file process_expression.h.

◆ process_expression_vector

typedef std::vector<process_expression> mcrl2::process::process_expression_vector

\brief vector of process_expressions

Definition at line 62 of file process_expression.h.

◆ process_identifier_list

typedef atermpp::term_list<process_identifier> mcrl2::process::process_identifier_list

\brief list of process_identifiers

Definition at line 82 of file process_identifier.h.

◆ process_identifier_vector

typedef std::vector<process_identifier> mcrl2::process::process_identifier_vector

\brief vector of process_identifiers

Definition at line 85 of file process_identifier.h.

◆ rename_expression_list

typedef atermpp::term_list<rename_expression> mcrl2::process::rename_expression_list

\brief list of rename_expressions

Definition at line 78 of file rename_expression.h.

◆ rename_expression_vector

typedef std::vector<rename_expression> mcrl2::process::rename_expression_vector

\brief vector of rename_expressions

Definition at line 81 of file rename_expression.h.

◆ untyped_multi_action_list

typedef atermpp::term_list<untyped_multi_action> mcrl2::process::untyped_multi_action_list

\brief list of untyped_multi_actions

Definition at line 65 of file untyped_multi_action.h.

◆ untyped_multi_action_vector

typedef std::vector<untyped_multi_action> mcrl2::process::untyped_multi_action_vector

\brief vector of untyped_multi_actions

Definition at line 68 of file untyped_multi_action.h.

Function Documentation

◆ alphabet()

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

inline

Definition at line 272 of file alphabet.h.

◆ alphabet_bounded()

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

inline

Definition at line 257 of file alphabet_bounded.h.

◆ alphabet_efficient()

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

inline

Definition at line 128 of file alphabet_efficient.h.

◆ alphabet_new()

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

inline

Definition at line 214 of file alphabet_new.h.

◆ alphabet_pcrl()

multi_action_name_set mcrl2::process::alphabet_pcrl	(	const process_expression &	x,
		const std::map< process_identifier, multi_action_name_set > &	pcrl_equation_cache
	)

inline

Computes the alphabet of a pCRL expression x, using a pCRL equation cache.

Definition at line 128 of file alphabet_pcrl.h.

◆ alphabet_reduce()

void mcrl2::process::alphabet_reduce	(	process_specification &	procspec,
		std::size_t	duplicate_equation_limit = `(std::numeric_limits<size_t>::max)()`
	)

Applies alphabet reduction to a process specification.

Parameters

procspec	A process specification
duplicate_equation_limit	If the number of equations is less than duplicate_equation_limit, the remove duplicate equations procedure is applied. Note that this procedure is not efficient, so it should not be used if the number of equations is big.

Definition at line 83 of file process.cpp.

◆ anonymize()

void mcrl2::process::anonymize ( process_specification & procspec )

inline

Definition at line 166 of file anonymize.h.

◆ balance_summands() [1/2]

template<typename T >

T mcrl2::process::balance_summands	(	const T &	x,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Reduces the nesting depth of the choice operator.

Definition at line 63 of file balance_nesting_depth.h.

◆ balance_summands() [2/2]

template<typename T >

void mcrl2::process::balance_summands	(	T &	x,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Reduces the nesting depth of the choice operator.

Definition at line 55 of file balance_nesting_depth.h.

◆ complete_data_specification()

void mcrl2::process::complete_data_specification ( process_specification & spec )

inline

Adds all sorts that appear in the process specification spec to the data specification of spec.

Parameters

spec	A process specification

Definition at line 210 of file process_specification.h.

◆ contains_tau()

bool mcrl2::process::contains_tau ( const multi_action_name_set & A )

inline

Definition at line 35 of file utility.h.

◆ eliminate_trivial_equations()

void mcrl2::process::eliminate_trivial_equations ( process_specification & procspec )

inline

Eliminates trivial equations, that have a process instance as the right hand side.

Definition at line 282 of file eliminate_trivial_equations.h.

◆ eliminate_unused_equations()

void mcrl2::process::eliminate_unused_equations	(	std::vector< process_equation > &	equations,
		const process_expression &	init
	)

inline

Definition at line 142 of file eliminate_unused_equations.h.

◆ equal_signatures()

bool mcrl2::process::equal_signatures	(	const action &	a,
		const action &	b
	)

inline

Compares the signatures of two actions.

Parameters

a	An action
b	An action

Returns: Returns true if the actions a and b have the same label, and the sorts of the arguments of a and b are equal.

Definition at line 1804 of file process_expression.h.

◆ expand_assignments()

process_instance mcrl2::process::expand_assignments	(	const process::process_instance_assignment &	x,
		const std::vector< process_equation > &	equations
	)

inline

Definition at line 86 of file expand_process_instance_assignments.h.

◆ expand_process_instance_assignments()

process_expression mcrl2::process::expand_process_instance_assignments	(	const process_expression &	x,
		const std::vector< process_equation > &	equations
	)

inline

Replaces embedded process instances by the right hand sides of the corresponding equations.

Definition at line 76 of file expand_process_instance_assignments.h.

◆ find_action_labels() [1/2]

template<typename T >

std::set< process::action_label > mcrl2::process::find_action_labels ( const T & x )

Returns all action labels that occur in an object.

Parameters

[in] x an object containing action labels

Returns: All action labels that occur in the object x

Definition at line 267 of file find.h.

◆ find_action_labels() [2/2]

template<typename T , typename OutputIterator >

void mcrl2::process::find_action_labels	(	const T &	x,
		OutputIterator	o
	)

Returns all action labels that occur in an object.

Parameters

[in]	x	an object containing action labels
[in,out]	o	an output iterator to which all action labels occurring in x are written.

Returns: All action labels that occur in the term x

Definition at line 258 of file find.h.

◆ find_action_names()

template<typename T >

std::set< core::identifier_string > mcrl2::process::find_action_names ( const T & x )

Returns all action names that occur in an object.

Parameters

[in] x an object containing action names

Returns: All action names that occur in the object x

Definition at line 278 of file find.h.

◆ find_all_variables() [1/3]

std::set< data::variable > mcrl2::process::find_all_variables ( const action & x )

Definition at line 77 of file process.cpp.

◆ find_all_variables() [2/3]

template<typename T >

std::set< data::variable > mcrl2::process::find_all_variables ( const T & x )

\brief Returns all variables that occur in an object \param[in] x an object containing variables \return All variables that occur in the object x

Definition at line 138 of file find.h.

◆ find_all_variables() [3/3]

template<typename T , typename OutputIterator >

void mcrl2::process::find_all_variables	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are written. \return All variables that occur in the term x

Definition at line 129 of file find.h.

◆ find_equation()

const process_equation & mcrl2::process::find_equation	(	const std::vector< process_equation > &	equations,
		const process_identifier &	id
	)

inline

Finds an equation that corresponds to a process identifier.

Parameters

[in]	equations	a sequence of process equations
[in]	id	The identifier of the equation that is searched for.

Returns: The equation with the given process identifier. Throws an exception if no such equation was found.

Definition at line 290 of file find.h.

◆ find_free_variables() [1/4]

std::set< data::variable > mcrl2::process::find_free_variables ( const action & x )

Definition at line 78 of file process.cpp.

◆ find_free_variables() [2/4]

std::set< data::variable > mcrl2::process::find_free_variables ( const process::process_specification & x )

Definition at line 79 of file process.cpp.

◆ find_free_variables() [3/4]

template<typename T >

std::set< data::variable > mcrl2::process::find_free_variables ( const T & x )

\brief Returns all variables that occur in an object \param[in] x an object containing variables \return All free variables that occur in the object x

Definition at line 170 of file find.h.

◆ find_free_variables() [4/4]

template<typename T , typename OutputIterator >

void mcrl2::process::find_free_variables	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are added. \return All free variables that occur in the object x

Definition at line 150 of file find.h.

◆ find_free_variables_with_bound() [1/2]

template<typename T , typename OutputIterator , typename VariableContainer >

void mcrl2::process::find_free_variables_with_bound	(	const T &	x,
		OutputIterator	o,
		const VariableContainer &	bound
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are written. \param[in] bound a container of variables \return All free variables that occur in the object x

Definition at line 161 of file find.h.

◆ find_free_variables_with_bound() [2/2]

template<typename T , typename VariableContainer >

std::set< data::variable > mcrl2::process::find_free_variables_with_bound	(	const T &	x,
		VariableContainer const &	bound
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in] bound a bound a container of variables \return All free variables that occur in the object x

Definition at line 182 of file find.h.

◆ find_function_symbols() [1/2]

template<typename T >

std::set< data::function_symbol > mcrl2::process::find_function_symbols ( const T & x )

\brief Returns all function symbols that occur in an object \param[in] x an object containing function symbols \return All function symbols that occur in the object x

Definition at line 245 of file find.h.

◆ find_function_symbols() [2/2]

template<typename T , typename OutputIterator >

void mcrl2::process::find_function_symbols	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all function symbols that occur in an object \param[in] x an object containing function symbols \param[in,out] o an output iterator to which all function symbols occurring in x are written. \return All function symbols that occur in the term x

Definition at line 236 of file find.h.

◆ find_identifiers() [1/3]

std::set< core::identifier_string > mcrl2::process::find_identifiers ( const process::process_specification & x )

Definition at line 80 of file process.cpp.

◆ find_identifiers() [2/3]

template<typename T >

std::set< core::identifier_string > mcrl2::process::find_identifiers ( const T & x )

\brief Returns all identifiers that occur in an object \param[in] x an object containing identifiers \return All identifiers that occur in the object x

Definition at line 203 of file find.h.

◆ find_identifiers() [3/3]

template<typename T , typename OutputIterator >

void mcrl2::process::find_identifiers	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all identifiers that occur in an object \param[in] x an object containing identifiers \param[in,out] o an output iterator to which all identifiers occurring in x are written. \return All identifiers that occur in the term x

Definition at line 194 of file find.h.

◆ find_sort_expressions() [1/6]

std::set< data::sort_expression > mcrl2::process::find_sort_expressions ( const process::action_label_list & x )

Definition at line 73 of file process.cpp.

◆ find_sort_expressions() [2/6]

std::set< data::sort_expression > mcrl2::process::find_sort_expressions ( const process::process_equation_vector & x )

Definition at line 74 of file process.cpp.

◆ find_sort_expressions() [3/6]

std::set< data::sort_expression > mcrl2::process::find_sort_expressions ( const process::process_expression & x )

Definition at line 75 of file process.cpp.

◆ find_sort_expressions() [4/6]

std::set< data::sort_expression > mcrl2::process::find_sort_expressions ( const process::process_specification & x )

Definition at line 76 of file process.cpp.

◆ find_sort_expressions() [5/6]

template<typename T >

std::set< data::sort_expression > mcrl2::process::find_sort_expressions ( const T & x )

\brief Returns all sort expressions that occur in an object \param[in] x an object containing sort expressions \return All sort expressions that occur in the object x

Definition at line 224 of file find.h.

◆ find_sort_expressions() [6/6]

template<typename T , typename OutputIterator >

void mcrl2::process::find_sort_expressions	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all sort expressions that occur in an object \param[in] x an object containing sort expressions \param[in,out] o an output iterator to which all sort expressions occurring in x are written. \return All sort expressions that occur in the term x

Definition at line 215 of file find.h.

◆ find_subterm()

process_expression mcrl2::process::find_subterm	(	const process_specification &	procspec,
		std::size_t	x,
		std::size_t	y
	)

inline

Definition at line 346 of file replace_subterm.h.

◆ is_action()

bool mcrl2::process::is_action ( const atermpp::aterm_appl & x )

inline

\brief Test for a action expression \param x A term \return True if \a x is a action expression

Definition at line 196 of file process_expression.h.

◆ is_action_label()

bool mcrl2::process::is_action_label ( const atermpp::aterm_appl & x )

inline

\brief Test for a action_label expression \param x A term \return True if \a x is a action_label expression

Definition at line 86 of file action_label.h.

◆ is_action_name_multiset()

bool mcrl2::process::is_action_name_multiset ( const atermpp::aterm_appl & x )

inline

\brief Test for a action_name_multiset expression \param x A term \return True if \a x is a action_name_multiset expression

Definition at line 76 of file action_name_multiset.h.

◆ is_allow()

bool mcrl2::process::is_allow ( const atermpp::aterm_appl & x )

inline

\brief Test for a allow expression \param x A term \return True if \a x is a allow expression

Definition at line 910 of file process_expression.h.

◆ is_at()

bool mcrl2::process::is_at ( const atermpp::aterm_appl & x )

inline

\brief Test for a at expression \param x A term \return True if \a x is a at expression

Definition at line 1062 of file process_expression.h.

◆ is_block()

bool mcrl2::process::is_block ( const atermpp::aterm_appl & x )

inline

\brief Test for a block expression \param x A term \return True if \a x is a block expression

Definition at line 606 of file process_expression.h.

◆ is_bounded_init()

bool mcrl2::process::is_bounded_init ( const atermpp::aterm_appl & x )

inline

\brief Test for a bounded_init expression \param x A term \return True if \a x is a bounded_init expression

Definition at line 1371 of file process_expression.h.

◆ is_choice()

bool mcrl2::process::is_choice ( const atermpp::aterm_appl & x )

inline

\brief Test for a choice expression \param x A term \return True if \a x is a choice expression

Definition at line 1599 of file process_expression.h.

◆ is_comm()

bool mcrl2::process::is_comm ( const atermpp::aterm_appl & x )

inline

\brief Test for a comm expression \param x A term \return True if \a x is a comm expression

Definition at line 834 of file process_expression.h.

◆ is_communicating_lpe()

bool mcrl2::process::is_communicating_lpe ( const process::process_expression & x )

inline

Returns true if x is in communicating LPE format.

Definition at line 115 of file is_communicating_lpe.h.

◆ is_communication_expression()

bool mcrl2::process::is_communication_expression ( const atermpp::aterm_appl & x )

inline

\brief Test for a communication_expression expression \param x A term \return True if \a x is a communication_expression expression

Definition at line 86 of file communication_expression.h.

◆ is_delta()

bool mcrl2::process::is_delta ( const atermpp::aterm_appl & x )

inline

\brief Test for a delta expression \param x A term \return True if \a x is a delta expression

Definition at line 401 of file process_expression.h.

◆ is_guarded()

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

inline

Checks if a process expression is guarded.

Definition at line 97 of file is_guarded.h.

◆ is_hide()

bool mcrl2::process::is_hide ( const atermpp::aterm_appl & x )

inline

\brief Test for a hide expression \param x A term \return True if \a x is a hide expression

Definition at line 682 of file process_expression.h.

◆ is_if_then()

bool mcrl2::process::is_if_then ( const atermpp::aterm_appl & x )

inline

\brief Test for a if_then expression \param x A term \return True if \a x is a if_then expression

Definition at line 1214 of file process_expression.h.

◆ is_if_then_else()

bool mcrl2::process::is_if_then_else ( const atermpp::aterm_appl & x )

inline

\brief Test for a if_then_else expression \param x A term \return True if \a x is a if_then_else expression

Definition at line 1295 of file process_expression.h.

◆ is_left_associative() [1/7]

bool mcrl2::process::is_left_associative ( const bounded_init & )

inline

Definition at line 53 of file print.h.

◆ is_left_associative() [2/7]

bool mcrl2::process::is_left_associative ( const choice & )

inline

Definition at line 50 of file print.h.

◆ is_left_associative() [3/7]

bool mcrl2::process::is_left_associative ( const left_merge & )

inline

Definition at line 52 of file print.h.

◆ is_left_associative() [4/7]

bool mcrl2::process::is_left_associative ( const merge & )

inline

Definition at line 51 of file print.h.

◆ is_left_associative() [5/7]

bool mcrl2::process::is_left_associative ( const process_expression & x )

inline

Definition at line 56 of file print.h.

◆ is_left_associative() [6/7]

bool mcrl2::process::is_left_associative ( const seq & )

inline

Definition at line 54 of file print.h.

◆ is_left_associative() [7/7]

bool mcrl2::process::is_left_associative ( const sync & )

inline

Definition at line 55 of file print.h.

◆ is_left_merge()

bool mcrl2::process::is_left_merge ( const atermpp::aterm_appl & x )

inline

\brief Test for a left_merge expression \param x A term \return True if \a x is a left_merge expression

Definition at line 1523 of file process_expression.h.

◆ is_linear() [1/3]

bool mcrl2::process::is_linear ( const process_equation & eqn )

inline

Returns true if the process equation is linear.

Definition at line 382 of file is_linear.h.

◆ is_linear() [2/3]

bool mcrl2::process::is_linear	(	const process_expression &	x,
		const process_equation &	eqn
	)

inline

Returns true if the process expression is linear.

Parameters

x	A process expression.
eqn	The linear equation belonging to the indicated process.

Definition at line 392 of file is_linear.h.

◆ is_linear() [3/3]

bool mcrl2::process::is_linear	(	const process_specification &	p,
		bool	verbose = `false`
	)

inline

Returns true if the process specification is linear.

Definition at line 347 of file is_linear.h.

◆ is_merge()

bool mcrl2::process::is_merge ( const atermpp::aterm_appl & x )

inline

\brief Test for a merge expression \param x A term \return True if \a x is a merge expression

Definition at line 1447 of file process_expression.h.

◆ is_multi_action()

bool mcrl2::process::is_multi_action ( const process_expression & x )

inline

Returns true if x is a multi action.

Definition at line 43 of file is_multi_action.h.

◆ is_pcrl()

bool mcrl2::process::is_pcrl ( const process_expression & x )

inline

Returns true if x is a pCRL expression. N.B. This test depends on the assumption that in mCRL2 a top level pCRL expression may never contain a non-pCRL expression.

Definition at line 29 of file utility.h.

◆ is_process_equation()

bool mcrl2::process::is_process_equation ( const atermpp::aterm_appl & x )

inline

\brief Test for a process_equation expression \param x A term \return True if \a x is a process_equation expression

Definition at line 86 of file process_equation.h.

◆ is_process_expression()

bool mcrl2::process::is_process_expression ( const atermpp::aterm_appl & x )

inline

\brief Test for a process_expression expression \param x A term \return True if \a x is a process_expression expression

Definition at line 92 of file process_expression.h.

◆ is_process_identifier()

bool mcrl2::process::is_process_identifier ( const atermpp::aterm_appl & x )

inline

\brief Test for a process_identifier expression \param x A term \return True if \a x is a process_identifier expression

Definition at line 91 of file process_identifier.h.

◆ is_process_instance()

bool mcrl2::process::is_process_instance ( const atermpp::aterm_appl & x )

inline

\brief Test for a process_instance expression \param x A term \return True if \a x is a process_instance expression

Definition at line 272 of file process_expression.h.

◆ is_process_instance_assignment()

bool mcrl2::process::is_process_instance_assignment ( const atermpp::aterm_appl & x )

inline

\brief Test for a process_instance_assignment expression \param x A term \return True if \a x is a process_instance_assignment expression

Definition at line 348 of file process_expression.h.

◆ is_process_specification()

bool mcrl2::process::is_process_specification ( const atermpp::aterm_appl & x )

inline

Test for a process specification expression.

Parameters

x A term

Returns: True if x is a process specification expression

Definition at line 44 of file process_specification.h.

◆ is_rename()

bool mcrl2::process::is_rename ( const atermpp::aterm_appl & x )

inline

\brief Test for a rename expression \param x A term \return True if \a x is a rename expression

Definition at line 758 of file process_expression.h.

◆ is_rename_expression()

bool mcrl2::process::is_rename_expression ( const atermpp::aterm_appl & x )

inline

\brief Test for a rename_expression expression \param x A term \return True if \a x is a rename_expression expression

Definition at line 87 of file rename_expression.h.

◆ is_right_associative() [1/7]

bool mcrl2::process::is_right_associative ( const bounded_init & )

inline

Definition at line 71 of file print.h.

◆ is_right_associative() [2/7]

bool mcrl2::process::is_right_associative ( const choice & )

inline

Definition at line 68 of file print.h.

◆ is_right_associative() [3/7]

bool mcrl2::process::is_right_associative ( const left_merge & )

inline

Definition at line 70 of file print.h.

◆ is_right_associative() [4/7]

bool mcrl2::process::is_right_associative ( const merge & )

inline

Definition at line 69 of file print.h.

◆ is_right_associative() [5/7]

bool mcrl2::process::is_right_associative ( const process_expression & x )

inline

Definition at line 74 of file print.h.

◆ is_right_associative() [6/7]

bool mcrl2::process::is_right_associative ( const seq & )

inline

Definition at line 72 of file print.h.

◆ is_right_associative() [7/7]

bool mcrl2::process::is_right_associative ( const sync & )

inline

Definition at line 73 of file print.h.

◆ is_seq()

bool mcrl2::process::is_seq ( const atermpp::aterm_appl & x )

inline

\brief Test for a seq expression \param x A term \return True if \a x is a seq expression

Definition at line 1138 of file process_expression.h.

◆ is_stochastic()

template<typename T >

bool mcrl2::process::is_stochastic ( const T & x )

Returns true if the LPS object x contains a stochastic distribution in one of its attributes.

Definition at line 49 of file is_stochastic.h.

◆ is_stochastic_operator()

bool mcrl2::process::is_stochastic_operator ( const atermpp::aterm_appl & x )

inline

\brief Test for a stochastic_operator expression \param x A term \return True if \a x is a stochastic_operator expression

Definition at line 1680 of file process_expression.h.

◆ is_sum()

bool mcrl2::process::is_sum ( const atermpp::aterm_appl & x )

inline

\brief Test for a sum expression \param x A term \return True if \a x is a sum expression

Definition at line 530 of file process_expression.h.

◆ is_sync()

bool mcrl2::process::is_sync ( const atermpp::aterm_appl & x )

inline

\brief Test for a sync expression \param x A term \return True if \a x is a sync expression

Definition at line 986 of file process_expression.h.

◆ is_tau()

bool mcrl2::process::is_tau ( const atermpp::aterm_appl & x )

inline

\brief Test for a tau expression \param x A term \return True if \a x is a tau expression

Definition at line 454 of file process_expression.h.

◆ is_untyped_multi_action()

bool mcrl2::process::is_untyped_multi_action ( const atermpp::aterm_appl & x )

inline

\brief Test for a untyped_multi_action expression \param x A term \return True if \a x is a untyped_multi_action expression

Definition at line 74 of file untyped_multi_action.h.

◆ is_untyped_process_assignment()

bool mcrl2::process::is_untyped_process_assignment ( const atermpp::aterm_appl & x )

inline

\brief Test for a untyped_process_assignment expression \param x A term \return True if \a x is a untyped_process_assignment expression

Definition at line 1761 of file process_expression.h.

◆ is_well_typed()

bool mcrl2::process::is_well_typed ( const process_specification & procspec )

inline

Returns true if the process specification is well typed. N.B. The check is very incomplete!

Definition at line 23 of file is_well_typed.h.

◆ join_summands()

template<typename FwdIt >

process_expression mcrl2::process::join_summands	(	FwdIt	first,
		FwdIt	last
	)

Returns or applied to the sequence of process expressions [first, last).

Parameters

first	Start of a sequence of process expressions.
last	End of a sequence of of process expressions.

Returns: The choice operator applied to the sequence of process expressions [first, last).

Definition at line 45 of file join.h.

◆ make_action()

template<class... ARGUMENTS>

void mcrl2::process::make_action	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_action constructs a new term into a given address. \

Parameters

t	The reference into which the new action is constructed.

Definition at line 181 of file process_expression.h.

◆ make_action_label()

template<class... ARGUMENTS>

void mcrl2::process::make_action_label	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_action_label constructs a new term into a given address. \

Parameters

t	The reference into which the new action_label is constructed.

Definition at line 71 of file action_label.h.

◆ make_action_name_multiset()

template<class... ARGUMENTS>

void mcrl2::process::make_action_name_multiset	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_action_name_multiset constructs a new term into a given address. \

Parameters

t	The reference into which the new action_name_multiset is constructed.

Definition at line 61 of file action_name_multiset.h.

◆ make_allow() [1/2]

template<class... ARGUMENTS>

void mcrl2::process::make_allow	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_allow constructs a new term into a given address. \

Parameters

t	The reference into which the new allow is constructed.

Definition at line 901 of file process_expression.h.

◆ make_allow() [2/2]

process_expression mcrl2::process::make_allow	(	const multi_action_name_set &	A,
		const process_expression &	x
	)

inline

Definition at line 72 of file utility.h.

◆ make_at()

template<class... ARGUMENTS>

void mcrl2::process::make_at	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_at constructs a new term into a given address. \

Parameters

t	The reference into which the new at is constructed.

Definition at line 1053 of file process_expression.h.

◆ make_block() [1/2]

template<class... ARGUMENTS>

void mcrl2::process::make_block	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_block constructs a new term into a given address. \

Parameters

t	The reference into which the new block is constructed.

Definition at line 597 of file process_expression.h.

◆ make_block() [2/2]

process_expression mcrl2::process::make_block	(	const core::identifier_string_list &	B,
		const process_expression &	x
	)

inline

Definition at line 120 of file utility.h.

◆ make_bounded_init()

template<class... ARGUMENTS>

void mcrl2::process::make_bounded_init	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_bounded_init constructs a new term into a given address. \

Parameters

t	The reference into which the new bounded_init is constructed.

Definition at line 1362 of file process_expression.h.

◆ make_choice()

template<class... ARGUMENTS>

void mcrl2::process::make_choice	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_choice constructs a new term into a given address. \

Parameters

t	The reference into which the new choice is constructed.

Definition at line 1590 of file process_expression.h.

◆ make_comm() [1/2]

template<class... ARGUMENTS>

void mcrl2::process::make_comm	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_comm constructs a new term into a given address. \

Parameters

t	The reference into which the new comm is constructed.

Definition at line 825 of file process_expression.h.

◆ make_comm() [2/2]

process_expression mcrl2::process::make_comm	(	const communication_expression_list &	C,
		const process_expression &	x
	)

inline

Definition at line 94 of file utility.h.

◆ make_communication_expression()

template<class... ARGUMENTS>

void mcrl2::process::make_communication_expression	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_communication_expression constructs a new term into a given address. \

Parameters

t	The reference into which the new communication_expression is constructed.

Definition at line 71 of file communication_expression.h.

◆ make_hide() [1/2]

template<class... ARGUMENTS>

void mcrl2::process::make_hide	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_hide constructs a new term into a given address. \

Parameters

t	The reference into which the new hide is constructed.

Definition at line 673 of file process_expression.h.

◆ make_hide() [2/2]

process_expression mcrl2::process::make_hide	(	const core::identifier_string_list &	I,
		const process_expression &	x
	)

inline

Definition at line 107 of file utility.h.

◆ make_if_then()

template<class... ARGUMENTS>

void mcrl2::process::make_if_then	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_if_then constructs a new term into a given address. \

Parameters

t	The reference into which the new if_then is constructed.

Definition at line 1205 of file process_expression.h.

◆ make_if_then_else()

template<class... ARGUMENTS>

void mcrl2::process::make_if_then_else	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_if_then_else constructs a new term into a given address. \

Parameters

t	The reference into which the new if_then_else is constructed.

Definition at line 1286 of file process_expression.h.

◆ make_left_merge() [1/2]

template<class... ARGUMENTS>

void mcrl2::process::make_left_merge	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_left_merge constructs a new term into a given address. \

Parameters

t	The reference into which the new left_merge is constructed.

Definition at line 1514 of file process_expression.h.

◆ make_left_merge() [2/2]

process_expression mcrl2::process::make_left_merge	(	const process_expression &	x,
		const process_expression &	y
	)

inline

Definition at line 62 of file utility.h.

◆ make_merge() [1/2]

template<class... ARGUMENTS>

void mcrl2::process::make_merge	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_merge constructs a new term into a given address. \

Parameters

t	The reference into which the new merge is constructed.

Definition at line 1438 of file process_expression.h.

◆ make_merge() [2/2]

process_expression mcrl2::process::make_merge	(	const process_expression &	x,
		const process_expression &	y
	)

inline

Definition at line 52 of file utility.h.

◆ make_process_equation()

template<class... ARGUMENTS>

void mcrl2::process::make_process_equation	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_process_equation constructs a new term into a given address. \

Parameters

t	The reference into which the new process_equation is constructed.

Definition at line 71 of file process_equation.h.

◆ make_process_identifier()

template<class... ARGUMENTS>

void mcrl2::process::make_process_identifier	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_process_identifier constructs a new term into a given address. \

Parameters

t	The reference into which the new process_identifier is constructed.

Definition at line 76 of file process_identifier.h.

◆ make_process_instance()

template<class... ARGUMENTS>

void mcrl2::process::make_process_instance	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_process_instance constructs a new term into a given address. \

Parameters

t	The reference into which the new process_instance is constructed.

Definition at line 263 of file process_expression.h.

◆ make_process_instance_assignment()

template<class... ARGUMENTS>

void mcrl2::process::make_process_instance_assignment	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_process_instance_assignment constructs a new term into a given address. \

Parameters

t	The reference into which the new process_instance_assignment is constructed.

Definition at line 339 of file process_expression.h.

◆ make_rename()

template<class... ARGUMENTS>

void mcrl2::process::make_rename	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_rename constructs a new term into a given address. \

Parameters

t	The reference into which the new rename is constructed.

Definition at line 749 of file process_expression.h.

◆ make_rename_expression()

template<class... ARGUMENTS>

void mcrl2::process::make_rename_expression	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_rename_expression constructs a new term into a given address. \

Parameters

t	The reference into which the new rename_expression is constructed.

Definition at line 72 of file rename_expression.h.

◆ make_seq()

template<class... ARGUMENTS>

void mcrl2::process::make_seq	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_seq constructs a new term into a given address. \

Parameters

t	The reference into which the new seq is constructed.

Definition at line 1129 of file process_expression.h.

◆ make_stochastic_operator()

template<class... ARGUMENTS>

void mcrl2::process::make_stochastic_operator	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_stochastic_operator constructs a new term into a given address. \

Parameters

t	The reference into which the new stochastic_operator is constructed.

Definition at line 1671 of file process_expression.h.

◆ make_sum()

template<class... ARGUMENTS>

void mcrl2::process::make_sum	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_sum constructs a new term into a given address. \

Parameters

t	The reference into which the new sum is constructed.

Definition at line 521 of file process_expression.h.

◆ make_sync() [1/2]

template<class... ARGUMENTS>

void mcrl2::process::make_sync	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_sync constructs a new term into a given address. \

Parameters

t	The reference into which the new sync is constructed.

Definition at line 977 of file process_expression.h.

◆ make_sync() [2/2]

process_expression mcrl2::process::make_sync	(	const process_expression &	x,
		const process_expression &	y
	)

inline

Definition at line 42 of file utility.h.

◆ make_untyped_multi_action()

template<class... ARGUMENTS>

void mcrl2::process::make_untyped_multi_action	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_untyped_multi_action constructs a new term into a given address. \

Parameters

t	The reference into which the new untyped_multi_action is constructed.

Definition at line 59 of file untyped_multi_action.h.

◆ make_untyped_process_assignment()

template<class... ARGUMENTS>

void mcrl2::process::make_untyped_process_assignment	(	atermpp::aterm_appl &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_untyped_process_assignment constructs a new term into a given address. \

Parameters

t	The reference into which the new untyped_process_assignment is constructed.

Definition at line 1752 of file process_expression.h.

◆ merge_action_specifications()

action_label_list mcrl2::process::merge_action_specifications	(	const action_label_list &	actspec1,
		const action_label_list &	actspec2
	)

inline

Merges two action specifications.

Definition at line 23 of file merge_action_specifications.h.

◆ normalize_sorts() [1/7]

process::action mcrl2::process::normalize_sorts	(	const action &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 66 of file process.cpp.

◆ normalize_sorts() [2/7]

process::action_label_list mcrl2::process::normalize_sorts	(	const action_label_list &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 67 of file process.cpp.

◆ normalize_sorts() [3/7]

template<typename T >

T mcrl2::process::normalize_sorts	(	const T &	x,
		const data::sort_specification &	sortspec,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 34 of file normalize_sorts.h.

◆ normalize_sorts() [4/7]

void mcrl2::process::normalize_sorts	(	process::process_equation_vector &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 68 of file process.cpp.

◆ normalize_sorts() [5/7]

void mcrl2::process::normalize_sorts	(	process_identifier_vector &	x,
		const data::sort_specification &	sortspec
	)

◆ normalize_sorts() [6/7]

void mcrl2::process::normalize_sorts	(	process::process_specification &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 69 of file process.cpp.

◆ normalize_sorts() [7/7]

template<typename T >

void mcrl2::process::normalize_sorts	(	T &	x,
		const data::sort_specification &	sortspec,
		typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 25 of file normalize_sorts.h.

◆ operator!=()

bool mcrl2::process::operator!=	(	const process_specification &	spec1,
		const process_specification &	spec2
	)

inline

Inequality operator.

Definition at line 240 of file process_specification.h.

◆ operator<<() [1/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 209 of file process_expression.h.

◆ operator<<() [2/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 99 of file action_label.h.

◆ operator<<() [3/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 89 of file action_name_multiset.h.

◆ operator<<() [4/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 923 of file process_expression.h.

◆ operator<<() [5/35]

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

inline

Definition at line 152 of file allow_set.h.

◆ operator<<() [6/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 1075 of file process_expression.h.

◆ operator<<() [7/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 619 of file process_expression.h.

◆ operator<<() [8/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 1384 of file process_expression.h.

◆ operator<<() [9/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 1612 of file process_expression.h.

◆ operator<<() [10/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 847 of file process_expression.h.

◆ operator<<() [11/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 99 of file communication_expression.h.

◆ operator<<() [12/35]

std::ostream & mcrl2::process::operator<<	(	std::ostream &	out,
		const data::sorts_list &	x
	)

inline

Definition at line 57 of file typecheck.h.

◆ operator<<() [13/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 414 of file process_expression.h.

◆ operator<<() [14/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 695 of file process_expression.h.

◆ operator<<() [15/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 1227 of file process_expression.h.

◆ operator<<() [16/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 1308 of file process_expression.h.

◆ operator<<() [17/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 1536 of file process_expression.h.

◆ operator<<() [18/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 1460 of file process_expression.h.

◆ operator<<() [19/35]

std::ostream & mcrl2::process::operator<<	(	std::ostream &	out,
		const multi_action_name &	alpha
	)

inline

Definition at line 62 of file multi_action_name.h.

◆ operator<<() [20/35]

std::ostream & mcrl2::process::operator<<	(	std::ostream &	out,
		const multi_action_name_set &	A
	)

inline

Definition at line 86 of file multi_action_name.h.

◆ operator<<() [21/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 99 of file process_equation.h.

◆ operator<<() [22/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 127 of file process_expression.h.

◆ operator<<() [23/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 104 of file process_identifier.h.

◆ operator<<() [24/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 285 of file process_expression.h.

◆ operator<<() [25/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 361 of file process_expression.h.

◆ operator<<() [26/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 200 of file process_specification.h.

◆ operator<<() [27/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 771 of file process_expression.h.

◆ operator<<() [28/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 100 of file rename_expression.h.

◆ operator<<() [29/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 1151 of file process_expression.h.

◆ operator<<() [30/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 1693 of file process_expression.h.

◆ operator<<() [31/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 543 of file process_expression.h.

◆ operator<<() [32/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 999 of file process_expression.h.

◆ operator<<() [33/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 467 of file process_expression.h.

◆ operator<<() [34/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 87 of file untyped_multi_action.h.

◆ operator<<() [35/35]

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

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 1774 of file process_expression.h.

◆ operator==()

bool mcrl2::process::operator==	(	const process_specification &	spec1,
		const process_specification &	spec2
	)

inline

Equality operator.

Definition at line 233 of file process_specification.h.

◆ parse_action_declaration()

process::action_label_list mcrl2::process::parse_action_declaration	(	const std::string &	text,
		const data::data_specification &	data_spec = `data::detail::default_specification()`
	)

Parses an action declaration from a string.

Parameters

	text	A string containing an action declaration
[in]	data_spec	A data specification used for sort normalization

Returns: A list of action labels

Exceptions

mcrl2::runtime_error when the input does not match the syntax of an action declaration.

Definition at line 111 of file process.cpp.

◆ parse_process_expression() [1/4]

process_expression mcrl2::process::parse_process_expression	(	const std::string &	text,
		const std::string &	data_decl,
		const std::string &	proc_decl
	)

inline

Parses and type checks a process expression.

Parameters

[in]	text	The input text containing a process expression.
[in]	data_decl	A declaration of data and actions ("glob m:Nat; act a:Nat;").
[in]	proc_decl	A process declaration ("proc P(n: Nat);").

Definition at line 89 of file parse.h.

◆ parse_process_expression() [2/4]

process_expression mcrl2::process::parse_process_expression	(	const std::string &	text,
		const std::string &	procspec_text
	)

inline

Parses and type checks a process expression.

Parameters

[in]	text	The input text containing a process expression.
[in]	procspec_text	A textual version of a process specification used as context

Definition at line 105 of file parse.h.

◆ parse_process_expression() [3/4]

template<typename VariableContainer >

process_expression mcrl2::process::parse_process_expression	(	const std::string &	text,
		const VariableContainer &	variables,
		const process_specification &	procspec
	)

Parses and type checks a process expression. N.B. Very inefficient!

Definition at line 117 of file parse.h.

◆ parse_process_expression() [4/4]

template<typename VariableContainer , typename ActionLabelContainer , typename ProcessIdentifierContainer >

process_expression mcrl2::process::parse_process_expression	(	const std::string &	text,
		const VariableContainer &	variables = `VariableContainer()`,
		const data::data_specification &	dataspec = `data::data_specification()`,
		const ActionLabelContainer &	action_labels = `std::vector<action_label>()`,
		const ProcessIdentifierContainer &	process_identifiers = `ProcessIdentifierContainer()`,
		const process_identifier *	current_equation = `nullptr`
	)

Definition at line 130 of file parse.h.

◆ parse_process_identifier()

process_identifier mcrl2::process::parse_process_identifier	(	std::string	text,
		const data::data_specification &	dataspec
	)

inline

Parses a process identifier.

Definition at line 64 of file parse.h.

◆ parse_process_specification() [1/2]

process_specification mcrl2::process::parse_process_specification ( const std::string & spec_string )

inline

Parses a process specification from a string.

Parameters

spec_string A string

Returns: The parse result

Definition at line 56 of file parse.h.

◆ parse_process_specification() [2/2]

process_specification mcrl2::process::parse_process_specification ( std::istream & in )

inline

Parses a process specification from an input stream.

Parameters

in	An input stream

Returns: The parse result

Definition at line 43 of file parse.h.

◆ pp() [1/44]

std::string mcrl2::process::pp ( const action & x )

Definition at line 35 of file process.cpp.

◆ pp() [2/44]

std::string mcrl2::process::pp ( const action_label & x )

Definition at line 36 of file process.cpp.

◆ pp() [3/44]

std::string mcrl2::process::pp ( const action_label_list & x )

Definition at line 27 of file process.cpp.

◆ pp() [4/44]

std::string mcrl2::process::pp ( const action_label_vector & x )

Definition at line 28 of file process.cpp.

◆ pp() [5/44]

std::string mcrl2::process::pp ( const action_list & x )

Definition at line 25 of file process.cpp.

◆ pp() [6/44]

std::string mcrl2::process::pp ( const action_name_multiset & x )

Definition at line 37 of file process.cpp.

◆ pp() [7/44]

std::string mcrl2::process::pp ( const action_vector & x )

Definition at line 26 of file process.cpp.

◆ pp() [8/44]

std::string mcrl2::process::pp ( const allow & x )

Definition at line 38 of file process.cpp.

◆ pp() [9/44]

std::string mcrl2::process::pp ( const at & x )

Definition at line 39 of file process.cpp.

◆ pp() [10/44]

std::string mcrl2::process::pp ( const block & x )

Definition at line 40 of file process.cpp.

◆ pp() [11/44]

std::string mcrl2::process::pp ( const bounded_init & x )

Definition at line 41 of file process.cpp.

◆ pp() [12/44]

std::string mcrl2::process::pp ( const choice & x )

Definition at line 42 of file process.cpp.

◆ pp() [13/44]

std::string mcrl2::process::pp ( const comm & x )

Definition at line 43 of file process.cpp.

◆ pp() [14/44]

std::string mcrl2::process::pp ( const communication_expression & x )

Definition at line 44 of file process.cpp.

◆ pp() [15/44]

std::string mcrl2::process::pp ( const delta & x )

Definition at line 45 of file process.cpp.

◆ pp() [16/44]

std::string mcrl2::process::pp ( const hide & x )

Definition at line 46 of file process.cpp.

◆ pp() [17/44]

std::string mcrl2::process::pp ( const if_then & x )

Definition at line 47 of file process.cpp.

◆ pp() [18/44]

std::string mcrl2::process::pp ( const if_then_else & x )

Definition at line 48 of file process.cpp.

◆ pp() [19/44]

std::string mcrl2::process::pp ( const left_merge & x )

Definition at line 49 of file process.cpp.

◆ pp() [20/44]

std::string mcrl2::process::pp ( const merge & x )

Definition at line 50 of file process.cpp.

◆ pp() [21/44]

std::string mcrl2::process::pp ( const multi_action_name & x )

inline

Pretty print function for a multi action name.

Definition at line 40 of file multi_action_name.h.

◆ pp() [22/44]

std::string mcrl2::process::pp ( const multi_action_name_set & A )

inline

Pretty print function for a set of multi action names.

Definition at line 69 of file multi_action_name.h.

◆ pp() [23/44]

std::string mcrl2::process::pp ( const process_equation & x )

Definition at line 51 of file process.cpp.

◆ pp() [24/44]

std::string mcrl2::process::pp ( const process_equation_list & x )

Definition at line 33 of file process.cpp.

◆ pp() [25/44]

std::string mcrl2::process::pp ( const process_equation_vector & x )

Definition at line 34 of file process.cpp.

◆ pp() [26/44]

std::string mcrl2::process::pp ( const process_expression & x )

Definition at line 52 of file process.cpp.

◆ pp() [27/44]

std::string mcrl2::process::pp ( const process_expression_list & x )

Definition at line 31 of file process.cpp.

◆ pp() [28/44]

std::string mcrl2::process::pp ( const process_expression_vector & x )

Definition at line 32 of file process.cpp.

◆ pp() [29/44]

std::string mcrl2::process::pp ( const process_identifier & x )

Definition at line 53 of file process.cpp.

◆ pp() [30/44]

std::string mcrl2::process::pp ( const process_identifier_list & x )

Definition at line 29 of file process.cpp.

◆ pp() [31/44]

std::string mcrl2::process::pp ( const process_identifier_vector & x )

Definition at line 30 of file process.cpp.

◆ pp() [32/44]

std::string mcrl2::process::pp ( const process_instance & x )

Definition at line 54 of file process.cpp.

◆ pp() [33/44]

std::string mcrl2::process::pp ( const process_instance_assignment & x )

Definition at line 55 of file process.cpp.

◆ pp() [34/44]

std::string mcrl2::process::pp ( const process_specification & x )

Definition at line 56 of file process.cpp.

◆ pp() [35/44]

std::string mcrl2::process::pp ( const rename & x )

Definition at line 57 of file process.cpp.

◆ pp() [36/44]

std::string mcrl2::process::pp ( const rename_expression & x )

Definition at line 58 of file process.cpp.

◆ pp() [37/44]

std::string mcrl2::process::pp ( const seq & x )

Definition at line 59 of file process.cpp.

◆ pp() [38/44]

std::string mcrl2::process::pp ( const stochastic_operator & x )

Definition at line 60 of file process.cpp.

◆ pp() [39/44]

std::string mcrl2::process::pp ( const sum & x )

Definition at line 61 of file process.cpp.

◆ pp() [40/44]

std::string mcrl2::process::pp ( const sync & x )

Definition at line 62 of file process.cpp.

◆ pp() [41/44]

template<typename T >

std::string mcrl2::process::pp ( const T & x )

Returns a string representation of the object x.

Definition at line 489 of file print.h.

◆ pp() [42/44]

std::string mcrl2::process::pp ( const tau & x )

Definition at line 63 of file process.cpp.

◆ pp() [43/44]

std::string mcrl2::process::pp ( const untyped_multi_action & x )

Definition at line 64 of file process.cpp.

◆ pp() [44/44]

std::string mcrl2::process::pp ( const untyped_process_assignment & x )

Definition at line 65 of file process.cpp.

◆ precedence() [1/12]

constexpr int mcrl2::process::precedence ( const at & )

inlineconstexpr

Definition at line 31 of file print.h.

◆ precedence() [2/12]

constexpr int mcrl2::process::precedence ( const bounded_init & )

inlineconstexpr

Definition at line 29 of file print.h.

◆ precedence() [3/12]

constexpr int mcrl2::process::precedence ( const choice & )

inlineconstexpr

Definition at line 22 of file print.h.

◆ precedence() [4/12]

constexpr int mcrl2::process::precedence ( const if_then & )

inlineconstexpr

Definition at line 27 of file print.h.

◆ precedence() [5/12]

constexpr int mcrl2::process::precedence ( const if_then_else & )

inlineconstexpr

Definition at line 28 of file print.h.

◆ precedence() [6/12]

constexpr int mcrl2::process::precedence ( const left_merge & )

inlineconstexpr

Definition at line 26 of file print.h.

◆ precedence() [7/12]

constexpr int mcrl2::process::precedence ( const merge & )

inlineconstexpr

Definition at line 25 of file print.h.

◆ precedence() [8/12]

int mcrl2::process::precedence ( const process_expression & x )

inline

Definition at line 33 of file print.h.

◆ precedence() [9/12]

constexpr int mcrl2::process::precedence ( const seq & )

inlineconstexpr

Definition at line 30 of file print.h.

◆ precedence() [10/12]

constexpr int mcrl2::process::precedence ( const stochastic_operator & )

inlineconstexpr

Definition at line 24 of file print.h.

◆ precedence() [11/12]

constexpr int mcrl2::process::precedence ( const sum & )

inlineconstexpr

Definition at line 23 of file print.h.

◆ precedence() [12/12]

constexpr int mcrl2::process::precedence ( const sync & )

inlineconstexpr

Definition at line 32 of file print.h.

◆ process_info()

void mcrl2::process::process_info ( const process_specification & procspec )

inline

Prints information about a process specification.

Definition at line 23 of file process_info.h.

◆ process_instance_replace() [1/2]

process_expression mcrl2::process::process_instance_replace	(	const process_expression &	x,
		const std::map< process_identifier, process_instance > &	substitutions
	)

inline

Definition at line 134 of file eliminate_trivial_equations.h.

◆ process_instance_replace() [2/2]

void mcrl2::process::process_instance_replace	(	process_specification &	procspec,
		const std::map< process_identifier, process_instance > &	substitutions
	)

inline

Definition at line 143 of file eliminate_trivial_equations.h.

◆ process_specification_to_aterm()

atermpp::aterm_appl mcrl2::process::process_specification_to_aterm ( const process_specification & spec )

inline

Conversion to aterm_appl.

Returns: The specification converted to aterm format.

Parameters

spec	A process specification

Definition at line 220 of file process_specification.h.

◆ process_variable_strongly_connected_components() [1/2]

std::vector< std::set< process_identifier > > mcrl2::process::process_variable_strongly_connected_components ( const std::vector< process_equation > & equations )

inline

Computes an SCC graph of the equations.

Definition at line 291 of file process_variable_strongly_connected_components.h.

◆ process_variable_strongly_connected_components() [2/2]

std::vector< std::set< process_identifier > > mcrl2::process::process_variable_strongly_connected_components	(	const std::vector< process_equation > &	equations,
		const process_expression &	init
	)

inline

Compute an SCC graph of the equations reachable from init.

Definition at line 299 of file process_variable_strongly_connected_components.h.

◆ push_allow()

process_expression mcrl2::process::push_allow	(	const process_expression &	x,
		const action_name_multiset_list &	V,
		std::vector< process_equation > &	equations,
		data::set_identifier_generator &	id_generator,
		std::map< process_identifier, multi_action_name_set > &	pcrl_equation_cache
	)

inline

Definition at line 735 of file alphabet_push_allow.h.

◆ push_block()

process_expression mcrl2::process::push_block	(	const core::identifier_string_list &	B,
		const process_expression &	x,
		std::vector< process_equation > &	equations,
		data::set_identifier_generator &	id_generator,
		std::map< process_identifier, multi_action_name_set > &	pcrl_equation_cache
	)

inline

Definition at line 358 of file alphabet_push_block.h.

◆ remove_data_parameters()

void mcrl2::process::remove_data_parameters ( process_specification & procspec )

inline

Definition at line 108 of file remove_data_parameters.h.

◆ remove_duplicate_equations()

void mcrl2::process::remove_duplicate_equations ( process_specification & procspec )

inline

Removes duplicate equations from a process specification, using a bisimulation algorithm.

Definition at line 196 of file remove_equations.h.

◆ replace_all_variables() [1/2]

template<typename T , typename Substitution >

T mcrl2::process::replace_all_variables	(	const T &	x,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 100 of file replace.h.

◆ replace_all_variables() [2/2]

template<typename T , typename Substitution >

void mcrl2::process::replace_all_variables	(	T &	x,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 91 of file replace.h.

◆ replace_data_expressions() [1/2]

template<typename T , typename Substitution >

T mcrl2::process::replace_data_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 58 of file replace.h.

◆ replace_data_expressions() [2/2]

template<typename T , typename Substitution >

void mcrl2::process::replace_data_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 48 of file replace.h.

◆ replace_free_variables() [1/4]

template<typename T , typename Substitution , typename VariableContainer >

T mcrl2::process::replace_free_variables	(	const T &	x,
		const Substitution &	sigma,
		const VariableContainer &	bound_variables,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 152 of file replace.h.

◆ replace_free_variables() [2/4]

template<typename T , typename Substitution >

T mcrl2::process::replace_free_variables	(	const T &	x,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies the substitution sigma to x. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 125 of file replace.h.

◆ replace_free_variables() [3/4]

template<typename T , typename Substitution , typename VariableContainer >

void mcrl2::process::replace_free_variables	(	T &	x,
		const Substitution &	sigma,
		const VariableContainer &	bound_variables,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 139 of file replace.h.

◆ replace_free_variables() [4/4]

template<typename T , typename Substitution >

void mcrl2::process::replace_free_variables	(	T &	x,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies the substitution sigma to x. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 113 of file replace.h.

◆ replace_process_identifiers() [1/2]

template<typename T , typename Substitution >

T mcrl2::process::replace_process_identifiers	(	const T &	x,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 197 of file replace.h.

◆ replace_process_identifiers() [2/2]

template<typename T , typename Substitution >

void mcrl2::process::replace_process_identifiers	(	T &	x,
		const Substitution &	sigma,
		typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *	= `0`
	)

Definition at line 188 of file replace.h.

◆ replace_sort_expressions() [1/2]

template<typename T , typename Substitution >

T mcrl2::process::replace_sort_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 36 of file replace.h.

◆ replace_sort_expressions() [2/2]

template<typename T , typename Substitution >

void mcrl2::process::replace_sort_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 26 of file replace.h.

◆ replace_subterm() [1/2]

process_expression mcrl2::process::replace_subterm	(	const process_expression &	expr,
		std::size_t	x,
		std::size_t	y,
		const process_expression &	replacement
	)

inline

Replace the subterm at position (x, y) with a given term.

Definition at line 327 of file replace_subterm.h.

◆ replace_subterm() [2/2]

process_specification mcrl2::process::replace_subterm	(	const process_specification &	procspec,
		std::size_t	x,
		std::size_t	y,
		const process_expression &	replacement
	)

inline

Replace the subterm at position (x, y) with a given term.

Definition at line 337 of file replace_subterm.h.

◆ replace_variables() [1/2]

template<typename T , typename Substitution >

T mcrl2::process::replace_variables	(	const T &	x,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 80 of file replace.h.

◆ replace_variables() [2/2]

template<typename T , typename Substitution >

void mcrl2::process::replace_variables	(	T &	x,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 71 of file replace.h.

◆ replace_variables_capture_avoiding() [1/4]

template<typename T , typename Substitution >

T mcrl2::process::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the substiution is applied. \param sigma A substitution. \param id_generator An identifier generator that generates names that do not appear in x and sigma

Definition at line 128 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [2/4]

template<typename T , typename Substitution >

T mcrl2::process::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the substiution is applied. \param sigma A substitution.

Definition at line 162 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [3/4]

template<typename T , typename Substitution >

void mcrl2::process::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the subsitution is applied. \param sigma A substitution. \param id_generator An identifier generator that generates names that do not appear in x and sigma

Definition at line 113 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [4/4]

template<typename T , typename Substitution >

void mcrl2::process::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the subsitution is applied. \param sigma A substitution.

Definition at line 144 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

template<typename T , typename Substitution , typename IdentifierGenerator >

T mcrl2::process::replace_variables_capture_avoiding_with_an_identifier_generator	(	const T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x using an identifier generator.. \details This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables. \param x The object to which the substiution is applied. \param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose. \param id_generator A generator that generates unique strings, not yet used as variable names. \return The result is the term x to which sigma has been applied.

Definition at line 158 of file replace_capture_avoiding_with_an_identifier_generator.h.

◆ replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

template<typename T , typename Substitution , typename IdentifierGenerator >

void mcrl2::process::replace_variables_capture_avoiding_with_an_identifier_generator	(	T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x using an identifier generator. \details This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables. \param x The object to which the subsitution is applied. \param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose. \param id_generator A generator that generates unique strings, not yet used as variable names.

Definition at line 139 of file replace_capture_avoiding_with_an_identifier_generator.h.

◆ rewrite() [1/4]

template<typename T , typename Rewriter , typename Substitution >

T mcrl2::process::rewrite	(	const T &	x,
		Rewriter	R,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly \param x an object containing expressions \param R a rewriter \param sigma a substitution \return the rewrite result

Definition at line 70 of file rewrite.h.

◆ rewrite() [2/4]

template<typename T , typename Rewriter >

T mcrl2::process::rewrite	(	const T &	x,
		Rewriter	R,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Rewrites all embedded expressions in an object x \param x an object containing expressions \param R a rewriter \return the rewrite result

Definition at line 40 of file rewrite.h.

◆ rewrite() [3/4]

template<typename T , typename Rewriter , typename Substitution >

void mcrl2::process::rewrite	(	T &	x,
		Rewriter	R,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly \param x an object containing expressions \param R a rewriter \param sigma a substitution

Definition at line 55 of file rewrite.h.

◆ rewrite() [4/4]

template<typename T , typename Rewriter >

void mcrl2::process::rewrite	(	T &	x,
		Rewriter	R,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Rewrites all embedded expressions in an object x \param x an object containing expressions \param R a rewriter

Definition at line 27 of file rewrite.h.

◆ sorts_list_intersection()

data::sorts_list mcrl2::process::sorts_list_intersection	(	const data::sorts_list &	sorts1,
		const data::sorts_list &	sorts2
	)

inline

Definition at line 43 of file typecheck.h.

◆ split_summands()

std::vector< process_expression > mcrl2::process::split_summands ( const process_expression & x )

inline

Splits a choice into a set of operands Given a process expression of the form p1 + p2 + .... + pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a + as main function symbol.

Parameters

x	A process expression.

Returns: A set of process expressions.

Definition at line 28 of file join.h.

◆ swap() [1/30]

void mcrl2::process::swap	(	action &	t1,
		action &	t2
	)

inline

\brief swap overload

Definition at line 215 of file process_expression.h.

◆ swap() [2/30]

void mcrl2::process::swap	(	action_label &	t1,
		action_label &	t2
	)

inline

\brief swap overload

Definition at line 105 of file action_label.h.

◆ swap() [3/30]

void mcrl2::process::swap	(	action_name_multiset &	t1,
		action_name_multiset &	t2
	)

inline

\brief swap overload

Definition at line 95 of file action_name_multiset.h.

◆ swap() [4/30]

void mcrl2::process::swap	(	allow &	t1,
		allow &	t2
	)

inline

\brief swap overload

Definition at line 929 of file process_expression.h.

◆ swap() [5/30]

void mcrl2::process::swap	(	at &	t1,
		at &	t2
	)

inline

\brief swap overload

Definition at line 1081 of file process_expression.h.

◆ swap() [6/30]

void mcrl2::process::swap	(	block &	t1,
		block &	t2
	)

inline

\brief swap overload

Definition at line 625 of file process_expression.h.

◆ swap() [7/30]

void mcrl2::process::swap	(	bounded_init &	t1,
		bounded_init &	t2
	)

inline

\brief swap overload

Definition at line 1390 of file process_expression.h.

◆ swap() [8/30]

void mcrl2::process::swap	(	choice &	t1,
		choice &	t2
	)

inline

\brief swap overload

Definition at line 1618 of file process_expression.h.

◆ swap() [9/30]

void mcrl2::process::swap	(	comm &	t1,
		comm &	t2
	)

inline

\brief swap overload

Definition at line 853 of file process_expression.h.

◆ swap() [10/30]

void mcrl2::process::swap	(	communication_expression &	t1,
		communication_expression &	t2
	)

inline

\brief swap overload

Definition at line 105 of file communication_expression.h.

◆ swap() [11/30]

void mcrl2::process::swap	(	delta &	t1,
		delta &	t2
	)

inline

\brief swap overload

Definition at line 420 of file process_expression.h.

◆ swap() [12/30]

void mcrl2::process::swap	(	hide &	t1,
		hide &	t2
	)

inline

\brief swap overload

Definition at line 701 of file process_expression.h.

◆ swap() [13/30]

void mcrl2::process::swap	(	if_then &	t1,
		if_then &	t2
	)

inline

\brief swap overload

Definition at line 1233 of file process_expression.h.

◆ swap() [14/30]

void mcrl2::process::swap	(	if_then_else &	t1,
		if_then_else &	t2
	)

inline

\brief swap overload

Definition at line 1314 of file process_expression.h.

◆ swap() [15/30]

void mcrl2::process::swap	(	left_merge &	t1,
		left_merge &	t2
	)

inline

\brief swap overload

Definition at line 1542 of file process_expression.h.

◆ swap() [16/30]

void mcrl2::process::swap	(	merge &	t1,
		merge &	t2
	)

inline

\brief swap overload

Definition at line 1466 of file process_expression.h.

◆ swap() [17/30]

void mcrl2::process::swap	(	process_equation &	t1,
		process_equation &	t2
	)

inline

\brief swap overload

Definition at line 105 of file process_equation.h.

◆ swap() [18/30]

void mcrl2::process::swap	(	process_expression &	t1,
		process_expression &	t2
	)

inline

\brief swap overload

Definition at line 133 of file process_expression.h.

◆ swap() [19/30]

void mcrl2::process::swap	(	process_identifier &	t1,
		process_identifier &	t2
	)

inline

\brief swap overload

Definition at line 110 of file process_identifier.h.

◆ swap() [20/30]

void mcrl2::process::swap	(	process_instance &	t1,
		process_instance &	t2
	)

inline

\brief swap overload

Definition at line 291 of file process_expression.h.

◆ swap() [21/30]

void mcrl2::process::swap	(	process_instance_assignment &	t1,
		process_instance_assignment &	t2
	)

inline

\brief swap overload

Definition at line 367 of file process_expression.h.

◆ swap() [22/30]

void mcrl2::process::swap	(	rename &	t1,
		rename &	t2
	)

inline

\brief swap overload

Definition at line 777 of file process_expression.h.

◆ swap() [23/30]

void mcrl2::process::swap	(	rename_expression &	t1,
		rename_expression &	t2
	)

inline

\brief swap overload

Definition at line 106 of file rename_expression.h.

◆ swap() [24/30]

void mcrl2::process::swap	(	seq &	t1,
		seq &	t2
	)

inline

\brief swap overload

Definition at line 1157 of file process_expression.h.

◆ swap() [25/30]

void mcrl2::process::swap	(	stochastic_operator &	t1,
		stochastic_operator &	t2
	)

inline

\brief swap overload

Definition at line 1699 of file process_expression.h.

◆ swap() [26/30]

void mcrl2::process::swap	(	sum &	t1,
		sum &	t2
	)

inline

\brief swap overload

Definition at line 549 of file process_expression.h.

◆ swap() [27/30]

void mcrl2::process::swap	(	sync &	t1,
		sync &	t2
	)

inline

\brief swap overload

Definition at line 1005 of file process_expression.h.

◆ swap() [28/30]

void mcrl2::process::swap	(	tau &	t1,
		tau &	t2
	)

inline

\brief swap overload

Definition at line 473 of file process_expression.h.

◆ swap() [29/30]

void mcrl2::process::swap	(	untyped_multi_action &	t1,
		untyped_multi_action &	t2
	)

inline

\brief swap overload

Definition at line 93 of file untyped_multi_action.h.

◆ swap() [30/30]

void mcrl2::process::swap	(	untyped_process_assignment &	t1,
		untyped_process_assignment &	t2
	)

inline

\brief swap overload

Definition at line 1780 of file process_expression.h.

◆ sync_multi_action_name()

multi_action_name mcrl2::process::sync_multi_action_name ( const sync & x )

inline

Computes a multi action name corresponding to a sync (provided that the sync is a pCRL expression).

Definition at line 59 of file is_multi_action.h.

◆ translate_user_notation() [1/5]

process::action mcrl2::process::translate_user_notation ( const action & x )

Definition at line 70 of file process.cpp.

◆ translate_user_notation() [2/5]

process::process_expression mcrl2::process::translate_user_notation ( const process::process_expression & x )

Definition at line 71 of file process.cpp.

◆ translate_user_notation() [3/5]

template<typename T >

T mcrl2::process::translate_user_notation	(	const T &	x,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 33 of file translate_user_notation.h.

◆ translate_user_notation() [4/5]

void mcrl2::process::translate_user_notation ( process::process_specification & x )

Definition at line 72 of file process.cpp.

◆ translate_user_notation() [5/5]

template<typename T >

void mcrl2::process::translate_user_notation	(	T &	x,
		typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 25 of file translate_user_notation.h.

◆ typecheck_action()

action mcrl2::process::typecheck_action	(	const core::identifier_string &	name,
		const data::data_expression_list &	parameters,
		data::data_type_checker &	typechecker,
		const data::detail::variable_context &	variable_context,
		const detail::action_context &	action_context
	)

inline

Definition at line 28 of file typecheck.h.

◆ typecheck_process_expression()

template<typename VariableContainer , typename ActionLabelContainer , typename ProcessIdentifierContainer >

process_expression mcrl2::process::typecheck_process_expression	(	const process_expression &	x,
		const VariableContainer &	variables = `VariableContainer()`,
		const data::data_specification &	dataspec = `data::data_specification()`,
		const ActionLabelContainer &	action_labels = `ActionLabelContainer()`,
		const ProcessIdentifierContainer &	process_identifiers = `ProcessIdentifierContainer()`,
		const process_identifier *	current_equation = `nullptr`
	)

Typecheck a process expression.

Parameters

x	An untyped process expression
variables	A sequence of data variables
dataspec	A data specification
action_labels	A sequence of action labels
process_identifiers	A sequence of process identifiers
current_equation	A pointer to the current equation. If this pointer is set, a check will be done it process instance assignments assign values to all their parameters.

Definition at line 702 of file typecheck.h.

◆ typecheck_process_specification()

void mcrl2::process::typecheck_process_specification ( process_specification & proc_spec )

inline

Type check a parsed mCRL2 process specification. Throws an exception if something went wrong.

Parameters

[in] proc_spec A process specification that has not been type checked.

Postcondition: proc_spec is type checked.

Definition at line 687 of file typecheck.h.

Namespaces

Classes

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ action_label_list

◆ action_label_vector

◆ action_list

◆ action_name_multiset_list

◆ action_name_multiset_vector

◆ action_vector

◆ communication_expression_list

◆ communication_expression_vector

◆ multi_action_name_set

◆ process_equation_list

◆ process_equation_vector

◆ process_expression_list

◆ process_expression_vector

◆ process_identifier_list

◆ process_identifier_vector

◆ rename_expression_list

◆ rename_expression_vector

◆ untyped_multi_action_list

◆ untyped_multi_action_vector

Function Documentation

◆ alphabet()

◆ alphabet_bounded()

◆ alphabet_efficient()

◆ alphabet_new()

◆ alphabet_pcrl()

◆ alphabet_reduce()

◆ anonymize()

◆ balance_summands() [1/2]

◆ balance_summands() [2/2]

◆ complete_data_specification()

◆ contains_tau()

◆ eliminate_trivial_equations()

◆ eliminate_unused_equations()

◆ equal_signatures()

◆ expand_assignments()

◆ expand_process_instance_assignments()

◆ find_action_labels() [1/2]

◆ find_action_labels() [2/2]

◆ find_action_names()

◆ find_all_variables() [1/3]

◆ find_all_variables() [2/3]

◆ find_all_variables() [3/3]

◆ find_equation()

◆ find_free_variables() [1/4]

◆ find_free_variables() [2/4]

◆ find_free_variables() [3/4]

◆ find_free_variables() [4/4]

◆ find_free_variables_with_bound() [1/2]

◆ find_free_variables_with_bound() [2/2]

◆ find_function_symbols() [1/2]

◆ find_function_symbols() [2/2]

◆ find_identifiers() [1/3]

◆ find_identifiers() [2/3]

◆ find_identifiers() [3/3]

◆ find_sort_expressions() [1/6]

◆ find_sort_expressions() [2/6]

◆ find_sort_expressions() [3/6]

◆ find_sort_expressions() [4/6]

◆ find_sort_expressions() [5/6]

◆ find_sort_expressions() [6/6]

◆ find_subterm()

◆ is_action()

◆ is_action_label()

◆ is_action_name_multiset()

◆ is_allow()

◆ is_at()

◆ is_block()

◆ is_bounded_init()

◆ is_choice()

◆ is_comm()

◆ is_communicating_lpe()

◆ is_communication_expression()

◆ is_delta()

◆ is_guarded()