The CSP₀ language can be seen as an “assembly language” for the CSP process algebra. It does not contain any of the high-level functional programming constructs that CSP<sub>M</sub> has. Instead, it’s intended that higher-level, more “useful” CSP languages (such as CSP<sub>M</sub>) will be compiled into CSP₀.
There is limited support for recursion in CSP₀, via finalized processes. A process must be declared with a process statement, but the process isn’t finalized until after it has been defined with an operator statement. Many process parameters require a finalized process, which don’t allow recursion. However, some process parameters work with processes that have been declared but not yet defined. The most notable of these parameters is the prefix statement; the underlying rule is that a process parameter only needs to be finalized we need to know its initials and afters set in order to define the operator’s semantics.
Identifiers must begin with a letter, underscore, or dollar sign. The remaining characters must be letters, numbers, periods, or underscores. Those that begin with a dollar sign must contain at least one more character — ‘$’ on its own is not a valid identifier.
The intention is that higher-level languages shouldn’t allow identifiers beginning with $; instead, these identifiers are available for the compiler that translates the higher-level language into CSP₀ in case it needs to create any temporary processes as part of the compilation process.
event ‹id›;Declares a new event. An event must be declared before it can be used in any process definition. It is illegal to declare an event more than once.
process ‹id›;Declares a new process. A process must be declared before it can be defined with an operator statement. It is illegal to declare a process more than once.
There are two predefined events (τ and ✓) and predefined processes (STOP and SKIP). The STOP process cannot perform any events whatsover. The SKIP process can perform a ✓, after which it behaves like STOP. The events are not directly accessible in a CSP₀ script. τ events are created automatically by certain CSP operators, while ✓ is only available via the SKIP process. Just like any other process, it’s illegal to try to redefine STOP or SKIP.
{ ‹e1›, ‹e2›... }An alphabet is a set of events (possibly empty), separated by commas, and surrounded by curly braces. It isn’t illegal for an event to appear in the alphabet more than once, but this has no effect.
{ ‹P1›, ‹P2›... }A process set is a set of process names (possibly empty), separated by commas, and surrounded by curly braces. It isn’t illegal for a process to appear in the set more than once, but this has no effect.
[[ ‹d1› -> ‹r1›, ‹d2› -> ‹r2›... ]]An event map is a set of event pairs. The events in each pair are separated by a right-arrow. The pairs in the list are separated by commas. The overall map is surrounded by double square brackets. As with alphabets, an event pair is allowed to appear in the map more than once, but this has no effect.
For detailed descriptions of the CSP operators, please see [1].
prefix ‹P› = ‹e› -> ‹Q›;Creates a prefix process. ‹P› can perform an ‹e› event, after which it behaves like ‹Q›. ‹P› must not be finalized. ‹Q› can either be finalized or not.
extchoice ‹P› = ‹Q› [] ‹R›;Creates an external choice process. ‹P› presents the environment with the choice of acting like ‹Q› or ‹R›. ‹P› must not be finalized. ‹Q› and ‹R› must both be finalized.
intchoice ‹P› = ‹Q› |~| ‹R›;Creates an internal choice process. ‹P› nondeterministically chooses whether to behave like ‹Q› or ‹R›. At least one of the subprocesses will be available, but the other might be refused. ‹P› must not be finalized. ‹Q› and ‹R› can either be finalized or not.
timeout ‹P› = ‹Q› [> ‹R›;Creates a timeout process. ‹P› behaves like ‹Q› initially, but at any point in the future (nondeterministically), it can start to refuse ‹Q› and behave like ‹R› instead. ‹P› must not be finalized. ‹Q› must be finalized. ‹R› can either be finalized or not.
seqcomp ‹P› = ‹Q› ; ‹R›;Creates a sequential composition process. ‹P› behaves like ‹Q› until a ✓ occurs (signaling termination), after which it behaves like ‹R›. ‹P› must not be finalized. ‹Q› must be finalized. ‹R› can either be finalized or not.
interleave ‹P› = ‹Q› ||| ‹R›;Creates an interleave process. ‹P› behaves like ‹Q› and ‹R› simultaneously. The events of ‹Q› and ‹R› can occur in any order. ‹P› cannot terminate until both ‹Q› and ‹R› have terminated. ‹P› must not be finalized. ‹Q› and ‹R› must both be finalized.
aparallel ‹P› = ‹Q› [| ‹α› |] ‹R›;Creates an alphabetized parallel process. ‹P› behaves like ‹Q› and ‹R› simultaneously; however, for all of the events in ‹α›, ‹Q› and ‹R› must both be able to perform the event for ‹P› to be able to perform it. ‹P› cannot terminate until both ‹Q› and ‹R› have terminated. ‹P› must not be finalized. ‹Q› and ‹R› must both be finalized.
iparallel ‹P› = ‹Q› [ ‹αQ› || ‹αR› ] ‹R›;Creates an interface parallel process. ‹P› behaves like ‹Q› and ‹R› simultaneously; however, for all of the events in the intersection of ‹αQ› and ‹αR›, ‹Q› and ‹R› must both be able to perform the event for ‹P› to be able to perform it. ‹P› cannot terminate until both ‹Q› and ‹R› have terminated. ‹P› must not be finalized. ‹Q› and ‹R› must both be finalized.
hide ‹P› = ‹Q› \ ‹α›;Creates a hiding process. ‹P› behaves like ‹Q›, but with all of the events in ‹α› hidden, and replaced with τs (which are invisible to the environment). ‹P› must not be finalized. ‹Q› must be finalized.
rename ‹P› = ‹Q› [[ ‹μ› ]];Creates a renaming process. ‹P› behaves like ‹Q›, but with all of the events renamed occording to ‹μ›. If one of ‹Q›’s events appears in the map’s domain, it is replaced with the events that it is mapped to. ‹P› must not be finalized. ‹Q› must be finalized.
rextchoice ‹P› = [] { ‹φ› };Creates a replicated external choice process. ‹P› presents the environment with the choice of acting like any of the processes in ‹φ›. ‹P› must not be finalized. Each process in ‹φ› must be finalized.
rintchoice ‹P› = |~| { ‹φ› };Creates a replicated internal choice process. ‹P› will nondeterministically choose to act like any of the processes in ‹φ›. ‹P› must not be finalized. Each process in ‹φ› can either be finalized or not. The set ‹φ› must not be empty.