# 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{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