Process Descriptions

By convention, we use upper case for Processes, and lower case for events, 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).