SEQ.OPEN manual page
Table of Contents

Name

seq.open - OPEN/CAESAR connection for traces encoded in the SEQ format

Synopsis

seq.open [seq_options] filename[.seq] [cc_options] prog[.a|.c|.o] [prog_options]

Description

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 sequence 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 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.

Processing of the Exploration Module

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.

Determination of Include or Link Mode

Only the ``link mode'' of OPEN/CAESAR is supported by seq.open.

Options

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

Exit status is 0 if everything is alright, 1 otherwise.

Authors

Hubert GARAVEL, Radu MATEESCU, and Bruno ONDET (INRIA Rhone-Alpes / VASY)

Operands

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)

Files

$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)

See Also

sequence , 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.

Bugs

Please report bugs to Hubert.Garavel@inria.fr

Table of Contents