[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.
>> I am trying to implement an kind of backtracking the CSP comunication,
>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