Information Technology Reference
In-Depth Information
Boolean parameter indicating whether the packet is interesting (
true
)ornot
(
false
).
sort
Packet
=
struct
packet
(
b
1
:
Bit
,
int
:
B
);
By extending the structured sort, we are required to update the definition of the
mapping for routing packets. As the second, third, and fourth bit have no effect
on the destination of a packet, the adaptation is straightforward.
map
dest
:
Packet
→
N
;
var
;
eqn
dest
(
packet
(
zero
,b
)) = 0;
dest
(
packet
(
one
,b
)) = 1;
b
:
B
4.2
The Act of Counting
There are several ways of modelling the counting of interesting packets. One
way is to introduce a parameter that reflects the number of interesting packets
that have been transferred. Another way is to introduce an action to indicate a
transferral of an interesting packet. We have chosen the latter solution. Thus,
the act of counting interesting packets will be performed by executing an action
inc
, that has no data parameters.
act
inc
;
Another decision that must be made is which entity actually performs the
counting. One solution is to introduce a separate process for this purpose. An-
other option is to enhance the functionality of either the input or the output
buffers. We have chosen to enhance the functionality of the output buffers. It
should be said that implementing the other solutions poses no real problems for
mCRL2.
To accommodate this behavior, the first summand of the output buffer from
the Simplified Switch is split into two cases, one for receiving and counting an
interesting packet and one for receiving a non-interesting packet. To decide if a
packet is interesting, the projection function
int
is used. The projection function
for a specific field of a structured sort is specified in the sort declaration. For the
sort
Packet
there are projection functions
b
1
and
int
for obtaining the values of
the first and second field, respectively.
proc
Output
(
i
:
N
,c
:
List
(
Packet
)) =
→
s
:
N
#
c<
cap
(
int
(
p
)
→
recv
(
s, i, p
)
|
inc
·
Output
(
i, p
c
)
p
:
Packet
+
¬
int
(
p
)
→
recv
(
s, i, p
)
·
Output
(
i, p
c
))
+
c
≈
[]
→
leave
(
i,
rhead
(
c
))
·
Output
(
i,
rtail
(
c
));
4.3
Adapting the Input Buffer
The Original Switch poses an additional restriction on the cases in which com-
munication between input and output buffer can be performed.
