Join definitions reflect the key idea behind the join-calculus. They define channels, bind them to names and define the receptors on channels.
|
The channels defined and bound are the set of lowercase-ident in channel-decl above. Channel names cannot be repeated inside the join-pattern of a given reaction, but can appear in several reaction in a reactions. A reaction define both a synchronization behavior as its join-pattern and a receptor as its process. More precisely, when messages are present on all the channels of a given reaction and that their values match the corresponding formal arguments ocaml-pattern above, then the reaction is active and the guarded process may be executed. A reactions is a list of competing reaction, as suggested by the keyword or. Implementation offers the limited guarantee that if exactly one reaction in a list of competing reactions is active, then the execution of its guarded process starts. If several reactions are active at the same time, then one of them is selected, which one being left unspecified purposely.
For example, the construct
| def | ident1 (patt1) | = | process1 |
| or | ident1 (patt1) & ident2 (patt2) | = | process2 |
| in | process |
defines two channels (ident1 and ident2) locally to process. These channels are defined by two join patterns. The first join patter n matches when there is a message on the channel ident1 and that the content of the message matches the pattern patt1. The second join pattern matches when there is a message on both channels and the content of each message matches its pattern. When a message is sent to the channel ident1, if one of the two join pattern matches, its associated process is executed. If the two join patterns match, one of the two process is executed.
The scope of the channel names defined by join-definition extends to all receptors (process in reaction). In other words, channel definitions are recursive by default. There may be several sets of competing behaviors (several reactions) in a join-definition, separated by the keyword and. Then, the set of channel names defined by the various reactions must be pairwise disjoint.
Moreover, in a reaction join-pattern = process, the scope of the variables inside the formal arguments (ocaml-pattern in channel-decl) extends to process. Those are bound by following the usual rules of the pattern matching of Objective Caml. All such variables must be pairwise distinct in a given join-pattern.
A reaction join-pattern = process defines a channel ident to be synchronous when reply … to ident occurs inside process. The reply construct can be seen as an asynchronous message sending on some implicit “continuation” channel. The scope of this continuation channel does not extend over def join definition that occur inside process above. If another reaction defines the channel ident in the set of competing behaviors reactions, then ident must also be defined as synchronous there.