Information Technology Reference
In-Depth Information
Table 2. mCRL2 encoding for channels and nodes
Sync = Σ d : Data A ( d ) |B ( d ) · Sync
LossySync = Σ d : Data ( A ( d ) |B ( d )+ A ( d )) · LossySync
SyncDrain = Σ d 1 ,d 2 : Data A ( d 1 ) |B ( d 2 ) · SyncDrain
AsyncDrain = Σ d : Data ( A ( d )+ B ( d )) · AsyncDrain
FIFO ( f : DataFIFO )= Σ d : Data
( isEmpty ( f ) → A ( d ) · FIFO ( full ( d )) B ( e ( f )) · FIFO ( empty ))
Filter = Σ d : Data ( expr ( d ) → A ( d ) |B ( d ) A ( d )) · Filter
Trans form = Σ d : Data A ( d ) |B ( f ( d )) · Trans form
Merger = Σ d : Data ( A ( d ) |C ( d )+ B ( d ) |C ( d )) · Merger
Replicator = Σ d : Data A ( d ) |B ( d ) |C ( d ) · Replicator
Such a Join synchronizes all coinciding source ends and atomically forms a tuple
of the data items received at these ends and transfers it to the sink end. We
define a binary join as
Join = Σ d 1 ,d 2 : Data A ( d 1 ) |B ( d 2 ) |C ( tuple ( d 1 ,d 2 )) · Join ;
For handling data structures formed after passing through the Join node, we need
to extend our global datatype with a notion of tuples. Since mCRL2 supports
standard algebraic datatypes, this is not a problem. Throughout the rest of
the paper, we assume that the global datatype is generated by n user-defined
datatypes, which we refer to as
D n . In concrete cases, they are inferred
from the coordinated components or services. If a circuit contains one or more
Join nodes, we define the global datatype as
D 1 ,...,
sort
Data =
struct
D 1 ( e 1 :
D 1 )
|
...
|
D n ( e n :
D n )
|
tuple ( p 1 : Data, p 2 : Data );
This definition allows us to instantiate elements of any basic type as well as
binary tuples, thus forming tree-like structures. Note, this datatype is suitable
for circuits with Join nodes that have two incoming ends only. In the general
case, for every Join node with k incoming ends a tuple k ( p 1 : Data, ..., p k : Data )
must be added to the definition.
After generating process definitions for all channels and nodes, we need to
compose them into one joint process which models the whole connector. This is
done using the following three steps:
1. Forming of the parallel composition of all channel and node processes.
2. Synchronizing of actions for coinciding channel and node ends.
3. Hiding of internal actions (optional).
The tentative last step is achieved by renaming into τ , an operation not intro-
duced above. Step 2 in fact involves an application of two mCRL2 operators: com-
munication and blocking. To elucidate the composition process, we now consider
a simple example. Consider the LossyFIFO connector composed of two channels
and a replication node:
Search WWH ::




Custom Search