mkprimer-trojka(1) - generate a promela primer for torx using trojka
Table of Contents
mkprimer-trojka - generate a promela primer for torx using trojka
mkprimer
[ options ... ] specification.trojka
When mkprimer(1) is invoked
on a specification file with a .trojka suffix, or when the --language promela
command line option is given, the specification file is interpreted as
a promela specification file, adapted for use with TorX. From the specification
file mkprimer(1) generates a torx-primer(5) program. In this manual page
we describe how to adapt a promela specification for use with TorX, and
we describe specific features of primers generated by trojka from promela
specifications.
The promela specification compiler of TorX,
trojka, runs its input file through the cpp(1) preprocessor, with the preprocessor
symbol TROJKA defined. This can be used to make a single specification that
can be used with both spin and trojka (TorX).
In
a promela specification for trojka, we describe the implmementation or
system under test (IUT, SUT). All communication via channels is taken to
be ``internal'', invisible, except for channels that are declared observable.
On an observable channel, we either only send or only receive; such a channel
is used to communicate with the ``environment''. Because we describe the system
(and its context, as far as necessary), seen from ``within'' the IUT/SUT, we
interpret a send statement (``!'') on an observable channel as output from
the IUT/SUT (i.e. as an observation from the tester's view), and a receive
statement (``?'') on an observable channel as input to the IUT/SUT, (i.e. as
a stimulus from the tester's view).
For use of such a specification with
the spin tool, we have to do two things: to remove the observable keyword
from the channel declaration (spin does not know about observable), and
to provide an environment prorcess that produces and consumes the actions
communicated over the observable channels. We usually do that as indicated
in the example below. This example consists of four parts: 1) the definition
of the macro OBSERVABLE, 2) the declaration of a channel, 3) the spefication
of the environment, and 4) the init statement in which we conditionally
start the environment process.
The Trojka promela primer
has limited support for symbolic testing. We first discuss the language
support for them, and then how they appear in the Primer-Driver interface.
Traditionally, in spin it is possible to use variables
in input (recveive, ?) statements, to bind variables to the values received.
In Trojka, the promela language (syntax) has been extended to also allow
the use of variables on output (send, !) statements. The syntax extension
has been derived from the C programming language. Note: this extension is
not compatible with spin, so when the extension is used, some #ifdef statements
may be needed to make the specification also usable with spin. The following
example statement specifies an output action on channel ``c'', with mtype ``something'',
values ``10'', ``value'' and variable ``variable''.
c ! something,10,value,&variable
As usual, variables need to be declared in advance.
Variables
in input and output actions will appear as var_type (with type the type
of the variable in promela) in the list of actions generated with the commands
C_INPUTS and C_OUTPUTS (see torx-primer(5) for these and other commands
from the Primer-Driver interface). That means that they also appear like
that in the lists of possible stimuli and observations shown in torx(1)
(when the menu command is given) and in xtorx(1).
When an input action (stimulus)
is requested or done with the C_GETINPUT and C_INPUT commands, all variables
are automatically instantiated (by choosing random values). This can be
influenced by giving explicit values instead of var_type fields in the
event parameter given with C_GETINPUT and C_INPUT commands. The instantiator(1)
is a TorX tool component that uses this functionality, by substituting
(amongs others) values randomly chosen from the values sets in its configuration
file for var_type fields in the event parameter of C_GETINPUT or C_INPUT
(as specified in its configuration file).
Another way to influence the automatic
subsitution is by invoking the generated primer with a -I command line option,
to disable automatic instantiation for the C_GETINPUT command. This can
be useful if (some) variable(s) should not be instantiated by the Primer,
but by the Adapter (because the information needed to instantiate is not
available in the primer, but only in the adapter; an example might be time-related
information).
A trojka primer does not generate a STATEID torx-log(4)
line.
The STATS torx-log(4) line generated by a trojka Primer consists of
a number of whitespace separated ``name value'' tuples.
- #statevector nr
- number
of allocated statevectors
- #statevectorstruct nr
- number of allocated statevector
structures
- memusage size
- size of memory used for the trojka state space
representation, in bytes (the trojka primer also consumes memory for other
things)
- #cutbranch nr
- number of branches that were cut in the analysis.
A branch may be cut if it contains a large (100?) sequence consisting of
only internal steps. Warning: if nr is non-zero, your test case may be unsound
(because the behaviour reached by the branch that was cut will not be taken
into accound).
- #analysedstates nr
- number of states analyed
- #matchedstates
nr
- number of states that match states already analysed
- maxdepth nr
- lenght
of the longest trace that was analysed
- #superstate nr
- number of states
in the superstate (state set representing current state, to handle non-determinism)
- #execaction nr
- number of actions executed to do the chosen action. This
nr gives an indication of the amount of non-determinism
- #possaction nr
- number
of different actions possible
When the driver provides
an mtype as part of a request to the primer, the matching is done in a
case-insensitive way.
#ifdef TROJKA
#define OBSERVABLE observable
#else
#define OBSERVABLE
#endif
chan c = [0] of { mtype, byte, byte, byte } OBSERVABLE;
chan d = [0] of { byte } OBSERVABLE;
#ifndef TROJKA
proctype environment() {
do
:: c ? _,_,_,_
:: d ! 1
:: d ! 2
:: /* all other actions that need to be produced or consumed */
od
/*
* instead of this all producing, all consuming environment,
* we may want to give a special scenario here
*/
}
#endif
init {
atomic {
run input(something);
run underlying_service(something);
...
#ifndef TROJKA
; run environment()
#endif
}
}
torx-intro(1), mkprimer(1), torx-primer(5), torx-adaptor(5), torx-log(4)
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: mkprimer-mcrl2(1) - generate a torx primer for mcrl2 using mcrl2
|
|
Appendix D: TorX Manual Pages: mkprimer(1) - generate a primer for torx
|