The Use of Model Transformation in the INESS Project - Formal Methods for Components and Objects - page 171

act enter : N × Packet ;

leave : N × Packet ;

The sending of a packet from an input buffer to an output buffer is described
by means of the send action. Similarly, for the receipt of a packet by an out-
put buffer, the action recv is used. To synchronize actions, mCRL2 provides
synchronous communication between processes, if all the action data parame-
ters in the synchronizing actions have the same value. To show (and observe)
that a send and receive synchronize, we use the action comm , which reflects the
successful synchronization of a send and a recv .
The actions send , recv and comm are each modeled with three data param-
eters. The first parameter is used to denote the identity of the input buffer
that sends the package, the second parameter denotes the identity of the output
buffer that receives the package, and the last parameter denotes the packet that
is actually being transferred. The first and second parameter provide handles
to observe the routing of packets; i.e., they are used to express and verify re-
quirements later on. The last data parameter is required to transfer and observe
the data flow between buffers. Note that the second parameter is a cosmetic
addition, as its can also be obtained from the data of the packet itself.

act send : N × N × Packet ;

recv : N × N × Packet ;

N × N ×

comm : Packet ;

In the Simplified Switch case study, the packet exchange between an input buffer,
say i , and an output buffer, say o , not only depends on the behavior expressed
in the processes, but also on the contents of the other input buffer. In mCRL2,
it is possible to use multi-party communication to establish the involvement of
another process. This means that we require actions that reveal information
about a third party in the communication. We introduce actions grant and free
for this purpose. Both grant ( i, j, p )and free ( i, j, p ) denote that input buffer i is
granted permission to send a packet p to output buffer j . One of these actions is
used for establishing priority and the other one for simultaneous packet transfer.
A more detailed explanation is provided later in this section.

act grant : N × N × Packet ;

free : N × N × Packet ;

3.4 The Output Buffers with Capacity cap

In mCRL2, a FIFO buffer Output with capacity cap is given by the following
process specification:

proc Output ( i : N ,c : List ( Packet )) =

→ s : N # c< cap recv ( s, i, p ) · Output ( i, p c )

p : Packet

+ c ≈ [] → leave ( i, rhead ( c )) · Output ( i, rtail ( c ));