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 expressions

Process expressions are defined using the following grammar

$\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}$

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:

Table 81 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

Table 82 Selected algorithms on processes
algorithm	description
alphabet_reduce	Applies alphabet reduction to a process specification
eliminate_trivial_equations	Eliminates trivial equations, that have a process instance as the right hand side
eliminate_unused_equations	Eliminates equations that are not reachable from the initial state
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

Table 83 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