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:

Definitions for 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. Boolean formulas can be either purely disjunctive (i.e., contain only "or" operators), or purely conjunctive (i.e., contain only "and" operators). In a block Bi with at most M equations, the boolean variables defined by the equations of Bi (i.e., occurring in the left-hand sides of the equations) have unique numbers in the range [0..M-1]. The numbering of the blocks in a BES and of equations in a block may contain "holes" and may not necessarily be increasing.

A boolean variable defined by an equation is disjunctive (resp. conjunctive) if the boolean formula in the right-hand side of the equation is purely disjunctive (resp. conjunctive).

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. A BES is said alternation-free if there are no cyclic dependencies between its blocks. In an alternation-free BES, the blocks are assumed to be sorted topologically such that, for all i in [0..N-1], the block Bi depends only upon the blocks Bj with j >= i.

Each equation block has the following attributes (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 below, together with the RBC format.

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 (see below).

TEXTUAL BES FILE (.bes) FORMAT

A textual BES file input.bes specifies a BES by giving all its equation blocks and, for each block, all the equations contained in that block. The syntax of .bes files is defined in the caesar_solve_1 manual page.

RANDOM BES CONFIGURATION FILE (.rbc) FORMAT

An RBC file input.rbc specifies a set of parameters controlling the random generation of a BES. The syntax of RBC files is similar to that of grid configuration files (GCF) defined for controlling the execution of the distributor tool on several machines connected by a network.

An RBC file has the following syntax: 

   <rbc>              ::= <random_options>
                          <bes_options>
                          <block_options>*
   <random_options>   ::= <random_directive>*
   <random_directive> ::= <random_variable> "=" <value> "\n"
   <random_variable>  ::= "number_of_blocks"
                       |  "alternation_free"
                       |  "strategy"
   <bes_options>      ::= <directive>*
   <block_options>    ::= <block_set>+ <directive>*
   <block_set>        ::= <interval>+ "\n"
   <interval>         ::= <block_index>
                       |  "["<block_index>".."<block_index>"]"
   <directive>        ::= <variable> "=" <value> "\n"
   <variable>         ::= "sign"
                       |  "unique_resolution"
                       |  "solve_mode"
                       |  "number_of_variables"
                       |  "equation_length"
                       |  "variable_ratio"
                       |  "local_variable_ratio"
                       |  "or_variable_ratio"
                       |  "or_variable_alternation"
                       |  "false_constant_ratio"
                       |  "shape"
   <value>            ::= <character-string>

where:

Any line starting with the "#" character is considered as a comment and ignored. Spaces and tabulations can be inserted before, between, or after terminal symbols.

Variables can be modified by directives as follows. First, all variables have a default value, which will be used unless overriden by some directive. A <random_directive> occurring in the <random_options> list assigns a <random_variable> associated to the BES. A <directive> occurring in the <bes_options> list assigns its <variable> for all equation blocks of the BES. A <directive> occurring in a <block_options> list assigns its <variable> only for the blocks mentioned in this <block_options>, possibly overriding the value specified for this <variable> in the <bes_options> list. If a variable is assigned multiple times, the value assigned by the last directive overrides the previous ones.

The meaning of the different <random_variable>s is the following:

number_of_blocks:
This variable specifies the number N of blocks contained in the BES. N must be greater than 0. Default value is 1.

Note: Due to the hazard of random generation, it is not guaranteed that all block indexes in the range [0..N-1] will be present in the BES.

alternation_free:
This variable indicates whether the BES is alternation-free (value true) or not (value false). Default value is true.

Note: The current version of the caesar_solve_1 library handles only alternation-free BESs. Therefore, specifying the value false for this variable will trigger error messages issued by the resolution algorithms, which detect the presence of cyclic dependencies between blocks.

strategy:
This variable specifies the value of the seed initializing the random number generator used for generating the BES. The value 0 means that an arbitrary seed is chosen automatically at each execution of the tool (nondeterministic case). A value greater than 0 is used as the seed, which will entail the generation of the same BES at each execution of the tool (deterministic case). Default value is 1.

The meaning of the different <variable>s is the following:

sign:
This variable specifies the probability (given in percent, as a natural number in the interval [0..100]) that the sign of the current block is mu rather than nu. A value of 0 (resp. 100) will fix the sign of the block to nu (resp. mu). Default value is 50.

unique_resolution:
This variable indicates whether the current block will be solved only once (value true) or several times (value false). Default value is false.

Note: Setting this variable in the bes_options section of the command line will also act on a BES provided as a file input.bes. For technical reasons, if this variable is set on the command line for a set L of block indexes, all the remaining blocks of the BES (of indexes not belonging to L) will have this variable set to the default value false. If another value is required for the remaining blocks, this may be specified either using additional unique_resolution directives on the command line, or by explicitly editing the input.bes file.

solve_mode:
This variable specifies the index of the resolution algorithm (see the caesar_solve_1 manual page) used for solving boolean variables defined in the current block. Default value is 0.

Note: Setting this variable in the bes_options section of the command line will also act on a BES provided as a file input.bes. For technical reasons, if this variable is set on the command line for a set L of block indexes, all the remaining blocks of the BES (of indexes not belonging to L) will be solved using the default resolution algorithm 0. If another resolution algorithm is required for the remaining blocks, this may be specified either using additional solve_mode directives on the command line, or by explicitly editing the input.bes file.

Note: If the value set to this variable denotes an unexisting resolution algorithm (e.g., 100), then an error message is issued and the execution is aborted.

number_of_variables:
This variable specifies the number M of boolean variables that may be defined in the current block (i.e., that may occur in the left-hand side of equations of the block). M must be greater than 0. Default value is 1.

Note: Due to the hazard of random generation, it is not guaranteed that all variable indexes in the range [0..M-1] will be defined by equations of the block.

equation_length:
This variable specifies the maximum length L (number of operands) of the boolean formulas occurring in the right-hand sides of equations of the current block. L must be greater than 0. The length of the right-hand side of an equation will be chosen randomly in the interval [1..L]. Default value is 1.

variable_ratio:
This variable specifies the percentage (natural number in the interval [0..100]) of boolean variables among the operands in the right-hand sides of equations of the current block (the remaining operands are boolean constants). Default value is 50.

local_variable_ratio:
This variable specifies the percentage (natural number in the interval [0..100]) of local variables (i.e., defined in the current block) among the variables in the right-hand sides of equations of the current block (the remaining variables are defined in other blocks). In an alternation-free BES containing N equation blocks, this variable must be set to 100 for the block of index N-1, since this block does not depend upon any other blocks of the BES. Default value is chosen automatically such that the variables occurring in the right-hand sides of equations are randomly spread over the blocks of the BES.

or_variable_ratio:
This variable specifies the percentage (natural number in the interval [0..100]) of disjunctive boolean variables among the local variables in the right-hand sides of equations of the current block (the remaining local variables in the right-hand sides of equations are conjunctive). Due to the way equations are generated, this variable will also correspond to the percentage of disjunctive boolean variables occurring in the left-hand sides of equations of the current block. Default value is 50.

or_variable_alternation:
This variable modifies the interpretation of or_variable_ratio according to the binary boolean operators occurring in the right-hand sides of the equations of the current block. If this variable is set to true, then all local variables occuring in the right-hand sides of purely disjunctive (resp. conjunctive) equations are forced to be conjunctive (resp. disjunctive). Said differently, the type of variables must strictly alternate between the left-hand side and the right-hand side of each equation. However, the total percentage of disjunctive boolean variables in all right-hand sides of equations will roughly correspond to the value of or_variable_ratio. If this variable is set to false, then the amount of disjunctive variables among the local variables occurring in the right-hand side of each equation is determined according to the value of or_variable_ratio. Default value is false.

false_constant_ratio:
This variable specifies the percentage (natural number in the interval [0..100]) of false among the constants in the right-hand sides of equations of the current block (the remaining constants are true). Default value is 50.

shape:
This variable specifies the shape of the current block, i.e., the structure of the dependency graph between the boolean variables defined in the block (see the caesar_solve_1 manual page). The following values are available for this variable: general indicates no constraint on dependencies; acyclic indicates the absence of cyclic dependencies; disjunctive (resp. conjunctive) indicates that the block is disjunctive (resp. conjunctive) according to the definition given in caesar_solve_1 . Default value is general.

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

random_options has the same syntax as the non-terminal <random_options> in the above grammar (except that some characters meaningful to the shell must be escaped or quoted properly). If it is non-empty, it is interpreted exactly as if its contents were inserted in the random BES configuration file, at the end of the <random_options> list and before the first <bes_options>.

bes_options has the same syntax as the non-terminal <bes_options> in the above grammar (except that some characters meaningful to the shell must be escaped or quoted properly). If it is non-empty, it is interpreted exactly as if its contents were inserted in the random BES configuration file, at the end of the <bes_options> list and before the first <block_options>.

block_options has the same syntax as a possibly empty list of non-terminals <block_options> (except that some characters meaningful to the shell must be escaped or quoted properly). If it is non-empty, it is interpreted exactly as if its contents were appended at the end of the random BES configuration file, after the last <block_options>.

Thus, the value of <random_variable>s can be set in three different ways, listed below by increasing precedence:

The value of <variable>s can be set in five different ways, listed below by increasing precedence:

Examples of Random Bes Configuration Files

The RBC file below specifies a random BES with a single equation block of maximal fixed point, which contains only conjunctive variables and does not contain any constant: 
   sign = 0
   number_of_variables = 1000
   equation_length = 10
   variable_ratio = 100
   or_variable_ratio = 0

This kind of BES is typically encountered by translating the model checking of satisfied safety properties (see the evaluator manual page). The local resolution of any variable of this BES will yield TRUE, since there is no false constant reachable from that variable.

The RBC file below specifies a random BES with a single maximal fixed point block with a small amount of constants, and in which disjunctive and conjunctive variables strictly alternate along dependencies: 

   strategy = 2
   sign = 0
   number_of_variables = 10000
   equation_length = 10
   variable_ratio = 98
   or_variable_alternation = true

This kind of BES typically underlies the comparison of equivalent nondeterministic LTSs modulo strong bisimulation (see the bisimulator manual page). The local resolution of the variable of index 0 of this BES will yield TRUE.

Finally, the RBC file below describes a random BES containing two equation blocks, the first one being a conjunctive maximal fixed point and the second one a disjunctive minimal fixed point: 

   number_of_blocks = 2
   variable_ratio = 90
   # conjunctive nu-block
   0
   sign = 0
   solve_mode = 4
   number_of_variables = 1000
   equation_length = 20
   or_variable_ratio = 5
   false_constant_ratio = 0
   shape = conjunctive
   # disjunctive mu-block
   1
   sign = 100
   solve_mode = 3
   number_of_variables = 2000
   equation_length = 10
   or_variable_ratio = 95
   false_constant_ratio = 80
   shape = disjunctive

This kind of BES corresponds to the model checking of certain fairness properties, such as the "fair reachability of predicates" (see the evaluator manual page). The local resolution of a variable of the first block may yield TRUE or FALSE, depending on the chosen strategy. The strategy is set by default to 1; setting it to 0 would yield different BESs at each execution of the tool.

Exit Status

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

Diagnostics

When the source is erroneous, error messages are issued.

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

Additional information is available from the CADP Web page located at http://cadp.inria.fr

Directives for installation are given in file $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.

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.

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

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

Table of Contents