mcrl2::process Namespace Reference

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...
struct	action_name_compare
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 Uses boost::flat_multiset for improved cache locality and memory efficiency. More...
struct	process_builder_base
	Base builder class for processes. 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...
struct	process_traverser_base
	Base class for action_formula_traverser. 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
using	process_expression_list = atermpp::term_list< process_expression >
	\brief list of process_expressions
using	process_expression_vector = std::vector< process_expression >
	\brief vector of process_expressions
using	action_list = atermpp::term_list< action >
	\brief list of actions
using	action_vector = std::vector< action >
	\brief vector of actions
using	action_label_list = atermpp::term_list< action_label >
	\brief list of action_labels
using	action_label_vector = std::vector< action_label >
	\brief vector of action_labels
using	action_name_multiset_list = atermpp::term_list< action_name_multiset >
	\brief list of action_name_multisets
using	action_name_multiset_vector = std::vector< action_name_multiset >
	\brief vector of action_name_multisets
using	action_name_set = std::set< core::identifier_string >
using	communication_expression_list = atermpp::term_list< communication_expression >
	\brief list of communication_expressions
using	communication_expression_vector = std::vector< communication_expression >
	\brief vector of communication_expressions
using	multi_action_name_set = std::set< multi_action_name >
	Represents a set of multi action names.
using	process_equation_list = atermpp::term_list< process_equation >
	\brief list of process_equations
using	process_equation_vector = std::vector< process_equation >
	\brief vector of process_equations
using	process_identifier_list = atermpp::term_list< process_identifier >
	\brief list of process_identifiers
using	process_identifier_vector = std::vector< process_identifier >
	\brief vector of process_identifiers
using	rename_expression_list = atermpp::term_list< rename_expression >
	\brief list of rename_expressions
using	rename_expression_vector = std::vector< rename_expression >
	\brief vector of rename_expressions
using	untyped_multi_action_list = atermpp::term_list< untyped_multi_action >
	\brief list of untyped_multi_actions
using	untyped_multi_action_vector = std::vector< untyped_multi_action >
	\brief vector of untyped_multi_actions

Functions
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.
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	balance_summands (T &x)
	Reduces the nesting depth of the choice operator.
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	balance_summands (const T &x)
	Reduces the nesting depth of the choice operator.
bool	is_action (const atermpp::aterm &x)
bool	is_process_instance (const atermpp::aterm &x)
bool	is_process_instance_assignment (const atermpp::aterm &x)
bool	is_delta (const atermpp::aterm &x)
bool	is_tau (const atermpp::aterm &x)
bool	is_sum (const atermpp::aterm &x)
bool	is_block (const atermpp::aterm &x)
bool	is_hide (const atermpp::aterm &x)
bool	is_rename (const atermpp::aterm &x)
bool	is_comm (const atermpp::aterm &x)
bool	is_allow (const atermpp::aterm &x)
bool	is_sync (const atermpp::aterm &x)
bool	is_at (const atermpp::aterm &x)
bool	is_seq (const atermpp::aterm &x)
bool	is_if_then (const atermpp::aterm &x)
bool	is_if_then_else (const atermpp::aterm &x)
bool	is_bounded_init (const atermpp::aterm &x)
bool	is_merge (const atermpp::aterm &x)
bool	is_left_merge (const atermpp::aterm &x)
bool	is_choice (const atermpp::aterm &x)
bool	is_stochastic_operator (const atermpp::aterm &x)
bool	is_untyped_process_assignment (const atermpp::aterm &x)
bool	is_process_expression (const atermpp::aterm &x)
std::string	pp (const process_expression &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const process_expression &x)
void	swap (process_expression &t1, process_expression &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_action (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const action &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const action &x)
void	swap (action &t1, action &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_process_instance (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const process_instance &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const process_instance &x)
void	swap (process_instance &t1, process_instance &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_process_instance_assignment (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const process_instance_assignment &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const process_instance_assignment &x)
void	swap (process_instance_assignment &t1, process_instance_assignment &t2) noexcept
	\brief swap overload
std::string	pp (const delta &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const delta &x)
void	swap (delta &t1, delta &t2) noexcept
	\brief swap overload
std::string	pp (const tau &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const tau &x)
void	swap (tau &t1, tau &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_sum (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const sum &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const sum &x)
void	swap (sum &t1, sum &t2) noexcept
	\brief swap overload
std::string	pp (const block &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const block &x)
void	swap (block &t1, block &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_hide (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const hide &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const hide &x)
void	swap (hide &t1, hide &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_rename (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const rename &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const rename &x)
void	swap (rename &t1, rename &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_comm (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const comm &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const comm &x)
void	swap (comm &t1, comm &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_allow (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const allow &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const allow &x)
void	swap (allow &t1, allow &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_sync (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const sync &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const sync &x)
void	swap (sync &t1, sync &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_at (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const at &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const at &x)
void	swap (at &t1, at &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_seq (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const seq &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const seq &x)
void	swap (seq &t1, seq &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_if_then (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const if_then &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const if_then &x)
void	swap (if_then &t1, if_then &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_if_then_else (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const if_then_else &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const if_then_else &x)
void	swap (if_then_else &t1, if_then_else &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_bounded_init (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const bounded_init &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const bounded_init &x)
void	swap (bounded_init &t1, bounded_init &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_merge (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const merge &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const merge &x)
void	swap (merge &t1, merge &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_left_merge (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const left_merge &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const left_merge &x)
void	swap (left_merge &t1, left_merge &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_choice (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const choice &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const choice &x)
void	swap (choice &t1, choice &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_stochastic_operator (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const stochastic_operator &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const stochastic_operator &x)
void	swap (stochastic_operator &t1, stochastic_operator &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_untyped_process_assignment (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const untyped_process_assignment &x, bool precedence_aware=true)
std::ostream &	operator<< (std::ostream &out, const untyped_process_assignment &x)
void	swap (untyped_process_assignment &t1, untyped_process_assignment &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_block (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const process_expression_list &x, bool precedence_aware=true)
std::string	pp (const process_expression_vector &x, bool precedence_aware=true)
std::set< data::sort_expression >	find_sort_expressions (const process::process_expression &x)
std::string	pp (const action_list &x, bool precedence_aware=true)
std::string	pp (const action_vector &x, bool precedence_aware=true)
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.
bool	operator< (const action &a1, const action &a2)
std::string	pp (const process::action_label_list &x, bool arg0)
std::string	pp (const process::action_label_vector &x, bool arg0)
std::string	pp (const process::process_identifier_list &x, bool arg0)
std::string	pp (const process::process_identifier_vector &x, bool arg0)
std::string	pp (const process::process_equation_list &x, bool arg0)
std::string	pp (const process::process_equation_vector &x, bool arg0)
std::string	pp (const process::action_label &x, bool arg0)
std::string	pp (const process::action_name_multiset &x, bool arg0)
std::string	pp (const process::communication_expression &x, bool arg0)
std::string	pp (const process::process_equation &x, bool arg0)
std::string	pp (const process::process_identifier &x, bool arg0)
std::string	pp (const process::process_specification &x, bool arg0)
std::string	pp (const process::rename_expression &x, bool arg0)
std::string	pp (const process::untyped_multi_action &x, bool arg0)
process::action_label_list	normalize_sorts (const process::action_label_list &x, const data::sort_specification &sortspec)
void	normalize_sorts (process::process_equation_vector &x, const data::sort_specification &sortspec)
void	normalize_sorts (process::process_specification &x, const data::sort_specification &)
void	translate_user_notation (process::process_specification &x)
std::set< data::sort_expression >	find_sort_expressions (const process::action_label_list &x)
std::set< data::sort_expression >	find_sort_expressions (const process::process_equation_vector &x)
std::set< data::sort_expression >	find_sort_expressions (const process::process_specification &x)
std::set< data::variable >	find_free_variables (const process::process_specification &x)
std::set< core::identifier_string >	find_identifiers (const process::process_specification &x)
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_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)
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	translate_user_notation (T &x)
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	translate_user_notation (const T &x)
void	remove_duplicate_equations (process_specification &procspec)
	Removes duplicate equations from a process specification, using a bisimulation algorithm.
template<class... ARGUMENTS>
void	make_action_label (atermpp::aterm &t, const ARGUMENTS &... args)
bool	is_action_label (const atermpp::aterm &x)
std::ostream &	operator<< (std::ostream &out, const action_label &x)
void	swap (action_label &t1, action_label &t2) noexcept
	\brief swap overload
bool	operator< (const action_label &a1, const action_label &a2)
	Total ordering on action labels: name first (string order), then sorts.
bool	is_action_name_multiset (const atermpp::aterm &x)
std::ostream &	operator<< (std::ostream &out, const action_name_multiset &x)
void	swap (action_name_multiset &t1, action_name_multiset &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_action_name_multiset (atermpp::aterm &t, const ARGUMENTS &... args)
action_name_set	action_names (const process_expression &x, const std::vector< process_equation > &equations)
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_efficient (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	anonymize (process_specification &procspec)
template<class... ARGUMENTS>
void	make_communication_expression (atermpp::aterm &t, const ARGUMENTS &... args)
bool	is_communication_expression (const atermpp::aterm &x)
std::ostream &	operator<< (std::ostream &out, const communication_expression &x)
void	swap (communication_expression &t1, communication_expression &t2) noexcept
	\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	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)
	Writes all variables that occur in an object to an output iterator.
template<typename T >
std::set< data::variable >	find_all_variables (const T &x)
	Returns all variables that occur in an object.
template<typename T , typename OutputIterator >
void	find_free_variables (const T &x, OutputIterator o)
	Writes all free variables that occur in an object to an output iterator.
template<typename T , typename OutputIterator , typename VariableContainer >
void	find_free_variables_with_bound (const T &x, OutputIterator o, const VariableContainer &bound)
	Writes all free variables that occur in an object to an output iterator.
template<typename T >
std::set< data::variable >	find_free_variables (const T &x)
	Returns all free variables that occur in an object.
template<typename T , typename VariableContainer >
std::set< data::variable >	find_free_variables_with_bound (const T &x, VariableContainer const &bound)
	Returns all free variables that occur in an object.
template<typename T , typename OutputIterator >
void	find_identifiers (const T &x, OutputIterator o)
	Writes all identifiers that occur in an object to an output iterator.
template<typename T >
std::set< core::identifier_string >	find_identifiers (const T &x)
	Returns all identifiers that occur in an object.
template<typename T , typename OutputIterator >
void	find_sort_expressions (const T &x, OutputIterator o)
	Writes all sort expressions that occur in an object to an output iterator.
template<typename T >
std::set< data::sort_expression >	find_sort_expressions (const T &x)
	Returns all sort expressions that occur in an object.
template<typename T , typename OutputIterator >
void	find_function_symbols (const T &x, OutputIterator o)
	Writes all function symbols that occur in an object to an output iterator.
template<typename T >
std::set< data::function_symbol >	find_function_symbols (const T &x)
	Returns all function symbols that occur in an object.
template<typename T , typename OutputIterator >
void	find_action_labels (const T &x, OutputIterator o)
	Writes all action labels that occur in an object to an output iterator.
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).
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.
bool	includes (const multi_action_name &x, const multi_action_name &y)
bool	contains (const multi_action_name &alpha, const core::identifier_string &a)
bool	has_empty_intersection (const multi_action_name &x, const multi_action_name &y)
multi_action_name	multiset_difference (const multi_action_name &alpha, const multi_action_name &beta)
multi_action_name	multiset_union (multi_action_name alpha, multi_action_name beta)
std::string	pp (const multi_action_name &x)
	Pretty print function for a multi action name.
multi_action_name_set	make_name_set (const action_name_multiset_list &v)
action_name_multiset_list	make_multiset_list (const multi_action_name_set &A)
bool	contains (const multi_action_name_set &A, const multi_action_name &a)
bool	subset_includes (const multi_action_name_set &A, const multi_action_name &x)
bool	includes (const multi_action_name_set &A, const multi_action_name &y)
multi_action_name_set	set_difference (const multi_action_name_set &A1, const multi_action_name_set &A2)
multi_action_name_set	set_union (const multi_action_name_set &A1, const multi_action_name_set &A2)
multi_action_name_set	set_intersection (const multi_action_name_set &A1, const multi_action_name_set &A2)
multi_action_name_set	remove_subsets (const multi_action_name_set &A)
std::set< core::identifier_string >	action_names (const multi_action_name_set &A)
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 > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	normalize_sorts (T &x, const data::sort_specification &sortspec)
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	normalize_sorts (const T &x, const data::sort_specification &sortspec)
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, bool precedence_aware=true)
	Returns a string representation of the object x.
template<class... ARGUMENTS>
void	make_process_equation (atermpp::aterm &t, const ARGUMENTS &... args)
bool	is_process_equation (const atermpp::aterm &x)
std::ostream &	operator<< (std::ostream &out, const process_equation &x)
void	swap (process_equation &t1, process_equation &t2) noexcept
	\brief swap overload
std::string	pp (const process_equation_list &x)
std::string	pp (const process_equation_vector &x)
template<class... ARGUMENTS>
void	make_process_identifier (atermpp::aterm &t, const ARGUMENTS &... args)
bool	is_process_identifier (const atermpp::aterm &x)
std::ostream &	operator<< (std::ostream &out, const process_identifier &x)
void	swap (process_identifier &t1, process_identifier &t2) noexcept
	\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)
atermpp::aterm	process_specification_to_aterm (const process_specification &spec)
	Conversion to aterm.
void	complete_data_specification (process_specification &spec)
	Adds all sorts that appear in the process specification spec to the data specification of spec.
bool	is_process_specification (const atermpp::aterm &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.
template<class... ARGUMENTS>
void	make_rename_expression (atermpp::aterm &t, const ARGUMENTS &... args)
bool	is_rename_expression (const atermpp::aterm &x)
std::ostream &	operator<< (std::ostream &out, const rename_expression &x)
void	swap (rename_expression &t1, rename_expression &t2) noexcept
	\brief swap overload
template<typename T , typename Substitution > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_sort_expressions (T &x, const Substitution &sigma, bool innermost)
template<typename T , typename Substitution > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_sort_expressions (const T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_data_expressions (T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_data_expressions (const T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_all_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_all_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_free_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_free_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution, typename VariableContainer > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_free_variables (T &x, const Substitution &sigma, const VariableContainer &bound_variables)
template<typename T , data::IsSubstitution Substitution, typename VariableContainer > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_free_variables (const T &x, const Substitution &sigma, const VariableContainer &bound_variables)
template<typename T , typename Substitution > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_process_identifiers (T &x, const Substitution &sigma)
template<typename T , typename Substitution > requires (std::is_base_of_v<atermpp::aterm, T>)
T	replace_process_identifiers (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding (T &x, Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma)
template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding_with_an_identifier_generator (T &x, Substitution &sigma, IdentifierGenerator &id_generator)
template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding_with_an_identifier_generator (const T &x, Substitution &sigma, IdentifierGenerator &id_generator)
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 > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	rewrite (T &x, Rewriter R)
template<typename T , typename Rewriter > requires std::is_base_of_v<atermpp::aterm, T>
T	rewrite (const T &x, Rewriter R)
template<typename T , typename Rewriter , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	rewrite (T &x, Rewriter R, const Substitution &sigma)
template<typename T , typename Rewriter , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	rewrite (const T &x, Rewriter R, const Substitution &sigma)
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)
std::set< data::sort_expression_list >	sorts_list_difference (const std::set< data::sort_expression_list > &sorts1, const std::set< data::sort_expression_list > &sorts2)
std::string	pp (const std::set< data::sort_expression_list > &ll)
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 &t, const ARGUMENTS &... args)
bool	is_untyped_multi_action (const atermpp::aterm &x)
std::ostream &	operator<< (std::ostream &out, const untyped_multi_action &x)
void	swap (untyped_multi_action &t1, untyped_multi_action &t2) noexcept
	\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

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

\brief list of action_labels

Definition at line 74 of file action_label.h.

action_label_vector

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

\brief vector of action_labels

Definition at line 77 of file action_label.h.

action_list

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

\brief list of actions

Definition at line 185 of file process_expression.h.

action_name_multiset_list

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

\brief list of action_name_multisets

Definition at line 61 of file action_name_multiset.h.

action_name_multiset_vector

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

\brief vector of action_name_multisets

Definition at line 64 of file action_name_multiset.h.

action_name_set

using mcrl2::process::action_name_set = typedef std::set<core::identifier_string>

Definition at line 27 of file action_names.h.

action_vector

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

\brief vector of actions

Definition at line 188 of file process_expression.h.

communication_expression_list

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

\brief list of communication_expressions

Definition at line 74 of file communication_expression.h.

communication_expression_vector

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

\brief vector of communication_expressions

Definition at line 77 of file communication_expression.h.

multi_action_name_set

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

Represents a set of multi action names.

Definition at line 47 of file multi_action_name.h.

process_equation_list

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

\brief list of process_equations

Definition at line 74 of file process_equation.h.

process_equation_vector

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

\brief vector of process_equations

Definition at line 77 of file process_equation.h.

process_expression_list

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

\brief list of process_expressions

Definition at line 57 of file process_expression.h.

process_expression_vector

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

\brief vector of process_expressions

Definition at line 60 of file process_expression.h.

process_identifier_list

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

\brief list of process_identifiers

Definition at line 79 of file process_identifier.h.

process_identifier_vector

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

\brief vector of process_identifiers

Definition at line 82 of file process_identifier.h.

rename_expression_list

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

\brief list of rename_expressions

Definition at line 75 of file rename_expression.h.

rename_expression_vector

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

\brief vector of rename_expressions

Definition at line 78 of file rename_expression.h.

untyped_multi_action_list

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

\brief list of untyped_multi_actions

Definition at line 64 of file untyped_multi_action.h.

untyped_multi_action_vector

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

\brief vector of untyped_multi_actions

Definition at line 67 of file untyped_multi_action.h.

Function Documentation

action_names() [1/2]

std::set< core::identifier_string > mcrl2::process::action_names ( const multi_action_name_set &  A )

inline

Definition at line 199 of file multi_action_name.h.

action_names() [2/2]

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

inline

Definition at line 300 of file action_names.h.

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_efficient()

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

inline

Definition at line 125 of file alphabet_efficient.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 126 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 82 of file process.cpp.

anonymize()

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

inline

Definition at line 165 of file anonymize.h.

balance_summands() [1/2]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::process::balance_summands

(

const T &

x

)

Reduces the nesting depth of the choice operator.

Definition at line 64 of file balance_nesting_depth.h.

balance_summands() [2/2]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::balance_summands

(

T &

x

)

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 206 of file process_specification.h.

contains() [1/2]

bool mcrl2::process::contains ( const multi_action_name &  alpha, const core::identifier_string &  a  )

inline

Definition at line 59 of file multi_action_name.h.

contains() [2/2]

bool mcrl2::process::contains ( const multi_action_name_set &  A, const multi_action_name &  a  )

inline

Definition at line 145 of file multi_action_name.h.

contains_tau()

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

inline

Definition at line 33 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 281 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 141 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 1807 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 85 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 75 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 271 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
	)

Writes all action labels that occur in an object to an output iterator.

Parameters

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

Definition at line 262 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 282 of file find.h.

find_all_variables() [1/3]

std::set< data::variable > mcrl2::process::find_all_variables

(

const action &

x

)

Definition at line 76 of file process.cpp.

find_all_variables() [2/3]

template<typename T >

std::set< data::variable > mcrl2::process::find_all_variables

(

const T &

x

)

Returns all variables that occur in an object.

Parameters

[in]

x

an object containing variables

Returns

All variables that occur in the object x

Definition at line 148 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
	)

Writes all variables that occur in an object to an output iterator.

Parameters

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

Definition at line 139 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 294 of file find.h.

find_free_variables() [1/4]

std::set< data::variable > mcrl2::process::find_free_variables

(

const action &

x

)

Definition at line 77 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 78 of file process.cpp.

find_free_variables() [3/4]

template<typename T >

std::set< data::variable > mcrl2::process::find_free_variables

(

const T &

x

)

Returns all free variables that occur in an object.

Parameters

[in]

x

an object containing variables

Returns

All free variables that occur in the object x

Definition at line 178 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
	)

Writes all free variables that occur in an object to an output iterator.

Parameters

[in]	x	an object containing variables
[in,out]	o	an output iterator to which all variables occurring in x are added.

Definition at line 159 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
	)

Writes all free variables that occur in an object to an output iterator.

Parameters

[in]	x	an object containing variables
[in,out]	o	an output iterator to which all variables occurring in x are written.
[in]	bound	a container of variables

Definition at line 169 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
	)

Returns all free variables that occur in an object.

Parameters

[in]	x	an object containing variables
[in]	bound	a container of variables

Returns

All free variables that occur in the object x

Definition at line 190 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

)

Returns all function symbols that occur in an object.

Parameters

[in]

x

an object containing function symbols

Returns

All function symbols that occur in the object x

Definition at line 250 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
	)

Writes all function symbols that occur in an object to an output iterator.

Parameters

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

Definition at line 241 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 79 of file process.cpp.

find_identifiers() [2/3]

template<typename T >

std::set< core::identifier_string > mcrl2::process::find_identifiers

(

const T &

x

)

Returns all identifiers that occur in an object.

Parameters

[in]

x

an object containing identifiers

Returns

All identifiers that occur in the object x

Definition at line 210 of file find.h.

find_identifiers() [3/3]

template<typename T , typename OutputIterator >

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

Writes all identifiers that occur in an object to an output iterator.

Parameters

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

Definition at line 201 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 72 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 73 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 74 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 75 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

)

Returns all sort expressions that occur in an object.

Parameters

[in]

x

an object containing sort expressions

Returns

All sort expressions that occur in the object x

Definition at line 230 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
	)

Writes all sort expressions that occur in an object to an output iterator.

Parameters

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

Definition at line 221 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 345 of file replace_subterm.h.

has_empty_intersection()

bool mcrl2::process::has_empty_intersection ( const multi_action_name &  x, const multi_action_name &  y  )

inline

Definition at line 64 of file multi_action_name.h.

includes() [1/2]

bool mcrl2::process::includes ( const multi_action_name &  x, const multi_action_name &  y  )

inline

Definition at line 54 of file multi_action_name.h.

includes() [2/2]

bool mcrl2::process::includes ( const multi_action_name_set &  A, const multi_action_name &  y  )

inline

Definition at line 158 of file multi_action_name.h.

is_action()

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

inline

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

Definition at line 194 of file process_expression.h.

is_action_label()

bool mcrl2::process::is_action_label ( const atermpp::aterm &  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 83 of file action_label.h.

is_action_name_multiset()

bool mcrl2::process::is_action_name_multiset ( const atermpp::aterm &  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 70 of file action_name_multiset.h.

is_allow()

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

inline

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

Definition at line 902 of file process_expression.h.

is_at()

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

inline

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

Definition at line 1054 of file process_expression.h.

is_block()

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

inline

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

Definition at line 598 of file process_expression.h.

is_bounded_init()

bool mcrl2::process::is_bounded_init ( const atermpp::aterm &  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 1363 of file process_expression.h.

is_choice()

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

inline

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

Definition at line 1591 of file process_expression.h.

is_comm()

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

inline

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

Definition at line 826 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 112 of file is_communicating_lpe.h.

is_communication_expression()

bool mcrl2::process::is_communication_expression ( const atermpp::aterm &  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 83 of file communication_expression.h.

is_delta()

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

inline

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

Definition at line 399 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 96 of file is_guarded.h.

is_hide()

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

inline

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

Definition at line 674 of file process_expression.h.

is_if_then()

bool mcrl2::process::is_if_then ( const atermpp::aterm &  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 1206 of file process_expression.h.

is_if_then_else()

bool mcrl2::process::is_if_then_else ( const atermpp::aterm &  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 1287 of file process_expression.h.

is_left_associative() [1/7]

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

inline

Definition at line 52 of file print.h.

is_left_associative() [2/7]

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

inline

Definition at line 49 of file print.h.

is_left_associative() [3/7]

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

inline

Definition at line 51 of file print.h.

is_left_associative() [4/7]

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

inline

Definition at line 50 of file print.h.

is_left_associative() [5/7]

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

inline

Definition at line 55 of file print.h.

is_left_associative() [6/7]

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

inline

Definition at line 53 of file print.h.

is_left_associative() [7/7]

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

inline

Definition at line 54 of file print.h.

is_left_merge()

bool mcrl2::process::is_left_merge ( const atermpp::aterm &  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 1515 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 379 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 389 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 344 of file is_linear.h.

is_merge()

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

inline

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

Definition at line 1439 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 42 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 27 of file utility.h.

is_process_equation()

bool mcrl2::process::is_process_equation ( const atermpp::aterm &  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 83 of file process_equation.h.

is_process_expression()

bool mcrl2::process::is_process_expression ( const atermpp::aterm &  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 90 of file process_expression.h.

is_process_identifier()

bool mcrl2::process::is_process_identifier ( const atermpp::aterm &  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 88 of file process_identifier.h.

is_process_instance()

bool mcrl2::process::is_process_instance ( const atermpp::aterm &  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 270 of file process_expression.h.

is_process_instance_assignment()

bool mcrl2::process::is_process_instance_assignment ( const atermpp::aterm &  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 346 of file process_expression.h.

is_process_specification()

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

inline

Test for a process specification expression.

Parameters

x

A term

Returns

True if x is a process specification expression

Definition at line 41 of file process_specification.h.

is_rename()

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

inline

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

Definition at line 750 of file process_expression.h.

is_rename_expression()

bool mcrl2::process::is_rename_expression ( const atermpp::aterm &  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 84 of file rename_expression.h.

is_right_associative() [1/7]

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

inline

Definition at line 70 of file print.h.

is_right_associative() [2/7]

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

inline

Definition at line 67 of file print.h.

is_right_associative() [3/7]

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

inline

Definition at line 69 of file print.h.

is_right_associative() [4/7]

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

inline

Definition at line 68 of file print.h.

is_right_associative() [5/7]

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

inline

Definition at line 73 of file print.h.

is_right_associative() [6/7]

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

inline

Definition at line 71 of file print.h.

is_right_associative() [7/7]

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

inline

Definition at line 72 of file print.h.

is_seq()

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

inline

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

Definition at line 1130 of file process_expression.h.

is_stochastic_operator()

bool mcrl2::process::is_stochastic_operator ( const atermpp::aterm &  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 1672 of file process_expression.h.

is_sum()

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

inline

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

Definition at line 528 of file process_expression.h.

is_sync()

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

inline

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

Definition at line 978 of file process_expression.h.

is_tau()

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

inline

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

Definition at line 452 of file process_expression.h.

is_untyped_multi_action()

bool mcrl2::process::is_untyped_multi_action ( const atermpp::aterm &  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 73 of file untyped_multi_action.h.

is_untyped_process_assignment()

bool mcrl2::process::is_untyped_process_assignment ( const atermpp::aterm &  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 1753 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 22 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 44 of file join.h.

make_action()

template<class... ARGUMENTS>

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

inline

\brief The function make_action constructs a new term into a given address. \

Parameters

t	The reference into which the new action is constructed.

Definition at line 179 of file process_expression.h.

make_action_label()

template<class... ARGUMENTS>

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

inline

\brief The function 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 68 of file action_label.h.

make_action_name_multiset()

template<class... ARGUMENTS>

void mcrl2::process::make_action_name_multiset ( atermpp::aterm &  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 98 of file action_name_multiset.h.

make_allow() [1/2]

template<class... ARGUMENTS>

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

inline

\brief The function make_allow constructs a new term into a given address. \

Parameters

t	The reference into which the new allow is constructed.

Definition at line 893 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 70 of file utility.h.

make_at()

template<class... ARGUMENTS>

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

inline

\brief The function make_at constructs a new term into a given address. \

Parameters

t	The reference into which the new at is constructed.

Definition at line 1045 of file process_expression.h.

make_block() [1/2]

template<class... ARGUMENTS>

void mcrl2::process::make_block ( atermpp::aterm &  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 1781 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 118 of file utility.h.

make_bounded_init()

template<class... ARGUMENTS>

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

inline

\brief The function 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 1354 of file process_expression.h.

make_choice()

template<class... ARGUMENTS>

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

inline

\brief The function make_choice constructs a new term into a given address. \

Parameters

t	The reference into which the new choice is constructed.

Definition at line 1582 of file process_expression.h.

make_comm() [1/2]

template<class... ARGUMENTS>

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

inline

\brief The function make_comm constructs a new term into a given address. \

Parameters

t	The reference into which the new comm is constructed.

Definition at line 817 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 92 of file utility.h.

make_communication_expression()

template<class... ARGUMENTS>

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

inline

\brief The function 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 68 of file communication_expression.h.

make_hide() [1/2]

template<class... ARGUMENTS>

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

inline

\brief The function make_hide constructs a new term into a given address. \

Parameters

t	The reference into which the new hide is constructed.

Definition at line 665 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 105 of file utility.h.

make_if_then()

template<class... ARGUMENTS>

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

inline

\brief The function 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 1197 of file process_expression.h.

make_if_then_else()

template<class... ARGUMENTS>

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

inline

\brief The function 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 1278 of file process_expression.h.

make_left_merge() [1/2]

template<class... ARGUMENTS>

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

inline

\brief The function 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 1506 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 60 of file utility.h.

make_merge() [1/2]

template<class... ARGUMENTS>

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

inline

\brief The function make_merge constructs a new term into a given address. \

Parameters

t	The reference into which the new merge is constructed.

Definition at line 1430 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 50 of file utility.h.

make_multiset_list()

action_name_multiset_list mcrl2::process::make_multiset_list ( const multi_action_name_set &  A )

inline

Definition at line 134 of file multi_action_name.h.

make_name_set()

multi_action_name_set mcrl2::process::make_name_set ( const action_name_multiset_list &  v )

inline

Definition at line 123 of file multi_action_name.h.

make_process_equation()

template<class... ARGUMENTS>

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

inline

\brief The function 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 68 of file process_equation.h.

make_process_identifier()

template<class... ARGUMENTS>

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

inline

\brief The function 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 73 of file process_identifier.h.

make_process_instance()

template<class... ARGUMENTS>

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

inline

\brief The function 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 261 of file process_expression.h.

make_process_instance_assignment()

template<class... ARGUMENTS>

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

inline

\brief The function 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 337 of file process_expression.h.

make_rename()

template<class... ARGUMENTS>

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

inline

\brief The function make_rename constructs a new term into a given address. \

Parameters

t	The reference into which the new rename is constructed.

Definition at line 741 of file process_expression.h.

make_rename_expression()

template<class... ARGUMENTS>

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

inline

\brief The function 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 69 of file rename_expression.h.

make_seq()

template<class... ARGUMENTS>

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

inline

\brief The function make_seq constructs a new term into a given address. \

Parameters

t	The reference into which the new seq is constructed.

Definition at line 1121 of file process_expression.h.

make_stochastic_operator()

template<class... ARGUMENTS>

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

inline

\brief The function 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 1663 of file process_expression.h.

make_sum()

template<class... ARGUMENTS>

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

inline

\brief The function make_sum constructs a new term into a given address. \

Parameters

t	The reference into which the new sum is constructed.

Definition at line 519 of file process_expression.h.

make_sync() [1/2]

template<class... ARGUMENTS>

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

inline

\brief The function make_sync constructs a new term into a given address. \

Parameters

t	The reference into which the new sync is constructed.

Definition at line 969 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 40 of file utility.h.

make_untyped_multi_action()

template<class... ARGUMENTS>

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

inline

\brief The function 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 58 of file untyped_multi_action.h.

make_untyped_process_assignment()

template<class... ARGUMENTS>

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

inline

\brief The function 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 1744 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 21 of file merge_action_specifications.h.

multiset_difference()

multi_action_name mcrl2::process::multiset_difference ( const multi_action_name &  alpha, const multi_action_name &  beta  )

inline

Definition at line 70 of file multi_action_name.h.

multiset_union()

multi_action_name mcrl2::process::multiset_union ( multi_action_name  alpha, multi_action_name  beta  )

inline

Definition at line 82 of file multi_action_name.h.

normalize_sorts() [1/7]

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

Definition at line 65 of file process.cpp.

normalize_sorts() [2/7]

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

Definition at line 66 of file process.cpp.

normalize_sorts() [3/7]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

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

Definition at line 31 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 67 of file process.cpp.

normalize_sorts() [5/7]

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

Definition at line 68 of file process.cpp.

normalize_sorts() [6/7]

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

normalize_sorts() [7/7]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

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

Definition at line 23 of file normalize_sorts.h.

operator!=()

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

inline

Inequality operator.

Definition at line 236 of file process_specification.h.

operator<() [1/2]

bool mcrl2::process::operator< ( const action &  a1, const action &  a2  )

inline

Total ordering on actions: label first, then arguments. Consistent with the ordering on action labels (name, then sorts). Including arguments makes this a proper total order.

Note that the sort order must be consistent with that on action labels, e.g. for efficient application of process operators such as allow and comm.

Definition at line 1832 of file process_expression.h.

operator<() [2/2]

bool mcrl2::process::operator< ( const action_label &  a1, const action_label &  a2  )

inline

Total ordering on action labels: name first (string order), then sorts.

Definition at line 126 of file action_label.h.

operator<<() [1/34]

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 207 of file process_expression.h.

operator<<() [2/34]

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 96 of file action_label.h.

operator<<() [3/34]

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 83 of file action_name_multiset.h.

operator<<() [4/34]

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 915 of file process_expression.h.

operator<<() [5/34]

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

inline

Definition at line 149 of file allow_set.h.

operator<<() [6/34]

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 1067 of file process_expression.h.

operator<<() [7/34]

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 611 of file process_expression.h.

operator<<() [8/34]

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 1376 of file process_expression.h.

operator<<() [9/34]

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 1604 of file process_expression.h.

operator<<() [10/34]

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 839 of file process_expression.h.

operator<<() [11/34]

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 96 of file communication_expression.h.

operator<<() [12/34]

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 412 of file process_expression.h.

operator<<() [13/34]

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 687 of file process_expression.h.

operator<<() [14/34]

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 1219 of file process_expression.h.

operator<<() [15/34]

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 1300 of file process_expression.h.

operator<<() [16/34]

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 1528 of file process_expression.h.

operator<<() [17/34]

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 1452 of file process_expression.h.

operator<<() [18/34]

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

inline

Definition at line 210 of file multi_action_name.h.

operator<<() [19/34]

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

inline

Definition at line 234 of file multi_action_name.h.

operator<<() [20/34]

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 96 of file process_equation.h.

operator<<() [21/34]

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 125 of file process_expression.h.

operator<<() [22/34]

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 101 of file process_identifier.h.

operator<<() [23/34]

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 283 of file process_expression.h.

operator<<() [24/34]

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 359 of file process_expression.h.

operator<<() [25/34]

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 196 of file process_specification.h.

operator<<() [26/34]

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 763 of file process_expression.h.

operator<<() [27/34]

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 97 of file rename_expression.h.

operator<<() [28/34]

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 1143 of file process_expression.h.

operator<<() [29/34]

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 1685 of file process_expression.h.

operator<<() [30/34]

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 541 of file process_expression.h.

operator<<() [31/34]

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 991 of file process_expression.h.

operator<<() [32/34]

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 465 of file process_expression.h.

operator<<() [33/34]

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 86 of file untyped_multi_action.h.

operator<<() [34/34]

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 1766 of file process_expression.h.

operator==()

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

inline

Equality operator.

Definition at line 229 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 110 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 88 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 104 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 116 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 129 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 63 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 55 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 42 of file parse.h.

pp() [1/49]

std::string mcrl2::process::pp	(	const action &	x,
		bool	precedence_aware = true
	)

Definition at line 34 of file process.cpp.

pp() [2/49]

std::string mcrl2::process::pp	(	const action_list &	x,
		bool	precedence_aware = true
	)

Definition at line 24 of file process.cpp.

pp() [3/49]

std::string mcrl2::process::pp	(	const action_vector &	x,
		bool	precedence_aware = true
	)

Definition at line 25 of file process.cpp.

pp() [4/49]

std::string mcrl2::process::pp	(	const allow &	x,
		bool	precedence_aware = true
	)

Definition at line 37 of file process.cpp.

pp() [5/49]

std::string mcrl2::process::pp	(	const at &	x,
		bool	precedence_aware = true
	)

Definition at line 38 of file process.cpp.

pp() [6/49]

std::string mcrl2::process::pp	(	const block &	x,
		bool	precedence_aware = true
	)

Definition at line 39 of file process.cpp.

pp() [7/49]

std::string mcrl2::process::pp	(	const bounded_init &	x,
		bool	precedence_aware = true
	)

Definition at line 40 of file process.cpp.

pp() [8/49]

std::string mcrl2::process::pp	(	const choice &	x,
		bool	precedence_aware = true
	)

Definition at line 41 of file process.cpp.

pp() [9/49]

std::string mcrl2::process::pp	(	const comm &	x,
		bool	precedence_aware = true
	)

Definition at line 42 of file process.cpp.

pp() [10/49]

std::string mcrl2::process::pp	(	const delta &	x,
		bool	precedence_aware = true
	)

Definition at line 44 of file process.cpp.

pp() [11/49]

std::string mcrl2::process::pp	(	const hide &	x,
		bool	precedence_aware = true
	)

Definition at line 45 of file process.cpp.

pp() [12/49]

std::string mcrl2::process::pp	(	const if_then &	x,
		bool	precedence_aware = true
	)

Definition at line 46 of file process.cpp.

pp() [13/49]

std::string mcrl2::process::pp	(	const if_then_else &	x,
		bool	precedence_aware = true
	)

Definition at line 47 of file process.cpp.

pp() [14/49]

std::string mcrl2::process::pp	(	const left_merge &	x,
		bool	precedence_aware = true
	)

Definition at line 48 of file process.cpp.

pp() [15/49]

std::string mcrl2::process::pp	(	const merge &	x,
		bool	precedence_aware = true
	)

Definition at line 49 of file process.cpp.

pp() [16/49]

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

inline

Pretty print function for a multi action name.

Definition at line 98 of file multi_action_name.h.

pp() [17/49]

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 217 of file multi_action_name.h.

pp() [18/49]

std::string mcrl2::process::pp	(	const process::action_label &	x,
		bool	arg0 = true
	)

Definition at line 35 of file process.cpp.

pp() [19/49]

std::string mcrl2::process::pp	(	const process::action_label_list &	x,
		bool	arg0 = true
	)

Definition at line 26 of file process.cpp.

pp() [20/49]

std::string mcrl2::process::pp	(	const process::action_label_vector &	x,
		bool	arg0 = true
	)

Definition at line 27 of file process.cpp.

pp() [21/49]

std::string mcrl2::process::pp	(	const process::action_name_multiset &	x,
		bool	arg0 = true
	)

Definition at line 36 of file process.cpp.

pp() [22/49]

std::string mcrl2::process::pp	(	const process::communication_expression &	x,
		bool	arg0 = true
	)

Definition at line 43 of file process.cpp.

pp() [23/49]

std::string mcrl2::process::pp	(	const process::process_equation &	x,
		bool	arg0 = true
	)

Definition at line 50 of file process.cpp.

pp() [24/49]

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

Definition at line 32 of file process.cpp.

pp() [25/49]

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

Definition at line 33 of file process.cpp.

pp() [26/49]

std::string mcrl2::process::pp	(	const process::process_identifier &	x,
		bool	arg0 = true
	)

Definition at line 52 of file process.cpp.

pp() [27/49]

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

Definition at line 28 of file process.cpp.

pp() [28/49]

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

Definition at line 29 of file process.cpp.

pp() [29/49]

std::string mcrl2::process::pp	(	const process::process_specification &	x,
		bool	arg0 = true
	)

Definition at line 55 of file process.cpp.

pp() [30/49]

std::string mcrl2::process::pp	(	const process::rename_expression &	x,
		bool	arg0 = true
	)

Definition at line 57 of file process.cpp.

pp() [31/49]

std::string mcrl2::process::pp	(	const process::untyped_multi_action &	x,
		bool	arg0 = true
	)

Definition at line 63 of file process.cpp.

pp() [32/49]

std::string mcrl2::process::pp

(

const process_equation_list &

x

)

pp() [33/49]

std::string mcrl2::process::pp

(

const process_equation_vector &

x

)

pp() [34/49]

std::string mcrl2::process::pp	(	const process_expression &	x,
		bool	precedence_aware = true
	)

Definition at line 51 of file process.cpp.

pp() [35/49]

std::string mcrl2::process::pp	(	const process_expression_list &	x,
		bool	precedence_aware = true
	)

Definition at line 30 of file process.cpp.

pp() [36/49]

std::string mcrl2::process::pp	(	const process_expression_vector &	x,
		bool	precedence_aware = true
	)

Definition at line 31 of file process.cpp.

pp() [37/49]

std::string mcrl2::process::pp

(

const process_identifier_list &

x

)

pp() [38/49]

std::string mcrl2::process::pp

(

const process_identifier_vector &

x

)

pp() [39/49]

std::string mcrl2::process::pp	(	const process_instance &	x,
		bool	precedence_aware = true
	)

Definition at line 53 of file process.cpp.

pp() [40/49]

std::string mcrl2::process::pp	(	const process_instance_assignment &	x,
		bool	precedence_aware = true
	)

Definition at line 54 of file process.cpp.

pp() [41/49]

std::string mcrl2::process::pp	(	const rename &	x,
		bool	precedence_aware = true
	)

Definition at line 56 of file process.cpp.

pp() [42/49]

std::string mcrl2::process::pp	(	const seq &	x,
		bool	precedence_aware = true
	)

Definition at line 58 of file process.cpp.

pp() [43/49]

std::string mcrl2::process::pp ( const std::set< data::sort_expression_list > &  ll )

inline

Definition at line 50 of file typecheck.h.

pp() [44/49]

std::string mcrl2::process::pp	(	const stochastic_operator &	x,
		bool	precedence_aware = true
	)

Definition at line 59 of file process.cpp.

pp() [45/49]

std::string mcrl2::process::pp	(	const sum &	x,
		bool	precedence_aware = true
	)

Definition at line 60 of file process.cpp.

pp() [46/49]

std::string mcrl2::process::pp	(	const sync &	x,
		bool	precedence_aware = true
	)

Definition at line 61 of file process.cpp.

pp() [47/49]

template<typename T >

std::string mcrl2::process::pp	(	const T &	x,
		bool	precedence_aware = true
	)

Returns a string representation of the object x.

Definition at line 488 of file print.h.

pp() [48/49]

std::string mcrl2::process::pp	(	const tau &	x,
		bool	precedence_aware = true
	)

Definition at line 62 of file process.cpp.

pp() [49/49]

std::string mcrl2::process::pp	(	const untyped_process_assignment &	x,
		bool	precedence_aware = true
	)

Definition at line 64 of file process.cpp.

precedence() [1/12]

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

inlineconstexpr

Definition at line 30 of file print.h.

precedence() [2/12]

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

inlineconstexpr

Definition at line 28 of file print.h.

precedence() [3/12]

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

inlineconstexpr

Definition at line 21 of file print.h.

precedence() [4/12]

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

inlineconstexpr

Definition at line 26 of file print.h.

precedence() [5/12]

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

inlineconstexpr

Definition at line 27 of file print.h.

precedence() [6/12]

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

inlineconstexpr

Definition at line 25 of file print.h.

precedence() [7/12]

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

inlineconstexpr

Definition at line 24 of file print.h.

precedence() [8/12]

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

inline

Definition at line 32 of file print.h.

precedence() [9/12]

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

inlineconstexpr

Definition at line 29 of file print.h.

precedence() [10/12]

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

inlineconstexpr

Definition at line 23 of file print.h.

precedence() [11/12]

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

inlineconstexpr

Definition at line 22 of file print.h.

precedence() [12/12]

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

inlineconstexpr

Definition at line 31 of file print.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 133 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 142 of file eliminate_trivial_equations.h.

process_specification_to_aterm()

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

inline

Conversion to aterm.

Returns

The specification converted to aterm format.

Parameters

spec	A process specification

Definition at line 216 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 288 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 296 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 700 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_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 195 of file remove_equations.h.

remove_subsets()

multi_action_name_set mcrl2::process::remove_subsets ( const multi_action_name_set &  A )

inline

Definition at line 185 of file multi_action_name.h.

replace_all_variables() [1/2]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::process::replace_all_variables	(	const T &	x,
		const Substitution &	sigma
	)

Definition at line 98 of file replace.h.

replace_all_variables() [2/2]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::replace_all_variables	(	T &	x,
		const Substitution &	sigma
	)

Definition at line 89 of file replace.h.

replace_data_expressions() [1/2]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::process::replace_data_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 55 of file replace.h.

replace_data_expressions() [2/2]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::replace_data_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 45 of file replace.h.

replace_free_variables() [1/4]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::process::replace_free_variables	(	const T &	x,
		const Substitution &	sigma
	)

\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 123 of file replace.h.

replace_free_variables() [2/4]

template<typename T , data::IsSubstitution Substitution, typename VariableContainer >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::process::replace_free_variables	(	const T &	x,
		const Substitution &	sigma,
		const VariableContainer &	bound_variables
	)

\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 150 of file replace.h.

replace_free_variables() [3/4]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::replace_free_variables	(	T &	x,
		const Substitution &	sigma
	)

\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 111 of file replace.h.

replace_free_variables() [4/4]

template<typename T , data::IsSubstitution Substitution, typename VariableContainer >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::replace_free_variables	(	T &	x,
		const Substitution &	sigma,
		const VariableContainer &	bound_variables
	)

\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 137 of file replace.h.

replace_process_identifiers() [1/2]

template<typename T , typename Substitution >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::process::replace_process_identifiers	(	const T &	x,
		const Substitution &	sigma
	)

Definition at line 195 of file replace.h.

replace_process_identifiers() [2/2]

template<typename T , typename Substitution >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::replace_process_identifiers	(	T &	x,
		const Substitution &	sigma
	)

Definition at line 187 of file replace.h.

replace_sort_expressions() [1/2]

template<typename T , typename Substitution >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::process::replace_sort_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 33 of file replace.h.

replace_sort_expressions() [2/2]

template<typename T , typename Substitution >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::replace_sort_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 23 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 326 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 336 of file replace_subterm.h.

replace_variables() [1/2]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::process::replace_variables	(	const T &	x,
		const Substitution &	sigma
	)

Definition at line 77 of file replace.h.

replace_variables() [2/2]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::replace_variables	(	T &	x,
		const Substitution &	sigma
	)

Definition at line 68 of file replace.h.

replace_variables_capture_avoiding() [1/4]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::process::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma
	)

\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 161 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [2/4]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::process::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator
	)

\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 127 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [3/4]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma
	)

\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 143 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [4/4]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator
	)

\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 112 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::process::replace_variables_capture_avoiding_with_an_identifier_generator	(	const T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator
	)

\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 187 of file replace_capture_avoiding_with_an_identifier_generator.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::replace_variables_capture_avoiding_with_an_identifier_generator	(	T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator
	)

\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 168 of file replace_capture_avoiding_with_an_identifier_generator.h.

rewrite() [1/4]

template<typename T , typename Rewriter >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::process::rewrite	(	const T &	x,
		Rewriter	R
	)

\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 39 of file rewrite.h.

rewrite() [2/4]

template<typename T , typename Rewriter , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::process::rewrite	(	const T &	x,
		Rewriter	R,
		const Substitution &	sigma
	)

\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 69 of file rewrite.h.

rewrite() [3/4]

template<typename T , typename Rewriter >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::rewrite	(	T &	x,
		Rewriter	R
	)

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

Definition at line 26 of file rewrite.h.

rewrite() [4/4]

template<typename T , typename Rewriter , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::rewrite	(	T &	x,
		Rewriter	R,
		const Substitution &	sigma
	)

\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 54 of file rewrite.h.

set_difference()

multi_action_name_set mcrl2::process::set_difference ( const multi_action_name_set &  A1, const multi_action_name_set &  A2  )

inline

Definition at line 163 of file multi_action_name.h.

set_intersection()

multi_action_name_set mcrl2::process::set_intersection ( const multi_action_name_set &  A1, const multi_action_name_set &  A2  )

inline

Definition at line 177 of file multi_action_name.h.

set_union()

multi_action_name_set mcrl2::process::set_union ( const multi_action_name_set &  A1, const multi_action_name_set &  A2  )

inline

Definition at line 170 of file multi_action_name.h.

sorts_list_difference()

std::set< data::sort_expression_list > mcrl2::process::sorts_list_difference ( const std::set< data::sort_expression_list > &  sorts1, const std::set< data::sort_expression_list > &  sorts2  )

inline

Definition at line 41 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 27 of file join.h.

subset_includes()

bool mcrl2::process::subset_includes ( const multi_action_name_set &  A, const multi_action_name &  x  )

inline

Definition at line 151 of file multi_action_name.h.

swap() [1/30]

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

inlinenoexcept

\brief swap overload

Definition at line 213 of file process_expression.h.

swap() [2/30]

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

inlinenoexcept

\brief swap overload

Definition at line 102 of file action_label.h.

swap() [3/30]

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

inlinenoexcept

\brief swap overload

Definition at line 89 of file action_name_multiset.h.

swap() [4/30]

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

inlinenoexcept

\brief swap overload

Definition at line 921 of file process_expression.h.

swap() [5/30]

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

inlinenoexcept

\brief swap overload

Definition at line 1073 of file process_expression.h.

swap() [6/30]

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

inlinenoexcept

\brief swap overload

Definition at line 617 of file process_expression.h.

swap() [7/30]

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

inlinenoexcept

\brief swap overload

Definition at line 1382 of file process_expression.h.

swap() [8/30]

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

inlinenoexcept

\brief swap overload

Definition at line 1610 of file process_expression.h.

swap() [9/30]

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

inlinenoexcept

\brief swap overload

Definition at line 845 of file process_expression.h.

swap() [10/30]

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

inlinenoexcept

\brief swap overload

Definition at line 102 of file communication_expression.h.

swap() [11/30]

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

inlinenoexcept

\brief swap overload

Definition at line 418 of file process_expression.h.

swap() [12/30]

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

inlinenoexcept

\brief swap overload

Definition at line 693 of file process_expression.h.

swap() [13/30]

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

inlinenoexcept

\brief swap overload

Definition at line 1225 of file process_expression.h.

swap() [14/30]

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

inlinenoexcept

\brief swap overload

Definition at line 1306 of file process_expression.h.

swap() [15/30]

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

inlinenoexcept

\brief swap overload

Definition at line 1534 of file process_expression.h.

swap() [16/30]

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

inlinenoexcept

\brief swap overload

Definition at line 1458 of file process_expression.h.

swap() [17/30]

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

inlinenoexcept

\brief swap overload

Definition at line 102 of file process_equation.h.

swap() [18/30]

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

inlinenoexcept

\brief swap overload

Definition at line 131 of file process_expression.h.

swap() [19/30]

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

inlinenoexcept

\brief swap overload

Definition at line 107 of file process_identifier.h.

swap() [20/30]

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

inlinenoexcept

\brief swap overload

Definition at line 289 of file process_expression.h.

swap() [21/30]

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

inlinenoexcept

\brief swap overload

Definition at line 365 of file process_expression.h.

swap() [22/30]

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

inlinenoexcept

\brief swap overload

Definition at line 769 of file process_expression.h.

swap() [23/30]

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

inlinenoexcept

\brief swap overload

Definition at line 103 of file rename_expression.h.

swap() [24/30]

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

inlinenoexcept

\brief swap overload

Definition at line 1149 of file process_expression.h.

swap() [25/30]

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

inlinenoexcept

\brief swap overload

Definition at line 1691 of file process_expression.h.

swap() [26/30]

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

inlinenoexcept

\brief swap overload

Definition at line 547 of file process_expression.h.

swap() [27/30]

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

inlinenoexcept

\brief swap overload

Definition at line 997 of file process_expression.h.

swap() [28/30]

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

inlinenoexcept

\brief swap overload

Definition at line 471 of file process_expression.h.

swap() [29/30]

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

inlinenoexcept

\brief swap overload

Definition at line 92 of file untyped_multi_action.h.

swap() [30/30]

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

inlinenoexcept

\brief swap overload

Definition at line 1772 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 58 of file is_multi_action.h.

translate_user_notation() [1/5]

process::action mcrl2::process::translate_user_notation

(

const action &

x

)

Definition at line 69 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 70 of file process.cpp.

translate_user_notation() [3/5]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::process::translate_user_notation

(

const T &

x

)

Definition at line 30 of file translate_user_notation.h.

translate_user_notation() [4/5]

void mcrl2::process::translate_user_notation

(

process::process_specification &

x

)

Definition at line 71 of file process.cpp.

translate_user_notation() [5/5]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::process::translate_user_notation

(

T &

x

)

Definition at line 23 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 25 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 748 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 733 of file typecheck.h.