[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: CSP-OZ Backtracking.

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
Maybe you could post a very short schema so that we can see what is
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.

Dr A E Lawrence