|
|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
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:
lotos.open [lotos_opt] spec[.lotos] [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:
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 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 lotos_opt, if any, are passed to caesar and to caesar.adt .
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.
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.
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.
The options below specify the kind of reduction of spec.
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.
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.
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.
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 this case, result.bcg is a deterministic Labelled Transition System, which is trace equivalent to spec.
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).
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 advice from Hubert Garavel and Radu Mateescu.
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.