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 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
- 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
- lpp
-
LNT pre-processor
- 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
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
- 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
Back to the CADP Home Page