Go to the first, previous, next, last section, table of contents.


3.2.12 Processes

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.



NuSMV <nusmv@irst.itc.it>