[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Assistance requested on a Hoare-y problem - corrected and cleaned up...
Well - the formatting was a disaster...and there was an unnecessary step...
"G. S. Stiles" wrote:
> Greetings -
>
> In my formatting below, I write the expression a -> (P || Q) as
>
> a -> (P
> ||
> Q)
> etc.
>
> 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
>
Note: the alphabet of NOISYVM includes toffee... but NOISYVM does not
do toffee.
>
> 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)
>
> 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:
>
> 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???
> It was certainly more fun than the lecture I was working on.
>
> 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
> ======================================================================
--
======================================================================
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
======================================================================