[ 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

torx-explorer(5) - interface to program to explore a labelled transition

Table of Contents

Name

torx-explorer - interface to program to explore a labelled transition system

Synopsis

EXPLORER [ options ]

Description

The EXPLORER module implements an (textual) interface to explore a labelled transition system (lts).

When active, the EXPLORER receives commands from the standard input and writes answers in return to the standard output. See section COMMANDS and ANSWERS for the available commands and answers. When a EXPLORER is used in the TORX tool it is connected to a PRIMER which has the control and initiative of all communications. When the EXPLORER is used as standalone the user plays the role of the PRIMER.

A command consist of a single line of text. The first character of a command indicates the type of the command. This first character is always in lowercase.

An answer consist of a single line of text or a multi-line of text. All single line answers start with the character of their command turned into uppercase. A multi-line answer has specific markers around the body of the answer. These markers consist of two characters at a single line, made up from the usual answer prefix character, with B and E appended, respectively. Each line of the body of a multi line answer starts with a two character prefix consisting of the usual uppercase answer prefix character, followed by the same character in lowercase. Each answer line can contain multiple fields. Arbitrary whitespace (one or more spaces or tabs) separates the fields from the (one or two character) prefix at the start of the line. The fields themselves are separated by a singe tab character. A fields cannot contain tab characters, is assumed not to start or end with spaces.

Instead of the usual answer, an error answer may occur in case of an error. Also error answers start with a two character prefix, consisting of the usual uppercase answer prefix character, followed by the character ``0''.

The following describes the syntax of the commands and answers:

interaction:
message* command message* answer-or-error
command:
lowercase(name) arguments-upto-end-of-line nl
answer-or-error:
single-line-answer | multi-line-answer | error
single-line-answer:
uppercase(name) arguments-upto-end-of-line nl
multi-line-answer:
uppercase(name)B nl multi-line-element* uppercase(name)E nl
multi-line-element:
message | result-element
result-element:
uppercase(element-name) arguments-upto-end-of-line nl
message:
debug | log | warning
debug:
A_DEBUG text-upto-end-of-line nl
log:
A_LOG text-upto-end-of-line nl
warning:
A_WARNING text-upto-end-of-line nl
error:
uppercase(name)0
arguments-upto-end-of-line nl

Representation

The interface uses numbers to identify transitions (a.k.a. events) and states. A single number identifies at the same time both a transition and the state to which the transition ``points''. If two transitions point to the same state, they will have different numbers. However, we can still tell that they point to the same state, because that information is present in the additional information that is given in the output of each interface command that ``generates'' new transitions. This additional information contains a field ``identical'' that either is empty (if this transition is the first one to ``point'' to its state), or, otherwise, contains the number of the ``first'' transition that pointed to the state. Subsequently generated transitions that point to the same state all have the same value for this field ``identical'', so, in a way, a user can treat the value of this field as the ``canonical'' identification of the state that a transition points to.

Boolean values are represented by the characters ``1'' and ``0'' for respectively true and false.

For the variable names, types and predicates that are used in a symbolic explorer we expect the following representation. The type as used in the field freevars ``looks like'' an identifier, i.e. it consists of upper and lowercase characters, digits and underscores. The normalised-varname as used in the fields label, preds, and freevars is constructed from the type of the ``original'' variable and a sequence number. By convention it has the form var_type$nr as show in the example at the end. The original-varname as used in the field freevars and in the predicates of the instantiate command ``looks like'' an identifier, i.e. it consists of upper and lowercase characters, digits and underscores. The predicates used in the instantiate command is a semi-colon separated list of predicates, where each of the individual predicates in the list should not contain newlines or semi-colons. One could imagine various syntaxes for the individual predicates in the list, depending on the purpose of the predicate. Possible purposes are to specify a specific value for a free variable, or to constrain the range of possible values for a free variable. The current symbolic primer(1) uses the instantiate command to specify specific values for free variables. It uses the syntax original-varname = expression for the predicates in the semi-colon separated list of predicates, as illustrated in the example at the end.

COMMMANDS and ANSWERS

The following commands give the core functionality of a non-symbolic explorer, to reset, to expand a state, to delete states, and to quit:
r
e event
d event ...
q
A symbolic explorer additionally offers the following commands to instantiate an event, and to ask for solutions to predicates:
i event predicates
p predicates
The command to ask whether a given event matches one of a list of events is implemented in the smile primer, but currently not used in the symbolic primer.
m event event ...
Below we describe these commands in more detail.

Reset

This commands tells the explorer to reset itself, and it returns the (transition pointing to) the initial state. It takes no parameters. The result is a single-line answer containing the fields describing the initial state:
event, solved, preds, freevars, identical
with
event
the event number;
solved
a boolean value that indicates whether or not the predicates for the initial state could be solved (i.e. whether or not it is known if a solution exists for the predicates of the initial state);
preds
the normalised (semi-colon separated) predicates of the initial state (normalised by replacing free variables names by names build from the type of the variable and a sequence number, to make it easier to compare them);
freevars
the (space-separated) list of free variables information, which contains for each free variable a (space-separated) list of three items: normalised-varname, original-varname, and type;
identical
the state to which the state reached by event is identical, or the empty string if this event is the first one that reaches that state.

Command:

r
Answer:
R event TAB solved TAB preds TAB freevars TAB identical

Expand

This commands tells the explorer to expand a given state. It takes as parameter a transition/state number. The result is a multi-line answer where each line of the body of the answer contains fields describing a transition and its corresponding resulting state:
event, visible, solved, label, preds, freevars, identical
with
event
the event number;
visible
a boolean value indicating whether or not the action is visible;
solved
a boolean value that indicates whether or not the predicates to reach the resulting state could be solved (i.e. whether or not it is known if a solution exists for the predicates of the resulting state);
label
a string containting a LOTOS-like event, containing normalised variables, if the event introduces free variables;
preds
the normalised (semi-colon separated) predicates of the resulting state (normalised by replacing free variables names by names build from the type of the variable and a sequence number, to make it easier to compare them);
freevars
the (space-separated) list of free variables information, which contains for each free variable a (space-separated) list of three items: normalised-varname, original-varname, and type;
identical
the state to which the state reached by event is identical, or the empty string if this event is the first one that reaches that state.

Command:

e event
Answer (multi-line):
EB
Ee event TAB visible TAB solved TAB label TAB preds TAB freevars TAB identical
...
EE

Delete

This commands tells the explorer that its user is no longer interested in a (list of) events/states, and will never refer to them in the future. This allows the explorer to delete them, and free memory, if it wants to. Parameter: a (whitespace separated) list of events/states; result: a single-line answer, containing no result (currently).

Command:

d event ...
Answer:
D

Quit

This commands tells the explorer to quit. It takes no parameters, and returns no result.

Command:

q
Answer:
Q

Instantiate

This commands tells the explorer to instatiate a given event using a given list of predicates. It takes as parameter an event, followed by a (semi-colon separated) list of predicates. The resultis a single-line answer, containing the result of instantiation of the given event using the predicates. If the instantiation is successful, the result line contains the same fields as a result line of the expand command; if instantiation is not successful, the error result contains the same fields as the solve command.

The fields of the successful result contain a description of an action and corresponding resulting state:

event, visible, solved, label, preds, freevars, identical
with
event
the event number;
visible
a boolean value indicating whether or not the action is visible;
solved
a boolean value that indicates whether or not the predicates to reach the resulting state could be solved (i.e. whether or not it is known if a solution exists for the predicates of the resulting state);
label
a string containting a LOTOS-like event, containing normalised variables, if the event introduces free variables;
preds
the normalised (semi-colon separated) predicates of the resulting state (normalised by replacing free variables names by names build from the type of the variable and a sequence number, to make it easier to compare them);
freevars
the (space-separated) list of free variables information, which contains for each free variable a (space-separated) list of three items: normalised-varname, original-varname, and type;
identical
the state to which the state reached by event is identical, or the empty string if this event is the first one that reaches that state.

The fields of the error result contain information about the (lack of) success of finding a solution, and, if a solution was found, the solution itself:

solved, found, preds, msg, err
with
solved
a boolean value that indicates whether or not the predicates could be solved;
found
a boolean value that indicates whether or not a solution could be found (only of interest when solved is 1);
preds
the (semi-colon separated) list of predicates that describe the solution found (only of interest when solved and found are both 1);
msg
a (semi-colon separated) list of messages, produced during the narrowing process;
err
a (semi-colon separated) list of error messages, produced during the narrowing process.

Command:

i event WS predicates
Answer (succesfull):
I event TAB visible TAB solved TAB label TAB preds TAB freevars TAB identical
Answer (error):
I0 solved TAB found TAB preds TAB msg TAB error

Solve

This commands tells the explorer to solve the given predicates. This does not influence the state of the explorer: the explorer is just used as ``ADT desk calculator''.
Note: this command is not used by the (symbolic) primer and is currently only there for the convenience of the user. It may be removed in later versions of this interface.
It takes as parameter a (semi-colon separated) list of predicates. The resultis a single-line answer, containing information about the success of finding a solution, and, if a solution was found, the solution itself:
solved, found, preds, msg, err
with
solved
a boolean value that indicates whether or not the predicates could be solved; (i.e. whether or not it could find a solution or prove that no solution exists);
found
a boolean value that indicates whether or not a solution could be found (only of interest when solved is 1);
preds
the (semi-colon separated) list of predicates that describe the solution found (only of interest when solved and found are both 1);
msg
a (semi-colon separated) list of messages, produced during the narrowing process;
err
a (semi-colon separated) list of error messages, produced during the narrowing process.

Command:

p predicates
Answer:
P solved TAB found TAB preds TAB msg TAB error

Match

This commands tells the explorer to try to match an event (generally representing a set of events) with a list of events (numbers) (also, each of them generally representing a set of events).
This could be used by the primer to combine the menu's of several states. However, currently it is not used, and it could be removed in later versions of this interface.
It takes as parameter an event, followed by whitespace, followed by a (whitespace separated) list of events. The result is a single-line answer, containing
found, event
with
found
a boolean value indication whether a matching event was found;
event
a matching event from the list, if a match was found, or the empty string, otherwise (none of the events of the list match).

Command:

m event event ...
Answer (sccessfull):
M found TAB event
Answer (error):
M0 error text upto end of line

Options

There are no general command line options for the explorer, that apply to each explorer, because its behaviour can not be parameterised, and therefore does not need command line options. As a consequence, the command line options are currently explorer specific: they are different for each individual explorer.

Example

In this example we show a session with the symbolic explorer for LOTOS (which uses the symbolic LOTOS simulator smile). In the session we use the r command to get the initial state (transition), which we explore using the e command; we instantiate one of the events two times, using different values for the free variables, and we explore the result of both the instantiations, one (10) only one ``step'' deeper, the other (5) until we have traverse all internal (invisible) transitions leading from it.
One line in the output of that explorer was too long to fit on a single line; we use a continuation mark \\ to indicate that an output line continues on the next line. 
$ smileexp cf-pe-sut-smile.cr
r
R 0    1            
e 0
EB
Ee    3    1    1    udp_in ! udp2 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_227_0
PDU    
Ee    2    1    1    udp_in ! udp3 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_226_0
PDU    
Ee    1    1    1    CFSAP_in ! cf1 ! join(var_UserTitle$1, var_ConfIdent$1)               \
    var_UserTitle$1 Smile_224_0 UserTitle var_ConfIdent$1 Smile_225_0 ConfIdent    
EE
i 1 Smile_225_0 = ut_A  ; Smile_224_0 = ci_one
I    4    1    1    CFSAP_in ! cf1 ! join(ut_A, ci_one)    Smile_225_0 = ut_A  ; Smile_224_0
= ci_one        1
e 4
EB
Ee    9    1    1    CFSAP_in ! cf1 ! datareq(var_DataField$1)        var_DataField$1 Smile_230_0
DataField
Ee    8    1    1    CFSAP_in ! cf1 ! leave            
Ee    7    1    1    udp_in ! udp3 ! udp_datareq(udp1, var_PDU$1)    var_PDU$1 Smile_229_0
PDU
Ee    6    1    1    udp_in ! udp2 ! udp_datareq(udp1, var_PDU$1)    var_PDU$1 Smile_228_0
PDU
Ee    5    0    1    i ! cf1 ! join(ut_A, ci_one)            
EE
i 1 Smile_225_0 = ut_B  ; Smile_224_0 = ci_two
I    10    1    1    CFSAP_in ! cf1 ! join(ut_B, ci_two)    Smile_225_0 = ut_B  ; Smile_224_0
= ci_two        1
e 10
EB
Ee    15    1    1    CFSAP_in ! cf1 ! datareq(var_DataField$1)        var_DataField$1 Smile_233_0
DataField
Ee    14    1    1    CFSAP_in ! cf1 ! leave
Ee    13    1    1    udp_in ! udp3 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_232_0
PDU
Ee    12    1    1    udp_in ! udp2 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_231_0
PDU
Ee    11    0    1    i ! cf1 ! join(ut_B, ci_two)
EE
e 5
EB
Ee    21    0    1    i ! udp1 ! udp_datareq(udp2, PDU_J(ut_A, ci_one))
Ee    20    0    1    i ! udp1 ! udp_datareq(udp3, PDU_J(ut_A, ci_one))
Ee    19    1    1    udp_in ! udp3 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_236_0
PDU
Ee    18    1    1    udp_in ! udp2 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_235_0
PDU
Ee    17    1    1    CFSAP_in ! cf1 ! datareq(var_DataField$1)        var_DataField$1 Smile_234_0
DataField
Ee    16    1    1    CFSAP_in ! cf1 ! leave
EE
e 20
EB
Ee    27    0    1    i ! udp1 ! udp_datareq(udp2, PDU_J(ut_A, ci_one))
Ee    26    1    1    udp_out ! udp3 ! udp_dataind(udp1, PDU_J(ut_A, ci_one))
Ee    25    1    1    udp_in ! udp2 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_239_0
PDU
Ee    24    1    1    udp_in ! udp3 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_238_0
PDU
Ee    23    1    1    CFSAP_in ! cf1 ! datareq(var_DataField$1)        var_DataField$1 Smile_237_0
DataField
Ee    22    1    1    CFSAP_in ! cf1 ! leave
EE
e 21
EB
Ee    33    0    1    i ! udp1 ! udp_datareq(udp3, PDU_J(ut_A, ci_one))
Ee    32    1    1    udp_out ! udp2 ! udp_dataind(udp1, PDU_J(ut_A, ci_one))
Ee    31    1    1    udp_in ! udp2 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_242_0
PDU
Ee    30    1    1    udp_in ! udp3 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_241_0
PDU
Ee    29    1    1    CFSAP_in ! cf1 ! datareq(var_DataField$1)        var_DataField$1 Smile_240_0
DataField
Ee    28    1    1    CFSAP_in ! cf1 ! leave
EE
e 27
EB
Ee    39    1    1    udp_out ! udp2 ! udp_dataind(udp1, PDU_J(ut_A, ci_one))
Ee    38    1    1    udp_out ! udp3 ! udp_dataind(udp1, PDU_J(ut_A, ci_one))
Ee    37    1    1    udp_in ! udp3 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_245_0
PDU
Ee    36    1    1    udp_in ! udp2 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_244_0
PDU
Ee    35    1    1    CFSAP_in ! cf1 ! datareq(var_DataField$1)        var_DataField$1 Smile_243_0
DataField
Ee    34    1    1    CFSAP_in ! cf1 ! leave
EE
e 33
EB
Ee    45    1    1    udp_out ! udp3 ! udp_dataind(udp1, PDU_J(ut_A, ci_one))
Ee    44    1    1    udp_out ! udp2 ! udp_dataind(udp1, PDU_J(ut_A, ci_one))
Ee    43    1    1    udp_in ! udp3 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_248_0
PDU
Ee    42    1    1    udp_in ! udp2 ! udp_datareq(udp1, var_PDU$1)        var_PDU$1 Smile_247_0
PDU
Ee    41    1    1    CFSAP_in ! cf1 ! datareq(var_DataField$1)        var_DataField$1 Smile_246_0
DataField
Ee    40    1    1    CFSAP_in ! cf1 ! leave
EE
q
Q

Note

The interface can likely be simplified with respect to the freevars fields: we should investigate whether or not we can `hide' the `original' free-variable names inside the explorer, and reduce the three-tuples of
normalised-varname, original-varname, type
to tuples of
varname, type

Question: would it be wise to change the interface such that the ``identical'' fields in the output of commands that ``generate'' events are never empty, but always contains the canonical state identifier -- which is identical to the transition identifier for transitions that are the ``first'' to point to a state? In that case, the user can always use the value of the field ``identical'' as canonical state identification (instead of having to check first if it is empty, and in that case using the transition identifier).

See Also

torx-intro(1), mkprimer(1), torx-adaptor(5), torx-primer(5), torx-config(4), torx-log(4), torx(1)

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: torx-adaptor(5) - a program that implements an interface to the SUT Valid HTML 4.01! Appendix D: TorX Manual Pages: torx-instantiator(5) - a program that implements an instantiator