Table of Contents
seq.open - OPEN/CAESAR connection for traces encoded in the SEQ format
seq.open [seq_options] filename[.seq] [cc_options] prog[.a|.c|.o] [prog_options]
Taking as input the graph
filename.seq, which represents a set
of one or more execution traces encoded in the simple SEQ format (see
the
seq
manual page for a definition of this format), and an OPEN/CAESAR
program
prog[
.a|
.c|
.o],
seq.open generates an executable program
prog by performing
appropriate calls to the C compiler. Finally,
prog is executed.
According
to the principles of the OPEN/CAESAR architecture, prog is obtained by
combining three different modules:
- the graph module is obtained by scanning
filename.seq
- the storage module is the standard OPEN/CAESAR library
- the
exploration module is prog[.a|.c|.o]
The seq.open tool was designed to handle
very large execution traces, such as those obtained by a random execution
of a real system. For this reason, seq.open works on-the-fly, without storing
in memory the entire contents of filename.seq. In order to speed up the exploration,
an hash-based cache table of bounded size is used to avoid multiple computations
of label strings and successor transitions.
The exploration module
prog[
.a|
.c|
.o] is supposed to contain an OPEN/CAESAR
application program, such as
exhibitor,
evaluator,
terminator...
The exploration
module can be supplied in three different forms. It can be either an archive
file (with .a suffix), or a source C program (with .c suffix) or an object
code file (with .o suffix).
If prog.a is not present in the current directory,
seq.open attempts to fetch it in the OPEN/CAESAR binary library $CADP/bin.`arch`.
If prog.c is not present in the current directory, seq.open attempts to fetch
it in the OPEN/CAESAR source library $CADP/src/open_caesar.
If prog.o is
not present in the current directory, seq.open attempts to fetch it in the
OPEN/CAESAR binary library $CADP/bin.`arch`.
If no suffix (.a, .c, .o) is specified
on the command line for the exploration module prog, seq.open will make
successive attempts to fetch this exploration module: first, as a source
C program with .c suffix; then as an archive file with .a suffix; finally
as an object code file with suffix .o.
Only
the ``link mode'' of OPEN/CAESAR is supported by
seq.open.
The
cc_options,
if any, are passed to the C compiler.
The prog_options, if any, are passed
to prog. The following options seq_options are currently available:
- -seqno number
- Select the number-th sequence in filename.seq as the only sequence to be
considered during exploration. number should be a positive integer. By default
(if this option is not present on the command line) or if seqno is equal
to zero, all sequences contained in filename.seq will be considered. If filename.seq
only contains a single sequence, using option `-seqno 1' may speed up the
execution by avoiding a preliminary scan of the sequence file.
- -cache number
- Select the size of the hash-based cache table used to avoid recomputations
of label strings and successor transitions. This size defines the number
of entries in the cache table. If number is not a prime, it will be replaced
by the closest higher prime number. By default (if this option is not present
on the command line), the cache size will be 49999.
- -stat
- Print statistics
about the usage of cache, such as the number of failures (the requested
data is not stored in the cache) and the number of successes (the requested
data is already in cache) every time a sink state is reached (i.e., at the
end of each sequence). Not a default option.
Exit status is 0
if everything is alright, 1 otherwise.
Hubert GARAVEL, Radu MATEESCU,
and Bruno ONDET (INRIA Rhone-Alpes / VASY)
- filename.seq
- sequence
graph (input)
- prog.a
- exploration module (archive, input)
- prog.c
- exploration
module (source, input)
- prog.o
- exploration module (object code, input)
- prog
- executable program (output)
- $CADP/com/seq.open
- ``seq.open'' shell script
- $CADP/bin.`arch`/libseq_open.a
- ``seq.open'' static library
- $CADP/incl/caesar_*.h
- OPEN/CAESAR interfaces
- $CADP/bin.`arch`/libcaesar.a
- OPEN/CAESAR library
- $CADP/src/open_caesar/*.c
- exploration modules (source)
- $CADP/bin.`arch`/*.a
- exploration modules (archive)
- $CADP/bin.`arch`/*.o
- exploration modules (object code)
seq
,
lotos.open
,
exhibitor
Additional information is available
from the CADP Web page located at http://cadp.inria.fr
Directives for installation
are given in files $CADP/INSTALLATION_*.
Recent changes and improvements
to this software are reported and commented in file $CADP/HISTORY.
Please
report bugs to
Hubert.Garavel@inria.fr
Table of Contents
