Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!romp!auschs!awdprime!awdprime.austin.ibm.com!dls From: dls@achilleus.austin.ibm.com (David Skeen) Newsgroups: comp.specification Subject: Problem with LOTOS specification Message-ID: Date: 12 Jun 91 00:23:29 GMT Sender: news@awdprime.UUCP Reply-To: David Skeen Organization: IBM Austin (PSP) Lines: 38 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