dls@achilleus.austin.ibm.com (David Skeen) (06/12/91)
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.combrendan@cs.uq.oz.au (Brendan Mahony) (06/13/91)
In <DLS.91Jun11202329@achilleus.austin.ibm.com> dls@achilleus.austin.ibm.com (David Skeen) writes: >CSP (and CCS) only allow a pair of processes to pass values at a gate. I have heard this from more than one person. Where does this bit of misinformation come from? CSP has special conventions for setting up 1::1 channels between processes (P >> Q), but the basic synchronisation mechanism (P || Q) is broadcast. -- Brendan Mahony | brendan@batserver.cs.uq.oz Department of Computer Science | heretic: someone who disgrees with you University of Queensland | about something neither of you knows Australia | anything about.
dls@achilleus.austin.ibm.com (David Skeen) (06/13/91)
In article <1918@uqcspe.cs.uq.oz.au> brendan@cs.uq.oz.au (Brendan Mahony) writes:
I have heard this from more than one person. Where does this bit of
misinformation come from? CSP has special conventions for setting up
1::1 channels between processes (P >> Q), but the basic synchronisation
mechanism (P || Q) is broadcast.
From Hoare's 1985 book: "We shall observe the convention that
channels are used for communication in only one direction and between
only two processes" (p134). I understand that (P || Q) means P in
parallel with Q, but I don't see (P >> Q).
Are we both talking about Communicating Sequential Processes?
--
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.combrendan@cs.uq.oz.au (Brendan Mahony) (06/14/91)
In <DLS.91Jun13105052@achilleus.austin.ibm.com> dls@achilleus.austin.ibm.com (David Skeen) writes: >From Hoare's 1985 book: "We shall observe the convention that >channels are used for communication in only one direction and between >only two processes" (p134). Does not the fact that he feels it necessary to call this a convention hit to you that this is not necessitated by the semantic domain? In fact there is no way to ensure that this convention is respected other than by hiding the channel, thus localising it to the processes it is intended to facilitate communication between. >I understand that (P || Q) means P in parallel with Q, Several semantics are given for (P || Q) in the 1985 book, none of them in anyway respect the above-stated convention regarding channels. In fact all are presented before the notion of channel is introduced. Any number of processes may synchronise on a single event in CSP, and hence it is equally easy to develop a convention for broadcast communications in CSP. >but I don't see (P >> Q). This is the piping operator introduced on p151. It means: run P in parallel with Q, but hide the communication channels from P to Q. It is the basic mechanism for setting up closed communication channels between pairs of processes. It is the sole support in CSP for the convention quoted above. -- Brendan Mahony | brendan@batserver.cs.uq.oz Department of Computer Science | heretic: someone who disgrees with you University of Queensland | about something neither of you knows Australia | anything about.
kremer@cs.utwente.nl (Harro Kremer) (06/14/91)
In article <DLS.91Jun11202329@achilleus.austin.ibm.com>, dls@achilleus.austin.ibm.com (David Skeen) writes: |> Is the example wrong, or my understanding of it? The example is correct. The parallel operator used in Bag is the |||, which is called the interleaving operator. Expressions on both sides of the operator do not synchronize at any gate. This value matching at the ouput gate between recursive instances of Bag is thus not possible. The characteristic of a bag that it can output its element in a different order that they were put into it is important. It distinguishes for example a bag from a set. The specification would be different for a fifo-queue. Harro -- ___ Harro Kremer <kremer@cs.utwente.nl> __/ \__________ | \___/ | Univ. of Twente, Dept. Computer Science, TIOS-group |___ __ ___ | P.O. Box 217, NL-7500 AE Enschede, The Netherlands | | | / \ (__ | tel: +31 53 89 3755 fax: +31 53 333815 | | | \__/ ___) | | | Freedom's just another word for nothing left to lose. |_________________| - Janis Joplin -
dls@achilleus.austin.ibm.com (David Skeen) (06/15/91)
I have had some e-mail responses which pointed out my mistake. I was equating process Bag[input,output] := input ?x:elem; (Bag[input,output] ||| output !x; stop) endproc with process Bag[input,output] := input ?x:elem; (Bag[input,output] || output !x; stop) endproc In the former case, ||| disallows any interaction at output between recursive instances of Bag; in the latter case, || would allow such interactions. Many thanks to those who explained this to me. -- 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