ParallelBehavior
The ParallelBehavior operators are used to construct the parallel composition of two behaviors.
Syntax Definition
ParallelBehavior ::= Behavior ( || | |?| | ||| ) Behavior .
Remarks
In synchronized parallel composition, written as B1 || B2, all steps of the composed behaviors must be synchronized; steps that cannot be synchronized are excluded from the result. The offered signature of this behavior is the intersection of the signatures of the subbehaviors.
In interleaved parallel composition, written as B1 ||| B2, all steps of the subbehaviors are produced. The offered signature of this behavior is the union of the signatures of the subbehaviors.
Synchronized-interleaved parallel composition, written as B1 |?| B2, is a combination of the two previous types of parallelization. Actions in the intersection of the offered signatures of the subbehaviors must synchronize while the remaining actions are interleaved. The offered signature is the union of the signatures of the subbehaviors.
Example
The following Cord code shows the use of the ParallelBehavior operators. This code is extracted from the stand-alone Operators sample (see Finding the Code Samples).
config EssentialActivities
{
action abstract static void Implementation.Eat();
action abstract static void Implementation.Drink();
}
config PartyActivities: EssentialActivities
{
action abstract static void Implementation.Dance();
action abstract static void Implementation.Sing();
action abstract static void Implementation.Leave();
action abstract static void Implementation.KeepPartying();
}
config RegularActivities: EssentialActivities
{
action abstract static void Implementation.Fast();
action abstract static void Implementation.Sleep();
}
config AllActivities: PartyActivities, RegularActivities
{ }
machine SyncParallel() : AllActivities
{
Party || NoParty
}
machine InterleavedParallel() : AllActivities
{
Party ||| NoParty
}
machine SyncInterleavedParallel() : AllActivities
{
Party |?| NoParty
}
In machine SyncParallel, behaviors Party and NoParty can synchronize on the Eat then Drink path. But they fail to synchronize from then on, so the SyncParallel behavior ends there.
In machine InterleavedParallel, all possible interleavings of machines Party and NoParty are included.
In machine SyncInterleavedParallel, Eat and Drink are in the intersection of configs PartyActivities and RegularActivites. All other paths are interleaved.