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

init ∂ {send,recv} ( Γ {send|recv→comm} (
Input (0 , []) Input (1 , []) Output (0 , []) Output (1 , [])));

To acquire the simultaneous packet transfer and prioritized packet transfer, the
model needs to be adapted in two ways. The first step takes care of the prioritized
packet transfer if packets route to the same destination. The second step takes
care of the required simultaneous packet transfer to different output buffers.

Prioritized packet transfer. The way in which we deal with the prioritized packet
transfer is as follows. The input buffer signals which transfers are allowed for
execution by the other input buffer by means of the grant -action. If a buffer is
empty it grants permission for any transfer in the other process of the input
queue. If the buffer is not empty it only grants permission for a transferral of
packets from each input buffer with a lower identity to the same output buffer.

proc Input ( i : ,c : List ( Packet )) =

# c< cap

N

→ enter ( i, p ) · Input ( i, p c )

p : Packet

+ c ≈ [] → send ( i, dest ( rhead ( c )) , rhead ( c )) · Input ( i, rtail ( c ));

→
n,m : N

+ c ≈ [] grant ( n, m, p ) · Input ( i, c )

→ n : N

p : Packet

+ c ≈ [] n<i → grant ( n, dest ( rhead ( c )) , rhead ( c )) · Input ( i, c )

To ensure that the grant -action synchronizes with the other corresponding send -
and recv -actions another communication function is added:

init ∂ {send,recv ,grant} ( Γ {send|recv→comm} ( Γ {send |recv |grant→comm} (
Input (0 , []) Input (1 , []) Output (0 , []) Output (1 , []))));

The nesting of the communication functions this way is necessary to ensure that
priority is given.

Maximal communication. In order to meet the second requirement, the input
buffer announces that it allows a simultaneous transferral of packets (from the
other input buffer) with a different destination via the free -action.

proc Input ( i : ,c : List ( Packet )) =

# c<cap

N

→ enter ( i, p ) · Input ( i, p c )

p : Packet

→ n : N

+ c

≈ n ≈ i ∧

dest ( p )

≈

dest ( rhead ( c ))

→

[]

p : Packet

send ( i, dest ( rhead ( c )) , rhead ( c )) | free ( n, dest ( p ) ,p ) · Input ( i, rtail ( c ))

+ c ≈ [] → send ( i, dest ( rhead ( c )) , rhead ( c )) · Input ( i, rtail ( c ))

→
n,m : N

+ c ≈ [] grant ( n, m, p ) · Input ( i, c )

→ n : N

p : Packet

+ c ≈ [] n<i → grant ( n, dest ( rhead ( c )) , rhead ( c )) · Input ( i, c );