caesar.open [caesar_opt] spec[.lotos] [cc_opt] exhibitor [exhibitor_opt]
exp.open [exp_opt] spec[.exp] [cc_opt] exhibitor [exhibitor_opt]
fsp.open [fsp_opt] spec[.lts] [cc_opt] exhibitor [exhibitor_opt]
lnt.open [lnt_opt] spec[.lnt] [cc_opt] exhibitor [exhibitor_opt]
seq.open [seq_opt] spec[.seq] [cc_opt] exhibitor [exhibitor_opt]
exhibitor performs an on-the-fly search in the Labelled Transition System (LTS), looking for execution sequences (also called "diagnostic sequences") that start from the initial state and match the specified pattern.
exhibitor displays on the standard output, in the simple SEQ format, the diagnostic sequence(s) found, if any. If no diagnostic sequence has been found, exhibitor displays an empty result (this case is covered by the simple SEQ format).
If the input pattern is empty (which is allowed by the syntax of the full SEQ format), exhibitor stops immediately, as no diagnostic sequence can be found.
If the input pattern contains more
sequence (see the seq
manual page for details), exhibitor
only searches for a single one, according to the number supplied with the
In the CADP toolbox, the SEQ format is the standard format
for diagnostic sequences. Many CADP tools take their inputs and/or deliver
their outputs in this format. Unfortunately, such diagnostic sequences are
not necessarily as short as possible and some information might have been
lost (e.g., sequences of
i-transitions have been compacted or eliminated,
the original gate names corresponding to
i-transitions have vanished, etc.).
In many cases, exhibitor solves these problems by allowing to find the shortest sequence matching a given pattern and by providing the source-level information which has been lost. It is also useful for verification and test purpose, because it can search and display automatically an execution scenario defined by a given pattern.
Two small examples will illustrate the differences between both algorithms.
Let S be the sequence
L1; L2; exit  L3; exitThe BFS algorithm will find the optimal solution:
L3; exitin a few steps, whereas the DFS algorithm might very well explore entirely the longest path:
L1; L2; exitbefore finding a better solution. Also, if there are *-s in the sequence to be searched and circuits in the LTS, the sequence found by the DFS algorithm might not be minimal.
L1; exit ||| L2; exit ||| ... ||| Ln; exitThe DFS algorithm will directly find a solution in n+1 steps, whereas the BFS will have to explore and store all the 2^n possible interleavings of transitions
L1, ..., Lnbefore finding a solution.
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 options exhibitor_options are currently available:
regular_expressions specified in the input stream. Not a default option. By default, all lower-case letters contained in
regular_expressions are turned to upper case, except for the special gates
"exit"(see the seq manual page for details).
For the DFS algorithm: print only those diagnostic sequences which are shorter than the last diagnostic sequence previously displayed. 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 DFS algorithm). Not a default option for the DFS algorithm.
For the DFS algorithm: 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).
Version 2 of exhibitor was developed by Hubert Garavel and Xavier Etchevers, with the help of Radu Mateescu.
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.Hubert.Garavel@inria.fr