By convention, we use upper case for Processes, and lower case for
events,
-
A process is some expression involving events and operators.
-
For example, a process (say GAME) describing a computer game might have an
alphabet: <#910#>InCoin, OutCome<#910#>.
-
Its (top level) behaviour might then be expressed as:
GAME = (InCoin #tex2html_wrap_inline3886# OutCome #tex2html_wrap_inline3888# GAME)
-
Note that a process can be recursive - this is how we describe
repetitive behaviour in CSP.
To describe behaviour that can vary (a bit more interesting) we use
the choice operator:
CLEVERERGAME = (InCoinLarge #tex2html_wrap_inline3890# OutCome #tex2html_wrap_inline3892# OutCome
#tex2html_wrap_inline3894# InCoin #tex2html_wrap_inline3896# OutCome) #tex2html_wrap_inline3898# CLEVERERGAME
(Assuming InCoinLarge is part of the alphabet of CLEVERERGAME).
-
Mutual recursion is also allowed.
-
There is a special process called STOP. It stops.
-
There is another special set of processes called
CHAOS. It is indistinguishable from any other process with the
same alphabet, but doesn't stop (i.e. its traces satisfies no
specification). CHAOS can generate all
possible traces for a given alphabet (it takes an alphabet as its
argument).