Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!ut-emx!ibmchs!auschs!awdprime!awdprime.austin.ibm.com!dls
From: dls@achilleus.austin.ibm.com (David Skeen)
Newsgroups: comp.specification
Subject: Re: Problem with LOTOS specification
Message-ID: <DLS.91Jun14163311@achilleus.austin.ibm.com>
Date: 14 Jun 91 20:33:11 GMT
References: <DLS.91Jun11202329@achilleus.austin.ibm.com>
Sender: news@awdprime.UUCP
Reply-To: David Skeen <dls@dce.austin.ibm.com>
Organization: IBM Austin (PSP)
Lines: 24
In-reply-to: dls@achilleus.austin.ibm.com's message of 12 Jun 91 00:23:29 GMT

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