Parallel Operator


processBehaviour “|||” processBehaviour


process1 ||| process2

The processes 1 and 2 run independently in parallel.
No synchronization between the processes is required.
Of course, the processes might communicate with each other.

When both processes have exited then parallel composition exits


The statement

ChannelId1 ? x ||| ChannelId2 ? y

describes the process that can, in any order, do the following two things:

  • Communicate variable x over ChannelId1

  • Communicate variable y over ChannelId2

The process ends when both communications have occurred.

In other words, the following three behaviours can be observed:

First 1 then 2

ChannelId1 ? x >-> ChannelId2 ? y

First 2 then 1

ChannelId2 ? y >-> ChannelId1 ? x


ChannelId1 ? x | ChannelId2 ? y