CADP On-Line Manual Pages


What is CADP?
Home Page Tools Overview Current Status
Installation
How to obtain CADP? Usage Statistics Issues & Patches
Documentation
Tutorials Publications Manual Pages Demo Examples FAQ
CADP Newsletters
Nr. 1 - Dec. 1996 Nr. 2 - Jun. 1997 Nr. 3 - Sep. 1997 Nr. 4 - Jan. 1999 Nr. 5 - Jul. 2001 Nr. 6 - Apr. 2007
CADP Community
Forum Education & Training Case Studies Research Tools
CADP Resources
VLTS Benchmarks Other Resources
About CADP
Contributors

This Page gives the latest versions of the manual pages of the tools available in the CADP toolbox.

Note 1: the Open/Caesar Application Programming Interfaces (APIs) are not listed below. To consult them, please refer to the "man" directory in the CADP distribution installed at your site.

Note 2: the manual pages below are the most recent versions of the CADP documentation. They do not list obsolete tools that have been removed from CADP. For the same reason, they might list tools that will only be available in the next releases of CADP (such tools might be not present in the CADP distribution already installed at your site, or the documentation may exhibit some differences and improvements).

bcg: Binary Coded Graphs: universal graph format
bcg_draw: display graphs encoded in the BCG format
bcg_edit: edit interactively the PostScript representation of BCG graphs
bcg_graph: generate various kinds of useful BCG graphs
bcg_info: display information about graphs encoded in the BCG format
bcg_io: convert graphs from and into the BCG format
bcg_labels: modify the labels of graphs encoded in the BCG format
bcg_lib: generate dynamic libraries for graphs encoded in the BCG format
bcg_merge: translation of a partitioned BCG graph into one single BCG graph
bcg_min: minimization of normal, probabilistic, or stochastic labeled transitions systems (LTS) encoded in the BCG format
bcg_open: OPEN/CAESAR connection for graphs encoded in the BCG format
bcg_read: a simple interface to read a BCG graph
bcg_steady: steady-state numerical analysis of (extended) continuous-time Markov chains encoded in the BCG format
bcg_transient: transient numerical analysis of (extended) continuous-time Markov chains encoded in the BCG format
bcg_write: a simple interface to produce a BCG graph
bes_solve: resolution of boolean equation systems
bisimulator: on-the-fly equivalence/preorder checking
caesar.adt: translation of LOTOS abstract data types into C
caesar.bdd: structural analysis of Basic Petri Nets
caesar: compilation & verification of LOTOS specifications
caesar.indent: LOTOS specifications pretty-printer
caesar.open: OPEN/CAESAR connection for the LOTOS language
caesar_area_1: The ``area_1'' library of OPEN/CAESAR
caesar_bitmap: The ``bitmap'' library of OPEN/CAESAR
caesar_diagnostic_1: The ``diagnostic_1'' library of OPEN/CAESAR
caesar_edge: The ``edge'' library of OPEN/CAESAR
caesar_graph: The ``graph'' library of OPEN/CAESAR
caesar_hash: The ``hash'' library of OPEN/CAESAR
caesar_hide_1: The ``hide_1'' library of OPEN/CAESAR
caesar_mask_1: The ``mask_1'' library of OPEN/CAESAR
caesar_rename_1: The ``rename_1'' library of OPEN/CAESAR
caesar_solve_1: The ``solve_1'' library of OPEN/CAESAR
caesar_stack_1: The ``stack_1'' library of OPEN/CAESAR
caesar_standard: The ``standard'' library of OPEN/CAESAR
caesar_table_1: The ``table_1'' library of OPEN/CAESAR
caesar_version: The ``version'' library of OPEN/CAESAR
contributor: CADP contribution assistant
cunctator: on-the-fly steady-state simulation of continuous-time Markov chains
declarator: test an OPEN/CAESAR implementation
determinator: elimination of nondeterminism for stochastic systems
distributor: state space generation using distributed reachability analysis
evaluator: on-the-fly model checking of regular alternation-free mu-calculus formulas
executor: random execution
exhibitor: search for execution sequences matching a given pattern
exp.open: OPEN/CAESAR connection for networks of communicating automata
exp2fc2: Conversion of .exp files to parallel .fc2 files
fsp.open: OPEN/CAESAR connection for the FSP language
fsp2lotos: FSP to LOTOS translator
generator: BCG graph generation using reachability analysis
installator: CADP installation assistant
lnt.open: OPEN/CAESAR connection for the LOTOS NT language
lnt2lotos: LOTOS NT to LOTOS translator
lpp: LOTOS / LOTOS NT pre-processor
ocis: Open/Caesar Interactive Simulator
predictor: predict the feasability of reachability analysis
projector: semi-composition and generation of Labelled Transition Systems
reductor: BCG graph generation using reachability analysis combined with on-the-fly reduction
seq.open: OPEN/CAESAR connection for traces encoded in the SEQUENCE format
simulator: interactive simulator with ASCII command-line interface
svl: Script Verification Language
terminator: deadlock detection
tgv: Test Generation from transitions systems using Verification techniques
tst: CADP installation and configuration auto-test facility
xeuca: graphical-user interface for the EUCALYPTUS tools
xsimulator: interactive simulator with X-windows interface
xtl: evaluation of value-based temporal logic formulas

Back to the VASY Home Page