[ 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-01-26
TorX Test Tool Information
Prev		Next

jararaca(1) - explore traces generated from regular expressions

Table of Contents

Name

jararaca - explore traces generated from regular expressions

Synopsis

jararaca [ options ... ] [ file ]
jararaca -h

jararaca implements a (non-symbolic) explorer for regular expressions, given in the jararaca input language. It reads the regular expressions from file, if given, or otherwise from standard input, and builds an automaton for it, that generates the set of traces that can be produced from the regular expression. The automaton is then extended with an epsilon selfloop with (label, event) string "epsilon" on the accept state. Jararaca then offers the TorX explorer-primer interface on standard input and output, to ``lazily'' explore this automaton, and hence, the set of traces. Jararaca uses the (label, event) strings defined for its atomic actions, instead of just using the action identifiers themselves.

Options

The following command line options are supported:

-h: print the version number and an overview of the command line options, and exit.
-a: use the action identifiers themselves instead of the (label, event) strings defined for them
-d: print RFSM in dot(1) format to standard output and exit
-e: run the explorer-primer interface on standard input and output (this is the default)
-l eps: add epsilon loop with (label, event) string eps to accept state. When the TorX combinator sees a special action in the menu of one of its explorer/primers (by default epsilon) it knows that jararaca has reached the accept state. (by default a selfloop with (label, event) string epsilon is added on the accept state)
-L: do not add epsilon self loop on the accept state
-p: print parsetree in dot(1) format to file dest.pt.dot where dest is either the name of the input file, or the string stdin if no input file was given and jararaca read its input from standard input.
-r: print RFSM in dot(1) format to file dest.rfsm.dot where dest is either the name of the input file, or the string stdin if no input file was given and jararaca read its input from standard input.
-s: output strings instead of action id's
-v: verbose mode

Input Format

The input file contains 4 sections, each of which starts with a special keyword that should appear at the start of a line. The sections have to appear in order, and the keyword the starts a next section at the same time closes the previous one. All identifiers should be defined before they can be used. C style comments are allowed (comments start with /* and end with */ and can not be nested)

The first section, which starts with the keyword %description on a single line, contains a non-formal description of the test purpose, its author, goal, date of writing, etc.

The second section, which starts with the keyword %declare on a single line, contains declarations of the actions that are used in the test purpose. An action declaration has the form

action aid "text-string" ;

This defines an action identifier aid, together with a ``verbose'' string representation text-string of it. The ``verbose'' string representation is used unless the -a option of jararaca is used. If the -a option is used, the strings may be left empty
(i.e. consisting just of ""). Action declarations can be grouped in named sets, as follows:

set sid {
action aid1 "text-string1" ,
action aid2 "text-string2" ,
...

};

This defines the action identifiers aid1, aid2, etc. with their string representations text-string1 and text-string2 as belonging to the set named sid. The action identifiers and the set names can be used in the third and fourth sections, which contain the regular expressions.

The third section, which starts with the keyword %define on a single line, contains named regular expressions, as

eid = regular-expression ;

This makes that a named regular-expression can be used as sub-expression in the regular expressions that follow it (in the third section and in the fourth section), by referring to its name eid.

The fourth (and last) section, which starts with the keyword %objective on a single line, contains the regular expression for which the automaton should be build, and which should be explored.

Regular Expressions

The semantics of the regular expressions are defined via a mapping function T that maps regular expressions on a set of sequences of actions (i.e. as a set of traces). In the definition we use . as concatenation operation on sequences of actions. Below we list the valid regular expressions, and their meaning.

Atomic regular expressions are:

aid: the action defined with action identifier aid in the %declare section
T(aid) = { aid }
sid: the action set defined with set identifier sid in the %declare section, which is interpreted as the choice over the elements a1, a2, ..., an if sid was defined as set {a1, a2, ..., an}
This is equivalent to regular expression (a1|a2| ...|an)
T(sid) = { a | exists <sid,A> and <a,s> in A }
eid: the regular expression defined with regular expression identifier eid in the %define section, which is interpreted as (e) if e is the regular expression that is assigned to eid
T(eid) = { s | exists <eid,re> and s in T(re) }

Regular expressions can be built recursively using the following operators, where e, e1, and e2 are regular expressions:

e1.e2: this gives the regular expression formed by concatenating regular expressions e1 and e2
T(e1.e2) = { s1.s2 | s1 in T(e1) and s2 in T(e2) }
e1|e2: this gives the regular expression formed by choosing regular expressions e1 or e2
T(e1|e2) = T(e1) union T(e2)
e1>e2: this gives the regular expression formed by determinstically concatenating regular expressions e1 and e2. This is done by removing the actions that appear at the ``head'' of e2 from the ``head'' of e1, and then non-deterministically doing e2, or doing e1 (minus the removed actions) followed by e2
e[m..n]: this general repetion operator gives the regular expression formed by doing e at least m and at most n times. m and n should be greater than or equal to zero, and n should be greater than or equal to m. The special value infinity is also allowed for m and n.
T(e[m..n]) = Union(m<=i<=n) T(e[i]) where
T(e[0]) = { EmptyString }
T(e[1]) = T(e)
T(e[2]) = { s1.s2 | s1 in T(e) and s2 in T(e) }
...

T(e[i]) = { s1. ... .si | s1 in T(e) and ... and si in T(e) }
...
e*: this gives the regular expression formed by doing e zero or more times.
This is equivalent to regular expressions e[0..] and e[0..infinity]
e+: this gives the regular expression formed by doing e one or more times
This is equivalent to regular expressions e[1..] and e[1..infinity]
e?: this gives the regular expression formed by doing e zero or one times
This is equivalent to regular expression e[0..1]
e[n]: this gives the regular expression formed by doing e exactely n times.
n should be greater than or equal to zero.
This is equivalent to regular expression e[n..n]
e[infinity]: this gives the regular expression formed by doing e infinitely many times.
This is equivalent to regular expression e.e[infinity] or e[infinity..infinity]
(e): this gives the regular expression e.
This is used for grouping, to avoid ambiguous expressions.
jararaca enforces the use of parentheses where necessary.

Examples

Conference Protocol Requirements

%description
 Testpurpose 1-9
    d.d. 12 december 2001
    author: Rene de Vries
    
    Goal: Test purposes for requirement 1-9 of conference protocol
%declare
    set LU {
        action o_PduJoin_P1 "udp_out!UDP2!UDP_DATAIND(UDP1,PDU_J(UT_A,CI_ONE))",
        action o_PduJoin_P2 "udp_out!UDP3!UDP_DATAIND(UDP1,PDU_J(UT_A,CI_ONE))",
        action o_PduAnswer_P1_C1 "udp_out!UDP2!UDP_DATAIND(UDP1,PDU_A(UT_A,CI_ONE))",
        action o_PduAnswer_P1_C2 "udp_out!UDP2!UDP_DATAIND(UDP1,PDU_A(UT_A,CI_TWO))",
        action o_PduAnswer_P2_C1 "udp_out!UDP3!UDP_DATAIND(UDP1,PDU_A(UT_A,CI_ONE))",
        action o_PduAnswer_P2_C2 "udp_out!UDP3!UDP_DATAIND(UDP1,PDU_A(UT_A,CI_TWO))",
        action o_PduData_P1 "udp_out!UDP2!UDP_DATAIND(UDP1,PDU_D(L_1,M1))",
        action o_PduData_P2 "udp_out!UDP3!UDP_DATAIND(UDP1,PDU_D(L_1,M1))",
        action o_PduLeave_P1_C1 "udp_out!UDP2!UDP_DATAIND(UDP1,PDU_L(UT_A,CI_ONE))",
        action o_PduLeave_P1_C2 "udp_out!UDP2!UDP_DATAIND(UDP1,PDU_L(UT_A,CI_TWO))",
        action o_PduLeave_P2_C1 "udp_out!UDP3!UDP_DATAIND(UDP1,PDU_L(UT_A,CI_ONE))",
        action o_PduLeave_P2_C2 "udp_out!UDP3!UDP_DATAIND(UDP1,PDU_L(UT_A,CI_TWO))",
        action o_SpDataInd "cfsap_out!CF1!DATAIND(UT_A,M1)"
    };
    setLI{
        action i_PduJoin_C1 "udp_in!UDP2!UDP_DATAREQ(UDP1,PDU_J(UT_A,CI_ONE))",
        action i_PduJoin_C2 "udp_in!UDP2!UDP_DATAREQ(UDP1,PDU_J(UT_A,CI_TWO))",
        action i_PduAnswer_P1_C1 "udp_in!UDP2!UDP_DATAREQ(UDP1,PDU_A(UT_A,CI_ONE))",
        action i_PduAnswer_P1_C2 "udp_in!UDP2!UDP_DATAREQ(UDP1,PDU_A(UT_A,CI_TWO))",
        action i_PduAnswer_P2_C1 "udp_in!UDP3!UDP_DATAREQ(UDP1,PDU_A(UT_A,CI_ONE))",
        action i_PduAnswer_P2_C2 "udp_in!UDP2!UDP_DATAREQ(UDP1,PDU_A(UT_A,CI_TWO))",
        action i_PduData_P1 "udp_in!UDP2!UDP_DATAREQ(UDP1,PDU_D(L_1,M1))",
        action i_PduData_P2 "udp_in!UDP3!UDP_DATAREQ(UDP1,PDU_D(L_1,M1))",
        action i_PduLeave "udp_in!UDP2!UDP_DATAREQ(UDP1,PDU_L(UT_A,CI_ONE))",
        action i_SpJoin_C1 "cfsap_in!CF1!JOIN(UT_A,CI_ONE)",
        action i_SpDataReq "cfsap_in!CF1!DATAREQ(M1)",
        action i_SpLeave "cfsap_in!CF1!LEAVE"
    };
    action delta "Delta";
%define
    
    /* general strategies */
    LUD = LU|delta;
    eager = LU*.delta;
    /* rewriting/combinations */
    i_PduData = i_PduData_P1 | i_PduData_P2;    
    SpJoinC1 = i_SpJoin_C1.LUD*;
    JoinedConf = SpJoinC1.i_PduAnswer_P1_C1.i_PduAnswer_P2_C1;
    
    o_PduJoin = o_PduJoin_P1 | o_PduJoin_P2;
    o_PduAnswer_P1 = o_PduAnswer_P1_C1 | o_PduAnswer_P1_C2;
    o_PduAnswer_P2 = o_PduAnswer_P2_C1 | o_PduAnswer_P2_C2;
    o_PduAnswer = o_PduAnswer_P1 | o_PduAnswer_P2;
    
    /* modeled requirements as test purpose */
    
    /* we assume 2 potential conference partners */
    Req1 = i_SpJoin_C1.(LUD*>o_PduJoin)[2]; 
    Req2 = i_SpJoin_C1.LUD*.i_PduJoin_C1.LUD*>o_PduAnswer;
    Req3 = i_SpJoin_C1.LUD*.i_PduJoin_C2.eager;
    Req4 = SpJoinC1.i_PduAnswer_P1_C1.i_PduAnswer_P2_C2.
        i_SpDataReq.i_PduData_P1.eager;
    Req5 = JoinedConf.i_SpDataReq.eager;
    Req6 = JoinedConf.i_PduData_P1.i_PduData_P2.eager;
    Req7 = JoinedConf.i_SpLeave.i_SpJoin_C1.eager.i_SpDataReq.eager;
    Req8 = JoinedConf.i_PduLeave.i_SpDataReq.eager;
    Req9 = SpJoinC1.i_PduData_P1.eager;
    
    
%objective
     Req1/*  */
     /* Req2 */
     /* Req3 */
     /* Req4 */
     /* Req5 */
     /* Req6 */
     /* Req7 */
     /* Req8 */
     /* Req9 */
     /*LUD */

Using a Preprocessor

Sometimes when we specify multiple requirements in a single jararaca(1) input file, it is useful to then use a simple shell script to select one of these requirements with a command line option or an environment variable (instead of editing the file to uncomment the selected requirement). The sh(1) (bourne shell) script below demonstrates how we invoke primer(1) as torx-primer(5) with jararaca(1) as torx-explorer(5), where the input file for jararaca(1) is preprocessed with cpp(1) using environment variable TPFLAG. The %objective section of the above script would then be replaced by just:

 %objective
     TP

and TPFLAG could then be used to define TP, for example to something like

-DTP=Req1

to select the first requirement.

#!/bin/sh
tpfile=confprot.tp
tmptpfile=/tmp/torx$$.tp
cfg=explorer-primer-config.txt
cpp -C -E -P $TPFLAG $tpfile > $tmptpfile
primer -f $cfg "$@" jararaca  $tmptpfile
rm -f $tmptpfile

Bugs

The environment variable TORX_ROOT is not supported.

Because the TorX explorer-primer interface ``works'' on standard input and standard output, it is not possible to read the regular expression from standard input and run the TorX explorer-primer interface or write the dot file to standard output and run the TorX explorer-primer interface.

Contact

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

Version

This manual page documents version 3.9.0 of torx.

Table of Contents

Name
Synopsis
Description
Options
Input Format
Regular Expressions
Examples
- Conference Protocol Requirements
- Using a Preprocessor
Bugs
See Also
Contact
Version

Prev	Table of Contents	Next
Appendix D: TorX Manual Pages: pui(1) - simple primer user interface		Appendix D: TorX Manual Pages: jararacy(1) - animate jararaca trace using lefty