Compression converts a labelled-transition system (LTS) into an equivalent LTS
that, hopefully, is smaller and thus more efficient to use in a check.
Generally, one of the many compression functions that FDR provides is applied to
a component of a parallel composition. For example, normal is one
commonly-used compression functions, as could, for instance be applied as
normal(Q) ||| R. Compression will have little affect on a process that
contains no hiding. Thus, it makes sense to compress a process that has just had
a significant amount of hiding applied to it. For example, if P \ A is used
at some point in a system and A contains a large number of the events P
can perform, then compressing P \ A may significantly reduce size of the
system that needs to be verified. Intuitively, compression removes the hidden
events in such a way as to preserve sufficient behaviour, but not too much. This
also implies that it is worth hiding as much as possible as early as possible
(i.e. as far down the process tree as possible), since that gives compression
more options to remove events.
Note it is not worth compressing a whole system. For example, when
verifying if Q is deadlock-free, there is no point in verifying
normal(Q) is deadlock-free instead, since FDR has to traverse the whole of
Q to construct the normalised version anyway.
FDR provides many compression functions, as listed in Compression Functions, all
of which are CSPM functions of type (Proc) -> Proc. Generally, the most
useful functions to apply are normal, wbisim, and the function
sbdia(P) = sbisim(diamond(P)) which combines sbisim and
diamond. Further advice on how to choose a compression function is given
in Compression Functions, but note that it is difficult to predict in advance
which compression function will be most effective, and thus some experimentation
will be required. The best method of assessing the effectiveness of compressions
is to use the machine structure viewer,
which can display details regarding the number of states and transitions that
are saved by compression.
A more advanced usage of compression is inductive compression. In this, the system is constructed in stages, with each intermediate stage being compressed. For example, when modelling a token ring, only the events on the very left-most and very right-most processes must not be hidden. Therefore, the system can be constructed inductively by taking the existing system, adding one more node, hiding the events between the old system and the new node, and then compressing it. Understanding Concurrent Systems describes this in more detail. Further, the file Inductive Compression contains some utility functions, written by Roscoe, for constructing systems in such a way.