Table of Contents
predictor - predict the feasability of reachability analysis
caesar.open [caesar_opt] spec[.lotos]
exp.open [exp_opt] spec[.exp] [cc_opt] predictor
fsp.open [fsp_opt] spec[.lts] [cc_opt] predictor
spec[.lnt] [cc_opt] predictor
seq.open [seq_opt] spec[.seq] [cc_opt] predictor
This program gives some predictive estimations concerning the
feasability of reachability analysis for the BCG graph spec.bcg
, the LOTOS
, the composition expression spec.exp
, the FSP program
, the LNT program spec.lnt
, 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 caesar_opt, if any, are passed to caesar
and to caesar.adt
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 seq_opt, if any, are passed
The options cc_opt, if any, are passed to the C compiler.
Exit status is 0 if everything is alright, 1 otherwise.
When the source is erroneous, error messages are issued.
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
The source code of this tool is available in file $CADP/src/open_caesar/predictor.c
- BCG graph (input)
of communicating LTSs (input)
- LOTOS specification (input)
- FSP specification (input)
- LNT specification (input)
OPEN/CAESAR Reference Manual, bcg
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