BES_SOLVE manual page


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

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

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. See the bes manual page for a definition of Boolean Equation Systems and their terminology.

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:

Explicitly, as a textual BES file input.bes, possibly compressed according to the extension .ext, containing all equations of the BES (see caesar_solve_1 for a description of the .bes format). If the filename extension is missing for the input file, the default extension is .bes. If present, the extension .ext must correspond to a known file compression format (e.g., .Z, .gz, .bz2, .xz, etc.). The list of currently supported extensions and compression formats is given by the $CADP/src/com/cadp_zip shell-script.
In this case, bes_solve will first read all the BES equations contained in the input.bes file, and then it will solve the boolean variables of interest on-the-fly.
The BES representation using .bes files allows to study the behaviour of local resolution algorithms either on (usually small) BESs constructed by hand, or on (usually large) BESs produced by evaluator or bisimulator as a result of encoding model checking and equivalence checking problems, respectively.

Implicitly, as a random BES configuration file input.rbc containing various parameters allowing to generate randomly the equations of the BES (see rbc for a description of the RBC format).
In this case, bes_solve will generate a random BES according to the parameters specified in input.rbc and solve the variables of interest, both activities being carried out on-the-fly.
The BES representation using .rbc files provides a very compact encoding for complex BESs with various forms. Moreover, since it consumes very few memory and CPU resources, random BES generation allows to measure the performance of resolution algorithms accurately on large examples of BESs.

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.

Bugs

Please report bugs to Radu.Mateescu@inria.fr.

Table of Contents

Name
Synopsis
Description
Boolean Equation Systems
General Options
Random, BES, and Block Options
Exit Status
Diagnostics
Bibliography
Authors
Operands
Files
See Also
Bugs