| [ Home | What's New | Contents | Overview | Contributors | Distribution | Examples | Documentation | Manual | Publications | Mailing List Archive | Problems ] | This page was last updated by Axel Belinfante on 2003-08-05 | |
| TorX Test Tool Information | ||
| Prev | Next | |
The names are used to ``link'' blocks, in the form of a DAG (directed acyclic graph). The ``root'' of the DAG is formed by a block of type campaign. The ``links'' are formed by name-value pairs in a block that refer to the names of other blocks, instead of specifying configuration parameters.
A particular ``link'' is made by the base field: it inherits the definition named in the field's value, provided that this definition is of the same type as the block that contains the base field.
To reduce the size of the configuration, a very primitive variable mechanism can be used to ``simulate'' parameterized blocks, and a primitive ``foreach'' construct can be used to create multiple instances of a configuration (with different variable instantiations).
At the top we have the ``campaign'', that consists of a set of ``executions''. Each ``execution'' consists of a single experiment, where all parameters under control of the test operator are fixed. So, the configuration of an ``execution'' describes the test architecture, the tools, the parameters of the tools etc. The only remaining ``parameter'' is the non-determinism of the implementation. To cope with that, we allow each ``execution'' to be run more than once, which gives us that each ``execution'' is (has?) a set of ``runs''.
The execution architecture is effectively identical to the test architecture (how are tester and iut connected), with the addition of information about the internal structure of the tester (what components are used, how are they connected).
In the test architecture we have the concepts ``Implementation Under Test'' (IUT), ``Implementation Access Point'' (IAP), ``Point of Control and Observation'' (PCO), ``Test Context'' and ``System Under Test''. In our view, the Adapter can only reach, access, communicate with, the IUT via the Test Context. The PCOs form the connection between the Adapter and the Test Context, and the IAPs form the connection between IUT and the Test Context. For the execution architecture we are not interested in the Test Context and the SUT, but we are interested in all the other concepts. In addition, we are interested in the concepts from the tool architecture: explorer, primer, combinator, test purpose, (batch) test, instantiator, driver, and adapter.
The IUT has one or more IAP's, and there are one or more PCO's. A PCO may coincide with an IAP, or there may be a test-context separating them, in which case there may be a many-to-many mapping between IAP's and PCO's. We currently assume that in the execution architecture we (may) have: one IUT, one adapter, one driver, zero or more explorers, zero or more primers, zero or more test purposes, zero or more combinators, zero or more batch tests, zero or more instantiators.
Not all fields of all blocks have to be given (we should mark the optional ones). The fields that may occur more than once in a block have a suffix ``*'' in the list below.
Note that the special field base may appear in every kind of block. base=value inherits the definition named in value, provided that that definition is of the same type as the block that contains the base field. Effectively, a block definition that starts in the following way:
will try to ``in-place insert'' the contents of block type=anothername at the start of block type=name. Examples of the usage of base can be found in the EXAMPLES section below.
type=name base=anothername ...
The block descriptions are in alphabetical order, as are the field descriptions in each block.
reference to definition elsewhere in the configuration
- codingdir
- the directory containing the coding library that will be used during test execution. In particular, this directory should contain implementations for the functions named in the multiplexer, encoder and decoder fields of the pco's.
- exec
- name of the program to execute when the adapter has to be started
- execdir
- directory in which the program named in the exec field has to be run
- execparams*
- arguments for the program named in the exec field. There may be multiple execparams fields: we need one for each argument.
- pco*
- value
- actual address. For network addressing we use the (plan9 derived) syntax giving (exclamation-mark separated) network, node and port as network!node!port. Currently known networks are pipe (just a single pipe, no node or port needed -- used when the implementation is started by the driver), and tcp and udp, where the nodename ``*'' refers to the local host. A port number may be omitted, which means that it can be chosen by the Operating System (or by the tool).
- comment
- to be used for documentation, not used by the tools
- dir
- the root of the campaing directory. All execution directories should be inside the campaign directory. The value of the dir field is available through the $campaign variable.
- experiment*
- reference to definition elsewhere in the configuration: an experiment that is part of the campaign
- makefile
- name of the top-level Makefile generated by campaign.
- mkinclude
- name of Makefile that is to be included in the top-level Makefile generated by campaign.
- iokind
- the type (kind) of the channel, which must be either input or output
- pco*
- reference to definition elsewhere in the configuration: a pco``connected'' to this channel
- sevent
- the event representing ``suspension'' or ``quiescense'' (usally this will be Delta) not implemented yet
- timeout
- time out value for the channel (only for channels with iokind=output)
- combinator*
- reference to definition elsewhere in the configuration
- config
- name of the configuration file that has to be generated by campaign for the combinator described in this block.
- exec
- name of the program to execute when the primer has to be started
- execdir
- directory in which the program named in the exec field has to be run
- execparams*
- arguments for the program named in the exec field. There may be multiple execparams fields: we need one for each argument.
- gen
- the program that can build (or generate) the combinator
- genparams*
- an argument for the program named in the gen field. There may be multiple genparams fields: we need one for each argument.
- partitioner*
- reference to definition elsewhere in the configuration
- primer*
- reference to definition elsewhere in the configuration
- test*
- reference to definition elsewhere in the configuration not implemented yet!
- tp*
- reference to definition elsewhere in the configuration not implemented yet!
- exec
- name of the program to execute when the driver has to be started
- execparams*
- arguments for the program named in the exec field. There may be multiple execparams fields: we need one for each argument.
- post
- program that has to be run after the driver has finished (not yet implemented)
- pre
- program that has to be run before the driver is started (not yet implemented)
the seed parameter to be used during test execution
- adapter
- reference to definition elsewhere in the configuration
- combinator
- reference to definition elsewhere in the configuration
- config
- name of the configuration file that has to be generated by campaign for the experiment described in this block. Usually this will be in the directory indicated in the dir field.
- dir
- the directory in which the execution should take place
- driver
- reference to definition elsewhere in the configuration
- driverparams*
- additional flags for the driver program
- impl
- reference to definition elsewhere in the configuration
- log
- name of file in which to store the execution log (which includes the execution trace)
- makefile
- name of the Makefile that has to be generated by campaign for the experiment described in this block. Usually this will be in the directory indicated in the dir field.
- maxdepth
- the maximum number of steps that will be executed in a test run for this experiment
- msg
- name of file in which to store the (stderr) messages produced by the various components during execution
- mkinclude
- name of Makefile that is to be included in the Makefile generated by campaign.
- mutant
- name of the implementation mutant tu run. This is used to define the MUTANT entry in the generated configuration file.
- partitioner
- reference to definition elsewhere in the configuration
- post
- program that has to be run at the end of the test execution run (What are the default parameters for this program?)
- postparams*
- additional arguments for the program given in the post field
- pre
- program that has to be run at the start of the test execution run (What are the default parameters for this program?)
- preparams*
- additional arguments for the program given in the pre field
- primer
- reference to definition elsewhere in the configuration
- runs
- number of execution runs that will be executed for this experiment
- seed
one of the values of the variable over which will be iterated
- name
- the name of the variable
- type
- the type of the variable. Usually this will be something like block.field
- value*
- address
- reference to definition elsewhere in the configuration. Currently we assume a single address for each iap.
additional arguments for the program given in the pre field
- configgen
- program that is able to generate a configuration file for the implementation, based on the configuration file together with parameters that are only known at run-time (e.g. port numbers chosen dynamically). (not yet implemented)
- configgenparams*
- arguments for the program named in the configgen field. There may be multiple configgenparams fields: we need one for each argument. (not yet implemented)
- exec
- name of the program to execute when the implementation has to be started
- execcontext
- program that is used as a filter between the implementation and the adapter. Such a filter can be used e.g. to translate between binary i/o done by the implementation and a hex encoding of it that is more pleasant for the adapter.
- execcontextparams*
- arguments for the program named in the execcontext field. There may be multiple execcontextparams fields: we need one for each argument.
- execdir
- directory in which the program named in the exec field has to be run
- execparams*
- arguments for the program named in the exec field. There may be multiple execparams fields: we need one for each argument.
- iap*
- reference to definition elsewhere in the configuration. This may contain information that is needed by the adapter, like port addresses at the implementation side of the test context.
- post
- program that has to be run after the implemention has finished
- postparams*
- additional arguments for the program given in the post field
- pre
- program that has to be run before the implemention is started
- preparams*
- config
- name of the configuration file that has to be generated by campaign for the partitioner described in this block.
- exec
- name of the program to execute when the partitioner has to be started
- execdir
- directory in which the program named in the exec field has to be run
- execparams*
- arguments for the program named in the exec field. There may be multiple execparams fields: we need one for each argument.
- gen
- the program that can build (or generate) the combinator
- genparams*
- an argument for the program named in the gen field. not implemented yet
- partfile
- the location of the partition configuration file (that associates the weights with the actions)
where it may be used to segment stream-like data received from the SUT
- address
- reference to definition elsewhere in the configuration. Currently we assume a single address for each pco.
- decoder
- name of the decoding function that is used to decode values that are received via this pco. This function must be present in the library indicated by the codingdir field of the adapter. In the future we will not need this function, but instead use patterns over the event (if necessary enhanced with predicates).
- encoder
- name of the encoding function that is used to encode values that are sent over this pco. This function must be present in the library indicated by the codingdir field of the adapter. In the future we will not need this function, but instead use patterns over the event (if necessary enhanced with predicates).
- ievent
- a pattern over the events of the specification, that is used to partition those events in input and output pco's. This pattern indicates an input event. For backwords compatibility we also allow the pattern to consist of just a single gate name, together with the specification of a multiplexer function that will partition events on the same gate.
- multiplexer
- name of the function that is used to map an event to a pco. This function must be present in the library indicated by the codingdir field of the adapter. In the future we will not need this function, but instead use patterns over the event (if necessary enhanced with predicates).
- oevent
- a pattern over the events of the specification, that is used to partition those events in input and output pco's. This pattern indicates an output event. For backwords compatibility we also allow the pattern to consist of just a single gate name, together with the specification of a multiplexer function that will partition events on the same gate.
- regexp
- the value is exported to the decoding function,
reference to definition elsewhere in the configuration
- channel*
- reference to definition elsewhere in the configuration. The channel definitions define the channels, the subset of the labels that they represent, and whether it is input or output.
- exec
- name of the program to execute when the primer has to be started
- execdir
- directory in which the program named in the exec field has to be run
- execparams*
- arguments for the program named in the exec field. There may be multiple execparams fields: we need one for each argument.
- gen
- the program that can build (or generate) the primer
- genparams*
- an argument for the program named in the gen field. There may be multiple genparams fields: we need one for each argument.
- spec
block
- foreach*
- the variable definitions
- prefix
- the prefix of the names of the resulting instantiations. Their names will consist of the prefix, followed by for each foreach clause a hyphen followed by the value of the variable. So, ``product=lotosmutants'' in the example below, generates names like ``lotos-mutants-000-3'' (first the prefix, followed by a hyphen and a mutant value, followed by a hyphen and a seed value).
- template
- a reference to the block that should be instantiated. It should be of the type given in the type field.
- type
- the type of the result, which should be identical to the type of the given template. This will be something like
- auxfile*
- the location of an auxiliary specification file. Currently they are used for user-supplied ADT implementation files (with .t and .f file name suffixes) that may be needed by CADP (via mkprimer(1)) to generate a Primer program from a LOTOS specification.
- dialect
- (optionally) describes tool dialect (e.g. to distinguish between LOTOS specs for lite and for CADP) (so far only used for documentation, not used by the campaign tool)
- file
- the location of the (main) specification file. (Note: in general a single specification could consist of several files. We can probably handle that by requesting that all files of a specification appear in the same directory, which then can be named here, and use the gen field to deal with it).
- language
- the specification language (only used for documentation, not used by the campaign tool)
- name
- the name of the variable
- type
- the type of the variable Usually this will be something like block.field
- value*
- the value of the variable. If the field given in the type field may appear more than once in its block, there may be multiple value fields for the variable definition.
#==============================================
spec=confprot01l
file=$campaign/specs/confprot01.lot
language=LOTOS dialect=lite
spec=confprot01c
file=$campaign/specs/confprot01.caesar.lot
auxfile=$campaign/specs/confprot01.caesar.t
auxfile=$campaign/specs/confprot01.caesar.f
language=LOTOS dialect=cadp
spec=confprot01p
file=$campaign/specs/conf-solo.trojka
language=PROMELA
primer=pl
spec=confprot01c
gen=mkprimer
genparams=
exec=$campaign/specs/confprot01.caesar
execdir=$campaign/specs
execparams=
channel=in
channel=out
primer=pp
spec=confprot01p
gen=mkprimer
genparams=
exec=$campaign/specs/conf-solo.sh
execdir=$campaign/specs
execparams=
channel=in
channel=out
impl=jan
pre=
post=
exec=$campaign/impls/confprot.sh
execparams=-c
# execparams=$campaign/executions/$experiment/cfg.txt
execparams=$campaign/cfg.txt
execparams=-DEBUG
execparams=-1
execparams=-CSAP
execparams=-MUTANT
execparams=v-mutant
execcontext=hexcontext
execcontextparams=--
configgen=
configgenparams=-o
configgenparams=$campaign/executions/$experiment/cfg.txt
iap=up
iap=low
driver=torx
configgen=
exec=torx
execparams=--log
execparams=$(log)
execparams=--seed
execparams=$(seed)
execparams=--depth
execparams=$(maxdepth)
execparams=$(config)
pre=
post=
address=aup name=v-add0 value=pipe
address=alow1 name=v-add1 value=udp!*!1075
address=alow2 name=v-add2 value=udp!*!1076
address=alow3 name=v-add3 value=udp!*!1077
address=alow4 name=v-add4 value=udp!*!1078
adapter=a codingdir=v-coding
pco=up1 pco=low2 pco=low3 pco=low4
channel=in iokind=input pco=up1 pco=low2 pco=low3 pco=low4
channel=out iokind=output pco=up1 pco=low2 pco=low3 pco=low4 timeout=2
pco=upbase encoder=enCodingOfCFsp decoder=CFsp_nl2CFsp regexp={RECVHEX[^0+0
pco=lowbase encoder=enCodingOfUdp decoder=udp_nl2udpsp regexp={RECVHEX[^0+0
multiplexer=pcoOfUdp
pco=up1 base=upbase address=aup ievent=v-iev0 oevent=v-oev0
pco=low2 base=lowbase address=alow2 ievent=v-iev2 oevent=v-oev2
pco=low3 base=lowbase address=alow3 ievent=v-iev3 oevent=v-oev3
pco=low4 base=lowbase address=alow4 ievent=v-iev4 oevent=v-oev4
iap=up address=aup
iap=low address=alow1
var=l-u-iev0 name=v-iev0 type=pco.ievent value=cfsap_in!*!*
var=l-u-oev0 name=v-oev0 type=pco.oevent value=cfsap_out!*
value=cfsap_out!*!*
var=l-l-iev2 name=v-iev2 type=pco.ievent value=udp_in!udp1!udp_req(udp2,*)
value=udp_in!udp2!*
var=l-l-oev2 name=v-oev2 type=pco.oevent value=udp_out!udp1!udp_ind(udp2,*)
value=udp_out!udp2!*
var=l-l-iev3 name=v-iev3 type=pco.ievent value=udp_in!udp1!udp_req(udp3,*)
value=udp_in!udp3!*
var=l-l-oev3 name=v-oev3 type=pco.oevent value=udp_out!udp1!udp_ind(udp3,*)
value=udp_out!udp3!*
var=l-l-iev4 name=v-iev4 type=pco.ievent value=udp_in!udp1!udp_req(udp4,*)
value=udp_in!udp4!*
var=l-l-oev4 name=v-oev4 type=pco.oevent value=udp_out!udp1!udp_ind(udp4,*)
value=udp_out!udp4!*
var=p-u-iev0 name=v-iev0 type=pco.ievent value=from_upper
var=p-u-oev0 name=v-oev0 type=pco.oevent value=to_upper
var=p-l-iev2 name=v-iev2 type=pco.ievent value=from_lower
var=p-l-oev2 name=v-oev2 type=pco.oevent value=to_lower
var=p-l-iev3 name=v-iev3 type=pco.ievent value=from_lower
var=p-l-oev3 name=v-oev3 type=pco.oevent value=to_lower
var=p-l-iev4 name=v-iev4 type=pco.ievent value=from_lower
var=p-l-oev4 name=v-oev4 type=pco.oevent value=to_lower
var=l-u-add0 name=v-add0 type=address.name value=cf1
var=l-l-add1 name=v-add1 type=address.name value=udp1
var=l-l-add2 name=v-add2 type=address.name value=udp2
var=l-l-add3 name=v-add3 type=address.name value=udp3
var=l-l-add4 name=v-add4 type=address.name value=udp4
var=p-u-add0 name=v-add0 type=address.name value=cf1
var=p-l-add1 name=v-add1 type=address.name value=1
var=p-l-add2 name=v-add2 type=address.name value=0
var=p-l-add3 name=v-add3 type=address.name value=2
var=p-l-add4 name=v-add4 type=address.name value=4
var=l-coding name=v-coding type=adapter.codingdir
value=$campaign/coding/LOTOS
var=p-coding name=v-coding type=adapter.codingdir
value=$campaign/coding/PROMELA
experiment=defaults
msg=msg
log=log
dir=$campaign/executions/$experiment
makefile=$campaign/executions/$experiment/torx.mk
config=$campaign/executions/$experiment/torx.if
pre=:
post=:
driver=torx
experiment=templatedefaults
base=defaults
runs=2
seed=v-seed
maxdepth=30
adapter=a
impl=jan
experiment=lotos
base=templatedefaults
primer=pl var=l-coding var=l-l-add1
var=l-u-iev0 var=l-u-oev0 var=l-u-add0
var=l-l-iev2 var=l-l-oev2 var=l-l-add2
var=l-l-iev3 var=l-l-oev3 var=l-l-add3
var=l-l-iev4 var=l-l-oev4 var=l-l-add4
experiment=promela
base=templatedefaults
primer=pp var=p-coding var=p-l-add1
var=p-u-iev0 var=p-u-oev0 var=p-u-add0
var=p-l-iev2 var=p-l-oev2 var=p-l-add2
var=p-l-iev3 var=p-l-oev3 var=p-l-add3
var=p-l-iev4 var=p-l-oev4 var=p-l-add4
foreach=seed
type=experiment.seed
name=v-seed
value=1 value=2 value=3 value=4 value=5
foreach=mutants
type=impl.execparams
name=v-mutant
value=000 value=100 value=111 value=214 value=247
value=276 value=289 value=293 value=294 value=332
value=345 value=348 value=358 value=384 value=398
value=444 value=462 value=467 value=548 value=666
value=687 value=738 value=749 value=782 value=836
value=856 value=945
product=lotosmutants
type=experiment
foreach=mutants
foreach=seed
prefix=lotos-mutants
template=lotos
product=promelamutants
type=experiment
foreach=mutants
foreach=seed
prefix=promela-mutants
template=promela
campaign=one
dir=/home/fmg/belinfan/src/cdr/utest_old_release/Examples/CampaignTemplate
makefile=$campaign/Makefile
product=lotosmutants
product=promelamutants
#==============================================
# ==============================================
driver=torx
configgen=
exec=torx
execparams=--log
execparams=$(log)
execparams=--seed
execparams=$(seed)
execparams=--depth
execparams=$(maxdepth)
execparams=$(config)
pre=
post=
spec=LOTOS
file=$campaign/specs/LOTOS/cf-pe-sut.caesar.lot
auxfile=$campaign/specs/LOTOS/cf-pe-sut.caesar.t
auxfile=$campaign/specs/LOTOS/cf-pe-sut.caesar.f
language=LOTOS
preproc=
dialect=cadp
primer=pl
spec=LOTOS
gen=mkprimer
genparams=
exec=$campaign/specs/LOTOS/cf-pe-sut.caesar
execdir=$campaign/specs/LOTOS
execparams=
channel=in
channel=out
impl=janbase
pre=
post=
exec=$campaign/impls/confprotv3c/confprot.sh
gen=make
execdir=$campaign/impls/confprotv3c
genparams=confprot
execparams=-a
execparams=pythagoras:1075
execparams=-a
execparams=pythagoras:1076
execparams=-a
execparams=pythagoras:1077
execcontext=hexcontext
execcontextparams=--
iap=up
iap=low
foreach=mutants
type=impl.execparams
type=experiment.mutant
name=v-nr
value=001
value=002
value=003
value=055
value=056
value=057
value=058
value=059
value=099
foreach=seeds
type=experiment.seed
name=var-s
value=789
value=161
value=78
value=102
value=360
value=301
value=24
value=197
value=694
value=278
foreach=maxdepths
type=experiment.maxdepth
name=v-mdepth
value=25
value=50
value=75
value=100
value=125
value=150
value=175
value=200
value=250
value=300
# value=400
# value=500
# value=700
# value=750
# value=1000
# value=2000
# value=4000
# value=8000
# value=50000
# value=100000
adapter=a
codingdir=var-coding
pco=up1
pco=low2
pco=low3
pco=upbase
encoder=enCodingOfCFsp
decoder=CFsp_nl2CFsp
regexp={RECVHEX[^0+0
pco=lowbase
encoder=enCodingOfUdp
decoder=udp_nl2udpsp
multiplexer=pcoOfUdp
regexp={RECVHEX[^0+0
pco=up1
base=upbase
address=up
ievent=v-iev0
oevent=v-oev0
pco=low2
base=lowbase
address=low2
ievent=v-iev2
oevent=v-oev2
pco=low3
base=lowbase
address=low3
ievent=v-iev3
oevent=v-oev3
iap=up
address=up
iap=low
address=low1
channel=in
iokind=input
pco=up1
pco=low2
pco=low3
channel=out
iokind=output
pco=up1
pco=low2
pco=low3
timeout=5
sevent=Delta
address=up
name=var-address0
value=pipe
address=low1
name=var-address1
value=udp!*!1075
address=low2
name=var-address2
value=udp!*!1076
address=low3
name=var-address3
value=udp!*!1077
var=l-u-iev0
name=v-iev0
type=pco.ievent
value=cfsap_in!*!*
var=l-u-oev0
name=v-oev0
type=pco.oevent
value=cfsap_out!*
value=cfsap_out!*!*
var=l-l-iev2
name=v-iev2
type=pco.ievent
value=udp_in!udp1!udp_req(udp2,*)
value=udp_in!udp2!*
var=l-l-oev2
name=v-oev2
type=pco.oevent
value=udp_out!udp1!udp_ind(udp2,*)
value=udp_out!udp2!*
var=l-l-iev3
name=v-iev3
type=pco.ievent
value=udp_in!udp1!udp_req(udp3,*)
value=udp_in!udp3!*
var=l-l-oev3
name=v-oev3
type=pco.oevent
value=udp_out!udp1!udp_ind(udp3,*)
value=udp_out!udp3!*
var=l-u-address
name=var-address0
type=address.name
value=cf1
var=l-l-address1
name=var-address1
type=address.name
value=udp1
var=l-l-address2
name=var-address2
type=address.name
value=udp2
var=l-l-address3
name=var-address3
type=address.name
value=udp3
var=l-coding
name=var-coding
type=adapter.codingdir
value=$campaign/coding/LOTOS
experiment=defaults
msg=msg
log=log
dir=$campaign/experiment/$experiment
makefile=$campaign/experiment/$experiment/torx.mk
mkinclude=experiment.incl
config=$campaign/experiment/$experiment/torx.if
runs=var-runs
seed=var-s
maxdepth=v-mdepth
var=l-u-iev0
var=l-u-oev0
var=l-l-iev2
var=l-l-oev2
var=l-l-iev3
var=l-l-oev3
var=l-u-address
var=l-l-address1
var=l-l-address2
var=l-l-address3
var=l-coding
primer=pl
adapter=a
impl=janbase
pre=:
post=:
driver=torx
# ================================================================
experiment=001
base=defaults
runs=1
maxdepth=1000
product=expr
type=experiment
foreach=seeds
prefix=expr
template=001
# ================================================================
campaign=main
dir=/home/fmg/feenstra/jf/campaign/confprot
makefile=$campaign/Makefile
experiment=product=expr
# ==============================================
In general, it will be easier to write a shell script to invoke torx(1) in the way described in torx(1) than it is to use campaign.
The main problem seems to be that we picked a limited syntax and stayed with it, even though it became increasingly painful to add to it the features that (we think) we need.
| Prev | Table of Contents | Next |
| Appendix D: TorX Manual Pages: autsimplify(1) - simplify automaton Aldebaran (.aut) file |
|
Appendix D: TorX Manual Pages: cppmkprimer(1) - preprocess input with cpp before invoking mkprimer |