CADP On-Line Manual Pages


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

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

Note: The manual pages below are the most recent versions of the CADP documentation, and refer to the current or immediately forthcoming release of CADP. If an earlier version of CADP version is installed at your site, the documentation may contain some differences.

1. CADP Languages and Formats

aut: simple file format for labelled transition systems
bcg: Binary Coded Graphs: binary file format for labelled transition systems
bes: text file format for Boolean Equation Systems
exp: language for describing networks of communicating automata
fsp: process calculus defined by Jeff Magee and Jeff Kramer (Imperial College); see the fsp2lotos and fsp.open manual pages
gcf: Grid Configuration File format
hid: file format for hiding labels; see the caesar_hide_1 manual page
lnt: newest specification language supported by CADP; adapted from E-LOTOS (ISO International Standard 15437:2001); see the tutorial page, section "Tutorials for LNT"
lotos: oldest specification language supported by CADP; (ISO International Standard 8807:1989); see the tutorial page, section "Tutorials for LOTOS"
mcl: Model Checking Language (versions 3, 4, and 5)
mcl3: Model Checking Language version 3 (regular alternation-free mu-calculus)
mcl4: Model Checking Language version 4 (value-passing modal mu-calculus)
mcl5: Model Checking Language version 5 (probabilistic value-passing modal mu-calculus)
nupn: Nested-Unit Petri Nets
pbg: Partitioned BCG File format
rbc: textual file format for random BES (Boolean Equation Systems) configuration
ren: file format for renaming labels; see the caesar_rename_1 manual page
seq: CADP common format for execution sequences (i.e., traces)
svl-lang: script language for verification scenarios
xtl-lang: language for value-based temporal logic formulas

2. CADP Command-Line Tools

bcg_cmp: equivalence comparison of normal, probabilistic, or stochastic labeled transitions systems (LTS) encoded in the BCG 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 or reduction 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_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
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 and behavioural analysis of Nested-Unit Petri Nets
caesar: compilation & verification of LOTOS specifications
caesar.indent: LOTOS specifications pretty-printer
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: a family of on-the-fly model checkers
evaluator3: on-the-fly model checking of MCL v3 formulas
evaluator4: on-the-fly model checking of MCL v4 formulas
evaluator5: on-the-fly model checking of MCL v5 formulas
executor: random execution
exhibitor: search for execution sequences matching a given pattern
exp.open: OPEN/CAESAR connection for EXP networks of communicating automata
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 LNT language
lnt2lotos: LNT to LOTOS translator
lnt_merge: merge a multi-module LNT model into a single-module LNT model
lotos.open: OPEN/CAESAR connection for the LOTOS language
nupn_info: query and transformation of Nested-Unit Petri Nets
ocis: Open/Caesar Interactive Simulator
pbg_cp: copy a partitioned BCG graph
pbg_info: display information about a partitioned BCG graph
pbg_mv: move a partitioned BCG graph
pbg_rm: remove a partitioned BCG graph
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
scrutator: pruning of Labelled Transition Systems
seq.open: OPEN/CAESAR connection for traces encoded in the SEQ format
simulator: interactive simulator with ASCII command-line interface
svl: compilation and execution of SVL scripts
terminator: deadlock detection
tgv: Test Generation from transitions systems using Verification techniques
traian: compilation of LNT specifications
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

3. CADP Application Programming Interfaces

Note: The manual pages of the Open/Caesar Application Programming Interfaces are available as part of the CADP software package.

bcg_read: a simple interface to read a BCG graph
bcg_write: a simple interface to produce a BCG graph
caesar_area_1: the ``area_1'' library of OPEN/CAESAR
caesar_bitmap: the ``bitmap'' library of OPEN/CAESAR
caesar_cache_1: the ``cache_1'' 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_solve_2: the ``solve_2'' 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

4. Deprecated or Deleted Tools

aldebaran: minimization and comparison of labelled transitions systems; deprecated in 2008 - see HISTORY file entries #1299, #1742, and #1827
caesar.aldebaran: combination of CAESAR and ALDEBARAN; deleted in 2002 - see HISTORY file entry #826
caesar.open: use lotos.open instead - OPEN/CAESAR connection for the LOTOS language; deprecated in 2020 - see HISTORY file entry #2569
des2aut: composition generation of a labelled transitions system; deleted in 2002 - see HISTORY file entry #783
exp2fc2: conversion of .exp files to parallel .fc2 files; deleted in 2014 - see HISTORY file entry #1844
fc2open: connection of FC2 format to OPEN/CAESAR; deleted in 2002 - see HISTORY file entry #819
lpp: LNT pre-processor - auxiliary tool for LNT2LOTOS; deleted in 2024 - see HISTORY file entry #3070
lnt_check: auxiliary script for LNT2LOTOS; deleted in 2024 - see HISTORY file entry #2986
lnt_depend: auxiliary script for LNT2LOTOS; deleted in 2024 - see HISTORY file entry #3062

Back to the CADP Home Page