Information Technology Reference
In-Depth Information
Fig. 4.
Counter
circuit
20
depth-first
breadth-first
none
15
10
5
0
20
25
30
5
10
15
Counter size (number of FIFOs)
Fig. 5.
Benchmarks for different encodings of the
Counter
circuit
connector to determine what processes communicate directly with each other.
This leads to a much faster linearization process. In particular, we found out that
a traversal over the connector graph is well-suited for this problem. In our exper-
iments, the depth-first traversal showed the best results.
As an example we tested the so-called
Counter
circuit shown in Figure 4.
This circuit consists of an exclusive router with
n
outputs, each connected to
another
FIFO
, which in turn are synchronized using a
SyncDrain
at their sink
ends. Here we are interested only in two actions: data arriving at the source
end of the exclusive router and the synchronized firing of the
SyncDrain
s. The
resulting transition system consists of
n
states and
n
transitions. Benchmarks
5
of the different optimizations are depicted in Figure 5. The linearization using
depth-first traversal took less than 5 seconds for the counter with 30
FIFO
s. The
breadth-first approach was still able to handle 10
FIFO
s in 20 seconds. However,
without any optimizations
mCRL2
needed more than 20 minutes to process the
counter with just 3
FIFO
s.
8 Related Work
In this section, we compare our framework to other tools for analyzing Reo
connectors. For an overview of related work with respect to the application of
our tool to business process and web service composition analysis refer to [6].
5
Benchmarks were taken on a standard machine with 4 cores and 8GB of memory,
running Linux 2.6.27 and the development version of
mCRL2
(revision 7467).
