BES_SOLVE manual page
Table of Contents

Name

bes_solve - resolution of boolean equation systems

Synopsis

bes_solve [general_options] input[.bes[.ext]] [bes_options] [block_options] [-sequential|-parallel file[.gcf] [global_options] [instance_options]]

or:

bes_solve [general_options] input[.rbc] [random_options] [bes_options] [block_options] [-sequential|-parallel file[.gcf] [global_options] [instance_options]]

Description

This program computes the value of one or several boolean variables of interest defined in some equation block(s) of a boolean equation system (BES), by applying an algorithm for local (or on-the-fly) resolution of BESs. The value of each boolean variable of interest (TRUE or FALSE) is displayed on the standard output.

The resolution is performed using the sequential algorithms provided by the caesar_solve_1 library of OPEN/CAESAR (see the corresponding manual page and the article [Mat06] for details). The resolution can be also performed using the prototype distributed resolution algorithms described in [JM05,JM06]. Therefore, bes_solve allows to test, cross-check, and study the performance of various local BES resolution algorithms.

The BES under resolution can be represented in two different forms:

Boolean Equation Systems

A BES is a collection of N equation blocks having unique numbers in the range [0..N-1]. A block is a set of recursive equations containing boolean variables in their left-hand sides and boolean formulas (defined over variables and the boolean constants true and false) in their right-hand sides.

A variable Xk defined in a block Bi depends upon a variable Xl defined in a block Bj if Xl occurs in the right-hand side of the equation defining Xk. A block Bi depends upon a block Bj if some variable of Bi depends upon some variable of Bj.

For further details on BESs, see the caesar_solve_1 manual page.

General Options

The following options specify various forms of output, but do not influence the resolution.
-bes output[.bes[.ext]]
If a single variable of interest is considered for resolution (see option -variable), print in file output[.bes] the portion of the BES reachable from that variable along variable dependencies. If several variables of interest are considered, for each variable of index i defined in the block of index j, print in file output_i_j[.bes] the portion of the BES reachable from that variable along variable dependencies. If the extension .bes.ext is present, the file containing the BES portion is compressed according to the corresponding format. Not a default option.

-diag diag[.bes[.ext]]
If a single variable of interest is considered for resolution (see option -variable), print in file diag[.bes] a diagnostic (portion of the BES) explaining the truth value of that variable. If several variables of interest are considered, for each variable of index i defined in the block of index j, print in file diag_i_j[.bes] a diagnostic (portion of the BES) explaining the truth value of that variable. If the extension .bes.ext is present, the file containing the diagnostic is compressed according to the corresponding format. This option is mutually exclusive with -nosolve. Not a default option.

-nosolve
Do not perform the resolution of the BES. This option is mutually exclusive with -diag. Not a default option.

-silent
Execute silently. Opposite of -verbose. Default option.

-stat
Display statistical information about the resolution of the BES. Not a default option.

Note: The number of boolean variables and dependencies displayed by the -stat option is generally smaller than the number of variables and dependencies of the BES contained in the output.bes file created with the -nosolve option. This is due to the on-the-fly nature of the resolution algorithms, which terminate as soon as they have determined the value of the variables of interest.

-verbose
Animate the user's screen, telling what is going on. Opposite of -silent. Default option is -silent.

-version
Display the current version number of the tool and stop. To be effective, this option should occur as the first argument on the command line. Subsequent options and/or arguments, if any, will be discarded. Not a default option.

The following options specify how the resolution is carried out.

-sequential
Perform the resolution of the BES in a sequential manner, by applying the resolution algorithms provided by the caesar_solve_1 library. This option is mutually exclusive with -parallel. Default option.

-parallel file[.gcf] [global_options] [instance_options]
Perform the resolution of the BES in a distributed manner, using several machines connected by a network. The list of these machines, together with various directives tuning the distributed computation, is given in the grid configuration file file[.gcf] (see the distributor manual page for details about the GCF format). The lists of options global_options and instance_options can be used for last-minute changes to the settings of the grid configuration file file[.gcf]. See the distributor manual page for a description of these options. This option is mutually exclusive with -sequential. Not a default option.

-variable v0 b0 ... vn bn
Indicates the indexes v0, ..., vn of the variables of interest and the indexes b0, ..., bn of the equation blocks defining those variables (n >= 0). The default value for n is 0 (i.e., only one variable of interest is considered for resolution) and the default value for both v0 and b0 is 0. If some bi is the index of a block undefined in the BES, or if some vj is the index of a variable undefined in the block of index bj (where 0 <= i, j <= n), then an error message is issued and the execution is aborted. Not a default option.

Random, Bes, and Block Options

The options random_options, bes_options, and block_options are described in the rbc manual page.

When the input is a textual BES file input.bes, the only directives bes_options and block_options that have effect on the equation blocks of the BES are those concerning the variables unique_resolution and solve_mode.

To provide for last-minute changes, the contents of the RBC file can be extended on the command line using the options random_options, bes_options, and block_options. The RBC file can even be empty, in which case input.rbc should be replaced with "-" on the command line.

Exit Status

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

Diagnostics

When the source is erroneous, error messages are issued.

Bibliography

[JM05] Ch. Joubert and R. Mateescu. Distributed Local Resolution of Boolean Equation Systems. In Francisco Tirado and Manuel Prieto (Eds.), Proceedings of the 13th Euromicro Conference on Parallel, Distributed and Network-Based Processing PDP'2005 (Lugano, Switzerland), pp. 264-271. IEEE Computer Society, February 2005. Available from http://cadp.inria.fr/publications/Joubert-Mateescu-05.html

[JM06] Ch. Joubert and R. Mateescu. Distributed On-the-Fly Model Checking and Test Case Generation. In Antti Valmari (Ed.), Proceedings of the 13th International Workshop on Model Checking of Software SPIN'2006 (Vienna, Austria), Lecture Notes in Computer Science vol. 3925, pp. 126-145. Springer Verlag, March-April 2006. Available from http://cadp.inria.fr/publications/Joubert-Mateescu-06.html

[Mat06] R. Mateescu. CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems. Springer International Journal on Software Tools for Technology Transfer (STTT), v. 8, no. 1, p. 37-56, 2006. Full version available as INRIA Research Report RR-5948. Available from http://cadp.inria.fr/publications/Mateescu-06-a.html

Authors

A prototype version of bes_solve was developed by Christophe Joubert and subsequently enhanced by Jerome Fereyre (both at INRIA/VASY).

Version 1.0 of bes_solve was entirely rewritten and documented by Radu Mateescu (INRIA/VASY), who also defined and implemented the RBC file format.

The option -parallel invokes the distributed BES resolution algorithm proposed in [JM06]. The implementation of this algorithm was a long-term effort carried out (chronologically) by Christophe Joubert, Jerome Fereyre, Hubert Garavel, Remi Herilier, Wendelin Serwe, Iker Bellicot, and Radu Mateescu.

Operands

input.rbc
random BES configuration file (input)

input.bes[.ext]
BES text file (input)

output.bes[.ext]
BES text file (output)

diag.bes[.ext]
diagnostic BES text file (output)

Files

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

See the caesar_solve_1 manual page for a description of the .bes files.

See Also

OPEN/CAESAR Reference Manual, bisimulator , caesar.open , caesar_solve_1 , evaluator , rbc

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 bugs to Radu.Mateescu@inria.fr.


Table of Contents