The hierarchy of models for CSP are useful because they provide differing amount of information about the processes, with a corresponding change in the cost of working in that model. It is more efficient to perform a check in the simplest model which provides the required detail.
Property Model
Safety Traces
Liveness Failures Deadlock-freedom
Livelock-freedom Failures-divergence
Note that the model_compress operation may produce better results
in a simple process model.
Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.