Re: CSP-OZ Backtracking.

[A E Lawrence <adrian.lawrence@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>]

lsfreitas@xxxxxxxxxx wrote:
> 
> Hi!
> 
> I am studing an CSP-OZ to Java traduction laws to make a real specification
> executable before real development.
> Much of the work has been done but we found a problem that I like to hear some
> comments about:
> It's like a kind of comunication/synchronization handshaken
> 
> 1) In the CSP-Z notation there is a guard condition for all CSP event, so, when
> one event synchronized with other (say in a parallel composition), that guard
> must be satisfacted, otherwise, no comunication is allowed at all.


I am not very familiar with OZ (we *are* talking about Object-Z as
presented by Duke and Rose?), but I do know a little Z. And I don't
follow "there is a guard condition for all CSP event"?

How would you write    P = a --> Skip ? 

Do you have to add some boolean which must be set true to obtain the
above?
Maybe you could post a very short schema so that we can see what is
involved.
Or perhaps everyone one else on this list knows what this means, in
which case just ignore me :-)

Oh, and I suspect that there is a connection with angelic vs demonic
nondeterminism in your speculative execution and backtracking.

Adrian
-- 
Dr A E Lawrence