B.5 Process Definition

B.5 Process Definition

A process is defined by one or more local processes. A process can optionally be parameterized and have re-labeling, hiding and alphabet extension parts.

 ProcessDef:               ProcessIdent Paramopt = ProcessBody                                           AlphabetExtensionopt Relabelopt Hidingopt . ProcessBody:             LocalProcess             LocalProcess , LocalProcessDefs LocalProcessDefs:             LocalProcessDef             LocalProcessDefs, LocalProcessDef LocalProcessDef:             ProcessIdent IndexRangesopt = LocalProcess AlphabetExtension:             + Set 

The scope of the name for a local process definition is the process in which it is contained. A local process is END, STOP, ERROR, a reference to another local process, a sequential composition, a conditional process or is defined using action prefix and choice.

 LocalProcess:              BaseLocalProcess              SequentialComposition              if Expression then LocalProcess              if Expression then LocalProcess else LocalProcess              ( Choice ) BaseLocalProcess:              END              STOP              ERROR              ProcessIdent Indicesopt Choice:            ActionPrefix            Choice | ActionPrefix ActionPrefix:            Guardopt PrefixActions -> LocalProcess PrefixActions:            ActionsLabels            PrefixActions -> ActionsLabels Guard:            when Expression 

Examples

 TIME = (tick -> TIME). S = STOP + {a,b,c}. R = (a -> R|b -> Q), Q = STOP. P = (a[i:1..3] ->         if i==1 then STOP else P).

The scope of a variable defined in an action label is the rest of the local process in which it is defined. However, the scope of a variable defined inside a set does not extend beyond that set, e.g. {a, b, c[i:0..2]}. Note that variables are a syntactic convenience to permit concise definitions. The example process P above can be expanded to an equivalent definition without variables and conditionals:

 P = (a[1] -> STOP | a[2] -> P | a[3] -> P).

In a similar way, processes with guards can be expressed by explicitly enumerating the choices that an action label set represents. For example, the process:

 P = (a[i:0..3] ->       ( when i==0 x -> STOP       | when i!=0 y -> P       )       ).

is equivalent to:

 P = (a[0] -> x -> STOP     |a[1] -> y -> P     |a[2] -> y -> P     |a[3] -> y -> P     ).

Index ranges for local processes are also a syntactic convenience. They define a set of local processes.

 Indices:              [ Expression ]              Indices [ Expression ] IndexRanges:              [ Expression ]              [ ActionRange ]              IndexRanges [ Expression ]              IndexRanges [ ActionRange ] 

Example

 P         = S[0], S[i:0..2] = (when i<3 a -> S[i+1]), S[3]      = STOP.

The scope of a variable used in a local process definition is the local process, i.e. it extends to the comma that terminates the definition. The example above could be defined without a variable as:

 P    = S[0], S[0] = (a -> S[1]), S[1] = (a -> S[2]), S[2] = (a -> S[3]), S[3] = STOP.

The reference to a local process can be replaced by substituting its definition, giving:

 P = (a -> (a -> (a -> STOP))).

This is exactly equivalent to:

 P = (a -> a -> a -> STOP).

Variables in FSP definitions can always be removed by syntactic transformation. Consequently, in Appendix C, which presents the semantics of FSP, variables are not considered.

A sequential composition is always defined within a process. The last process in the sequential composition must be END, STOP, ERROR, or a reference to a local process. The composition essentially concatenates processes with the last (i.e. END) state of a sequential process replaced with the first state of the subsequent process in the composition list.

 SequentialComposition:               SeqProcessList ; BaseLocalProcess SeqProcessList:               ProcessRef               SeqProcessList ; ProcessRef ProcessRef:               ProcessIdent Argumentopt Argument:               ( ArgumentList ) ArgumentList:               Expression               ArgumentList , Expression 

Examples

 P(I=1) = (a[I]-> b[I] -> END). SC = P(1);P(2);SC.

The process SC above is defined below without sequential composition and has exactly the same behavior.

 SC = (a[1] -> b[1] -> a[2] -> b[2] -> SC).