1.4. Further operators
Many programming languages have the concept of sequential composition. P;Q does whatever P does until it terminates, and then does what Q does. This makes sense in the world of CSP – what the process ‘does’ is to communicate with its environment – provided we understand what ‘terminates’ means. CSP programs can stop communicating for a variety of reasons, such as reaching the state Stop, deadlocking some other way, or getting into some race condition. All of these really correspond to the process getting stuck in some way rather than terminating gracefully, and while you can imagine wanting some operator that handles errors in a process P by passing control on to a second one Q, it would not be an ordinary sequential composition. ...
Get The Modelling and Analysis of Security Protocols: the CSP Approach now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
