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

RE: CSP-OZ Backtracking.


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.


>	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

>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
>          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.