torx-config(4) - configuration file for torx tester
Table of Contents
torx-config - configuration file for torx tester
A torx(1)
configuration file contains all information that is needed for a test execution
run. Some of the the configation file entries can be overriden with command
line options of torx(1), as will be indicated in the ENTRIES section below.
Currently, the configuration file contains information that is used by
different components of torx: it contains information for the PRIMER, for
the DRIVER, and for the ADAPTER. In some cases, the same information is
used by more than a single component.
For most settings, only one entry
should appear in the configuration file(s) of torx(1). The settings for
which multiple entry lines are allowed, are prefixed with an asterisk (*)
in the ENTRIES section below.
Currently, the configuration file has the
following format. Each configuration entry consists of a single line. Such
a line starts with a keyword that indicates the kind of entry. Empty lines
and lines containing only whitespace are ignored. Comment lines start with
optional whitespace followed by a hash symbol (#). All relative file- and
directory names are interpreted relative to the (location of) the configuation
file in which they appear, not relative to the location from which torx(1)
is started. If an argument of an entry contains whitespace, it should be
enclosed between curly brackets ``{'' and ``}'' (because we treat each entry line
as a tcl list). See the EXAMPLES below to get an idea of how these rules
work out in practice.
The configration file entries are grouped in
the following sections: 1) general ones, 2) execution-run related, 3) PRIMER
related, 4) ADAPTER related, 5) INSTANTIATOR related, 6) internal, implementation
related: settings that should not need to be changed.
For most settings,
only one entry should appear in the configuration file(s) of torx(1). The
settings for which multiple entry lines are allowed, are prefixed with
an asterisk (*) below. Note that this asterisk is not part of the entry
keyword!
This section contains the general configuration entries
that may be useful in general.
- *INCLUDE filename
- Read the entries from filename
at the point where this entry is encountered (and then continue processing
the file in which the INCLUDE entry was encountered). Warning: currently
NO check is made against recursive inclusion. Be careful!
This
section contains the settings that you may want to vary from one test-execution-run
to another, even without varying the other settings, to re-execute with
a different seed or depth. It is no coincidence that most of these settings
can be overruled from the command line of torx(1).
- MAXSTEPS number
- (torx(1)
options: --depth, --no-depth) The number of steps to do. Also indicates that
these steps should be done in ``automatic'' mode, when torx(1) is started. Default
value: unset (i.e. torx(1) will by default be in single-stepping mode).
- LOGFILE
filename
- (torx(1) options: --log, --no-log) The filename of the logfile that
should be written. If a relative filename is given, it is taken to be relative
to the directory containg the configuration file. If a file with the resulting
name already exists, the filename will be extended with the sequence ~number~
where number is the smalles number that makes the filename unique. Default
value: unset
- *LOGMON command
- (torx(1) options: --logmon, --no-logmon) torx(1)
will start torx log monitoring command as a background process that can
continue to run even after torx itself has exited, and provides the command
with the text of the log file on its standard input. No LOGFILE need to
be set for this to work. torx(1) captures the standard output and standard
error output of command (as long as torx is running) and prints this on
standard error (preceded by a prefix). This is typically used to start tools
that give a particular ``view'' of (an aspect of) the test run. Visualization
can be such view; see for example anifsm(1). The command may have the form
commandwitharguments # xtorxToolsmenuentry in which case the command with
arguments will be run and the xtorx Tools menu entry will be present in
the xtorx(1) Tools menu. Default value: unset
- TRACEFILE filename
- (torx(1)
options: --trace, --no-trace) The filename of the tracefile that should be read.
If a relative filename is given, it is taken to be relative to the directory
containg the configuration file. Default value: empty
- SEED number
- (torx(1)
options: --seed, --no-seed) The seed of the randum number generators used by
the components of TorX. Default value: 4
This section contains the
settings that you usually only have to specify once when you start a test-campaign.
- SPEC filename
- The filename of the explorer/primer program. The explorer/primer
program will be started from the directory given with the SPECRUNDIR entry.
Note that the default value for SPECRUNDIR is not the current working directory!
Default value: unset
- *SPECFLAGS arguments
- (Additional) arguments that will
be given as arguments to the explorer/primer program when it is started.
Default value: unset
- SPECRUNDIR directory
- The directory from which the
explorer/primer program will be started. Default value: the directory containing
the explorer/primer program as specified in the SPEC entry.
- SPECSOURCE filename
- The filename of the specification from which the explorer/primer program
was built. If specified, xtorx(1) will enable the ``Show primer'' menu entry,
and when that menu entry is activated, xtorx(1) will invoke xtorx-showspec(1)
with the filename as argument. Default value: unset
- SOURCESPEC filename
- Deprecated. Use SPECSOURCE filename instead.
- PRIMERS filename
- The filename
from which xtorx(1) will initialise its Primers menu (as if it was opened
with its Open Primers... menu entry). If torx(1) is invoked without command
line option --gui and if both PRIMERS and PRIMER are set, it will use PRIMERS
to initialise its list of primers, and use PRIMER to select one from this
list, in order to produce the side effects necessary to run the selected
primer. Default value: unset.
- PRIMER entryname
- The menu entry that xtorx(1)
will select in its Primers menu, or show in its title-bar if no Primers
menu is present. If torx(1) is invoked without command line option --gui and
if both PRIMERS and use PRIMER are set, it will use PRIMERS to initialise
its list of primers, and PRIMER to select one from this list, in order
to produce the side effects necessary to run the selected primer. Default
value: empty.
- GUIDES filename
- The filename from which xtorx(1) will initialise
its Guides menu (as if it was opened with its Open Guides... menu entry). If
torx(1) is invoked without command line option --gui and if both GUIDES and
GUIDE are set, it will use GUIDES to initialise its list of guides, and
use GUIDE to select one from this list, in order to produce the side effects
necessary to run the selected guide. Default value: unset.
- GUIDE entryname
- The menu entry that xtorx(1) will select in its Guides menu, or show in
its title-bar if no Guides menu is present. If torx(1) is invoked without
command line option --gui and if both GUIDES and GUIDE are set, it will use
GUIDES to initialise its list of guides, and use GUIDE to select one from
this list, in order to produce the side effects necessary to run the selected
guide. Default value: empty.
- *INPUT gatename ignored encoding-routine [pcoOf-routine]
- This feature specifies that the events on LOTOS gate gatename are to be
interpreted as input events. See the ADAPTER section for an explanation
of the remaining arguments.
- *OUTPUT gatename
- This feature specifies that
the events on LOTOS gate gatename are to be interpreted as output events.
In addition, it can have the same additional arguments as the INPUT feature,
but these are all ignored for the OUTPUT feature.
- CHOOSEINPUTS boolean
- Indicate
whether or not the DRIVER should select inputs from the menu, if the user
does not choose. This is needed if an iochooser is used to choose values
for ``symbolic'' events in the Promela specification. Allowed values: 0 (false),
1 (true). Default value: 0
- LABEL-DELTA string
- The string representation of
the action/event that represents the delta action, i.e. quiescence, in the
communication with the explorer/primer component. This value should be parseable
as a LOTOS event. Default value: Delta Note: this value is just a default
which is available to primer and adapter when they are started, and both
can choose to ignore it. This value is also used when the driver has to
send a quiescence event to the primer, and the adapter did not include
an event.
This section contains the settings that you usually only
have to specify once when you start a test-campaign.
- ADAPTOR filename
- The
filename of the adapter. It will be started as a subprocess of torx(1). It
will be invoked with the configuration file arguments that are given to
torx. Note: the adapter will be started from the directory given with the
ADAPTORRUNDIR entry. Note that the default value for ADAPTORRUNDIR is not
the current working directory (except for the adapters supplied with TorX,
for which the current working directory is the default ADAPTORRUNDIR )
Default value: adaptor
- *ADAPTORFLAGS arguments
- (Additional) arguments that
will be given as arguments to the explorer/primer program when it is started.
Default value: unset
- ADAPTORRUNDIR directory
- The directory from which the
adapter program will be started. Default value: the directory containing
the adapter program as specified in the ADAPTOR entry.
- ADAPTORCONTEXT filename
- The filename of the program that will be used to as filter between TorX
and adapter when TorX starts the adapter. The filter works in two ways:
both the standard input written to the IUT/SUT and the standard output
read from the IUT/SUT will be filtered by the program. Default value:
unset
- IUT filename
- The filename of the SUT/IUT. The presence of this feature
indicates that the SUT/IUT has to be started by torx(1). It will be started
as a subprocess of torx(1), and torx(1) will have three pipes to it: to
its standard input, standard output and standard error. The standard input
and standard output pipes constitute the PCO address pipe (see the ADDRESS
entry, below) Note: the SUT/IUT will be started from the directory given
with the IUTRUNDIR entry. Note that the default value for IUTRUNDIR is not
the current working directory! If this feature is not present, TorX supposes
that the SUT/IUT is already running, or started outside TorX, and TorX
only has to be able to connect to it. Default value: unset
- *IUTFLAGS arguments
- (Additional) arguments that will be given as arguments to the SUT/IUT program
when it is started. Default value: unset
- IUTRUNDIR directory
- The directory
from which the SUT/IUT program will be started. Default value: the directory
containing the SUT/IUT program as specified in the IUT entry.
- IUTSOURCE
filename
- The filename of the specification from which the IUT/SUT program
was built. This is particularly useful when we use a ``simulator'' as IUT/SUT.
If specified, xtorx(1) will enable the ``Show mutant'' menu entry, and when
that menu entry is activated, xtorx(1) will invoke xtorx-showspec(1) with
the filename as argument. Default value: unset
- SOURCEIUT filename
- Deprecated.
Use IUTSOURCE filename instead.
- MUTANTS filename
- The filename from which
xtorx(1) will initialise its Mutants menu (as if it was opened with its
Open Mutants... menu entry). If torx(1) is invoked without command line option
--gui and if both MUTANTS and MUTANT are set, torx will use MUTANTS to initialise
its list of mutants, and use MUTANT to select one from this list, in order
to produce the side effects necessary to run the selected mutant. Default
value: unset.
- MUTANT entryname
- The menu entry that xtorx(1) will select
in its Mutants menu, or show in its title-bar if no Mutants menu is present.
If torx(1) is invoked without command line option --gui and if both MUTANTS
and MUTANT are set, it will use MUTANTS to initialise its list of mutants,
and use MUTANT to select one from this list, in order to produce the side
effects necessary to run the selected mutant. Default value: empty.
- IUTCONTEXT
filename
- The filename of the program that will be used to as filter between
TorX and IUT/SUT when TorX starts the IUT/SUT. The filter works in two
ways: both the standard input written to the IUT/SUT and the standard
output read from the IUT/SUT will be filtered by the program. This feature
is only useful (and currently only used) when a tcl-style adapter is used.
The filter program will be invoked with as arguments the IUT program together
with its arguments. The hexcontext(1) program can be used here. Default value:
unset
- IUTCONTEXTFLAGS flags
- Additional arguments for the program given
as IUTCONTEXT. For hexcontext(1) a useful flag is --. Default value: unset
- IUTTIMEOUT real
- The timeout value for the IUT/SUT, in seconds. Fractions
are allowed. Infinity is denoted with ``-1''. Default value: 11 seconds.
- USEGCI
boolean
- Indicate whether or not the GCI-style adapter should be used. If
the GCI-style adapter is not used, the tcl-style adapter will be used. Allowed
values: 0 (false, i.e. use tcl-style adapter), 1 (true, i.e. use GCI). Default
value: 0
- GCIADAPTER name
- Indicate the name of the tcl-package that implements
the adapter. This package is expected to be found either in the library
directory of TorX, or in the directory specified in the CODING feature.
Default value: gcitcl
- CODING directory
- The directory that contains the
conding routines, either in the form of tcl files (when the tcl-style adapter
is used), or in the form of a tcl package (when the gci-style adapter is
used). Default value: unset
- *INPUT gatename ignored encoding-routine [pcoOf-routine]
- This feature specifies that the events on LOTOS gate gatename are to be
interpreted as input events. In addition, it specifies that the tcl routine
encoding-routine is to be used to encode events on gate gatename, and the
optional pcoOf-routine has to be used to map an event on gate gatename to
its pco (if all events on a gate are mapped onto the same pco, this routine
may be omitted). The encoding-routine routine is invoked with two arguments:
1) the gatename, and 2) a list of value-expressions. The result should be
a string that can be send to the IUT. The pcoOf-routine routine is invoked
with two arguments: 1) the gatename, and 2) a list of value-expressions.
The result should be a pconame that appears in the configuration file. If
feature USEGCI is set, then the encoding-routine and pcoOf-routine are ignored,
and the GCI-specific configuration is used. The deprecated ignored field
was meant to specify the sort-list of the gate - but it is simply ignored.
- *OUTPUT gatename
- This feature specifies that the events on LOTOS gate
gatename are to be interpreted as output events. In addition, it can have
the same additional arguments as the INPUT feature, but these are all ignored
for the OUTPUT feature.
- *ADDRESS addressname protocol [host] [port] [program]
[flags]
- Specification of an address to connect to the SUT/IUT, with optional
host, port, program to be used to connect, and flags to be given to the
program. For the host field, the special name currenthost can be used as
a ``wildcard'' referring to the current host: that value is substituted by
the result of torx-hostname(1). If the connector program is omitted, it
defaults to a program with the same name as the protocol. The addressname
can be used in the encoding- and decoding routines to be referred to as
abstract address name (i.e. to allow change of the actual hostname/port-number
without having to change the coding routines).
Currently implemented values
for protocol:
- udp
- in which case host and port should be given; the
connector program may be omitted (i.e. defaults to a program with the same
name as the protocol, i.e. udp and the connector flags should be {--port
${P}} (where ${P} is a variable that represents the port number) for the
udp(1) program supplied with TorX. (See the first example in the EXAMPLES
section below.)
- telnet
- in which case host and port should be given, the
connector program and flags may be omitted, and the telnet(1) program
will be used to connect to the IUT.
- pipe
- in which case host, port, connector
program and flags may be omitted, and the pipes made to IUT when it is
started from XtorX are used.
- manual
- (currently only supported for stimulation,
not for observation; currently only supported via the GCI-based adapter)
in which case, for all stimili that have to be given on the pco with this
address, TorX will ask the human operator to perform the actual stimulation.
- *PCO pconame gatenames addressnames decoding-tuple-list
- where gatenames is
either a single gatename (for an uni-directional pco), or an output gatename
followed by an input gatename, enclosed between ``{'' and ``}'' (for a bi-directional
pco), and decoding-tuple-list is a list of white-space separated tuples. Each
tuple is enclosed between ``{'' and ``}'', and contains the fields ignored, decoding-routine,
and optional regexp. The ignored field was meant to specify the abstract
and concrete types of the data sent over the pco, but this information
has never been put to use. This feature specifies that pco pconame functions
as uni-directional or bi-directional pco for events on the given gatename
or gatenames. In addition, this feature assigns address addressname to this
pco (addressname should be specified in an ADDRESS entry elsewhere in the
configuration file). Finally, this feature specifies how to do observations
on this pco: all regexp regular expressions of the decoding-tuple-list are
concatenated. When an observation is made, for each pco the combined regular
expression is tried on the output received on the pco. For the first pco
for which the combined regular expression matches the output received on
a pco, the first specified decoding-routine of the pco is invoked with two
arguments: 1) the pconame, and 2) a list of strings. The first string in
this list is the match of the regular expression on the observed output;
the optional remaining strings correspond to sub-expressions of the regular
expression. NOTE: it is currently best to specify for each pco exactely
one decoding-routine and one regexp.
This section contains the
settings that you usually only have to specify once when you start a test-campaign.
- INST filename
- The filename of an instantiator. The presence of this feature
indicates that the instantiator has to be started by torx(1). It will be
started as a subprocess of torx(1), and torx(1) will have three pipes to
it: to its standard input, standard output and standard error. Over the
standard input and output, torx(1) will issues the commands and expect
the responses described in torx-instantiator(5). Note: the instantiator will
be started from the directory given with the INSTRUNDIR entry. Note that
the default value for INSTRUNDIR is not the current working directory!
Note that the adaptsim(1) adaptor also honors the INST config entry, and
that when TorX starts an adaptor, it gives it the same configuration files.
If this feature is not present, TorX supposes that no instantiator is needed.
Default value: unset
- *INSTFLAGS arguments
- (Additional) arguments that will
be given as arguments to the instantiator program when it is started. Default
value: unset
- INSTRUNDIR directory
- The directory from which the instantiator
program will be started. Default value: the directory containing the instantiator
program as specified in the INST entry.
It is not advised to change
the settings in this section, unless you know very well what you are doing,
because they influence the ``heart'' of the system - changing a setting here
might break the system.
- SPECTIMEOUT real
- The timeout value for the communication
with the explorer/primer, in seconds. Fractions are allowed. Infinity is
denoted with ``-1''. Default value: -1 (i.e. infinity).
- ADAPTORTIMEOUT real
- The timeout
value for the communication with the adaptor, in seconds. Fractions are
allowed. Infinity is denoted with ``-1''. Default value: -1 (i.e. infinity).
- PROMPT
string
- The prompt used by the non-GUI interface to TorX, i.e. by torx(1). Note
that currently xtorx(1) uses the prompt string to keep itself synchronised
with torx(1). Default value: "tester> ".
- DEBUG number
- The level of debugging
information that should be printed. Default value: 1
The example
configuration below is what is used for the LOTOS primer for the Conference
Protocol case study. Note that we have expanded here some of the ignored
arguments of the INPUT, OUTPUT, and PCO entries.
#==============================================
IUTTIMEOUT 2
# MAXSTEPS 7
CODING ./CODING/LOTOS
IUTCONTEXT hexcontext --
IUT ./IUT/conf.jan.longrun.sh
SPEC ./LOTOS/primer.sh
SPECSOURCE ./LOTOS/cf-pe-sut.caesar.lot
# for input, the conversion function of the INPUT def IS used
# for input, the pcoOf function of the INPUT def for CFSAP is NOT used
# for input, the pcoOf function of the INPUT def for udp IS used
# for output, the conversion function of the OUTPUT def is NOT used
# for output, the pcoOf function of the OUTPUT def is NOT used
INPUT CFSAP_in { CFAddr CFsp } enCodingOfCFsp
OUTPUT CFSAP_out { CFAddr CFsp }
INPUT udp_in { udpAddr udpsp } enCodingOfUdp pcoOfUdp
OUTPUT udp_out { udpAddr udpsp } deCodingOfUdp pcoOfUdp
ADDRESS cf1 pipe
ADDRESS udp1 udp currenthost 1075 {--port ${P}}
ADDRESS udp2 udp currenthost 1076 {--port ${P}}
ADDRESS udp3 udp currenthost 1077 {--port ${P}}
# for input, the conversion function of the PCO def is NOT used
# for output, the conversion function of the PCO def IS used
PCO cf1 { CFSAP_out CFSAP_in } cf1 { SFsp_nl CFsp_nl2CFsp {RECVHEX[^\n]+\n}
}
PCO udp2 { udp_out udp_in } udp2 { udp_nl udp_nl2udpsp {RECVHEX[^\n]+\n}
}
PCO udp3 { udp_out udp_in } udp3 { udp_nl udp_nl2udpsp {RECVHEX[^\n]+\n}
}
### we may want to use several SEEDs, to reproduce errors.
# do not specify seed here; use from command line
# SEED 4
# do not specify logfile here; use from command line
# LOGFILE logs/conference.lotos.log
# next line used a log file as initial trace
# do not specify tracefile here; use from command line
# TRACEFILE conf.trace
#==============================================
The example configuration below shows the very minimal that is needed to
use a simulator as IUT. We assume here that the specification is in file
sim.lot. We also assume that the specification that is to be used as simulator-IUT
is in impl.lot. Finally, we assume that when mkprimer(1) was invoked to process
sim.lot and impl.lot, for both files the same input and output gates have
been specified with the --inputs and --outputs flags of mkprimer(1).
#==============================================
# instead of using INPUT and OUTPUT to specify the input and output gates,
# we just include a file generated by mkprimer.
# we could just as well include impl.gates: spec.gates and impl.gates
# are identical (w.r.t. INPUT and OUTPUT entries that they contain),
# because we invoked mkprimer with the same --inputs and --outputs flags
# when we invoked in to process spec.lot and impl.lot .
INCLUDE sim.gates
# use the adapter supplied with torx for simulator-as-iut usage
ADAPTOR adaptsim
# specify spec and iut, and the source of it
SPEC sim
SPECSOURCE sim.lot
IUT sim
IUTSOURCE sim.lot
# This PCO entry is not really used, but without it torx will complain.
PCO ignored
#==============================================
The interpretation of relative paths in file and directory names,
relative to the configuration file, only works when torx(1) is started
in the directory containing the configuration file (when torx(1) is started
via xtorx(1) this is the case - xtorx(1) takes care of this). For configuration
files included via the INCLUDE entry, it only works if the included file
is in the same directory as the file containing the INCLUDE line.
The INPUT
and OUTPUT entries combine information for the Primer with information
for the Adapter; it would be better to separate those (or at least to allow
the user to specify this information in separate entries).
The configuration
of the PCO entry should be simplified.
The tcl-list interpretation of the
entry lines, resulting in all those ``{'' and ``}'', is not very nice.
When a GCI-style
Adapter is used, very little from the configuration file is used - instead,
configuration information is hard-coded into the C code of the GCI-style
Adapter. This should be changed, such that a GCI-style Adapter also uses
the information from a (the) configuration file, preferably in such a way
that the same configuration file can be used both for a tcl-style and for
a GCI-style Adapter.
The use of adaptor/adapter should be normalised!
torx-intro(1), torx(1), torx-primer(5), torx-adaptor(5), torx-instantiator(5),
xtorx(1), xtorx-showspec(1), torx-hostname(1), telnet(1), udp(1), hexcontext(1),
anifsm(1)
By Email: <torx_support@cs.utwente.nl>
This manual
page documents version 3.9.0 of torx.
Table of Contents
|
Prev
|
Table of Contents
|
Next
|
|
Appendix D: TorX Manual Pages: xtorx(1) - gui for the torx on-the-fly tester
|
|
Appendix D: TorX Manual Pages: torx-log(4) - log file generated by torx tester
|