"@concurrency{...}" activity primitive

The "@schedule{...}" and "@concurrency{...}" primitives are syntactic sugar to describe the scheduling of a machine’s executable components.

The "@concurrency{...}" primitive may contain the scheduling operator for the remaining components (that are neither in "@schedule{...}" nor in "@run{...}"). If this primitive is empty, the default operator is the interleaving operator "|i|".

The link between policies described with the "@schedule{...}" and "@concurrency{...}" primitives is the weak sequence "|;;|"

Example

For example, suppose we have a machine M containing four executable components A, B, C and D, with primitives :

Its implicit scheduling policy, triggered by primitive "@run{...}", will be :

Which is equivalent, by transitivity of operator "|;;|", to :