RBC manual page

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

• A sign mu (resp. nu), indicating whether the block denotes the minimal (resp. maximal) fixed point of the functional induced by the equations of the block.
• A solve mode indicating the boolean resolution algorithm used for solving variables defined in the block.
• A clause unique indicating whether the resolution algorithm will be invoked only once or several times for solving variables defined in the block.

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

• `<random_options>` is a (possibly empty) list of directives applicable to the BES.
• `<bes_options>` is a (possibly empty) list of directives applicable to every equation block of the BES.
• `<block_options>` defines a set of block indexes together with a (possibly empty) list of directives applicable to these blocks exclusively.
• `<interval>` is an interval on natural numbers denoting a set of indexes of equation blocks of the BES. An `<interval>` can contain either a single index specified as `<block_index>`, or a range of block indexes specified as "`[`"`<block_index>`".."`<block_index>`"`]`".
• `<block_index>` is a natural number denoting the index of an equation block of the BES.
• `<random_directive>` (resp. `<directive>`) is an assignment of a `<value>` to a `<random_variable>` (resp. a `<variable>`), followed by a newline character.

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.

• random_options has the same syntax as the non-terminal `<random_options>` in the RBC 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 RBC 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 RBC 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 RBC 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 RBC 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:

• default value,
• value given by `<random_options>` in the RBC file,
• value given by random_options on the command line.

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

• default value,
• value given by `<bes_options>` in the RBC file,
• value given by bes_options on the command line,
• value given by `<block_options>` in the RBC file,
• value given by block_options on the command line.

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