A component specified by possible CSP events and successor behaviours. has no transitions. CSP prefixing, CSP choice and CSP parallel composition construct larger components.
Behave as until it performs a visible CSP event in , then switch to . The triggering event is included in the visible CSP trace.
Allow to proceed while is ready to interrupt. The first visible CSP event of discards and leaves the derivative of . A CSP internal action of alone does not discard .
Relabel visible CSP events according to a function or relation, preserving CSP internal actions. An injective relabelling preserves event identity; a non-injective one can merge distinct actions. In relational renaming, an original event with no image is disabled. Thus partial relational renaming can also restrict an interface.
Events in require both CSP processes; other visible CSP events advance one participant independently. CSP internal actions do not synchronize.
The alphabets assigned to participants determine their shared CSP events. An event in both assigned alphabets requires both participants; one assigned only to a single participant advances that participant. Replicated composition synchronizes all participants whose assigned alphabets contain the event.
The process may internally choose either branch, independently of the environment's offered CSP events. Consequently it can have more CSP stable failures than the corresponding CSP external choice, despite having the same CSP traces.
The first visible CSP event resolves the choice; the environment can select an event offered by only one branch. CSP internal actions can advance a branch without selecting it.
An unobservable transition that the environment cannot block. CSP hiding turns selected visible CSP events into CSP internal actions.
A state with no outgoing CSP internal action. A CSP stable failure records a refusal only after such a state has been reached.
Articles by others on the same topic
There are currently no matching articles.