Introduction

The Process library contains classes and algorithms for general processes. The code in the Process library is contained in the namespace process.

The following C++ classes are defined for the Process Library:

• process_specification

• process_equation

• process_identifier

• rename_expression

• communication_expression

• action_name_multiset

Process expressions

Process expressions are defined using the following grammar

\[\begin{split}\begin{array}{lrl} p & ::= & a(e_1, \ldots, e_n) \: \mid \: P(e_1, \ldots, e_n) \: \mid \: P(d_1 = e_1, \ldots, d_n = e_n) \: \mid \: \delta \: \mid \: \tau \: \mid \: \sum\limits_{d_1:D_1, \ldots, d_n:D_n}p \\ & ~ & \: \mid \: \partial _{B}(p) \: \mid \: \tau _{I}(p) \: \mid \: \rho _{R}(p) \: \mid \: \Gamma _{C}(p) \: \mid \: \bigtriangledown _{V}(p) \: \mid \: p\ |\ p \: \mid \: p^{@}t \: \mid \: p\cdot p \\ & ~ & \: \mid \: c\rightarrow p \: \mid \: c\rightarrow p\diamond p \: \mid \: p << p \: \mid \: p\ ||\ p \: \mid \: p\ ||\_\ p \: \mid \: p + p, \end{array}\end{split}\]

where \(a(e_1, \ldots, e_n)\) is an action, \(d_i\) is a variable of sort \(D_i\), \(e_i\) is a data expression, \(B\) and \(I\) are lists of strings, \(R\) is a list of rename expressions, \(C\) is a list of communication expressions, \(V\) is a list of action name multi sets, \(t\) is a data expression of sort Real, and \(c\) is a data expression of sort Bool.

The following C++ classes are defined for process expressions:

process expression classes

Expression	C++ class
\(a(e_1, \ldots, e_n)\)	action
\(P(e_1, \ldots, e_n)\)	process_instance
\(P(d_1 = e_1, \ldots, d_n = e_n)\)	process_instance_assignment
\(\delta\)	delta
\(\tau\)	tau
\(\sum\limits_{d:D}p\)	sum
\(\partial _{B}(p)\)	block
\(\tau _{B}(p)\)	hide
\(\rho _{R}(p)\)	rename
\(\Gamma _{C}(p)\)	comm
\(\bigtriangledown _{V}(p)\)	allow
\(p\ |\ p\)	sync
\(p^{@}t\)	at
\(p\cdot p\)	seq
\(c\rightarrow p\)	if_then
\(c\rightarrow p\diamond p\)	if_then_else
\(p << p\)	bounded_init
\(p\ ||\ p\)	merge
\(p\ ||\_\ p\)	left_merge
\(p + p\)	choice

Algorithms on processes

Selected algorithms on processes

algorithm	description
alphabet_reduce	Applies alphabet reduction to a process specification
eliminate_single_usage_equations	Eliminates equations that are used only once, using substitution
eliminate_trivial_equations	Eliminates trivial equations, that have a process instance as the right hand side
eliminate_trivial_sums	Eliminates trivial equations, that have a sum of process instances as the right hand side
is_guarded	Checks if a process expression is guarded
is_linear	Determines if a process specification is linear
normalize_sorts	Applies sort normalization to a process data type
remove_duplicate_equations	Removes duplicate equations from a process specification, using a bisimulation algorithm
rewrite	Applies a rewriter to a process data type
translate_user_notation	Applies translation of user notation to a process data type

Search and Replace functions

Search and Replace functions

algorithm	description
find_identifiers	Finds all identifiers occurring in a process data type
find_sort_expressions	Finds all sort expressions occurring in a process data type
find_function_symbols	Finds all function symbols occurring in a process data type
find_all_variables	Finds all variables occurring in a process data type
find_free_variables	Finds all free variables occurring in a process data type
replace_sort_expressions	Replaces sort expressions in a process data type
replace_data_expressions	Replaces data expressions in a process data type
replace_variables	Replaces variables in a process data
replace_variables_capture_avoiding	Replaces variables in a process data type, and avoids unwanted capturing
replace_free_variables	Replaces free variables in a process data type
replace_all_variables	Replaces all variables in a process data type, even in declarations