W3C home > Mailing lists > Public > public-ws-chor@w3.org > March 2005

Fwd: Workunits (non-blocking)

From: Steve Ross-Talbot <steve@enigmatec.net>
Date: Thu, 3 Mar 2005 11:54:43 +0000
To: Kohei Honda <kohei@dcs.qmul.ac.uk>
Message-Id: <d80b54d78e54f0c13e4076d95b604cf0@enigmatec.net>
Cc: "'WS-Choreography List'" <public-ws-chor@w3.org>, Gary Brown <gary@enigmatec.net>
Dear Kohei,

please ignore the previous email on workunits. I now state what the 
actual operational semantics are as agreed by the working group at the 
F2F this Monday and Tuesday.

If there are any potential problems with this can you let us know my 
emailing the group itself on the public mailing list in the cc-line 
above.




Best regards

Steve T




Begin forwarded message:

> From: Steve Ross-Talbot <steve@enigmatec.net>
> Date: 28 February 2005 20:27:59 GMT
> To: Kohei Honda <kohei@dcs.qmul.ac.uk>
> Cc: Gary Brown <gary@enigmatec.net>
> Subject: Workunits (non-blocking)
>
> Dear Kohei,
>
>
> Workunit (G) (R)
> 	Body
>
> Then a typical evaluation proceeds as follows
> 	(G) Body (R G) Body (R G) Body
>
> Where G is the guard condition and R is the repeat condition a Body is 
> the body of code inside the workunit
>
> Thus it is really modeled in the following three cases
>
> 	IF G and R are not empty and so need evaluation THEN:
>
> 	while (G)
> 	{	
> 		Body
> 	} until (R)
>
> 	IF G is always T THEN:
>
> 	repeat
> 	{
> 		Body
> 	} until (R)
>
> 	IF R is always F THEN:
>
> 	if (G)
> 	{
> 		Body
> 	}
>
> Does this clarify the semantic of the non-blocking workunit enough to 
> make it non-problematic for model checking?
>
> Cheers
>
> Steve T
>



Received on Thursday, 3 March 2005 11:57:14 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:01:07 UTC