[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Assistance requested on a Hoare-y problem
Dyke,
What a quick response! Sunday is my CSP day, so I'll look at it then.
Thanks.
Roy
--
Roy Wilson
E-mail: designrw@xxxxxxxxxxxxxxxx
On 1/7/01, 2:23:21 PM, "G. S. Stiles" <dyke.stiles@xxxxxxxxxxx> wrote
regarding Re: Assistance requested on a Hoare-y problem:
> Greetings -
> In my formatting below, I write the expression a -> (P || Q) as
> a -> (P
> ||
> Q)
> Roy Wilson wrote:
> >
> >
> > Hi,
> >
> > I'm working my way through Hoare's Communicating Sequential Processes
book. I
> > am semi-stuck on Example X1 on p. 69. It seems that the chief tool ought
to be
> > L6 on p. 71, but I've had no luck.
> >
> > I have done graduate work (in the US :-)) in theory of computation,
category
> > theory, and the kind of stuff in Appendix A of Roscoe's book, so I'm not
a
> > stranger to symbolic manipulation, despite my possible stupidity in this
> > matter.
> >
> > If anyone who has actually done a line by line derivation would care to
> > communicate the first and second lines (please, no use of "clearly" :-))
of
> > the proof, I'd be most appreciative.
> >
> > Roy
> >
> > Roy Wilson
> > designrw@xxxxxxxxxxxxxxxx
> NOISYVM = (coin -> clink -> choc -> clunk -> NOISYVM)
> CUST = (coin -> (toffee -> CUST | curse -> choc -> CUST))
> NOISYVM || CUST = (coin -> clink -> choc -> clunk -> NOISYVM)
> ||
> (coin -> (toffee -> CUST | curse
->
> choc -> CUST))
> by L4A: = coin -> (clink -> choc -> clunk -> NOISYVM)
> ||
> (toffee -> CUST | curse ->
choc
> -> CUST)
> by L6: = coin -> (clink -> ((choc -> clunk -> NOISYVM)
> ||
> (toffee ->
CUST
> | curse -> choc -> CUST))
> |
> (toffee -> ((clink -> choc
->
> clunk -> NOISYVM)
> ||
> CUST))
> Since NOISYVM cannot engage in toffee, but any occurrence of toffee must
> involve both NOISYVM and CUST - since it appears in both alphabets - the
event
> toffee
> can never occur - leading to
> NOISYVM || CUST = coin -> (clink -> (choc -> clunk ->
> NOISYVM))
> ||
> (curse ->
choc ->
> CUST)
> Using L6 again:
> NOISYVM || CUST = coin -> (clink -> ((choc -> clunk ->
> NOISYVM)
>
||
> (curse -> choc -> CUST)))
> |
> (curse ->
> ((clink -> choc -> clunk -> NOISYVM)
>
||
> (choc -> CUST)))
> Applying L5B to the first component of the |, and L5A to the second:
> (NOISYVM || CUST) = coin -> (clink -> curse -> ((choc -> clunk ->
> NOISYVM)
> ||
> (choc -> CUST)))
> |
> (curse -> clink
> -> ((choc -> clunk -> NOISYVM)
> ||
> (choc -> CUST)))
> Applying L4A twice to both ||:
> NOISYVM || CUST = coin -> (clink -> curse -> choc -> clunk ->
> (NOISYVM
> ||
> CUST))
> |
> (curse -> clink
->
> choc -> clunk -> (NOISYVM
> ||
> CUST))
> NOISYVM || CUST = uX.(coin -> ((clink -> curse -> choc -> clunk -> X)
> |
> (curse -> clink
->
> choc -> clunk -> X))
> Does this do it???
> Dyke.
> --
> ======================================================================
> Dyke Stiles >>>>>> new address!!>>> dyke.stiles@xxxxxxxxxxx
> Professor and Chair, Graduate Committee
> Department of Electrical and Computer Engineering
> Utah State University
> 4120 Old Main Hill
> Logan UT 84322-4120
> Voice: +1-435-797-2840 FAX: +1-435-797-3054
> Research: http://www.engineering.usu.edu/ece/research/rtpc/
> Play: http://www.engineering.usu.edu/ece/research/rtpc/utah/utah.html
> ======================================================================