Process Expressions
In the following we list possible constructions for process expressions
and describe their behaviour.
Parentheses may be used to group process expressions.
- atomic action
a
- Execution of the atomic action a.
- internal step
skip
- Execution of an internal step not visible to the environment.
In ACP based extensions it is known as tau.
- deadlock
delta
- A deadlock cannot be executed.
- process
P
- The process P will be replaced by an alternative composition of
all the process definitions of which the left hand side matches with
P.
- sequential composition
x . y
- Process expression x is executed and upon termination followed
by the execution of process expression y.
- alternative composition
x + y
- A non-deterministic choice between process expressions x and
y is made.
Choosing a deadlock is forbidden.
- parallel composition
x || y
- The process expressions x and y are executed in
parallel in which possible communications can take place.
- generalized alternative composition
sum(v in S, x)
- An abbreviation of the alternative composition of, for every value
of v in the sort or set S, the process expression
x in which v is replaced by the value.
- generalized parallel composition
merge(v in S, x)
- An abbreviation of the parallel composition of, for every value
of v in the sort or set S, the process expression x
in which v is replaced by the value.
- encapsulation
encaps(H, x)
- Can only execute actions from process expression x that are
not an element of set H.
- hiding
hide(I, x)
- Let the executed actions from process expression x behave as
the internal step
skip.
- conditional expression
[t = u] -> x
- If the terms t and u are equal, the conditional
expression evaluates to the process expression x, and to
deadlock otherwise.
In addition to the above described process constructions, PSF also has
the following constructions.
- interruption
interrupt(x, y)
- The executions of process expression x can be interrupted by
process expression y at any time.
After the execution of process expression y has finished,
the execution of process expression x resumes.
- disruption
disrupt(x, y)
- The execution of process expression x can be interrupted by
process expression y at any time.
After the execution of process expression y has finished,
instead of continueing the execution of process expression x,
the execution of the whole process expression is finished.
- priority
prio(S1 > ... > Sn, x)
- Gives priority of actions in process expression x that appear
in set Si over actions that appear in set
Sj for j > i.
This means that when there is a choice between actions only
the actions with the highest priority and the actions without
a priority can be chosen.
With the priority operator, the use of the keyword
atoms
is extended to not only denote the set type atoms,
but also to denote the set of all atomic actions.
The process expression prio(S ,x) is an
abbreviation of prio(S > atoms, x).
- iteration
x * y
- Chooses between process expressions x and y.
If x is chosen, upon termination of the execution of x
the iteration is repeated.
If y is chosen, upon termination of the execution of y
the iteration finishes.
- nesting
x # y
- Chooses between process expressions x and y.
If x is chosen, upon termination of the execution of x
the nesting is repeated.
If y is chosen, upon termination of the execution of y,
x is executed the number of times x has been chosen.