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

Table of Contents

Name

predictor - predict the feasability of reachability analysis

Synopsis

bcg_open [bcg_opt] spec[.bcg] [cc_opt] predictor

or:

exp.open [exp_opt] spec[.exp] [cc_opt] predictor

or:

fsp.open [fsp_opt] spec[.lts] [cc_opt] predictor

or:

lnt.open [lnt_opt] spec[.lnt] [cc_opt] predictor

or:

lotos.open [lotos_opt] spec[.lotos] [cc_opt] predictor

or:

seq.open [seq_opt] spec[.seq] [cc_opt] predictor

Description

This program gives some predictive estimations concerning the feasability of reachability analysis for the BCG graph spec.bcg, the composition expression spec.exp, the FSP program spec.lts, the LNT program spec.lnt, 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.
  Also, on 32-bit machines or 64-bit machines running processes in 32-bit mode,
  these 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 be considered.
  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.

  Options

  The options bcg_opt, if any, are passed to bcg_lib .

  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.

  Environment Variables

  $CADP_MEMORY

  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.

  Exit Status

  Exit status is 0 if everything is alright, 1 otherwise.

  Diagnostics

  When the source is erroneous, error messages are issued.

  Author

  Hubert Garavel (INRIA Rhone-Alpes)

  Operands

  spec.bcg

  BCG graph (input)

  spec.exp

  network of communicating LTSs (input)

  spec.lts

  FSP specification (input)

  spec.lnt

  LNT specification (input)

  spec.lotos

  LOTOS specification (input)

  spec.seq

  sequence file (input)

  Files

  The source code of this tool is available in file $CADP/src/open_caesar/predictor.c

  See Also

  OPEN/CAESAR Reference Manual, bcg , bcg_open , caesar , caesar.adt , exp , exp.open , fsp.open , lnt.open , lotos , lotos.open , seq , seq.open

  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.

  Bugs

  Please report new bugs to Hubert.Garavel@inria.fr

  ---

  Table of Contents

  • Name
  • Synopsis
  • Description
  • Options
  • Environment Variables
  • Exit Status
  • Diagnostics
  • Author
  • Operands
  • Files
  • See Also
  • Bugs