RE: CSP-OZ Backtracking.

[lsfreitas@xxxxxxxxxx]

Hi!

This is the point but I am not tring to find or derive some new theory... :)

The point is in the implementation (Java) version of the specification, we will
need this kind of behaviour. 
Note that we are interchanging CSP and Object-Z. The Object-Z part of the specification
(that belongs to data definition
) will introduce some data guards (the one that should be satisfacted to the
comunitation to take place or backtrack otherwise). 
So the backtracking condition was introduced by the combined CSP-OZ specification
not by other kind of CSP-OZ.

... 

bye
Leo
				
>	Hi
>
>> I am trying to implement an kind of backtracking the CSP comunication,
>> like
>> 
>It sounds like you want a CSP in which a process may engage
>in an event speculatively, hoping that the other processes will
>eventually confirm their participation.  If they in fact decline, then
>the invalidated event would have to be rolled back.
>
>I don't know of such a CSP theory, maybe one of the theoretical types
>could comment.  But it seems like you could define such a theory.
>Perhaps you could come up with a set of re-writing rules which
>compile "tentative" events into sets of events of the conventional
>variety.
>


>For example, if you wanted, say one level of (the compiler types
>would say) look-ahead, the tenatative CSP processes
>
>	P  ||  Q  Where P= (A [] B])      and Q=  A < some_condition >C
>
>might speculatively allow P to transition to A based on the *hope* that
>Q will choose A.  If the some_condition term evaluates to TRUE, the
>the transition would become, in some sence "real".  But if it evaluates
>to FALSE, then P would have to backtrack back to the alt and engage
>in B.  You could get this kind of behavior by re-writing the processes
>as:
>
>          P=  (A1 -> (A2 [] (C1 -> B))) [] B
>
>and   Q= (A2 < some_condition >C1)
>
>Where A1,A2 are drived from A, C1 from C.
>
>I suspect that for some pre-determined level of look-ahead, re-writing
>rules could always be derived.......If its not already invented, maybe it 

>should be.
>-jc
>
>
				
http://webmail.svn.com.br