exp.open [exp_opt] spec[.exp] [cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
fsp.open [fsp_opt] spec[.lts] [cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
lnt.open [lnt_opt] spec[.lnt] [cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
lotos.open [lotos_opt] spec[.lotos] [cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
seq.open [seq_opt] spec[.seq] [cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
The specification and the test purpose are Inputs/Outputs Labeled Transition Systems (IOLTS). The specification is either the BCG graph spec.bcg, the composition expression spec.exp, the FSP program spec.lts, the LNT program spec.lnt, the LOTOS program spec.lotos, or the sequence file spec.seq.
The test purpose is described either in a BCG file tp.bcg or in an AUT file tp.aut.
TGV uses the bcg_io tool to transparently convert a test purpose in AUT format into the BCG format, and to transform the generated test case or complete test graph into the AUT format.bcg manual page. aut manual page.
Accepting (respectively refusing) states must be given as loop-transitions
with the predefined label
The purpose must own one accepting state at least.
All action names are regular expressions (according to the definition given in the manual page of the POSIX regexp ). The test purpose is written in accordance with the specification label names (before renaming and hidding). It can also have transitions labelled with invisible actions of the specification.
If the predefined label "
*" (which means
otherwise) is present on a transition
leaving some state s, this label represents all other actions than those
already present on the outgoing transitions of state s.
So, for an AUT test purpose, a transition has the following grammar:
<transition> ::= '(' <from_state> ',' <action> ',' <to_state> ')' | '(' <state> ',' 'ACCEPT'|'accept' ',' <state> ')' | '(' <state> ',' 'REFUSE'|'refuse' ',' <state> ')' | '(' <from_state> ',' '*' ',' <to_state> ')' <action> ::= <UNIX_regexp> | '"' <UNIX_regexp> '"'
Note: if the extension of the test purpose filename is omitted (or is different from .bcg and .aut), the file is first searched with .bcg extension and then with .aut extension.
Actions labels of this LTS are based on those
of the specification, plus some predefined labels as
DEADLOCK, LIVELOCK used in lock transitions. A tag (
from the tester's viewpoint, is added to each label. In some transitions,
a verdict (
PASS or (
INCONCLUSIVE is also added
to the label.
PASS verdict on a transition means that in the state reached
by this transition, the tester has detected no implementation error in
INCONCLUSIVE verdict is present on a transition corresponding
to a possible output of the specification that leads to a sequence not
satisfying the test purpose.
There is no
FAIL verdict, as fail transitions
are implicit (from each state, unrecognized actions lead to a
A verdict not enclosed in parentheses means that the tester has reached a stable state from which no output of the implementation under test (IUT) is expected.bcg_lib .
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 cc(1).
The options tgv_opt, if any, are passed to the TGV program.
*", silently add on state s a self-loop transition labelled with "
*". By default, such a self-loop transition is added too, but a warning message is emitted for each such state s.
des (0, 3, 2) (0, *, 0) (0, "dummy:", 1) (1, ACCEPT, 1).
LOCK) and prints those that remain after conflicts have been resolved. Use -keeplock (without -csg) to keep all the computed locks (the produced test graph is no more completely controllable).
OUTPUTLOCK, DEADLOCK, LIVELOCK) with option -difflock.
<file.io> ::= 'input' | 'output' \n <regexp-list> <regexp-list> ::= <regexp> \n <regexp-list> | "<regexp>" \n <regexp-list> | <empty>
Semantically, if the first line is equal to
the body of the file describes all the inputs actions (respectively all
Note: If option -io is not given, TGV uses by default the file $CADP/src/tgv/default.io the contents of which are:
caesar_hide_1 manual page for the grammar description and examples. caesar_rename_1 manual page for the grammar description and examples.
Note 1: renaming patterns are applied before hiding patterns. Renaming and hiding patterns are applied after the synchronous product SPECxTP.
Note 2: the .io file must be written in accordance with the .ren (or .rename ) and .hid (or .hide ) files (because the .io file is read after the renaming and hiding).
produced". Otherwise, the message "
No test case" is printed: may be it is because the test purpose is not valid, or because of an error in the description of files .io or .hid or .ren Thierry.Jeron@irisa.fr), Pierre Morel, and SÚverine Simon. A few patches were brought by Wendelin Serwe and Hubert Garavel in December 2004. Since then, TGV has been ported to 64-bit architectures and regularly maintained by Wendelin Serwe and Hubert Garavel. bcg , bcg_open , caesar , caesar.adt , exp , exp.open , fsp.open , lnt.open , lotos , lotos.open , seq , seq.open email@example.com