A E Lawrence wrote:
Jim Davies wrote:The `standard' language of CSP - being the one defined in the original book, which is essentially the same as the one used in Roscoe's book, which is again the same as the one used in Schneider's book (the differences are cosmetic) doesn't attempt an explicit treatment of * time * priority Actually, Alan Jeffrey showed some years ago that a treatment of either would be a treatment of both, effectively (more specifically: csp + discrete time = csp + priority). When you abstract from time, you are abstracting from priority, and vice versa. But either way, it doesn't have it.
I forgot to add that I think the above identification of priority and time only applies in an interleaving semantics. Of course, original pure CSP is based on an interleaving semantics. Indeed, that is one gloss we can give nowadays to the word "sequential" in the name which we may otherwise think to be an anachronism.
But when we are modelling a synchronous circuit in full detail, interleaving semantics is inadequate. But it is possible to add true concurrency into CSP with very little change including retention of traces.
Of course, you can no longer have ( a -> Stop) ||| (b -> Stop) = (a -> b -> Stop) [] (b -> a -> Stop) in general. When true concurrency is present there is another possibility:a and b happening together. Furthermore, most implementations, in hardware at least will be "eager" : that is perform a and b together if they are both offered. In HCSP there is an eager refinment of ||| that does exactly that. All this works out with very little change to standard CSP. And if you have an (global) alphabet which excludes concurrent events -- then you get standard CSP back. And the equation above holds again.
I expect to present that and more at CPA2002 :-) Adrian -- Dr A E Lawrence