Forall - process replication


Processes may be replicated in composite process definitions using process labelling e.g. a[i:0..3]:P. However, if the process is not labelled then an explicit replicator must be used as in the example below:

range Key = 0..3
range Val = 0..1

TUPLE(K=0)   = (in[K][v:Val] -> TUPLE[v]),
TUPLE[v:Val] = (read[K][v] -> TUPLE[v] | out[K][v] -> TUPLE).

||TUPLESPACE  = forall [i:Key] 
	           TUPLE(i).

Note that the following composite declarations define exactly the same process.

||C0 = (a[0]:X || a[1]:X || a[2]:X || a[3]:X).

||C1 = a[0..3]:X.

||C2 = forall[i:0..3] a[i]:X.