FSP stands for Finite State Processes. This appendix contains a comprehensive specification of the syntax of FSP together with a commentary on features such as variable scope that are not treated explicitly in the body of the book. A formal description of the semantics of the FSP process operators may be found in Appendix C.
In specifying the syntax of FSP, we have followed the approach used in the Java Language Specification. In particular, the syntax is specified using a context-free grammar that consists of a number of productions. Each production is defined by a non-terminal symbol as its left-hand side and a sequence of one or more terminal and non-terminal symbols as its right-hand side. In the following, non-terminal symbols are shown in italic type and terminal symbols in a fixed width bolded type. The definition of a non-terminal is introduced by its name followed by a colon. One or more alternative right-hand sides for the non-terminal then follow on succeeding lines. For example, the following production specifies the syntax for an FSP constant definition.
The production below specifies an argument list as consisting of either a single expression or a list of expressions separated by commas:
The subscripted suffix "opt", which may appear after a terminal or non-terminal, indicates an optional symbol.
In addition to definitions ...