4.2.1 Share components

When FDR builds state-machines from the CSP process descriptions, it does so as an acyclic graph of process operators where the leaves of the graph are simple transition systems. Although FDR can build the operator tree efficiently, construction of the leaves can be expensive. For example, it is much more efficient to build an N-place buffer as

BUFF(N,in,out) =
  let
    COPY = in?x->out!x->COPY
  within [out<->in] x : {1..N}  COPY

than

BUFF(N,in,out) =
  let
    B(s) =
      not null(s) & out!head(s) -> B(tail(s))
    []
      #s < N & in?x -> B(s^<x>)
  within B(<>)

and it is more efficient (assuming P and Q are both used) to write

P = BUFF(10, in, out)
Q = P [[ in<-left, out<-right ]]

than to write

P = BUFF(10, in, out)
Q = BUFF(10, left, right)

since the renaming can be built directly and the leaf process is then shared between P and Q.

Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.