In this section we define the various operators that are available in CSP_{M}. We include only the briefest of descriptions of each operator, instead choosing to focus on CSP_{M}-specific issues. For more information about each of the operators see either The Theory and Practice of Concurrency or Understanding Concurrent Systems.
Note that regular expressions can be mixed with the process expression, providing doing so makes type-sense. For example:
P(x) = if x == 0 then STOP else (STOP [] STOP)
Q(x) = let P = STOP [] STOP within P [] P
are both valid CSP expressions.
The relative binding strengths of the operators is given in Binding Strength.
External Choice
P [] Q
¶Blackboard: | \(P \extchoice Q\) |
---|
Offers the choice of the initial events of P
and Q
, which must be
of type Proc
.
Guarded Expression
b & P
¶Blackboard: | \(b \mathrel{\&} P\) |
---|---|
Parameters: |
If b
is true then behaves like P
, otherwise behaves like
STOP
.
Hide
P \ A
¶Blackboard: | \(P \hide A\) |
---|
Behaves like P
, which must be of type Proc
, but if P
performs
any event from A
, which must be of type {Event
}, the event is
hidden and turned into an internal event (i.e. a tau).
Internal Choice
P |~| Q
¶Blackboard: | \(P \intchoice Q\) |
---|
This non-deterministically picks one of P
and Q
, which must be of
type Proc
, and then runs the chosen process.
Prefix
e -> P
¶Blackboard: | \(e \prefix P\) |
---|
This process performs the event e
, which must be of type Event
and then runs P
, which must be of type Proc
. FDR also supports a
number of more general forms of the prefix operator, which are particularly
useful for offering the choice of several events. For example, suppose the
following channel declarations are in scope:
channel c : {0..1}
channel d : {0..1}.Bool
The choice of c.0
and c.1
can be written as using
External Choice
as c.0 -> P [] c.1 -> P
, or more concisely
using Prefix
as c?x : {0, 1} -> P
or c?x -> P
(in this case the
set of allowed values is automatically deduced from the channel declaration).
It is also possible to write d.0.y -> P [] d.1.y -> P
more concisely as
d?x!y -> P
. Note that d?x.y -> P
would not be equivalent as the
second .
would be transformed to a ?
(see here for more information). Writing ?x
causes a new
variable x
to be introduced that is bound to the value that was
communicated. For example, a simple Echo process could be defined by
Echo(c) = c?x -> c!x -> Echo(c)
.
The general form of a Prefix consists of an expression followed by a number
of fields, each of which matches some component of the event. In
particular, the general form is e<f_1><f_2><...><f_n>
where e
is an
expression of type a => Event
and each f_i
is a field of type t_i
such that a = t_1 . t_2 . <...> . t_n
. The
available field types are as follows.
?p
External Choice
) of any value that matches
the pattern p
, which must be of a type that
satisfies Complete
. The set of allowed values is deduced
from the channel or datatype declaration. For example, given the above
channel declarations then the set of events that c?x
ranges over is
c.0
and c.1
as x
matches the first field of the channel c
.?p : S
External Choice
) of any value from the set
S
, which must be an expression of type
{a}
, that matches the pattern p
,
which must be of type a
and satisfy Complete
.!e
e
, which must be an expression.$p
This behaves exactly as ?p
, but instead offers the non-deterministic
choice of the available events (using Internal Choice
). At the
present time, fields containing $
may only appear before fields
containing ?
or !
.
New in version 3.0.
$p : S
This behaves exactly as ?p : S
, but instead offers the
non-deterministic choice of the available events (using
Internal Choice
). At the present time, fields containing $
may
only appear before fields containing ?
or !
.
New in version 3.0.
The set expressions in each of the fields are able to use the value of
variables bound by patterns to the left of the field. This means that
expressions such as d?x?y:f(x) -> P
are allowed.
The following table gives a number of prefix forms and the explicit process that they are equivalent to.
Process | Equivalent To |
---|---|
c?x -> P(x) |
c.0 -> P(0) [] c.1 -> P(1) |
c?x : {0} -> P(x) |
c.0 -> P(0) |
d?x : {0.True, 1.False} -> P(x) |
d.0.True -> P(0.True) [] d.1.False -> P(1.False) |
d?x!False -> P(x) |
d.0.False -> P(0) [] d.1.False -> P(0) |
d?x.y -> P(x,y) |
d?x?y -> P(x,y) |
c$x -> P(x) |
c.0 -> P(0) |~| c.1 -> P(1) |
d$x?y -> P(x,y) |
(d.0.False -> P(0,False) [] d.0.True -> P(0,True))
|~| (d.1.False -> P(1,False) [] d.1.True -> P(1,True)) |
d?x?y:{x==0} -> P(x,y) |
d.0.True -> P(0,True) [] d.1.False -> P(1,False) |
Warning
Note that any .
that occurs after a ?
essentially becomes a ?
(equally, any .
after a !
becomes a !
and any .
after a
$
becomes a $
). For example, d?x.y -> STOP
is not
equivalent to d?x!y
, but instead it is equivalent to
d?x?y
. This is because .
binds tighter than ?
, meaning
that d?x.y
is bracketed as d?(x.y)
.
Project
P |\ A
¶Blackboard: | \(P \project A\) |
---|
Behaves like P
, which must be of type Proc
, but if P
performs
any event not in A
, which must be of type {Event
}, the event is
hidden and turned into an internal event (i.e. a tau).
Rename
P[[from <- to]]
¶Blackboard: | \(P \rename{from \leftarrow to}\) |
---|---|
Parameters: |
The renaming operator renames all events that P performs according to the
given relation. The relation is specified, as above, and causes all events of
the form from.x
that P
performs to to.x
(or, if from
and
to
are events, renames from
to to
). For example, in the
following, P
and Q
are equivalent:
channel c, d : {0..1}
channel e : Bool.{0..2}
P = (c.0 -> STOP [] d.1 -> STOP)[[c <- e.false, d <- e.true]]
Q = e.false.0 -> STOP [] e.true.1 -> STOP
It is also possible to combine the above using set statements, as follows:
P[[c.x <- e.false.(x+1), d.x <- e.true.(x+1) | x <- {0..1}, x == 0]]
This renames c.0
to e.false.1
and d.0
to e.true.1
. Note that
the generators in the above must be set generators.
Warning
If from
and to
are channels, rather than events, care must be
taken to ensure that the renaming will not result in invalid events being
created, otherwise a runtime error will occur. For example, given the
above definitions, evaluating:
(d.true.2 -> STOP)[[d.true <- c]]
would result in an error, as
2
is not in the set of values that can be sent down d
.
Note
Unlike the blackboard CSP operator, the renaming relation is not required to be total. Events that are not in the domain of the renaming relation are unaffected by the renaming.
Alphabetised Parallel
P [A || B] Q
¶Blackboard: | \(P \alphaparallel{A}{B} Q\) |
---|---|
Parameters: |
Runs P
and Q
in parallel, allowing P
to only perform events from
A
, Q
to only perform events from B
and forcing P
and Q
to
synchronise on \(A \cap B\). Equivalent to (P [| diff(Events, A) |]
STOP) [| inter(A, B) |] (Q [| diff(Events, B) |] STOP)
.
See also
Generalised Parallel
P [| A |] Q
¶Blackboard: | \(P \parallel{A} Q\) |
---|---|
Parameters: |
Runs P
and Q
in parallel forcing them to synchronise on events in
A
. Any event not in A
may be performed by either process.
See also
Interleave
P ||| Q
¶Blackboard: | \(P \interleave Q\) |
---|---|
Parameters: |
Runs P
and Q
in parallel without any synchronisation. Equivalent to
P [| {} |] Q
.
See also
FDR also has replicated, or indexed, version of a number of operators. These
provide an easy way to construct a process that consists of a number of
processes composed using the same operator. For example, suppose P ::
then
(
Int
) ->
Proc
||| x : {0..2} @ P(x)
evaluates P
for each value of
x
in the given set and then interleaves them. Thus, the above is equivalent
to P(0) ||| P(1) ||| P(2)
.
The general form of a replicated operator is op <statements> @ P
where
op
is a piece of operator syntax, statements are a list of
Statements and P
is the process definition (which can make use of
the variables bound by the statements). Each of the operators evaluates P
for each value the statements take before composing them together using op
.
Replicated Alphabetised Parallel
|| <set statements> @ [A] P
¶Evaluates P
and A
for each value of the Statements and
composes the resulting processes together using Alphabetised Parallel
,
where each process has the corresponding alphabet A
. If the resulting set
of processes is empty then this evaluates to SKIP
. For example, in
the following Q
and R
are equivalent:
channel a : {0..3}
P(x) = a.x -> STOP
A(x) = {a.x}
Q = || x : {0..3} @ [A(x)] P(x)
R = a.0 -> STOP ||| a.1 -> STOP ||| a.2 -> STOP ||| a.3 -> STOP
Replicated External Choice
[] <set statements> @ P
¶Replicated external choice evaluates P
for each value of the
Statements and composes the resulting processes together using
External Choice
. If the resulting set of processes is empty (e.g. []
x : {} @ x
), then STOP
is returned.
Hint
In CSP_{M} there is no way of writing a process equivalent to the blackboard
CSP \(?ev : X \prefix P(ev)\), which offers the choice of all events
\(ev\) that are in \(X\), just using the prefixing operator.
However, using the replicated external choice operator, an equivalent
process can be defined as [] ev : X @ ev -> STOP
.
Replicated Generalised Parallel
[| A |] <set statements> @ P(x)
¶Evaluates P
for each value of the Statements and composes
the resulting processes together using Generalised Parallel
,
synchronising them on the set A
. If the resulting set of processes is
empty then this evaluates to SKIP
.
Replicated Interleave
||| <set statements> @ P(x)
¶Evaluates P
for each value of the Statements and composes
the resulting processes together using Interleave
. If the resulting set
of processes is empty then this evaluates to SKIP
.
Replicated Internal Choice
|~| <set statements> @ P(x)
¶Replicated internal choice evaluates P
for each value of the
Statements and composes the resulting processes together using
Internal Choice
. If the resulting set of processes is empty then an
error is thrown.
Replicated Linked Parallel
[l <-> r] <sequence statements> @ P(x)
¶Evaluates P
, l
and r
for each value of the
Statements and composes the resulting processes together
in the same order as the statements using Linked Parallel
. In
particular suppose P
, l
and r
evaluate to P1
, P2
, etc
then the following process is constructed P1 [l1 <-> r1] P2 [l2 <-> r2]
...
. If the resulting sequence of processes is empty then an error is
thrown.
As with Linked Parallel
, the linking of events may be specified using
comprehensions. For example:
channel c, d : Bool
Q(0) = c.True -> STOP
Q(1) = d.True -> STOP
P = [c.x <-> d.x | x <- <False, True>, x] y : <0,1> @ Q(y)
then P
is equivalent to Q(0) [c.True <-> d.True] Q(1)
.
Replicated Sequential Composition
; <sequence statements> @ P(x)
¶Evaluates P
for each value of the Statements and
composes the resulting processes together in the same order as the statements
using Sequential Composition
. If the resulting sequence of processes is
empty then this evaluates to SKIP
.
Replicated Synchronising Parallel
[+ A +] <set statements> @ P(x)
¶Evaluates P
for each value of the Statements and composes the
resulting processes together using Synchronising External Choice
. If
the resulting sequence of processes is empty then this evaluates to
STOP
.
New in version 2.94.
Exception
P [| A |> Q
¶Blackboard: | \(P \exception{A} Q\) |
---|---|
Parameters: |
This process initially behaves like P
, but if P
ever performs an
event from the set A
, then the process Q
is started.
New in version 2.91.
Interrupt
P /\ Q
¶Blackboard: | \(P \interrupt Q\) |
---|
This operator initially behaves like P ||| Q
, but if any action of Q
is performed P
is discarded and the process behaves as Q
. Both P
and Q
must be of type Proc
.
Linked Parallel
P [c <-> d] Q
¶Blackboard: | \(P [c \leftrightarrow d] Q\) |
---|---|
Parameters: |
Linked parallel runs P
and Q
in parallel, forcing them to synchronise
on the c
and d
events and then hides the synchronised events.
Assuming that f
is a fresh name it is equivalent to (P[[c <- f]] [| {|
f |} |] Q[[d <- f]]) \ {| f |}
. However, compiling linked parallel will be
significantly faster than the above simulation.
As with Rename
, multiple channels may be linked and set
statements may be used to specify the linking. For
example, P [a <-> b, c <-> d] Q
and P [a.x <-> b.x, c.x <-> d.x | x <-
X, f(x)] Q
are both valid syntax. Again, as with Rename
, care must be
taken to ensure that the channels have the same allowed values, otherwise a
runtime error will occur.
Sequential Composition
P ; Q
¶Blackboard: | \(P \sequentialcomp Q\) |
---|
Behaves like P
until it terminates (by turning into SKIP
) at
which point Q
is run. Both P
and Q
must be of type Proc
.
Sliding Choice or Timeout
P [> Q
¶Blackboard: | \(P \timeout Q\) |
---|
Initially it offers the choice of the initial events of P
, but can
non-deterministically change into a state where only the events of Q
are
available. If P
performs a tau to P'
, then P [> Q
will perform a
tau transition to P' [> Q
(i.e. timeout is not resolved by taus). Both
P
and Q
must be of type Proc
.
Synchronising External Choice
P [+ A +] Q
¶Blackboard: | \(P \syncextchoice{A} Q\) |
---|
This operator is a hybrid of External Choice
and :op`Generalised Parallel`.
Initially it offers the initial events of both P
and Q
,
which must be of type Proc
. As with Generalised Parallel
,
P
and Q
are required to synchronise on events from A
, which must
be of type
. If either {
Event
}
P
or Q
performs any event
not in A
(including a tick or a tau) then the operator behaves like
External Choice
and discards the argument that did not do an event.
Thus, [+ A +]
is resolved only by performing events not in A
, whilst
events from A
are performed simultaneously by both branches. For example,
given the following:
P = a -> b -> STOP [+ {a} +] a -> c -> STOP
Q = a -> (b -> STOP [] c -> STOP)
P
and Q
are equivalent.
New in version 2.94.
Synchronising Interrupt
P /+ A +\ Q
¶Blackboard: | \(P \syncinterrupt{A} Q\) |
---|
This operator is analogous to Synchronising External Choice
in that it
is a hybrid of Interrupt
and Generalised Parallel
. Initially it
offers the initial events of both P
and Q
, which must be of type
Proc
. As with Generalised Parallel
, P
and Q
are
required to synchronise on events from A
, which must be of type
. As with {
Event
}
Interrupt
, any event that P
performs
does not resolve the operator (except for tick, which terminates it). If
Q
ever performs a visible event that is not in A
then this resolves
the choice and the process behaves as Q
. For example, given the
following:
P = a -> b -> STOP /+ {a} +\ a -> c -> STOP
Q = a -> (b -> STOP /\ c -> STOP)
R = a -> (b -> c -> STOP [] c -> STOP)
P
, Q
and R'
are equivalent.
New in version 2.94.