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**] ## 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**. ## Options

The options *bcg_opt*, if any, are passed to **bcg_lib**
. ## 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*. ## Exit Status

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

When the source is
erroneous, error messages are issued.
## Bibliography

## Authors

## Operands

## Files

## See Also

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

Please report new bugs to cadp@inria.fr

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**]

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:

*Partial reduction*just compresses, cuts, or merges transitions of*spec*in a way that preserves the given relation. In general, partial reduction does not yield a minimal Labelled Transition System.*Total reduction*additionally merges on-the-fly all strongly bisimilar states of the partially reduced Labelled Transition System into a unique representative state. Total reduction thus yields a Labelled Transition System that is minimal modulo strong bisimulation. In general, total reduction does not necessarily yield a Labelled Transition System that is minimal modulo the chosen relation, except in some cases such as tau*.a and safety equivalences.

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.

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.

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:

- In case of trace reduction, for each label
*L*, there exists a transition*S*--*L*-->*S'*if and only if the set*S'*= {*s'*| exists*s*in*S*such that*s*--*L*-->*s'*} is not empty.In this case,

*result***.bcg**is a deterministic Labelled Transition System, which is trace equivalent to*spec*. - In case of weak trace
reduction, for each visible label
*L*, there exists a transition*S*--*L*-->*S'*if and only if the set*S'*= {*s'*| exists*s*in*S*such that*s*--tau*.*L*-->*s'*} is not empty, where "tau" denotes the invisible label. This definition expresses that each transition in*result***.bcg**results from zero or more invisible transitions followed by a visible one.In this case,

*result***.bcg**is a deterministic Labelled Transition System, does not contain invisible transitions, and is weakly trace equivalent to*spec*(i.e., it contains the same transition sequences as*spec*by considering only visible transitions).

- [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

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.

*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)

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.

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.**