BCG_CMP manual page

Table of Contents## Name

bcg_cmp - equivalence comparison of normal, probabilistic, or stochastic
labeled transitions systems (LTS) encoded in the BCG format
## Synopsis

**bcg_cmp**
[*bcg_options*] [**-strong** | **-branching** | **-divbranching** | **-observational** | **-sharp** [**-total**
| **-partial** | **-gate**] *sharp_filename*] | **-divsharp** [**-total** | **-partial** | **-gate**] *sharp_filename*]
[**-normal** | **-prob** | **-rate** [**-self**]] [**-epsilon** *eps*] [**-format** *format_string*] [**-class**
*class_file*] [**-diag** [**-bfs**|**-dfs**] *diag_file***.bcg**] *input_1***.bcg** *input_2***.bcg** ## Description

**bcg_cmp** implements various algorithms
to perform comparison of graphs encoded in the BCG format according to
strong bisimulation, branching bisimulation, divbranching bisimulation,
observational equivalence, sharp bisimulation, or divsharp bisimulation.
A graph input by **bcg_cmp** can be:
## General
Options

The following *bcg_options* are currently supported: **-version**, **-create**,
**-update**, **-remove**, **-cc**, **-tmp**, **-uncompress**, **-compress**, **-register**, **-short**, **-medium**,
and **-size**. See the **bcg**
manual page for a description of these options.
## Particular Options

The following options are also supported:
## Environment Variables

See the **bcg**
manual page for a description
of the environment variables used by all the BCG application tools.
## Exit
Status

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

**bcg_cmp**
was developped by Frederic Lang (INRIA/CONVECS). It shares a substantial
amount of code with **bcg_min**. See the **bcg_min**
manual page for more
information.
## Operands

## Files

## See
Also

**bcg**
, **bcg_min**
, **seq**
, **sprintf**(3C) ## Bugs

Please report bugs to cadp@inria.fr.

where *bcg_options*
is defined below (see GENERAL OPTIONS).

**bcg_cmp** takes as inputs the BCG
graphs *input_1***.bcg** and *input_2***.bcg**, and compares these graphs according to
some bisimulation relation.

- either a "normal" LTS, whose transitions
are either labelled with "normal" labels or with the "internal" label (usually
noted "tau" in the scientific literature and displayed as the character
string "
`i`

" by the various BCG tools), - or a "probabilistic LTS": these
are LTS with "normal" labelled transitions, as well as "special" transitions,
whose labels are either of the form "
`prob %p`

" or "*label*`; prob %p`

", where`%p`

denotes a floating-point number in the range ]0..1] and*label*denotes a character string that does not contain the "`;`

" character. For each state, the sum of "`%p`

" values on special transitions leaving the state must be less or equal than 1 (see ANNEX 1 of the**bcg_min**manual page for a discussion on how the probabilistic LTS model generalizes other theoretical models published in the literature), - or a "stochastic LTS": these are LTS with
"normal" labelled transitions, as well as "special" transitions, whose
labels are either of the form "
`rate %f`

" or "*label*`; rate %f`

", where`%f`

denotes a strictly positive floating-point number and*label*denotes a character string that does not contain the "`;`

" character (see ANNEX 2 of the**bcg_min**manual page for a discussion on how the stochastic LTS model of**bcg_min**generalizes other theoretical models published in the literature).

**-strong**- Perform
LTS comparison according to strong bisimulation. On (Discrete or Continuous
Time) Markov Chains and on Markov Reward Models, this equivalence agrees
with lumpability of [KS76] (see ANNEX 1, ANNEX 2, and BIBLIOGRAPHY of the
**bcg_min**manual page). Default option. **-branching**- Perform LTS comparison according to branching bisimulation. It is worth noticing that the notion of branching bisimulation is rather meaningless for probabilistic systems. Not a default option.
**-divbranching**- Perform LTS comparison according to divbranching (shorthand for divergence-preserving branching) bisimulation [GW96]. Divbranching bisimulation differs from branching bisimulation only in the way cycles of internal transitions (also called divergences) are treated. It is known that all states traversed by a cycle of internal transitions belong to the same branching equivalence class. While divergences are ignored by ordinary branching bisimulation, they are assimilated to a self-looping internal transition in each such equivalence class by divbranching bisimulation. Unlike branching bisimulation, divbranching bisimulation preserves inevitability properties. Like branching bisimulation, it is worth noticing that the notion of divbranching bisimulation is rather meaningless for probabilistic systems. Not a default option.
**-observational**- Perform LTS comparison according to
observational equivalence [Mil89]. It is worth noticing that observational
equivalence is computationally more expensive than branching bisimulation,
so that comparison may fail even for graphs containing only few thousands
of states. To reduce the risk of failure, in a first step the input graphs
are automatically reduced according to branching bisimulation. This is sound
because branching bisimulation is a graph relation stronger than observational
equivalence. However, this optimisation is not applied if the
**-class**option is set, so that**bcg_cmp**can print the equivalence classes relatively to the states of the input graphs, instead of the states of the branching minimal intermediate graph produced in the first step. This option cannot be combined with neither**-prob**nor**-rate**options. Not a default option. **-sharp [ -total|-partial|-gate ]***sharp_filename*- Perform LTS comparison according to
sharp bisimulation (the variant of the bisimulation defined in [LMM20]
that does not preserve the divergences present in
*input1***.bcg**and*input2***.bcg**), using the rules defined in*sharp_filename*to partition labels between strong and weak actions. See Section FORMAT FOR SHARP LABEL PARTITIONING of the**bcg_min**manual page for details on the syntax of*sharp_filename*. The**-total**,**-partial**, and**-gate**options specify the "total matching", "partial matching", and "gate matching" semantics, respectively.In "total matching" semantics, the regular expressions contained in

*sharp_filename*denote full labels (i.e., gates possibly followed by experiment offers). A label matches if it matches some rule in*sharp_filename*entirely.In "partial matching" semantics, the regular expressions contained in

*sharp_filename*denote substrings of labels. A label matches if it contains a substring that matches some rule in*sharp_filename*.At last, in "gate matching" semantics, the regular expressions contained in

*sharp_filename*denote gates. A label matches if its first word (called gate) matches some rule in*sharp_filename*. In this case, regular expressions in*sharp_filename*should not contain characters forbidden in gate identifiers (e.g., " ", "(", or "!").Option

**-total**is the default.This option cannot be combined with neither

**-prob**nor**-rate**options. Not a default option. **-divsharp [ -total|-partial|-gate ]***sharp_filename*- Perform LTS comparison according to divsharp bisimulation (the variant
of the bisimulation defined in [LMM20] that preserves the divergences present
in
*input1***.bcg**and*input2***.bcg**). See**-sharp**option above for the partitioning of labels between strong and weak actions. This option cannot be combined with neither**-prob**nor**-rate**options. Not a default option. **-normal**- Consider
*input_1***.bcg**and*input_2***.bcg**as normal LTSs. With this option, labels of the form "`rate %f`

" or "*label*`; rate %f`

" or "`prob %p`

" or "*label*`; prob %p`

" are processed as ordinary labels, without special meaning attached. Default option. **-prob**- Consider
*input_1***.bcg**and*input_2***.bcg**as probabilistic LTSs. With this option, each label of the form "`prob %p`

" or "*label*`; prob %p`

" is recognized as denoting a probabilistic transition with probability`%p`

.**bcg_cmp**will stop with an error message if, for some probabilistic transition,`%p`

is out of ]0..1], or if the probabilistic transitions going out of the same state have a cumulated sum strictly greater than 1. With this option, labels of the form "`rate %f`

" or "*label*`; rate %f`

" are processed as ordinary labels. Not a default option. **-rate [ -self ]**- Consider
*input_1***.bcg**and*input_2***.bcg**as stochastic LTSs. With this option, each label of the form "`rate %f`

" or "*label*`; rate %f`

" is recognized as denoting a stochastic transition with rate`%f`

.**bcg_cmp**will stop with an error message if, for some stochastic transition,`%f`

is less or equal to 0. If the**-branching**or the**-divbranching**option is selected, and some state has both an outgoing stochastic transition and an outgoing internal (i.e., "tau") transition,**bcg_cmp**will print a warning and ignore the stochastic transition in order to preserve the notion of maximal progress. With this option, labels of the form "`prob %p`

" or "*label*`; prob %p`

" are processed as ordinary labels. Not a default option.

If**-self**sub-option is given, all self loops (i.e., transitions that remain within the same equivalence class) having labels of the form "`rate %f`

" are ignored. This implements the weak Markovian equivalences described in [Bra02] and [BHKW05]. Not a default sub-option. **-epsilon***eps*- Set the precision
of floating-point comparisons to
*eps*, where*eps*is a real value. When*eps*is out of [0..1[,**bcg_cmp**reports an error. Default value for*eps*is 1E-6. **-format***format_string*- Use
*format_string*to control the format of the floating-point numbers contained in transition labels (these numbers correspond to the occurrences of`%f`

and`%p`

mentioned in section DESCRIPTION above). The value of*format_string*should obey the same conventions as the*format*parameter of function**sprintf**(3C) for values of type`double`

. Default value for*format_string*is`"%g"`

, meaning that floating-point numbers are printed with at most six digits after the "." (i.e., the radix character). Other values can be used, for instance`"%.9g"`

to obtain nine digits instead of six, or by replacing the`"%g"`

flag with other flags, namely`"%e"`

,`"%E"`

,`"%f"`

,`"%G"`

, possibly combined with additional flags (e.g., to specify precision). **-class***class_file*- If
*class_file*is the character '-', then display the equivalence classes on standard output. Otherwise, display the equivalence classes in a file named*class_file*. Not a default option. **-diag [-bfs***|***-dfs]***diag_file***.bcg**- When the comparison of
*input_1*and*input_2*yields FALSE, generate a diagnostic (counterexample) in BCG format (see the**bcg**manual page for details) explaining this result. The diagnostic is generated by the**bisimulator**tool of CADP, in the file*diag_file***.bcg**. This option has no effect when the comparison of input_1 and*input_2*yields TRUE, since in this case the diagnostic would be larger than*input_1*and*input_2*, and would not bring any useful information.Option

**-bfs**or**-dfs**, if present, is passed to**bisimulator**. Option**-bfs**may be slightly slower but generates smaller diagnostics than option**-dfs**. Option**-bfs**is the default option.Note that diagnostics are generated only for comparisons of normal LTSs and according to strong bisimulation, branching bisimulation, divbranching bisimulation, and observational equivalence. In particular, if the

**-diag**option is used in combination with any of the**-sharp**,**-divsharp**,**-prob**, and**-rate**options, then a warning is issued and no diagnostic is generated.The BCG file containing the diagnostic can be visualized using the

**bcg_draw**and**bcg_edit**tools of CADP (see respective manual pages for details).The diagnostic is a directed acyclic graph included (modulo the preorder corresponding to the equivalence relation considered) both in

*input_1*and*input_2*.If the diagnostic is a sequence of transitions, it will also be displayed on standard output using the simple SEQ format (see the

**seq**manual page for the definition of this format). Not a default option.

Note:
Options **-strong**, **-branching**, **-divbranching**, **-sharp**, **-divsharp**, and **-observational**
are mutually exclusive. If they occur simultaneously on the command line,
the option occurring last is selected.

Note: Options **-normal**, **-prob**, and
**-rate** (with or without **-self** sub-option) are mutually exclusive. If they occur
simultaneously on the command line, the option occurring last is selected.

*input_1***.bcg**- BCG graph (input)
*input_2***.bcg**- BCG graph (input)
*input_1***@1.o**- dynamic library (input or output)
*input_2***@1.o**- dynamic library (input or output)

**$CADP/bin.`arch`/bcg_cmp**- ``
**bcg_cmp**'' binary program

See the **bcg**
manual page for a description of the other files.

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