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
Accepting (respectively refusing) states must be given as
loop-transitions with the predefined label
refuse). The purpose must own one accepting state at least.
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:
'(' <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 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)
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 TGV program.
The following tgv_opt
- 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).
- 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.
- For each state s of the test purpose such that s
does not have, for each action a of the specification, an outgoing transition
labelled with a, and s does not have an outgoing transition labelled with
the predefined label "
*", 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.
- -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 tags (
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 input or output,
nor with 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.
is recommended to write an .io
file, to distinguish between inputs and outputs.
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:
This is an optional input file. See the caesar_hide_1
page for the grammar description and examples.
This is an optional
input file. See the caesar_rename_1
manual page for the grammar description
Note 1: renaming patterns are applied before hiding patterns.
Renaming and hiding patterns are applied after the synchronous product
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: "
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
Thierry JÚron (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.
report any bug to email@example.com
Table of Contents