The SEQ format (where SEQ stands for SEQuence) is used to specify a finite set (possibly empty) of execution sequences belonging to a Labelled Transition System (LTS). Each of these sequences is finite and starts from the initial state of the LTS. Thus, a SEQ file specifies a subgraph of the LTS; in this subgraph, only the initial state may have more than one successor state (namely, if there are several sequences).
The SEQ 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. Files in the SEQ format are expected to have a .seq extension.
There are two versions of the SEQ format:
Both versions of the SEQ 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 SEQ format is
described below using a notation similar to the BNF (Backus-Naur Form) notation.
However, as the angle brackets
> used in BNF are also meaningful in
the SEQ format, there are some differences with respect to the standard
'<while>', etc.). In particular,
'\t'denote the newline and tabulation characters.
sequence_list, etc.). Contrary to the standard BNF notation, non-terminal symbols are not enclosed within angle brackets.
*) for zero or more repeated occurrences, and vertical bar (
|) for alternates.
Note: it should be understood that
'*' do not have the same meaning:
the former is the meta-symbol denoting repeated occurrences, whereas the
latter denotes the terminal character "star".
stringis a sequence of characters, enclosed between double quotes characters
'"', that denotes a label of the LTS:
string ::= '"' valid_character* '"'where
valid_characterdenotes any character different from double quote (
'"') and from end-of-line (
'\n'). Consequently, a
stringcannot encompass several lines; however, there can be several
strings on the same line (see, e.g.,
strings can be used in both the simple
and full SEQ format, with the same lexical conventions.
regular_expressionis a notation for a set of labels. The
regular_expressions of the SEQ format are based upon UNIX basic regular expressions (see the regexp(5) and regexp manual page for a detailed description of UNIX basic regular expressions). Syntactically, a
regular_expressionof the SEQ format is a UNIX basic regular expression enclosed between square brackets
regular_expression ::= '[' UNIX_basic_regular_expression ']'Unlike standard UNIX basic regular expressions, each
regular_expressionmust satisfy two additional restrictions:
regular_expressionwould be confused with another meaningful token
UNIX_basic_regular_expression. This precludes the use of very particular regular expressions such as
'abc]d'. This restriction should not be a problem for OPEN/CAESAR users.
encompass several lines; however, there can be several
on the same line (see, e.g.,
Note: the choice
'|' is not supported in UNIX basic regular expressions. For instance,
[PUT.*|GET.*]will search for a label of the form
"PUT.*|GET.*"rather than for either
"GET.*". However, the intended meaning can be obtained using the choice operator available in the syntax of
labels (see below):
[PUT.*] | [GET.*]
regular expressions can only be used in the full SEQ format.
blankis a (possibly empty) sequence of space characters
' 'and/or tab
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
Note: end-of-line characters (
'\n') are not part of
blanks. On the contrary, they are meaningful in the SEQ format as they are
used in the definition of many non-terminal symbols.
Both versions of the
SEQ format share the same lexical conventions for
commentis a sequence of characters that is meaningless and ignored. There are two kinds of
'\001'(control-A) and that ends with the special character
'\002'(control-B) is a
commentof this form may encompass several lines of text. The characters
'\002'have been selected because they are not visible by the user.
commentextends up to the end-of-line. This definition includes the case of lines that contain nothing but
Both versions of the SEQ format
share the same lexical conventions for
sequence_list ::= '' | sequence | sequence '' '\n' sequence_list sequence ::= string '\n' | string '\n' sequence | '<deadlock>' '\n'
Note: this grammar defines a regular language.
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
simple_label) appears on a single line of text.
Note: from the grammar, the postfix operators
'*', and the
'<until>' operators have the lowest priority. Then,
the binary operators
'^' have the same, intermediate priority. Finally,
the prefix operator
'~' has the highest priority.
Note: the simple SEQ format
is the subset of the full SEQ format in which each
label_group is constrained
to be simply a
Let (S0 T1 ... Tn Sn) be an execution sequence that starts from some state S0 (not necessarily the initial state of the LTS) and that reaches some state Sn by applying n successive transitions T1, ..., Tn. The number n of transitions can be null.
A SEQ file contains a finite list of execution
sequences, separated by
'' keyword. This list can be empty, as specified by the
'' token in the
BNF-like grammar. The semantics of the full format is only defined for a
sequencemust be selected; for instance, the -seqno of the exhibitor tool enables the user to indicate which
sequenceis to be considered. In such case, the semantics of the full format is the set of all execution sequences (S0 T1 ... Tn Sn) such that S0 is equal to the initial state of the LTS and such that the sequence-matching relation "(S0 T1 ... Tn Sn) |====
sequence" defined hereafter is satisfied.
For any transition T of the LTS, let L(T) denote the character string generated from the label of transition T.
Let "T |=
simple_label" be a relation expressing
that the transition T "matches"
simple_label. This relation is defined by
induction on the syntax of
simple_label and it is mutually recursive with
the relation "T |==
label" defined in the next subsection.
'(' label ')'
Let "T |==
be a relation expressing that the transition T "matches"
label. This relation
is defined by induction on the syntax of
labeland T |=
labelor T |=
labelexclusive-or T |=
apply to entire
label strings, from the first character to the last one,
and not to substrings. For instance, the
'PUT !0' will match the regular
'PUT.*', but not
'PUT'. Consequently, the special characters
'$' of UNIX basic regular expressions are useless in the SEQ format, and
should not be used.
Let "(S0 T1 ... Tn Sn)
label_group" be a relation expressing that the execution sequence (S0
T1 ... Tn Sn) matches
label_group. This relation is defined by induction on
the syntax of
'<until>' used in the syntactic definition
label_group are merely shorthand notations introduced for user convenience.
They are defined as follows:
label '+'is equivalent to:
label '\n' label '*'It denotes a sequence of one or more transitions matching
'<while>' labelis equivalent to:
label '*'It denotes a sequence of zero or more transitions matching
'<until>' labelis equivalent to:
'(~' label ')*' '\n' labelIt denotes a sequence of zero or more transitions that do not match
label, followed by a transition matching
'<while>' label1 '<until>' label2is equivalent to:
'(' label1 '& ~' label2 ')*' '\n' label2It denotes a sequence of zero or more transitions that match
label1and do not match
label2, followed by a transition matching
Let "(S0 T1 ... Tn Sn) |====
sequence" be a relation expressing
that the execution sequence (S0 T1 ... Tn Sn) matches
sequence. This relation
is defined by induction on the syntax of
label_group '\n' sequence
exhibitor interprets the full SEQ format in particular ways, described hereafter. exhibitor operates on the fly and is based on the OPEN/CAESAR's graph module, it implements the aforementioned T(L) notation by invoking the
CAESAR_STRING_LABEL()function (see the caesar_graph manual page). caesar when printing labels as character strings, all lower-case letters contained in
regular_expressions are turned to upper case. However, the
regular_expressions (case-insensitively) equal to
"exit"are recognized as special values (denoting the internal gate and the termination gate) and turned to lower case.
This is the default option, but it can be overriden using the -case option of exhibitor if case sensitivity needs to be preserved.
sequence, exhibitor will search for execution sequences (S0 T1 ... Tn Sn)
such that S0 is equal to the initial state of the LTS and such that (S0
T1 ... Tn Sn) |====
In the above second semantic rule defining sequence
matching (namely, "(S0 T1 ... Tn Sn) |====
label_group '\n' sequence"), 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 of exhibitor (see the exhibitor manual page for a detailed decription of this 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
"A". It should be written instead:
(~ "A") * "A"Note: translating the
label '*' '\n' labelwould not be correct because, due to the determinization strategy, this sequence is never recognized (one always remains in the '*'-group).
"A" "B"* "C"*is reduced to:
"A"If the sequence becomes empty due to this reduction, exhibitor emits a warning and stops.
"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
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.
It is easy to create a SEQ file manually, using a text editor. It is also possible to produce a SEQ file automatically, using the bcg_io tool, which converts to the simple SEQ format a graph (encoded in various other formats) consisting of a set of sequences all starting from the initial state. Finally, many CADP tools for simulation, model checking, equivalence checking, etc. generate their output in SEQ format when such output denotes an execution sequence or a set of execution sequences (as opposed to more general labelled transition systems).
The tool seq.open reads a SEQ file in the simple SEQ format.
The tool exhibitor reads a SEQ file in the full SEQ format.
SEQ files can be converted to many other graph formats using the bcg_io tool.
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.firstname.lastname@example.org