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.
 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 ELOTOS (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 alternationfree
mucalculus)
 mcl4

Model Checking Language version 4 (valuepassing modal
mucalculus)
 mcl5

Model Checking Language version 5 (probabilistic valuepassing
modal mucalculus)
 nupn

NestedUnit 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)
 svllang

script language for verification scenarios
 xtllang

language for valuebased temporal logic formulas
 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 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

steadystate numerical analysis of (extended) continuoustime
Markov chains encoded in the BCG format
 bcg_transient

transient numerical analysis of (extended) continuoustime
Markov chains encoded in the BCG format
 bes_solve

resolution of boolean equation systems
 bisimulator

onthefly equivalence/preorder checking
 caesar.adt

translation of LOTOS abstract data types into C
 caesar.bdd

structural and behavioural analysis of NestedUnit Petri
Nets
 caesar

compilation & verification of LOTOS specifications
 caesar.indent

LOTOS specifications prettyprinter
 caesar.open

OPEN/CAESAR connection for the LOTOS language
 contributor

CADP contribution assistant
 cunctator

onthefly steadystate simulation of continuoustime 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 onthefly model checkers
 evaluator3

onthefly model checking of MCL v3 formulas
 evaluator4

onthefly model checking of MCL v4 formulas
 evaluator5

onthefly 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
 lpp

LNT preprocessor
 nupn_info

query and transformation of NestedUnit 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

semicomposition and generation of Labelled Transition
Systems
 reductor

BCG graph generation using reachability analysis combined
with onthefly reduction
 scrutator

pruning of Labelled Transition Systems
 seq.open

OPEN/CAESAR connection for traces encoded in the SEQ format
 simulator

interactive simulator with ASCII commandline interface
 svl

compilation and execution of SVL scripts
 terminator

deadlock detection
 tgv

Test Generation from transitions systems using Verification techniques
 tst

CADP installation and configuration autotest facility
 xeuca

graphicaluser interface for the EUCALYPTUS tools
 xsimulator

interactive simulator with Xwindows interface
 xtl

evaluation of valuebased temporal logic formulas
Note: The manual pages of the Open/Caesar Application Programming Interfaces are available as part of the CADP software package.
 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
 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
Back to the CADP Home Page