Synchronous Operator

Syntax

communications “|” communications

Semantics

communication1 | communication2

Both communication1 and communication2 are execute at the same time.
These communications can only occur when both have a set of matching processes to communicate with.

Examples

The statement

ChannelId1 ? x | ChannelId2 ? y

desribe the process that at the same time

  • communicates variable x over ChannelId1 and

  • communicates variable y over ChannelId2

For this, both communications must, of course, be possible.

The statement

CreateAccount ? account | CreateUser ? id ? pw1 ? pw2 [[ (id(account) == id) /\ (pw(account) == pw1) /\ (pw(account) == pw2) ]]
desribe the process that at the same time creates an account using a data type and by the triplet of id, password, and confirm password.
Thus the synchronous operator is used to link the different levels of abstraction.