B.6 Composite Process


B.6 Composite Process

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 ] 

Examples

 ||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.

Example

 ||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   ).




Concurrency(c) State Models & Java Programs
Concurrency: State Models and Java Programs
ISBN: 0470093552
EAN: 2147483647
Year: 2004
Pages: 162

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net