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. ## Syntax of the RBC Format

The format of *filename***.rbc**
is defined by the following BNF grammar: ## 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 ## 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: ## How to Create a RBC File

At present, RBC files must be written
by hand. ## 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
## See Also

OPEN/CAESAR Reference Manual, **bes_solve**
, **bisimulator**
,
**caesar.open**
, **caesar_solve_1**
, **evaluator**
## Bugs

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

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.

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

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

.

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.

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.

[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

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