|
| 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 |
The BES specified by the RBC file 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.
<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_blocksNote: 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_freetrue) 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
The meaning of the different <variable>s
is the following:
sign
unique_resolutiontrue) 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
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_variablesNote: 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
variable_ratio
local_variable_ratio
or_variable_ratio
or_variable_alternationor_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
shapegeneral 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 bes
. 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> 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> 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>
(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:
<random_options>
in the RBC file,
The
value of <variable>s can be set in five different ways, listed below by increasing
precedence:
<bes_options> in the RBC file,
<block_options>
in the RBC file,
[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.