SequencingBehavior
Two SequencingBehavior operators are available for behavior composition: Loose sequencing and Tight sequencing.
Syntax Definition
SequencingBehavior ::= Behavior -> Behavior | Behavior ; Behavior /*right-assoc*/ .
Remarks
Loose sequencing, B1 -> B2, denotes the set of traces which start with B1, followed by arbitrary actions from the context signature, then concluded with B2. It can be syntactically reduced to B1; ... ; B2. The offered signature is the context signature.
Tight sequencing, B1 ; B2, denotes the set of traces obtained by concatenating the traces of B1 to those of B2. The offered signature is the union of the signatures of the operands.
Sequencing operators are right-associative.
Example
The following Cord code shows the use of the SequencingBehavior operators. This code is extracted from the stand-alone Operators sample (see Finding the Code Samples).
machine TightSequence() : AllActivities
{
Party; NoParty
}
machine LooseSequence() : AllActivities
{
Party -> NoParty
}
In machine TightSequence, the Tight SequencingBehavior operator (;) constructs the set of traces obtained by concatenating the traces of the first operand to those of the second one.The second behavior is appended at all accepting states.
In machine LooseSequence, the Loose SequencingBehavior operator (->) allows an arbitrary number of actions from the context signature to occur between its first and its second operand. The second behavior is appended at all accepting states.