[ 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 2006-06-30
TorX Test Tool Information
Prev   Next

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.

Symbolic Testing

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.

Language Support

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 Primer

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

Primer-driver Interface

When the driver provides an mtype as part of a request to the primer, the matching is done in a case-insensitive way.


Macro Observable

#ifdef TROJKA
#define OBSERVABLE observable

Channel Definition

chan c  = [0] of { mtype, byte, byte, byte }  OBSERVABLE;
chan d  = [0] of { byte }  OBSERVABLE;


#ifndef TROJKA
proctype environment() {
    :: c ? _,_,_,_
    :: d ! 1
    :: d ! 2
    :: /* all other actions that need to be produced or consumed */
     * instead of this all producing, all consuming environment,
     * we may want to give a special scenario here

Init Statement

init {
    atomic {
        run input(something);
        run underlying_service(something);
#ifndef TROJKA
        ; run environment()

See Also

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 Valid HTML 4.01! Appendix D: TorX Manual Pages: mkprimer(1) - generate a primer for torx