Table of Contents
predictor - predict the feasability of reachability analysis
exp.open [exp_opt] spec[.exp]
fsp.open [fsp_opt] spec[.lts] [cc_opt] predictor
lnt.open [lnt_opt] spec[.lnt] [cc_opt] predictor
spec[.lotos] [cc_opt] predictor
seq.open [seq_opt] spec[.seq] [cc_opt]
This program gives some predictive estimations concerning
the feasability of reachability analysis for the BCG graph spec.bcg
composition expression spec.exp
, the FSP program spec.lts
, the LNT program
, the LOTOS program spec.lotos
, or the sequence file spec.seq
. It displays:
- The state size (in bytes). Notice that this size only refers to the "static"
part of the state vector; the "dynamic" part (dynamic data structures such
as lists, trees, etc.) cannot be taken into account.
- One or several estimations
of the amount of memory available on the current machine. If the environment
variable $CADP_MEMORY (see below) is set, then its value is used. Otherwise,
predictor invokes an auxiliary program named cadp_memory to determine a
relevant value or, whenever possible, three values of interest: (1) the
amount of free memory currently available, (2) the total amount of memory
physically installed on the current machine, and (3) the sum of free memory
and free swap currently available.
- Notice that relying on the swap may
significantly decrease the performance of
- model checking algorithms.
on 32-bit machines or 64-bit machines running processes in 32-bit mode,
estimations take into account the fact that, even if 4 gigabytes of memory
are physically available, only a part of it (e.g., 3 gigabytes) can be used
by application programs.
- For each estimation of the amount of memory available,
an upper bound on the number of states that can be generated exhaustively
(e.g., using "standard" CAESAR, OPEN/CAESAR's Generator, etc.). Notice that
this number is not merely the quotient of the amount of memory available
divided by the state size, because auxiliary data structures must also
- Notice, however, that this number is only an upper bound,
since the amount of
- memory required for dynamic data types, hash tables,
and other data structures, etc., is not taken into account.
Note: the predictor
program is not very useful when applied to BCG graphs, since the graph
has already been generated.
The options bcg_opt, if any, are passed
The options exp_opt, if any, are passed to exp.open
The options fsp_opt, if any, are passed to fsp.open
The options lnt_opt,
if any, are passed to lnt.open
The options lotos_opt, if any, are
passed to caesar
and to caesar.adt
The options seq_opt, if
any, are passed to seq.open
The options cc_opt, if any, are passed
to the C compiler.
Exit status is 0 if everything is alright,
When the source is erroneous, error messages are
Hubert Garavel (INRIA Rhone-Alpes)
- If this variable is
set, its value gives an estimation of the amount of memory (in kilobytes)
that can be allocated by a process on the current machine; if this variable
is not set, a default value will be determined automatically. See the $CADP/INSTALLATION_2
file for details.
The source code of this tool
is available in file $CADP/src/open_caesar/predictor.c
- BCG graph
- network of communicating LTSs (input)
- FSP specification
- LNT specification (input)
- LOTOS specification
- sequence file (input)
Reference Manual, bcg
Additional information is
available from the CADP Web page located at http://cadp.inria.fr
for installation are given in files $CADP/INSTALLATION_*.
and improvements to this software are reported and commented in file $CADP/HISTORY.
Please report new bugs to Hubert.Garavel@inria.fr
Table of Contents