Table of Contents
tgv - Test Generation from transitions systems using Verification techniques
caesar.open [caesar_opt] spec[.lotos] [cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
exp.open [exp_opt] spec[.exp] [cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
[fsp_opt] spec[.lts] [cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
spec[.lnt] [cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
seq.open [seq_opt] spec[.seq]
[cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
TGV allows the generation
of an abstract test case from a specification and a test purpose. The generation
is done "on-the-fly" on the synchronous product of the specification with
the test purpose. It is based on Tarjan's algorithm. During the depth-first
search (DFS), TGV performs abstraction and determinisation of this product.
The DFS stops when an accepting state of test purpose is reached. During
the backtracking, TGV synthesizes the transitions of the test case.
specification and the test purpose are Inputs/Outputs Labeled Transition
Systems (IOLTS). The specification is either the BCG graph spec.bcg, the
LOTOS program spec.lotos, the composition expression spec.exp, the FSP program
spec.lts, the LNT program spec.lnt, or the sequence file spec.seq.
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.
See the bcg
See the aut
purpose is an abstract description of a subset of the specification, allowing
to choose behaviors to test, and consequently allowing to reduce the specification
exploration. Final states of the test purpose graph are either accepting
states (the purpose is reached) or refusing states (parts of the specification
are rejected). Accepting (respectively refusing) states must be given as
loop-transitions with the predefined label
).The purpose must own one accepting state at least. The
) is used to complete the action grammar.
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.
So, for an AUT test purpose, a transition has the following grammar:
'(' <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.
If the test purpose is valid, i.e. allows to
select sequences of the specification leading to an accepting state, TGV
produces an LTS that is the description of the test graph in the BCG format
) or AUT (.aut
Actions labels of this LTS are exactly the same
as specification ones, plus some predefined labels as
DEADLOCK, LIVELOCK used in lock transition. A type (
from the tester, is added to each label. In some transitions, a verdict
PASS or (
INCONCLUSIVE is also added to the label.
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. A
PASS verdict on a transition means that in the state reached
by this transition, the tester has detected no implementation error in
the IUT. An
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. The
FAIL transitions are implicit (from each
state, unrecognized actions lead to a
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 cc_opt, if
any, are passed to cc(1).
The options tgv_opt, if any, are passed to the
The following tgv_opt
are currently available:
- Verbose mode: TGV displays information about the calculations going on.
Not a default option.
- -io file[.io]
- Specify the inputs/outputs of the specification,
according to file[.io] (in case of renaming with -rename option, the .io file
must contain renamed labels).
- -rename file[.ren|.rename]
- Use the renaming rules
defined in file[.ren|.rename] to rename the labels of the product SPEC x TP.
- -hide file[.hid|.hide]
- Use the hiding rules defined in file[.hid|.hide] to hide
some labels of the product SPEC x TP.
- Priority to actions of the
test purpose. By default, the actions of the specification are prior.
- Priority to the outputs. By default, the inputs are prior.
- -hash n
- Fix the
table hash size to n (by default, 100000).
- -depth n
- Fix the maximum preamble-body
depth search to n.
- -output file[.bcg|.aut] [-parse|-unparse]
- Specify the namefile[.bcg|.aut]
of the output file in which TGV will display the test case. If the filename
extension is .aut, the result is an AUT file. Otherwise, the result file
is a BCG file with the .bcg extension. By default, the result is printed
on the BCG file tgv_result.bcg.
If the produced test case is in BCG format, options -parse and -unparse
can be specified to control label parsing (see the bcg_write
page for a technical discussion about label parsing). Option -parse enables
label parsing and option -unparse disables label parsing. By default, label
parsing is enabled.
- Display all fired labels. Notice that displaying
all labels of the specification can be obtained by using this option with
the following test purpose:
des (0, 3, 2)
(0, *, 0)
(0, "dummy:", 1)
(1, ACCEPT, 1).
- By default, TGV computes lock transitions (
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
- Avoid the printing of lock transitions with
option -unlock. Make difference between lock types (
LIVELOCK) with option -difflock.
- Compute the complete test graph
(option -csg) or compute a controllable test case without loop (option -unloop).
By default, TGV computes controllable test cases with loops.
- Search a postamble from pass and inconclusive states (i.e. a path to
stable states in which no message from the IUT is expected).
- -postdepth n
- Fix the maximum postamble depth search to n.
- Compute a random test
case. Not a default option.
- -randomseed n
- Use n as seed for random test-case
- Do not annotate transition labels with io-type (input or
output) and/or verdicts, but generate separate, self-looping verdict transitions
for each verdict state. This option is incompatible with options
- Produce a test case with test timers (TAC and
TNOAC). TAC is started when the tester is waiting for an output from the
IUT. TNOAC allows to detect a lock state of the IUT.
- Open a
window for monitoring in real-time the generation of the test case or complete
test graph. Not a default option.
- Enable label parsing when reading
files in the AUT format and/or writing files in the BCG format (see the
manual page for a technical discussion about label parsing).
Note that this also applies to the implicit conversions of command-line
arguments in the AUT format. Default option.
- Disable label parsing
when reading files in the AUT format and/or writing files in the BCG format
(see the bcg_write
manual page for a technical discussion about
label parsing). Note that this also applies to the implicit conversions
of command-line arguments in the AUT format. Not a default option.
It is recommended to write an .io
file, to distinguish
between inputs and outputs. The .io
file describes a set of actions, according
to the following grammar:
<file.io> ::= 'input' | 'output' \n <regexp-list>
<regexp-list> ::= <regexp> \n <regexp-list>
| "<regexp>" \n <regexp-list>
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:
see the caesar_hide_1
manual page for the grammar description
see the 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).
If TGV produces a test
case, the execution finishes with the following message: "
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
TGV also exists for an SDL specification. In
that case, TGV is connected to ObjectGeode (VERILOG). Please contact Thierry
) for further information.
), 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 maintained by Wendelin
Serwe and Hubert Garavel.
Please report any bug to firstname.lastname@example.org
Table of Contents