5.1.1 Methods of compression

FDR2 currently provides six different methods of taking a transition system (or state machine) and attempting to compress it into a more efficient one. Each compression function must first be declared by the transparent operator before it can be used (see A.6.2 Transparent). The functions must be spelt exactly as given below or the relevant operation will not take place -- in fact, since they are transparent, FDR will ignore an unknown function (i.e., treat it as the identity function) and simply give a warning in the status window (see 2.7 Options).

explicate

Enumeration: by simply tabulating the transition system, rather than deducing the operational semantics "on the fly". This obviously cannot reduce the number of nodes, but does allow them to be represented by small (integer) values, as opposed to a representation of their natural structure. This in turn makes subsequent manipulations substantially faster.

sbisim

Strong, node-labelled, bisimulation: the standard notion enriched (as discussed in [Roscoe94]) by the minimal acceptance and divergence labelling of the nodes. This was used in FDR1 for the final stage of normalising specifications.

tau_loop_factor

-loop elimination: since a process may choose automatically to follow a action, it follows that all the processes on a -loop (or, more properly, in a strongly connected component under -reachability) are equivalent.

diamond

Diamond elimination: this carries out the node-compression discussed in the last section systematically, so as to include as few nodes as possible in the output graph. This is perhaps the most novel of the techniques, and the technical details are discussed in 5.2.2.2 Diamond elimination.

normalise

Normalisation: discussed extensively elsewhere,(11) this can give significant gains, but it suffers from the disadvantage that by going through powerspace nodes it can be expensive and lead to expansion.

Normalisation (as described in 1.3.3 Checking refinement) is essential (and automatically applied, if needed) for the top level of the left-hand side of a refinement check, but in FDR2 is made available as a general compression technique through the transparent function normalise. (For historical reasons, this function is also available as normal and normalize.)

model_compress

Factoring by semantic equivalence: the compositional models of CSP we are using all represent much weaker congruences than bisimulation. Therefore, if we can afford to compute the semantic equivalence relation over states it will give better compression than bisimulation to factor by this equivalence relation.

It makes sense to factorise only by the model in which the check is being carried out. This is therefore made an implicit parameter to a single transparent function model_compress. The technical details of this method are discussed in 5.2.2.1 Computing semantic equivalence.

Both -loop elimination and factoring by a semantic equivalence use the notion of factoring a GLTS by an equivalence relation; details can be found in [RosEtAl95].

Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.