[ 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

instantiator(1) - instantiate free variables for torx

Table of Contents

Name

instantiator - instantiate free variables for torx

Synopsis

instantiator [ -f configFile ] [ -s seed ]

Description

instantiator is an experimental TorX component that is meant as a filter between Driver and Primer: it reads (on standard input) the messages that are sent from Driver to Primer, and instatiates variables in these messages, and writes the resulting messages to standard output. The ``instantiation'' is just syntactical substitution. Which variables have to be instantiated, from which domains, can be expressed in configuration file, which can be named using the -f configFile flag. If no -f configFile flag is given, instantiator tries to read file ``instconfig.txt''. The instatiation values are chosen randomly from the domains given in the configuration file; the seed of the random number generator can be set using the -s seed flag. If necessary, instantiator will repeatedly (recursively) try to apply instantiation rules, until no changes occur. This can be used to instantiate a variable with an expression that contains new variables that then will also be instantiated, etc.

Use in Torx

We usually use the instantiator in the following way. We make a small wrapper shell script of the following form:

#! /bin/sh
instantiator -s 0 -f  instconfig.txt | primer-program "$@"
where primer-program is the actual primer program file that has to be invoked. So, all standard input send to the primer-program first passes through the instantiator. In the torx-config(4) configuration file (or in other places where we have to give the primer program file) we now give the wrapper script instead of the ``real'' primer program.

Configuration File Format

The configuration file consists a number of substitution entries of the form:
type : position : prefix : regexp : domain
Empty lines, lines containing only whitespace and comment lines (lines starting with optional whitespace followed by #) are ignored. Continuation lines are allowed: these should end with a \ character; this character is replaced by a space character when the lines are joined. leading and trailing whitespace in the lines, and in the fields (type, position, prefix, regexp, domain) is ignored.
type
is the type of the variable, as given in the expression that we have to instantiate. In general, variables in TorX have the form var_type[$i] with var_ a fixed prefix, and $i an optional numerical suffix to make the variables unique. Note: variables of the type mtype are treated special: as soon as a value is found for it, it is substituted, so the found value can be used as ``context'' in the regular expression regexp field.
position
is a non-negative (usually also non-zero) number that refers to the part of the event (action) that has to which the rule applies, where we take the ! character as a separator in the action, as in pos0!pos1!pos2 etc. The special value ``*'' makes the rule applicable to any position.
prefix
is a regular expression that refers to the command in the TorX Primer-Driver interface (see torx-primer(5)) for which the rule applies. This will usually be the command C_INPUT (for torx version 2.*) or the command C_GETINPUT (for torx version 3.*). Note that it will only look at the event field of this command (this is hardcoded in instantiator; maybe this should be configurable too). Note: all lines belonging to the same instantiation group should have the same prefix (because, as soon as an instantiation is possible using one of the prefixes, the rules of the other prefixes will not be tried).
regexp
is a regular expression that specifies the ``context'' of the rule. For a rule to be applicable, the regexp has to be matched.
domain
specifies (enumerates) the values that can be chosen from. Currently there are two syntaxes allowed. The first is a set-like notation, consisting of an enumeration of values, enclosed between { and }, separated by commas, where the values themselves do not contain commas. No whitespace is allowed between { and }. The disadvantage of this format is that the values may not contain commas. Example: {val1,val2,val3,val4}
The second format does not have this restriction. Also this contains of an enumeration of values, now enclosed between ( and ), separated by whitespace, where the values themselves may not contain whitespace. Example: ( e1(e2,e3) b1 c1 d1(e3,f3(g,h)) )

Examples

Conference Protocol in Promela

Here we have to instantiate events of the form
from_upper!LEAVE!var_byte!var_byte from_lower!PDU_JOIN!var_byte!var_byte!var_byte!var_byte
All (most) variables here are of type ``byte'', even though semantically these ``bytes'' represent different things. That is why we need the position field here, to distinguish the different semantical domains.


# ==================================
# empty lines and comment lines are ignored.
# comment lines are lines that start with
# (optional whitespace followed by) a hash sign (#).
byte:2:C_INPUT:from_upper!JOIN!.*!.*:{1,2,3,4}
byte:3:C_INPUT:from_upper!JOIN!.*!.*:{1,2}
# NOTE: _both_ lines of this regexp group have same prefix;
# if one line has C_INPUT and the other C_INPU(S?) then
# only one instantiation will be done even if an input line
# contains two var_byte fields...
byte:2:C_INPUT(S?):from_upper!LEAVE!.*!.*:{1,2,3,4}
byte:3:C_INPUT(S?):from_upper!LEAVE!.*!.*:{1,2}
byte:2:C_INPUT:from_upper!DREQ!.*!.*:{1,2,3,4}
byte:3:C_INPUT:from_upper!DREQ!.*!.*:{1}
byte:2:C_INPUT:from_lower!PDU_JOIN!.*!.*!.*!.*:{1,2,3,4}
byte:3:C_INPUT:from_lower!PDU_JOIN!.*!.*!.*!.*:{1,2}
byte:4:C_INPUT:from_lower!PDU_JOIN!.*!.*!.*!.*:{0,2}
byte:5:C_INPUT:from_lower!PDU_JOIN!.*!.*!.*!.*:{1}
# ==================================

Conference Protocol in Promela

Another more elaborate example for the same events. Here we first replace the ``byte'' variables with new variable names with a more expressive type name, which we then instantiate.


# ==================================
byte:2:C_INPUT:from_upper!JOIN!.*!.*:{var_usertitle}
byte:3:C_INPUT:from_upper!JOIN!.*!.*:{var_conferenceid}
byte:2:C_INPUT:from_upper!LEAVE!.*!.*:{var_usertitle}
byte:3:C_INPUT:from_upper!LEAVE!.*!.*:{var_conferenceid}
byte:2:C_INPUT:from_upper!DREQ!.*!.*:{var_len}
byte:3:C_INPUT:from_upper!DREQ!.*!.*:{var_data}
byte:2:C_INPUT:from_lower!PDU_JOIN!.*!.*!.*!.*:{var_usertitle}
byte:3:C_INPUT:from_lower!PDU_JOIN!.*!.*!.*!.*:{var_conferenceid}
byte:4:C_INPUT:from_lower!PDU_JOIN!.*!.*!.*!.*:{var_udpaddr_src}
byte:5:C_INPUT:from_lower!PDU_JOIN!.*!.*!.*!.*:{var_udpaddr_dst}
byte:2:C_INPUT:from_lower!PDU_ANSWER!.*!.*!.*!.*:{var_usertitle}
byte:3:C_INPUT:from_lower!PDU_ANSWER!.*!.*!.*!.*:{var_conferenceid}
byte:4:C_INPUT:from_lower!PDU_ANSWER!.*!.*!.*!.*:{var_udpaddr_src}
byte:5:C_INPUT:from_lower!PDU_ANSWER!.*!.*!.*!.*:{var_udpaddr_dst}
byte:2:C_INPUT:from_lower!PDU_LEAVE!.*!.*!.*!.*:{var_usertitle}
byte:3:C_INPUT:from_lower!PDU_LEAVE!.*!.*!.*!.*:{var_conferenceid}
byte:4:C_INPUT:from_lower!PDU_LEAVE!.*!.*!.*!.*:{var_udpaddr_src}
byte:5:C_INPUT:from_lower!PDU_LEAVE!.*!.*!.*!.*:{var_udpaddr_dst}
byte:2:C_INPUT:from_lower!PDU_DATA!.*!.*!.*!.*:{var_len}
byte:3:C_INPUT:from_lower!PDU_DATA!.*!.*!.*!.*:{var_data}
byte:4:C_INPUT:from_lower!PDU_DATA!.*!.*!.*!.*:{var_udpaddr_src}
byte:5:C_INPUT:from_lower!PDU_DATA!.*!.*!.*!.*:{var_udpaddr_dst}
mtype:1:C_INPUT:from_lower!.*!.*!.*!.*!.*:{PDU_JOIN,PDU_ANSWER,PDU_LEAVE,PDU_DATA}
mtype:1:C_INPUT:from_upper!.*!.*!.*:{JOIN,LEAVE,DREQ}
usertitle:*:C_INPUT:from_upper!.*!.*!.*:{101,102,103,104}
conferenceid:*:C_INPUT:from_upper!.*!.*!.*:{51,52}
udpaddr_src:*:C_INPUT:from_upper!.*!.*!.*:{0,2}
udpaddr_dst:*:C_INPUT:from_upper!.*!.*!.*:{1}
len:*:C_INPUT:from_upper!.*!.*!.*:{21}
data:*:C_INPUT:from_upper!.*!.*!.*:{31,32,33,34}
usertitle:*:C_INPUT:from_lower!.*!.*!.*!.*!.*:{101,102,103,104}
conferenceid:*:C_INPUT:from_lower!.*!.*!.*!.*!.*:{51,52}
udpaddr_src:*:C_INPUT:from_lower!.*!.*!.*!.*!.*:{0,2}
udpaddr_dst:*:C_INPUT:from_lower!.*!.*!.*!.*!.*:{1}
len:*:C_INPUT:from_lower!.*!.*!.*!.*!.*:{21}
data:*:C_INPUT:from_lower!.*!.*!.*!.*!.*:{31,32,33,34}
unknown:*:C_INPUT:from_upper!.*!.*!.*:( join(var_usertitle,var_conferenceid)
\
                                        answer(var_usertitle,var_conferenceid)
\
                                        leave(var_usertitle,var_conferenceid)
\
                                        data(var_len,var_data) )
# ==================================

Conference Protocol in LOTOS, Symbolic

Here the variables already have a clear type, so we don't have to look at the position instantiate. We do use the ``repeated rule application'' feature to construct ``complex'' values, by repeatedly instantiating variables with expressions that contain new variables, that are then instantiated, etc.


# ==================================
DataField     :*:C_INPUT:.*:{m1,m2,m3,m4}
DataFieldLen  :*:C_INPUT:.*:{l}
UserTitle     :*:C_INPUT:.*:{ut_A,ut_B,ut_C,ut_D}
ConfIdent     :*:C_INPUT:.*:{ci_one}
# ConfIdent     :*:C_INPUT:.*:{ci_one,ci_two}
UDPAddress_dst:*:C_INPUT:.*:{udp1}
UDPAddress_src:*:C_INPUT:.*:{udp2,udp3}
CFsp          :*:C_INPUT:.*:( datareq(var_DataField)               \
                              join(var_UserTitle,var_ConfIdent)    \
                              leave                                )
UDPsp         :*:C_INPUT:.*:( udp_datareq(var_UDPAddress_dst,var_PDU) )
#UDPsp        :*:C_INPUT:.*:( udp_dataind(var_UDPAddress_dst,var_PDU) )
PDU           :*:C_INPUT:.*:( PDU_J(var_UserTitle,var_ConfIdent)     \
#                              PDU_A(var_UserTitle,var_ConfIdent)     \
#                              PDU_L(var_UserTitle,var_ConfIdent)     \
                              PDU_D(var_DataFieldLen,var_DataField)  )
# ==================================

See Also

torx-intro(1), torx-primer(5)

Contact

By Email: <torx_support@cs.utwente.nl>

Version

This manual page documents version 3.9.0 of torx.


Table of Contents


Prev Table of Contents Next
Appendix D: TorX Manual Pages: hexcontext(1) - run program in hexadecimal context Valid HTML 4.01! Appendix D: TorX Manual Pages: intersector(1) - combine multiple torx primers