Thread View: comp.specification
6 messages
6 total messages
Started by David Skeen
Wed, 12 Jun 1991 00:23
Problem with LOTOS specification
Author: David Skeen
Date: Wed, 12 Jun 1991 00:23
Date: Wed, 12 Jun 1991 00:23
38 lines
1992 bytes
1992 bytes
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
Re: Problem with LOTOS specification
Author: Brendan Mahony
Date: Wed, 12 Jun 1991 23:55
Date: Wed, 12 Jun 1991 23:55
14 lines
1158 bytes
1158 bytes
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.
Re: Problem with LOTOS specification
Author: David Skeen
Date: Thu, 13 Jun 1991 14:50
Date: Thu, 13 Jun 1991 14:50
16 lines
1476 bytes
1476 bytes
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.com
Re: Problem with LOTOS specification
Author: Brendan Mahony
Date: Fri, 14 Jun 1991 04:18
Date: Fri, 14 Jun 1991 04:18
34 lines
2168 bytes
2168 bytes
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.
Re: Problem with LOTOS specification
Author: Harro Kremer
Date: Fri, 14 Jun 1991 13:53
Date: Fri, 14 Jun 1991 13:53
25 lines
1705 bytes
1705 bytes
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 -
Re: Problem with LOTOS specification
Author: David Skeen
Date: Fri, 14 Jun 1991 20:33
Date: Fri, 14 Jun 1991 20:33
24 lines
1322 bytes
1322 bytes
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
Thread Navigation
This is a paginated view of messages in the thread with full content displayed inline.
Messages are displayed in chronological order, with the original post highlighted in green.
Use pagination controls to navigate through all messages in large threads.
Back to All Threads