4.2.2 Factor state

The formulation of BUFF above (see 4.2.1 Share components) is not only more efficient because the COPY components are shared (and thus need only be calculated once), but also because the state of the buffer has been distributed across separate processes. In general, if we have a process P with two state variables x and y ranging over X and Y, so that

P(x, y) = f(P, x, y)

for some function f, and we can split the state so that

P(x, y) = Q(x) || R(y)

for some processes Q and R in parallel, then the time taken to build the state-machine corresponding to P can be reduced from #X*#Y in the first case to #X+#Y in the second. (Of course, the exploration of the product space still has to be performed, but it can be done more efficiently as the check proceeds.) Such a change may not improve performance if the state is not independent, for example if we write

BUFF(N,in,out) =
  let
    B(n, s) =
      n>0 & out!head(s) -> B(n-1,tail(s))
    []
      n<N & in?x -> B(n+1,s^<x>)
  within B(0, <>)

then separating n and s will not be productive.

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