Defining Processes¶

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.

Basic Operators¶

operator 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.

operator Guarded Expression b & P¶

Blackboard:	$b \mathrel{\&} P$
Parameters:	b (`Bool`) – The process guard. P (`Proc`) – The process to behave as if `b` is true.

If b is true then behaves like P, otherwise behaves like STOP.

operator 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).

operator 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.

operator 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.

Input ?p: Offers the choice (using 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.
Restricted Input ?p : S: Offers the choice (using 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.
Output !e: This allows only the value of e, which must be an expression.
Non-deterministic Input $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.
Non-deterministic Restricted Input $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).

operator 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).

See also

Hide: It is equivalent to P \ diff(Events, A), but may be more efficient when Events is large.

operator Rename P[[from <- to]]¶

Blackboard:	$P \rename{from \leftarrow to}$
Parameters:	P (`Proc`) – The process to rename. from (`a =>` `Event`) – The channel to rename events from. to (`a =>` `Event`) – The channel to rename events to.

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.

Parallel Operators¶

operator Alphabetised Parallel P [A || B] Q¶

Blackboard:	$P \alphaparallel{A}{B} Q$
Parameters:	P (`Proc`) – The left process. A (`{Event}`) – The set of events that `P` is allowed to perform. B (`{Event}`) – The set of events that `Q` is allowed to perform. Q (`Proc`) – The right process.

See also

Enumerated Sets: For details on how to easily construct synchronisation sets.

operator Generalised Parallel P [| A |] Q¶

Blackboard:	$P \parallel{A} Q$
Parameters:	P (`Proc`) – The left process. A (`{Event}`) – The synchronisation alphabet. Q (`Proc`) – The right process.

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

Enumerated Sets: For details on how to easily construct synchronisation sets.

operator Interleave P ||| Q¶

Blackboard:	$P \interleave Q$
Parameters:	P (`Proc`) – The left process. Q (`Proc`) – The right process.

Runs P and Q in parallel without any synchronisation. Equivalent to P [| {} |] Q.

See also

Enumerated Sets: For details on how to easily construct synchronisation sets.

Replicated Operators¶

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 :: (Int) -> Proc then ||| 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.

operator 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

operator 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.

operator 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.

operator 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.

operator 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.

operator 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).

operator 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.

operator 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.

Advanced Operators¶

operator Exception P [| A |> Q¶

Blackboard:	$P \exception{A} Q$
Parameters:	P (`Proc`) – The initial process. A (`{Event}`) – The set of exception events. Q (`Proc`) – The process to behave like once an exception has been thrown.

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.

operator 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.

operator Linked Parallel P [c <-> d] Q¶

Blackboard:	$P [c \leftrightarrow d] Q$
Parameters:	P (`Proc`) – The left process. Q (`Proc`) – The right process. c (`a =>` `Event`) – The channel of the left process to synchronise. d (`a =>` `Event`) – The channel of the right process to synchronise.

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.

operator 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.

operator 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.

operator 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 {Event}. If either 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.

operator 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 {Event}. As with 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.

Blackboard:	\(b \mathrel{\&} P\)
Parameters:	b (`Bool`) – The process guard. P (`Proc`) – The process to behave as if `b` is true.

Blackboard:	\(P \rename{from \leftarrow to}\)
Parameters:	P (`Proc`) – The process to rename. from (`a =>` `Event`) – The channel to rename events from. to (`a =>` `Event`) – The channel to rename events to.

Blackboard:	\(P \alphaparallel{A}{B} Q\)
Parameters:	P (`Proc`) – The left process. A (`{Event}`) – The set of events that `P` is allowed to perform. B (`{Event}`) – The set of events that `Q` is allowed to perform. Q (`Proc`) – The right process.

Blackboard:	\(P \parallel{A} Q\)
Parameters:	P (`Proc`) – The left process. A (`{Event}`) – The synchronisation alphabet. Q (`Proc`) – The right process.

Blackboard:	\(P \interleave Q\)
Parameters:	P (`Proc`) – The left process. Q (`Proc`) – The right process.

Blackboard:	\(P \exception{A} Q\)
Parameters:	P (`Proc`) – The initial process. A (`{Event}`) – The set of exception events. Q (`Proc`) – The process to behave like once an exception has been thrown.

Blackboard:	\(P [c \leftrightarrow d] Q\)
Parameters:	P (`Proc`) – The left process. Q (`Proc`) – The right process. c (`a =>` `Event`) – The channel of the left process to synchronise. d (`a =>` `Event`) – The channel of the right process to synchronise.