Communications

Syntax

communications

communication (”|” communication)* (Condition)?

communication

channelName (“!” valExpr | “?” varDecl )*

channelName

CapsId

Semantics

Specify communication.
The direction of communication is NOT specified.
Zero or more data can be communicated.
The list of data types of the provided data must match
the list of data types as specified in the channel definition.
The operator ! denotes that the data item is fully specified: a known value is communicated.
The operator ? denotes that the data item is underspecified: (part of) the value that is communicated is unknown.
The predefined channel EXIT must be used to communicate process termination.
Communication over the predefined channel EXIT might include exit values.

Examples

Communication without data

Let Channel be a channel over which can be communicated without any data.
The statement
Channel

specifies that the process wants to communicate.

Besides channels that communicate without any data,
this construct can also be used to obtain simpler models by abstracting away the actual data that is communicated.

Communication of fully specified data

Let Channel_Int be a channel over which one integer at a time can be communicated.
The statement
Channel_Int ! 3
specifies that the process wants to communicate the integer value 3.
Note The same statement can be used to both send and receive the Integer value 3.

The statement

Channel_Int ! id
specifies that the process wants to communicate the integer value of variable id .
Note No new variable is introduced for id.

Communication of underspecified data

Let Channel_Int be a channel over which one integer at a time can be communicated.
The statement
Channel_Int ? x
specifies that the process wants to communicate an integer value.
After communication, the value will be stored in the newly introduced variable x.
Note The same statement can be used to both send and receive the underspecified variable x.

The actual communication might be

Channel_Int ! 3
Channel_Int ! -3

or

Channel_Int ! -12345678901234567890

Communication of constrained data

Let Channel_Int be a channel over which one integer at a time can be communicated.
The statement
Channel ? x [[ x >= 0 ]]
specifies that the process wants to communicate a constrained integer value.
The integer value is constrained to be larger than or equal to zero.
The value is stored in the newly introduced variable x.

The actual communication might be

Channel ! 3

but NOT a negative value like

Channel ! -3

Communication of multiple data items

Let Channel_Int_List be a channel over which one integer and one list at a time can be communicated.
The statement
Channel_Int_List ! id ? list [[ isCstr_Int(list) ]]

specifies that the process wants to communicate the following two data: the value of the variable id and a non-empty list.