Formal Theory of Basic COSY

A basic COSY path program is a collection of paths in program and endprogram parentheses. A path is an expression, similar to a regular expression (see Appendix B.3), built from event names, semicolons, commas, conventional parentheses and Kleene stars, enclosed by path and end parentheses. For instance:$${{\Pr }_{1}} = \left\{ \begin{gathered} {\text{ }}\underline {program} \hfill \\ P(1):\underline {path} {\text{ }}a;b;c{\text{ }}\underline {end} \hfill \\ P(2):\underline {path} {\text{ }}(d;e)*;b{\text{ }}\underline {end} \hfill \\ {\text{ }}\underline {endprogram} \hfill \\ \end{gathered} \right.{\text{ }}$$In every expression as described above, the semicolon specifies sequential occurrences of the events named or subexpressions, and comma specifies a mutually exclusive occurrence of one of the events named or subexpressions. The comma binds more strongly than the semicolon, so that the expression “a;b, c” means “first event a must occur, after which exclusively either event b or event c must occur”. An expression may be enclosed in conventional parentheses with Kleene star appended, as for instance “(d, e)*” which means that the enclosed specification applies zero or more times. In other words, an expression between path and end may be understood as an ordinary regular expression. The only difference is that “∪” is replaced by “,”, concatenation is replaced by “;”, and mutually exclusive choice binds more strongly than concatenation1. Thus for instance “a; b, c” is equivalent to “a(b ∪ c)” in the traditional notation for regular expressions. Moreover, by definition, the parentheses path and end correspond to “(” and “)*” respectively, so that a single path specifies repeated (or cyclic) sequences of event occurrences.