Go to the first, previous, next, last section, table of contents.
Processes are used to model interleaving concurrency. A process
is a module which is instantiated using the keyword `process'
(see section 3.2.1 State Variables). The program executes a step by
non-deterministically choosing a process, then executing all of the
assignment statements in that process in parallel. It is implicit that
if a given variable is not assigned by the process, then its value
remains unchanged. Each instance of a process has a special boolean
variable associated with it called running
.
The value of this variable is 1
if and only if the process
instance is currently selected for execution.
A process may run only when its parent is running. In addition no two
processes with the same parents may be running at the same time.