A composite process is distinguished from a primitive process by prefixing its definition with ||. Composite processes are constructed using parallel composition, re-labeling, priority and hiding. Process labeling and sharing are specialized forms of re-labeling. The replication and conditional constructs are purely syntactic conveniences.
CompositeDef: || ProcessIdent Paramopt = CompositeBody Priorityopt Hidingopt . CompositeBody: PrefixLabelopt ProcessRef Relabelopt PrefixLabelopt ( ParallelComposition ) Relabelopt forall Ranges CompositeBody -- replication if Expression then CompositeBody -- conditional if Expression then CompositeBody else CompositeBody PrefixLabel: ActionLabels : -- process labeling ActionLabels :: -- process sharing ActionLabels :: ActionLabel: ParallelComposition CompositeBody ParallelComposition || CompositeBody Priority: >> Set << Set Ranges: [ ActionRange ] Ranges [ ActionRange ]
||S = a[1..3]:P. ||S = {a[1],a[2],a[3]}:P. ||S = forall[i:1..3] a[i]:P. ||S = forall[i:1..3] a:P/{a[i]/a}. ||S = (a[1]:P || a[2]:P || a[3]:P).
The composite process definitions above are exactly equivalent and define the same composite process. The syntax for re-labeling is described in section B.8. The scope of a variable in a composite process is the CompositeBody in which it is defined together with any other CompositeBody contained within that CompositeBody definition.
||S = forall[i:1..4] if (i<=2)then (forall[j:1..2] a[i][j]:P) else (forall[j:1..2] b[i][j]:P).
The definitions of the two occurrences of the variable j do not conflict in the above example since they are each defined in a different CompositeBody. Neither CompositeBody is contained within the other. The replication can be unfolded to give the equivalent definition for S shown below.
||S = ( a[1][1]:P || a[1][2]:P || a[2][1]:P || a[2][2]:P ||b[3][1]:P || b[3][2]:P || b[4][1]:P || b[4][2]:P ).