B.7 Parameters

B.7 Parameters

Process and composite process parameters must always have a default value. This means that a process can always be compiled into a finite Labeled Transition System (LTS). The default parameter value may be changed by an argument when the process, whether composite or primitive, forms part of another composite process.

 Param:              ( ParameterList ) ParameterList:              Parameter              ParameterList , Parameter Parameter:              ParameterIdent = Expression 

Example

  P(X=1)  = (a[X] -> STOP). ||S(Y=2) = (P(Y+1) || P(Y+2)).

The scope of a parameter is the process or composite in which it is defined. Parameter substitution creates a new process with each occurrence of the parameter replaced by the argument value. This is simply macro expansion. Substituting the parameters in the example results in the following equivalent definition.

 P3   = (a[3] -> STOP). P4   = (a[4] -> STOP). ||S2 = (P3 || P4).