|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
or:
exp.open [exp_opt] spec[.exp] [cc_opt] tgv [tgv_opt] test_purpose[.bcg|.aut] test_case[.bcg]
or:
fsp.open [fsp_opt] spec[.lts] [cc_opt] tgv [tgv_opt] test_purpose[.bcg|.aut] test_case[.bcg]
or:
lnt.open [lnt_opt] spec[.lnt] [cc_opt] tgv [tgv_opt] test_purpose[.bcg|.aut] test_case[.bcg]
or:
lotos.open [lotos_opt] spec[.lotos] [cc_opt] tgv [tgv_opt] test_purpose[.bcg|.aut] test_case[.bcg]
or:
seq.open [seq_opt] spec[.seq] [cc_opt] tgv [tgv_opt] test_purpose[.bcg|.aut] test_case[.bcg]
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 test_purpose.bcg or in an AUT file test_purpose.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.
Accepting
(respectively refusing) states must be given as loop-transitions with the
predefined label ACCEPT or accept (respectively REFUSE or refuse). 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 LOCK, OUTPUTLOCK,
DEADLOCK, LIVELOCK used in lock transitions. A tag (INPUT or OUTPUT), seen
from the tester's viewpoint, is added to each label. In some transitions,
a verdict (PASS) or PASS or (INCONCLUSIVE) or INCONCLUSIVE is also added
to the label.
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.
In general, there are no explicit FAIL verdicts
since, from each state, any unrecognized action of the IUT leads to an
implicit FAIL verdict. However, with the -timer option, explicit FAIL verdicts
can be generated when timeouts occur.
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.
The produced graph is in general not minimal for strong bisimulation. See the bcg_min manual page for information about how to minimize the produced graph.
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 lotos_opt, if any, are passed to caesar and to caesar.adt .
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 -all)
to keep all the computed locks (the produced test graph is no more completely
controllable).
OUTPUTLOCK, DEADLOCK,
LIVELOCK) with option -difflock.
-timer, -difflock, and -unlock.
<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 input (respectively output),
the body of the file describes all the inputs actions (respectively all
outputs actions).
Note: If option -io is not given, TGV uses by default the file $CADP/src/tgv/default.io the contents of which are:
input
[^!]*[?].*
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).
File file 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