Table of Contents
terminator - deadlock detection
bcg_open [
bcg_opt]
spec[
.bcg]
[
cc_opt]
terminator [
terminator_opt]
terminator_param
or:
caesar.open [caesar_opt]
spec[.lotos] [cc_opt] terminator [terminator_opt] terminator_param
or:
exp.open
[exp_opt] spec[.exp] [cc_opt] terminator [terminator_opt] terminator_param
or:
fsp.open [fsp_opt] spec[.lts] [cc_opt] terminator [terminator_opt] terminator_param
or:
lnt.open [lnt_opt] spec[.lnt] [cc_opt] terminator [terminator_opt] terminator_param
or:
seq.open [seq_opt] spec[.seq] [cc_opt] terminator [terminator_opt] terminator_param
This program attempts to detect deadlocks (i.e. states without
successors) in the BCG graph
spec.bcg, the LOTOS program
spec.lotos, the
composition expression
spec.exp, the FSP program
spec.lts, the LOTOS NT program
spec.lnt, or the sequence file
spec.seq. It is based on the ``bit state space''
verification technique proposed by Gerard Holzmann.
When the program detects
deadlock states, it displays diagnostic sequences, i.e., execution sequences
leading from the initial state to the deadlock states. Diagnostic sequences
are displayed using the simple SEQUENCE format (see the exhibitor
man page for a description of this format).
Note: the deadlock detection
performed using this technique is partial: due to potential hash-code collisions,
some states may not be visited. Therefore, this program is likely to find
only a subset of the existing deadlocks. It might even fail to find deadlocks
when they exist.
Note: in its first form (i.e., when applied to the BCG graph
spec.bcg), this program is probably not the best way to perform deadlock
detection.
Note: the exhibitor
program can also be used to find the
shortest sequence leading to a deadlock.
The options
bcg_opt, if
any, are passed to
bcg_lib
.
The options caesar_opt, if any, are passed
to caesar
and to caesar.adt
.
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 seq_opt,
if any, are passed to seq.open
.
The options cc_opt, if any, are passed
to the C compiler.
The following terminator_options are currently available:
- -depth depth
- Consider only execution sequences whose number of transitions
is less or equal than depth (where depth is greater than zero). Prune the
exploration of the graph when the distance from the initial state becomes
greater than depth transitions. By default (if this option is not present
on the command-line) or if depth is equal to zero, all sequences will be
considered.
- -none
- Don't print any diagnostic sequence. Not a default option.
- -all
- Print all diagnostic sequences. Not a default option.
- -first
- Print the
first diagnostic sequence encountered and stop just after. Not a default
option.
- -decr
- Print only those diagnostic sequences which are shorter than
the last diagnostic sequence previously diplayed. Prune the exploration
of the graph in order to find diagnostic sequences of decreasing sizes.
It is not guaranteed that the final sequence is minimal (some shorter
sequence might exist, which can not be found by the program).
- by default
- (in absence of -none, -all, -first, -decr)
Print only the shortest diagnostic sequence obtained. Prune the exploration
of the graph in order to find diagnostic sequences of decreasing sizes.
It is not guaranteed that the final sequence is minimal (some shorter
sequence might exist, which can not be found by the program).
The parameters
terminator_param have the following formats, where order is an integer
denoting the order in which the transitions will be fired (see functions
CAESAR_CREATE_EDGE_LIST() and CAESAR_CREATE_STACK_1(), in the caesar_edge
and caesar_stack_1
manual pages), and where size, size_1, and size_2
are integer numbers denoting the sizes of bitmap tables:
- If terminator_param
= order size
=> automatic search using a single bitmap table with size entries. If size
is equal to zero, then the bitmap table will be as large as possible,
within the limits of the available computer memory.
- If terminator_param
= order size_1 size_2
=> automatic search using two bitmap tables with size_1 and size_2 entries,
respectively.
- If terminator_param is empty
=> interactive mode.
Exit status is 0 if everything is alright,
1 otherwise.
When the source is erroneous, error messages are
issued.
Hubert Garavel (INRIA Rhone-Alpes)
- spec.bcg
- BCG graph
(input)
- spec.exp
- network of communicating LTSs (input)
- spec.lotos
- LOTOS specification
(input)
- spec.lts
- FSP specification (input)
- spec.lnt
- LOTOS NT specification
(input)
- spec.seq
- sequence file (input)
The source code of this tool
is available in file
$CADP/src/open_caesar/terminator.c
CAESAR
Reference Manual, OPEN/CAESAR Reference Manual,
bcg_open
,
bcg
,
caesar.open
,
caesar
,
caesar.adt
,
exp.open
,
fsp.open
,
lnt.open
,
exhibitor
,
seq.open
Additional information
is available from the CADP Web page located at http://cadp.inria.fr
Directives
for installation are given in file $CADP/INSTALLATION.
Recent changes and
improvements to this software are reported and commented in file $CADP/HISTORY.
Please report new bugs to
Hubert.Garavel@inria.fr
Table of Contents
