Fwd: Workunits (non-blocking)

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
>