RBC manual page
Table of Contents

Name

rbc, RBC - textual file format for random BES (Boolean Equation Systems) configuration

Description

An RBC (Random BES Configuration) file filename.rbc specifies a set of parameters controlling the random generation of a Boolean Equation System (BES). The corresponding BES can be generated and solved on the fly using the bes_solve tool, which computes the value of one or several boolean variables of interest defined in some equation block(s) of the BES.

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):

Syntax of the RBC Format

The format of filename.rbc is defined by the following BNF grammar:
   <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.

Semantics of the RBC Format

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.

Examples of RBC 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.

How to Create a RBC File

At present, RBC files must be written by hand.

The contents of an RBC file passed as argument to the bes_solve tool can also be extended 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.

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:

How to Read a RBC File

At present, there is one single CADP tool, bes_solve , that reads and processes RBC files.

Bibliography

[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), 8(1):37-56, 2006. Full version available as INRIA Research Report RR-5948. Available from http://cadp.inria.fr/publications/Mateescu-06-a.html

[GLMS13] H. Garavel, F. Lang, R. Mateescu, and W. Serwe. CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. Springer International Journal on Software Tools for Technology Transfer (STTT), 15(2):89-107, 2013. Available from http://cadp.inria.fr/publications/Garavel-Lang-Mateescu-Serwe-13.html

See Also

OPEN/CAESAR Reference Manual, bes_solve , 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 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