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.
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.
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.