In CADP, BES is also a text file format to represent Boolean Equation Systems.
false), and binary operators of disjunction (
or) and conjunction (
Without loss of generality, it is assumed that each boolean formula
is either purely disjunctive (i.e., contains only
or operators), or purely
conjunctive (i.e., contains only
and operators). Formulas containing both
operators can be easily eliminated by introducing auxiliary variables. The
true) is considered as a disjunctive (resp. conjunctive)
A boolean variable is said to be defined by an equation if this variable occurs on the left-hand side of this equation. A boolean variable is said to be defined in a block if it is defined by an equation of this block.
Each boolean variable occurring on the right-hand side of an equation in a BES must be defined by some equation of this BES (but not necessarily in the same block).
Multiple definitions of a variable are forbidden, i.e., a variable is defined by at most one equation.
Recursive definitions of a variable are allowed (e.g., a variable occurs both on the left- and right-hand side of the same equation).
A boolean variable defined by an equation is disjunctive (resp. conjunctive) if the boolean formula on the right-hand side of this equation is purely disjunctive (resp. conjunctive).
If a variable X' occurs on the right-hand side of the equation defining a variable X, then X (directly) depends on variable X'.
If a variable defined in a block B depends on a variable defined in a block B', then block B (directly) depends on block B'.
A BES is said alternation-free if there are no cyclic dependencies between its blocks (but there can be cyclic dependencies between variables inside blocks).
Each equation block has a sign, which is equal to
nu) if the block denotes the minimal (resp. maximal) fixed point of the
functional induced by the equations of the block; see [Mat06] for a mathematical
definition of this functional.
BES can be either represented in binary form (in internal memory) using the caesar_solve_1 library, or in textual form (in files with .bes extension) using the syntax described below.
In a BES file, lexical tokens may be separated
by any sequence of spaces, tabulations, carriage returns, newlines, vertical
tabulations, form feeds (these characters are those recognized by the POSIX
isspace()), or comments, which are enclosed between
these sequences are always skipped and ignored.
BES files are case-sensitive: upper-case and lower-case letters are considered to be different.
textual syntax of BES files is described by the following context-free grammar,
<empty> denotes the empty sequence of symbols and
<nat> denotes a non-negative
<axiom> ::= <block-list> <block-list> ::= <block> | <block> <block-list> <block> ::= block <sign> <block-idf> <unique> <mode> is <equation-list> end block <sign> ::= mu | nu <block-idf> ::= B<nat> <unique> ::= <empty> | unique <mode> ::= <empty> | mode <nat> <equation-list> ::= <equation> | <equation> <equation-list> <equation> ::= <local-variable-idf> = <formula> <local-variable-idf> ::= X<nat> <global-variable-idf> ::= X<nat>_<nat> <formula> ::= <atomic-form> | <disjunctive-form> | <conjunctive-form> <atomic-form> ::= false | true | <local-variable-idf> | <global-variable-idf> <disjunctive-form> ::= <atomic-form> or <atomic-form> | <atomic-form> or <disjunctive-form> <conjunctive-form> ::= <atomic-form> and <atomic-form> | <atomic-form> and <conjunctive-form>
In a BES file, each block has a unique identifier of
<nat> is called the block index. Blocks may occur in
the file in any order w.r.t. their indexes, and these indexes are not necessarily
contiguous (i.e., there may be ``holes'' in the block numbering). If for some
i there is no block
Bi defined in the file, it is considered that
Bi is empty.
In each equation block, each
boolean variable defined by an equation (i.e., occurring on the left-hand
side of an equation) has an identifier of the form
X<nat>, which is unique
in the block, where
<nat> is called the variable index. Variables may be defined
in the block in any order w.r.t. their indexes, and these indexes are not
necessarily contiguous (i.e., there may be ``holes'' in the variable numbering).
Variable identifiers occurring in formulas have two forms:
X<nat1>_<nat2>is a global identifier that denotes the variable
X<nat1>defined in the block
B<nat2>. Global identifiers can be used for any variable occurring on the right-hand side of an equation.
X<nat>is a local identifier that denotes the variable
X<nat>defined in the current block.
One can attach an
mode <nat> to each equation block. Such a clause specifies
that the variables defined in this equation block should be computed using
the resolution algorithm named A
<nat> of the caesar_solve_1
<nat> is called the resolution mode of the block. If the
is absent, the resolution mode is set to 0 by default, meaning that the
resolution algorithm A0 will be used.
Since the caesar_solve_1 library does not operate globally, but locally, to compute a given variable defined in a given equation block, the same equation block may be solved several times, each time for computing a different variable of this block. Of course, caching is used to avoid recomputing variables already calculated.
It is however possible to help the solver by attaching an optional clause
unique to an equation block. Such a clause indicates that the block will
be solved only once, meaning that the value of a single variable defined
in the block will be computed. This increases the memory performance of
certain resolution algorithms. Any attempt at solving twice an equation
block having the
unique clause will trigger a run-time error. By default,
unique clause it absent, one assumes that several variables of the
equation block will need to be computed.
block nu B0 is X0 = X1 and X2 X1 = X0 or X1 or X2 X2 = X0_1 and X3 X3 = X1 or X4 X4 = true end block block mu B1 is X0 = X1 or X2 X1 = false X2 = X2 and X3 X3 = X0 or X1 or X3 end block
The global variable
X0_1, which is present on the right-hand side of the
equation defining variable
X2 in block
B0, references the variable
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.email@example.com