i've always thought the spin(1) protocol analyser was
a perfect match for the concurrency primitives found in
plan 9 and in Limbo.

i've just had to think again.

these concurrency primitives allow for dynamic creation of processes
and channels.  in particular, a fairly common idiom is (using Limbo
syntax for brevity):

	c := chan of int;
	spawn someproc(c);
	<-c;

where someproc() does something, sends on the channel c,
and continues on its way.

this idiom translates quite naturally into Promela:

	chan c = [0] of {bit};
	run someproc(c);
	c?0

the problem is that promela allows only a static number
of channels, and it doesn't garbage-collect old channels, so
that, for instance, this Promela program:

	active proctype x()
	{
		do
		:: _nr_pr == 1 ->
			run f()
		od
	}
	
	proctype f()
	{
		chan sync = [0] of {bit};
	}

dies very quickly, saying "too many queues".  (the _nr_pr condition is
necessary to prevent exiting processes from building up).

this is a pity, especially given that the spin manual itself suggests
replacing function calls with process invocations - the "factorial"
example given there dies if n > 257.

i imagine there are a few spin users out there.  is there a neat
general solution to this problem (for instance, an automatic
transformation).

or should i just give up on making a spin model of my system?

i've attached a copy of the model.

  cheers,
    rog.