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 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` |

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 |

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 |