4.3 Choice of Model

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.

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.