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_specificationprocess_equationprocess_identifierrename_expressioncommunication_expressionaction_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:
| 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¶
| 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¶
| 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 |
