Information Technology Reference
In-Depth Information
By adapting the communications in the outermost communication operator to
{
we achieve that packet transfers are only allowed in
case the other input buffer grants permission. This way simultaneous packet
transfers are achieved whenever possible. All possible communications are now
permitted by either a
grant
-ora
free
-action.
send
|
recv
|
free
→
comm
}
init
∂
{send,recv ,grant,free}
(
Γ
{send|recv |grant→comm}
(
Γ
{send|recv |free→comm}
(
Input
(0
,
[])
Input
(1
,
[])
Output
(0
,
[])
Output
(1
,
[]))));
The order in which the communication operators are applied to the parallel
composition of the buffers is of no importance. It is not allowed to declare both
communication operators by means of one communication operator since the left-
hand sides of the communication patterns share an action, which might lead to a
non-unique solution. For that reason the communication operators are placed in
a hierarchial composition. We conjecture that the order of these communication
operators is of no importance. To provide (partial) evidence, we have validated
this claim, by using the mCRL2 tool set to establish that the respective labelled
transition systems are strongly bisimilar (even isomorphic) for the case that the
capacity of the buffers is 1, 2 and 3.
4 Specification of the Original 2
×
2Switch
The Original Switch is an extension of the Simplified Switch. The Original switch
contains an additional counter, that counts interesting packets that are trans-
ferred from input to output buffers. A packet is considered interesting if its
second, third, and fourth bit are all 0. The counter is restricted. Therefore the
value can only be incremented by one per clock cycle. So when both input buffers
are capable of transferring interesting packets, priority is given to the transferral
of packets from input buffer 0 and the transferral of packets from input buffer
1 is delayed. Thus, we may only transfer packets simultaneously if they are not
both interesting. In all other cases a process needs to either take or grant priority
as in the Simplified Switch case study.
In this section, we adapt the model of the Simplified Switch to obtain a model
that corresponds to the design intent of the Original Switch. Thereto, we need
to extend a part of the data specification and adapt the behaviors of the buffer
processes slightly.
4.1
Packets
The fact that the second, third and fourth bit of a packet have become relevant
for the behaviour of the switch means that we have to reconsider our defini-
tion of the data type representing packets. We can introduce packets with four
bits (all relevant ones) in a way similar to the current definition. Instead, and
more abstractly, we decide to model packets as before but now with an additional
