EXHIBITOR manual page
Table of Contents

Name

exhibitor - search for execution sequences matching a given pattern

Synopsis

bcg_open [bcg_opt] spec[.bcg] [cc_opt] exhibitor [exhibitor_opt]

or:

caesar.open [caesar_opt] spec[.lotos] [cc_opt] exhibitor [exhibitor_opt]

or:

exp.open [exp_opt] spec[.exp] [cc_opt] exhibitor [exhibitor_opt]

or:

fsp.open [fsp_opt] spec[.lts] [cc_opt] exhibitor [exhibitor_opt]

or:

lnt.open [lnt_opt] spec[.lnt] [cc_opt] exhibitor [exhibitor_opt]

or:

seq.open [seq_opt] spec[.seq] [cc_opt] exhibitor [exhibitor_opt]

Description

exhibitor takes two different inputs:

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 the diagnostic sequence(s) found, if any, using the simple SEQUENCE format. The case in which no diagnostic sequence has been found is also covered by the simple SEQUENCE format.

In the CADP toolbox, the SEQUENCE format is the standard format for specifying diagnostic sequences. For instance, aldebaran and OPEN/CAESAR tools produce diagnostic sequences 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.

Description of the Sequence Format

Basically, the SEQUENCE format is used to specify a finite set (possibly empty) of execution sequences. Each execution sequence starts from the initial state and is constituted by a finite, sequential list of labels. A branching structure (i.e., non-deterministic choice) is only allowed at the initial state, if there is more than one sequence.

The SEQUENCE format has been carefully designed so as to be easily readable and writable by both humans and computer programs. For this reason, it is a character-based format.

There are two versions of the SEQUENCE format:

Both versions of the SEQUENCE format are compatible in the sense that the simple format is a subset of the full format. Therefore, the simple format can be used at every place where the full format is allowed.

The syntax of the SEQUENCE formats are described below using a notation similar to the BNF (Backus-Naur Form) notation. However, as the angle brackets < and > used in BNF are also meaningful in the SEQUENCE format, there are some differences with respect to the standard BNF notation:

Note: it should be understood that * and '*' do not have the same meaning: the former is the meta-symbol denoting repeated occurrences, whereas the latter denotes the terminal character "star".

Strings

A string is a sequence of characters, enclosed between double quotes characters '"', that denotes a label of the LTS. All the characters of a string must be different from '"' (double-quote) and '\n' (end-of-line). As a consequence, a string cannot encompass several lines; however, there can be several strings on the same line. 
 string ::= '"' valid_character '"'
where valid_character denotes any character different from double quote ('"') and from end-of-line ('\n') Both versions of the SEQUENCE format share common lexical conventions for strings.

Regular Expressions

A regular_expression is a notation for a set of labels. The regular_expressions of the SEQUENCE format are based upon UNIX regular expressions (see the regexp(5) and regexp manual page for a detailed description of UNIX regular expressions). Syntactically, a regular_expression of the SEQUENCE format is a UNIX regular expression enclosed between square brackets '[' and ']': 
 regular_expression ::= '[' UNIX_regular_expression ']'
There are two restrictions that the UNIX_regular_expression must satisfy:

Like strings, regular_expressions cannot encompass several lines; however, there can be several regular_expressions on the same line.

regular expressions can only be used in the full SEQUENCE format.

Blanks

A blank is a (possibly empty) sequence of space characters ' ' and/or tab '\t' characters: 
  blank ::= ( ' ' | '\t' )*
Blanks can appear anywhere, at the beginning of a line, at the end of a line, or between two tokens. They are ignored (except, of course, in strings and regular expressions).

Note: end-of-line characters ('\n') are not part of blanks. On the contrary, they are meaningful in the SEQUENCE format as they are used in the definition of many non-terminals symbols.

Both versions of the SEQUENCE format share common lexical conventions for blanks.

Comments

A comment is a sequence of characters that is meaningless and ignored. There are two kinds of comments:

Both versions of the SEQUENCE format share common lexical conventions for comments.

Syntax of the Full Format

The following BNF-like grammar defines the syntax of the full SEQUENCE format. The axiom of the grammar is sequence_list. 
sequence_list     ::= ''
                   |  sequence
                   |  sequence '[]' '\n' sequence_list

sequence          ::= label_group '\n'
                   |  label_group '\n' sequence 
                   |  '<deadlock>' '\n'

label_group       ::= label
                   |  label '*'
                   |  label '+'
                   |  '<while>' label
                   |  '<until>' label
                   |  '<while>' label '<until>' label

label             ::= simple_label
                   |  label '&' simple_label
                   |  label '|' simple_label
                   |  label '^' simple_label

simple_label      ::= '<any>'
                   |  string
                   |  regular_expression
                   |  '~' simple_label
                   |  '(' label ')'
Note: each label_group (and consequently each label and simple_label) appears on a single line of text.

Note: from the grammar, the postfix operators '+' and '*', and the '<while>' and '<until>' operators have the lowest priority. Then, the binary operators '&', '|', and '^' have the same, intermediate priority. Finally, the prefix operator '~' has the highest priority.

Syntax of the Simple Format

The following BNF-like grammar defines the syntax of the simple SEQUENCE format. The axiom of the grammar is sequence_list. 
sequence_list     ::= ''
                   |  sequence
                   |  sequence '[]' '\n' sequence_list
sequence          ::= string '\n'
                   |  string '\n' sequence
                   |  '<deadlock>' '\n'
Note: the simple SEQUENCE format is the subset of the full SEQUENCE format in which each label_group is constrained to be simply a string.

Note: this BNF grammar defines a regular language.

Semantics of the Full Format

The semantics of the full format is defined as follows; the semantics of the simple format can be derived as a special case.

A SEQUENCE file defines a finite list of execution sequences, separated by the '[]' keyword. This list can be empty, as specified by the '' token in the BNF grammar (in such case, exhibitor stops immediately). If the list contains more than one sequence, a unique one is selected according to the number supplied with -seqno option (see below).

Let T be any transition of the LTS. Let L(T) denote the character string generated from the label of transition T by applying the CAESAR_STRING_LABEL() function of OPEN/CAESAR's graph module (see the caesar_graph manual page).

Let "T |= simple_label" and "T |== label" be two relations expressing that a transition T "matches" a simple_label and a label. These relations are mutually recursive and they are recursively defined by induction on the syntaxes of simple_label and label.

- Definition of "T |= simple_label":

T |= '<any>'
is always true

T |= string
iff L(T) is equal to string

T |= regular_expression
iff L(T) matches regular_expression

T |= '~' simple_label
iff not T |= simple_label

T |= '(' label ')'
iff T |== label

- Definition of "T |== label":

T |== simple_label
iff T |= simple_label

T |== label '&' simple_label
iff T |== label and T |= simple_label

T |== label '|' simple_label
iff T |== label inclusive-or T |= simple_label

T |== label '^' simple_label
iff T |== label exclusive-or T |= simple_label

Note: in order to be compatible with the conventions used by CAESAR when printing labels as ASCII strings, all lower-case letters contained in strings and regular_expressions are turned into upper-case, excepted the two special gates 'i' and 'exit', which are recognized and turned into lower-case letters. This is the default option, but it can be overriden using the -case option (see below) if case-sensitivity is desired.

Note: regular_expressions apply to entire label strings, from the first character to the last one, and not to substrings. For instance, the label 'PUT !0' will match the regular expression 'PUT.*', but not 'PUT'. Consequently, the special characters '^' and '$' of UNIX regular expressions are useless in the SEQUENCE format, and should not be used.

Let (S0 T1 ... Tn Sn) be an execution sequence that starts from some state S0 and that reaches some state Sn by applying n successive transitions T1, ..., Tn. The number n of transition can be null.

Let "(S0 T1 ... Tn Sn) |=== label_group" be a relation expressing that the execution sequence (S0 T1 ... Tn Sn) matches a label_group. This relation is defined by induction on the syntax of label_group.

- Definition of "(S0 T1 ... Tn Sn) |=== label_group":

(S0 T1 ... Tn Sn) |=== label
iff n = 1 and T1 |== label

(S0 T1 ... Tn Sn) |=== label '*'
iff for all i in {1 ... n} Ti |== label

The cases of '+', '<while>' and '<until>' will be tackled hereafter.

Let "(S0 T1 ... Tn Sn) |==== sequence" be a relation expressing that the execution sequence (S0 T1 ... Tn Sn) matches a sequence. Given a sequence, exhibitor will search for execution sequences (S0 T1 ... Tn Sn) such that S0 is the initial state of the LTS and such that (S0 T1 ... Tn Sn) |==== sequence. This relation is defined by induction on the syntax of sequence.

- Definition of "(S0 T1 ... Tn Sn) |==== sequence":

(S0 T1 ... Tn Sn) |==== label_group '\n'
iff (S0 T1 ... Tn Sn) |=== label_group

(S0 T1 ... Tn Sn) |==== label_group '\n' sequence
iff there exists some state Sm in the sequence (S0 T1 ... Tn Sn) such that:
(S0 T1 ... Tm Sm) |=== label_group and
(Sm Tm+1 ... Tn Sn) |==== sequence

(S0 T1 ... Tn Sn) |==== '<deadlock>' '\n'
iff n = 0 (the sequence is reduced to a single state) and
S0 is a sink state (no transition goes out from S0)

Note: In the second semantic rule above, if there exist several states Sm, the one with the greatest index m is selected. By doing so, exhibitor reduces potentially non-deterministic sequences into deterministic ones. Intuitively, every time that exhibitor has the choice between remaining in a '*'-group or leaving it, it will remain in the '*'-group. For instance, if the label "B" has to be matched against the sequence: 

      (~ "A") *
      "B"
there is a conflict, since "B" matches both lines of the sequence. In such case, the sequence will not be recognized successfully, since the label "B" will be used to match the first line of the sequence instead of the second line. Therefore, the determinization strategy gives priority to the longest match.

The -conflict option can be used to display the list of all conflicts which have been solved using this determinization strategy.

The solution to this problem consists in avoiding the conflict by making the sequence more precise: 

      (~ "A" & ~ "B") *
      "B"
Similarly, the sequence: 
      <any>*
      "A"
will never be recognized, because of the conflict between <any> and "A". It should be written instead: 
      (~ "A") *
      "A"
In the syntactic definition of label_group, the following constructs are simply shorthand notations introduced for user convenience:

Sequence Reduction

exhibitor removes all trailing '*'-groups at the end of the sequence to be searched, because these groups are meaningless. For instance, the following sequence: 
      "A"
      "B"*
      "C"*
is reduced to: 
      "A"
If the sequence becomes empty due to this reduction, exhibitor emits a warning and stops.

Examples of Patterns

The following sequence: 
     "i" *
     "PUT"
     "i" *
     "GET"
searches for an action "PUT", followed by an action "GET", with any number of invisible actions "i" before and between.

The following sequence: 

     <until> [PUT !TRUE !.*]
     <until> [GET !FALSE !.*]
searches for an action of the form "PUT !TRUE !.*", followed by an action of the form "GET !FALSE !.*", with any number of visible or invisible actions before and between.

The following sequence: 

    <until> ([SEND !.*] & ~ "SEND !NULL")
searches for an action of the form "SEND !.*" such that the offer associated with gate "SEND" is different from "NULL".

The following sequence: 

     <until> "OPEN !1"
     <while> ~ "CLOSE !1" <until> "OPEN !2"
searches for an action "OPEN !1", followed by an action "OPEN !2" without any "CLOSE !1" action between them.

The following sequence: 

      <any>*
      <deadlock>
searches for deadlocks. Thus, exhibitor can be used as an alternative to terminator , although it implements totally different algorithms.

The alternation operator '|' is not supported in regular expressions, i.e.: 

      [PUT.*|GET.*]
will search for a label of the form "PUT.*|GET.*" rather than for either "PUT.*" or "GET.*". However, the intended meaning can be obtained by the following pattern: 
      [PUT.*] | [GET.*]

Search Algorithms

exhibitor implements two different search algorithms, one based on a breadth-first search (BFS) and another one based on a depth-first search (DFS). Both algorithms have their own merits. Here is a brief comparison:

Two small examples will illustrate the differences between both algorithms. Let S be the sequence '<until> "exit"'.

Options

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 options exhibitor_options are currently available:

-seqno number
Select the number-th sequence in the input stream as the pattern to be searched for. number should be a non-zero, positive integer. It should be less or equal to the number of sequences contained in the input stream. By default, the first sequence will be selected.

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

-conflict
When the search is done, print information about those labels that created non-determinism conflicts, solved in a deterministic way (see the semantics of the SEQUENCE format above). Not a default option.

-case      
Preserve case-sensitivity in the strings and regular_expressions specified in the input stream. Not a default option. By default, all lower-case letters contained in strings and regular_expressions are turned to upper-case (the special gates "i" and "exit" excepted).

-bfs      
Use the breadth-first search algorithm. Default option.

-dfs      
Use the depth-first search algorithm. Not a default option.

-none      
Don't print any diagnostic sequence. Not a default option.

-all      
Print all diagnostic sequences. With the BFS algorithm, all the printed sequences are minimal. Not a default option.

-first      
Print the first diagnostic sequence encountered and stop just after. Not a default option for the DFS algorithm.

-decr      
For the BFS algorithm: this option is identical to -first.

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.

by default
(in absence of -none, -all, -first, -decr) For the BFS algorithm: default is identical to -first.

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

Exit Status

When the source is erroneous, error messages are issued. Exit status is 0 if everything is alright, 1 otherwise.

Authors

Version 1 of exhibitor was developed by Hubert Garavel (INRIA Rhone-Alpes).

Version 2 of exhibitor was developed by Hubert Garavel and Xavier Etchevers, with the help of Radu Mateescu.

Operands

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)

(standard input)
pattern in SEQUENCE format (input)

Files

The binary code of exhibitor is available in $CADP/bin.`arch`/exhibitor.a

See Also

CAESAR Reference Manual, OPEN/CAESAR Reference Manual, bcg_open , bcg , caesar.open , caesar , caesar.adt , caesar_graph , cc(1), exp.open , fsp.open , lnt.open , seq.open

Additional information is available from the CADP Web page located at http://www.inrialpes.fr/vasy/cadp

Directives for installation are given in file $CADP/INSTALLATION.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.

Bugs

Please report new bugs to Hubert.Garavel@inria.fr

Table of Contents