REDUCTOR manual page
Table of Contents

Name

reductor - BCG graph generation using reachability analysis combined with on-the-fly reduction

Synopsis

bcg_open [bcg_opt] spec[.bcg] [cc_opt] reductor [reductor_opt] result[.bcg]

or:

caesar.open [caesar_opt] spec[.lotos] [cc_opt] reductor [reductor_opt] result[.bcg]

or:

exp.open [exp_opt] spec[.exp] [cc_opt] reductor [reductor_opt] result[.bcg]

or:

fsp.open [fsp_opt] spec[.lts] [cc_opt] reductor [reductor_opt] result[.bcg]

or:

lnt.open [lnt_opt] spec[.lnt] [cc_opt] reductor [reductor_opt] result[.bcg]

or:

seq.open [seq_opt] spec[.seq] [cc_opt] reductor [reductor_opt] result[.bcg]

Description

This program performs exhaustive reachability analysis and generates the Labelled Transition System corresponding to the BCG graph spec.bcg, the LOTOS program spec.lotos, the composition expression spec.exp, the FSP program spec.lts, the LNT program spec.lnt, or the sequence file spec.seq.

During the generation, this Labelled Transition System is reduced on-the-fly with respect to a relation chosen among strong equivalence, tau-divergence, tau-compression, tau-confluence, tau*.a equivalence, safety equivalence, trace equivalence, or weak trace equivalence. The resulting Labelled Transition System is encoded in the BCG format and stored into file result.bcg.

For most of the above relations, the reductor tool allows two levels of reduction:

By default, reductor performs only partial reduction. Total reduction can be done using the -total option (see OPTIONS below).

Note: The eight relations implemented in reductor are partially ordered from the strongest (strong bisimulation) to the weakest (weak trace equivalence) as follows. We include branching bisimulation and observational equivalence in this picture, although they are not implemented in reductor.

                         strong
                            |
                      +-----+-----+
                      |           |
                      |     tau-divergence
                      |           |
                      |     tau-compression
                      |           |
                      |     tau-confluence
                      |           |
                    trace    (branching)
                      |           |
                      |      +----+----+
                      |      |         |
                      |   tau*.a (observational)
                      |      |         |
                      |      +----+----+
                      |           |
                      |        safety
                      |           |
                      +-----+-----+
                            |
                        weak trace

Note: The above order shows that branching bisimulation (and weaker relations) is preserved by tau-divergence, tau-compression, and tau-confluence. Although branching bisimulation is not implemented in reductor, tau-divergence, tau-compression and tau-confluence can thus be used as preprocessing steps for branching bisimulation minimization, which itself can be done using bcg_min .

Note: The tau-divergence, tau-compression, and tau-confluence reductions remove some of the internal transitions, and the tau*.a, safety, and weak trace reductions remove all internal transitions present in the Labelled Transition System. These transitions are usually called tau-transitions in the literature, and are displayed as the character string "i" by the various BCG tools.

Note: Although they reduce the number of states and they eliminate all tau-transitions, the tau*.a and safety reductions may increase the total number of transitions. The weak trace reduction may even increase the total number of states as it determinizes the Labelled Transition System.

Options

The options bcg_opt, if any, are passed to bcg_lib .

The options caesar_opt, if any, are passed to caesar and to caesar.adt .

The options exp_opt, if any, are passed to exp.open .

The options fsp_opt, if any, are passed to fsp.open .

The options lnt_opt, if any, are passed to lnt.open .

The options seq_opt, if any, are passed to seq.open .

The options cc_opt, if any, are passed to the C compiler.

The options reductor_opt currently available are described below.

The options below specify the equivalence relation used for reducing (partially or totally) spec.

-safety
Generate in result.bcg a Labelled Transition System (partially or totally) reduced modulo safety equivalence [BFG+91]. Partial safety reduction both eliminates the tau-transitions and cuts the redundant transitions (as defined in [Mou92]) of spec. See also the bisimulator manual page for a formal definition of safety equivalence. Not a default option.

-strong
Generate in result.bcg a Labelled Transition System (partially or totally) reduced modulo strong equivalence [Par81]. Partial strong reduction replaces duplicate transitions (i.e., transitions with same source state, target state, and label) by a single transition. See also the bisimulator manual page for a formal definition of strong bisimulation. Not a default option.

-taucompression
Generate in result.bcg a Labelled Transition System (partially or totally) reduced modulo tau-compression. Partial tau-compression reduction eliminates all strongly connected components of tau-transitions.

Partial tau-compression reduction is usually fast (linear in the size of the Labelled Transition System). Tau-compression reduction preserves branching bisimulation. Not a default option.

-tauconfluence
Generate in result.bcg a Labelled Transition System (partially or totally) reduced modulo tau-confluence [PLM03], which is a partial order reduction preserving branching bisimulation. Tau-confluence subsumes tau-compression, thus leading to potentially stronger reductions, but it can be slower. Not a default option.

-taudivergence
Generate in result.bcg a Labelled Transition System (partially or totally) reduced modulo tau-divergence. Partial tau-divergence reduction replaces each strongly connected component of tau-transitions by a self-looping tau-transition.

Partial tau-divergence reduction is usually fast (linear in the size of the Labelled Transition System). Tau-divergence reduction preserves both branching bisimulation and the livelocks of spec.

-taustar
Generate in result.bcg a Labelled Transition System reduced modulo tau*.a equivalence [FM91]. Partial tau*.a reduction eliminates the tau-transitions of spec. See also the bisimulator manual page for a formal definition of tau*.a equivalence. Default option (for backward compatibility with versions 1.* to 3.* of reductor).

-trace
Generate in result.bcg a Labelled Transition System reduced modulo trace equivalence. Partial trace reduction determinizes spec using a classical automata determinization algorithm, see section ABOUT TRACE AND WEAK TRACE EQUIVALENCES below for more details. This option is not compatible with -total. Not a default option.

-weaktrace
Generate in result.bcg a Labelled Transition System reduced modulo weak trace equivalence. Partial weak trace reduction eliminates the tau-transitions of spec and determinizes it using a classical automata determinization algorithm, see section TRACE AND WEAK TRACE EQUIVALENCES below for more details. This option is not compatible with -total. Not a default option.

The options below specify the kind of reduction of spec.

-partial
Perform partial reduction. Default option.

-total [ -class ]
Perform total reduction instead of partial reduction. The Labelled Transition System generated in result.bcg is thus both partially reduced for the chosen relation and minimized modulo strong bisimulation.

If the -class option is set, display the classes of strongly bisimilar states of the partially reduced Labelled Transition System on standard output. Not a default option.

Note: Although it yields generally smaller Labelled Transition Systems, the -total option often slowers the generation.

The options below specify various features available in addition to the reduction of spec.

-monitor
Open a window for monitoring in real-time the generation of result.bcg.

-hide [ -total | -partial | -gate ] hiding_filename
Use the hiding rules defined in hiding_filename to hide (on the fly) the labels of the Labelled Transition System being generated. See the caesar_hide_1 manual page for a detailed description of the appropriate format for hiding_filename.

The -total, -partial, and -gate options specify the "total matching", "partial matching", and "gate matching" semantics, respectively. See the caesar_hide_1 manual page for more details about these semantics. Option -total is the default.

Note that label hiding does not operate on spec, but on the Labeled Transition System resulting from the reduction of spec. As a consequence, result.bcg may be not minimal with respect to the chosen relation.

-rename [-total|-single|-multiple|-gate] renaming_filename
Use the renaming rules defined in renaming_filename to rename (on the fly) the labels of the Labelled Transition System being generated. See the caesar_rename_1 manual page for a detailed description of the appropriate format for renaming_filename.

The -total, -single, -multiple, and -gate options specify the "total matching", "single partial matching", "multiple partial matching", and "gate matching" semantics, respectively. See the caesar_rename_1 manual page for more details about these semantics. Option -total is the default.

Note that label renaming does not operate on spec, but on the Labeled Transition System resulting from the reduction of spec. As a consequence, result.bcg may be not minimal with respect to the chosen relation.

As for the bcg_labels tool, several hiding and/or renaming options can be present on the command-line, in which case they are processed from left to right.

-uncompress, -compress, -register, -short, -medium, -size
These options control the form under which the BCG graph result.bcg is generated. See the bcg manual page for a description of these options.

-tmp
This option specifies the directory in which temporary files are to be stored. See the bcg manual page for a description of this option.

About Trace and Weak Trace Equivalences

The algorithm used to reduce spec modulo trace and weak trace equivalences is the classical "subset construction" algorithm used to determinize finite automata [ASU86]. Each state S of result.bcg corresponds to a set of states {s1, ..., sn} belonging to the input Labelled Transition System spec.

Starting from the initial state of result.bcg, which is the singleton set containing the initial state of spec, the transitions going out of each state S of result.bcg are computed as follows:

Exit Status

Exit status is 0 if everything is alright, 1 otherwise.

Diagnostics

When the source is erroneous, error messages are issued.

Bibliography

[ASU86]
A. V. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques and Tools. Addison-Wesley, 1986.

[BFG+91]
A. Bouajjani, J-C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis. Safety for Branching Time Semantics. In Proceedings of 18th ICALP. Springer Verlag, July 1991.

[FM91]
J-C. Fernandez and L. Mounier. ``On the Fly'' Verification of Behavioural Equivalences and Preorders. In K. G. Larsen and A. Skou (Eds.), Proceedings of the 3rd Workshop on Computer-Aided Verification CAV'91 (Aalborg, Denmark), Lecture Notes in Computer Science vol. 575. Springer Verlag, July 1991.

[Mou92]
Laurent Mounier. Methodes de verification de specifications comportementales : etude et mise en oeuvre. PhD thesis, Universite Joseph Fourier, Grenoble 1, 1992.

[Par81]
D. Park. Concurrency and Automata on Infinite Sequences. In Peter Deussen (Ed.), Theoretical Computer Science, Lecture Notes in Computer Science vol. 104, pages 167-183. Springer Verlag, March 1981.

[PLM03]
G. Pace, F. Lang, and R. Mateescu. Calculating Tau-Confluence Compositionally. In W.A. Hunt Jr and F. Somenzi (Eds.), Proceedings of the 15th Computer-Aided Verification conference CAV'2003 (Boulder, Colorado, USA), Lecture Notes in Computer Science vol. 2725. Springer Verlag, July 2003. Available from http://cadp.inria.fr/publications/Pace-Lang-Mateescu-03.html

Authors

Versions 1.*, 2.*, and 3.* of reductor have been developed by Hubert Garavel.

Version 4.* of reductor was developed by Frederic Lang and Radu Mateescu (INRIA Rhone-Alpes).

Version 5.* of reductor, merging features previously belonging to determinator , was developed by Frederic Lang, with advices of Hubert Garavel and Radu Mateescu.

Operands

spec.bcg
BCG graph (input)

spec.exp
network of communicating LTSs (input)

spec.lotos
LOTOS specification (input)

spec.lts
FSP specification (input)

spec.lnt
LNT specification (input)

spec.seq
sequence file (input)

Files

The binary code of reductor is available in $CADP/bin.`arch`/reductor.a

See the caesar_hide_1 , caesar_rename_1 , bcg_labels manual pages for a description of hiding and renaming conventions.

See Also

OPEN/CAESAR Reference Manual, bcg_open , bcg , caesar.open , caesar , caesar.adt , exp.open , fsp.open , lnt.open , seq.open

Additional information is available from the CADP Web page located at http://cadp.inria.fr

Directives for installation are given in files $CADP/INSTALLATION_*.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.

Bugs

Please report new bugs to cadp@inria.fr


Table of Contents