Information Technology Reference
In-Depth Information
X 1 X 2 Y 2 Y 1
A
B
Following the systematic translation scheme, sorts X 1 and Y 1 are internal ports
of the channels that are connected together. Although, these channel ends can be
connected directly, for genericity we assume that they both connect to a node.
Since the mCRL2 specification language does not allow the use of the same action
name in several groups of communicating actions within a single communication
operator, we introduce two ports X 2 and Y 2 to connect channel ends to the
node. To keep the example small, we assume that the channel ends A and B
form the boundary of the connector without connecting to nodes. Thus, the
three constituents of the LossyFIFO circuit are translated to the following mCRL2
processes:
LossySync = Σ d : Data ( A ( d ) |X 1 ( d )+ A ( d )) · LossySync ;
Node = Σ d : Data X 2 ( d ) |Y 2 ( d ) · Node ;
FIFO ( f : DataFIFO )= Σ d : Data
isEmpty ( f ) → Y 1 ( d ) · FIFO ( full ( d )) B ( e ( f )) · FIFO ( empty );
For obtaining the mCRL2 process for the LossyFIFO connector, we first form the
parallel composition of the three processes above, force actions corresponding to
the connected channel and node ends communicate, and finally hide the actions
X and Y that represent the data flow at the internal node/channel ports by
renaming them to τ .Inthe mCRL2 syntax, cf. Section 3, this reads
Connector = ρ N→N\{X,Y } (
{X 1 ,X 2 ,Y 1 ,Y 2 } (
Γ {X 1 |X 2 →X,Y 1 |Y 2 →Y } (
LossySync
Node
FIFO )));
However, this direct approach does not exploit the information about the circuit
structure, and, as we show later, the further processing of the obtained specifi-
cation is very inecient. Therefore, we build up the process for a Reo connector
in a stepwise fashion, i.e.,
Connector1 = ρ N→N\{Y } ( {Y 1 ,Y 2 } ( Γ {Y 1 |Y 2 →Y } ( Node
FIFO )));
Connector = ρ N→N\{X} ( {X 1 ,X 2 } ( Γ {X 1 |X 2 →X} ( LossySync
Connector1 )));
In this version, we first compose the node and the FIFO ,synchronizeandhide
their connected ends, and then continue with the rest of the circuit. This helps us
to keep the intermediate state spaces relatively small. Note that we can use the
topology of the connector to determine an order of the processes that significantly
decreases the run-time of the linearization algorithm. A comparison of the actual
run-times of the two approaches is discussed in Section 7.
5 Correctness of the Translation
In this section, we prove the correctness of the mapping of Reo to mCRL2 dis-
cussed above. For simplicity we only consider connectors with disjoint sets of
 
Search WWH ::




Custom Search