🚀 go-pugleaf

Reference:  E. Brinksma.  Constraint-oriented specification in a
constructive formal description technique.  In Stepwise Refinement of
Distributed Systems: Models, Formalisms, Correctness: REX Workshop
Proceedings 1990, pp 130-152.

I am learning LOTOS, and I've run across an example in this article
that seems to be wrong.  Here it is:

  process Bounded_Bag[input,output](n:nat) :=
	Bag[input,output] || Bound[input,output](n)
	where

		process Bag[input,output] :=
			input ?x:elem;
			(Bag[input,output]
			 ||| output !x; stop)
		endproc

		process Bound[input,output](n:nat) :=
			(output ?x:elem; Bound[input,output](n+1)
			 [] [n>1] -> input ?x:elem; Bound[input,output](n-1))
		endproc

I believe that value matching between recursive instances of process
Bag at gate output would lose data (and invalidate n as a bound,
effectively lowering it); the fact that Bounded_Bag re-orders its
values could be all right (but would not be for a bounded FIFO queue).
This problem only affects processes with non-tail recursion; it arises
because LOTOS (unlike CSP and CCS) allows mulitple processes to
participate in an interaction and defines the concept of value
matching.  CSP and CCS only allow a pair of processes to pass values
at a gate.

Is the example wrong, or my understanding of it?
--
Dave Skeen                     IBM Internal: dls@achilleus.austin.ibm.com
D61/803  Zip 2603              IBM VNET:     SKEEN at AUSTIN
Austin, TX 78758               Internet:     dls@dce.austin.ibm.com