Testing Runtime

Command Line Options

TRON binary is based on verifyta utility from Uppaal, hence there are a few options available to tune the Uppaal engine too. I will explain only TRON specific ones and some of verifyta that might effect testing. The following is printed on screen when TRON is run in command line:

./tron -h
Usage: tron [options] -I adapter model.xml [-- parameters to adapter]
Options:
  -A  Use convex-hull approximation.
  -D filename
      specify a file for driver log (default /dev/null).
  -F future
      The amount of future in mtu to be precomputed (default 0),
      To disable precomputation set it to -1 (not recommended).
  -H n
      Set the hash table size for bit state hashing to 2**n
      (default = 27)
  -I filename
      dynamic C-library with adapter to an implementation, or:
      TraceAdapter -- interact via textual stdin/stdout;
      SocketAdapter -- remote TCP/IP socket adapter.
  -P delay
      short,long: try random delay from one of intervals (mtu),
      eager: delay as little as possible for chosen transition,
      lazy: delay as much as possible for chosen transition,
      random: delay within bounds specified by model (default).
  -Q log
      use logical (simulated) clock instead of host clock.
      or specify port number for simulated clock: -Q 6521
  -S filename
      Append the verdict, I/O and duration to file (default /dev/null)
  -U  Unpack reduced constraint systems before relation test.
  -V  Print version information and exit.
  -X integer
      Value to initialize random number generator (default time)
  -h  Print this message.
  -i <dot|gui>
      Print a signal flow diagram of the system and exit:
        dot: outputs dot graph, expects formated standard input:
             "input" (channel)* "output" (channel)*
        gui: non-partitioned flow information for TRON GUI;
  -o filename
      Redirect output to file instead of stdout, see also -v
  -s <0|1|2>
      Select search order.
        0: Breadth first (default)
        1: Depth first
        2: Random depth first
  -u inpDelay,inpRes,outDelay,outRes
  -u inpRes,outRes
      Observation uncertainty intervals in microseconds:
      inpDelay: the least delay that takes to deliver input,
      inpRes:   possible additional delay for delivering input,
      outDelay: the least delay that takes to observe output,
      outRes:   possible additional delay for observing output.
  -v <0+1+2+4+8+16>
      Specify verbosity of the output.
      For -o test logging verbosity bit-flags:
        = 0: only verdict, disable trace output (default),
        & 1: progress indicator for interactive experiments,
        & 2: test events applied in the UPPAAL engine,
        & 4: available input and delay choices for simulation,
        & 8: backup state set and prepare for final diagnostics,
        &16: dumps current state set on each update.
      For -i partitioning: 0-none, 1-errors, 2-warnings, 3-diagnostics.
  -w integer
      Specify additional number of time units to attempt to violate invariants.
      Works under assumption that invariants are not used in Environment.
  -q  Do not display the copyright message.

Environment variables:
  UPPAAL_DISABLE_SWEEPLINE   disable sweepline method
  UPPAAL_DISABLE_OPTIMISER   disable peephole optimiser
  UPPAAL_OLD_SYNTAX          use version 3.4 syntax

The value of these variables does not matter. Defining them is
enough to activate the feature in question.

Here is a more detailed description of testing specific options:

-I filename specifies the adapter to connect to IUT. It is either the name of a built-in adapter (such as TraceAdapter and SocketAdapter) or the filename of dynamically loaded C-library. See Building Test Adapter on how to make one.
-D filename specifies where the output of the Driver (component that time-stamps input and output events) should be redirected to. The EBNF of the output is the following:
```
DriverLog ::= ( line EOL )*
line ::= timestamp | event
timestamp ::= "delay" integer
event ::= channelname "(" paramlist ")"
paramlist ::= | integer ( "," integer )*
```
The timestamp line means that the system has delayed until the specified absolute time moment in microseconds counting from the beginning of testing. The event line means an input or an output event observation at the last delay timestamp in the driver. The specific input or output nature is specified by channel name and the bounded variable integer values.
-S filename specifies where the verdict information should be saved (usually used for gathering Statistics of many TRON runs). If specified, each line of the file will consist of five elements: 1) integer for random seed used (see -X) 2) verdict 3) number of inputs 4) number of outputs 5) time used in model time units.
-v <0+1+2+4+8+16> specifies what testing information should be visible on the output by bit-flags:
- 1 progress indicator, useful in interactive command-line when no other testing information is specified;
- 2 events applied in Uppaal engine (mainly for debugging);
- 4 choices considered when emulating the environment;
- 8 makes a copy of the current state set before applying delay and output events, this enables some diagnostic information when test verdict is failed or inconclusive but also costs a bit of additional memory;
- 16 shows the current reachable state set before each update.
The numbers above should be added and final integer result used in -v option. For example, for progress indicator (1) and diagnostic information (8) one should use -v 9 as 1+8=9.
-o filename redirects the testing information (specified by -v) to the file rather than standard output stream.
-H n specifies the size of hash table in Uppaal engine for detecting loops in passed list states (as in verifyta), the size in testing can be much smaller as the TRON considers only the current reachable state set which is much smaller than the whole state space of the system (as in verification process);
-F future specifies the future input event horizon for environment emulation in model time units, the further horizon the more TRON should pre-compute into the future when choosing input event; the value should be as large as possible for richer input choices but small enough for TRON to be able to compute respond within 1 model time unit; the default is 1 model time unit (disabling it with 0 is not recommended);
-P delay constrains the choice of delay by the following heuristics:
- random the choice is based on available delays in the model and concrete delay is chosen by pseudo-random number generator; if delays are not bounded by invariant TRON may choose very large delays and hence appear idle for very long time;
- lazy the choice is based on available delays in the model and concrete delay is taken by choosing the longest possible; TRON may delay for very long if constraints (invariants) allow it;
- eager the choice is based on available delays in the model and concrete delay is taken by choosing the shortest delay possible;
- short,long are integers and specify the longest delay choice for short and long delay. The concrete delay is then chosen randomly based on the model and longest possible delay. The choice of a short or a long delay is random;
-w integer prolongs the model delay by specified number of model time units possibly breaking the invariants in the model; it was created as a workaround for proper IUT and environment invariant separation to be able to test the IUT invariants under assumption that the environment model did not contain any invariants; today correct partitioning (see Test Interface Specification) of the system model is recommended instead of this option;
-u inpDelay,inpRes,outDelay,outRes see Observation Uncertainties for explanation.
-Q log specifies that virtual time framework should be used rather than host machine's clock, string log can also be replaced by an integer meaning the port number for external virtual clock users, see Virtual Time for more details;
-X integer specifies the value of random seed for the random number generator which drives the environment emulation choices; it could be useful to attempt to replicate an identical test run although it is very hard to ensure the same flow of time and event interleaving;

-i <dot|gui> generates the signal flow of the system model in graphviz format; when specified, TRON expects the input/output interface to be fed into standard input stream in the following EBNF format:

TIS ::= inputs outputs precision timeout
inputs ::= "input" channels ";"
outputs ::= "output" channels ";"
precision ::= "precision" integer ";"
timeout ::= "timeout" integer ";"
channels ::= | channel ( "," channel )* ";"
channel ::= channelname "(" variables ")"
variables ::= | variablename ( "," variablename)*

See also Test Interface Specification. When -i is specified, -v option has a different special meaning:

-v <0|1|2|3> specifies what information is produced in partitioning (-i) mode: 0 -- silent, no errors are shown, 1 - only errors are shown, 2 - warnings are shown, 3 - errors, warnings and rules being applied are shown. See also Test Interface Specification.

Interpreting Messages

Here is the beginning of output from smart lamp demo:

UPPAAL TRON 1.4 Beta 2 using UPPAAL 4.1.0 (rev. 2765), October 2006

Compiled with g++-4.1.2 -Wall -DNDEBUG -O2    -DBOOST_DISABLE_THREADS

Copyright (c) 1995 - 2006, Uppsala University and Aalborg University.

```
All rights reserved.
```
```
Options for the UPPAAL engine:
```
```
  Search order is breadth first
```
```
  Using no space optimisation
```

  State space representation uses minimal constraint systems

  Observation uncertainties: 0, 0, 0, 0 (microseconds).

  Future precomputation: closure(300 mtu).

```
  Input delay extended by: 0
```
```
  OS scheduler: non-real-time.
```
```
socket connect: Connection refused
```
```
(* 9 tries left *)
```
```
  Environment processes: user.
```
```
  Timeunit: 10000us
```
```
  Timeout: 1000000mtu
```
```
  Inputs: grasp(), release()
```
```
  Outputs: level(adapLevel)
```

Lines 1-2 specify the version and the build environment of TRON binary, might be important when building the C-library adapter. Lines 3-4 contain copyright information. Lines 5-11 show the state of Uppaal engine and TRON options. Line 12 says that TRON is using non-real-time process scheduler which is used for all virtual time runs. In real time mode TRON will attempt to gain high priority and select real-time round-robin scheduler if possible (available and enough permissions given), which would minimize the scheduling disturbances from other processes. Lines 13-14 show that TRON attempted socket connection (to IUT) but failed and it will retry doing so for 9 times with 2 second intervals. Lines 15-19 show the model partitioning and testing interface information: environment consists of just user process (user invariants will be considered when offering input), model time unit is interpreted as 10000 microseconds, and 1000000 model time units are allocated for testing.

The messages are typical from TRON standard output stream when bit-flag 2 is selected in -v option:

```
TEST: delay to [245.. on 1
```

TEST: grasp()@1225896-1225940 at [245..246) on 1

TEST: level(0)@1771740 at [353..356) on 5

TEST: level(1)@2752912 at [549..552) on 3

TEST: level(2)@3777576 at [755..756) on 3

TEST: level(3)@4798399 at [959..960) on 3

```
TEST: delay to [1153.. on 3
```
```
TEST: delay to [1159.. on 3
```

TEST: release()@5798049-5798094 at [1159..1162) on 3

```
TEST: delay to [1169.. on 13
```
```
TEST: delay to [1175.. on 13
```

Lines 20, 26-27, 29-30 mean that TRON has chosen a delay and nothing happened until it has expired, for example line 20 says that TRON is applying a delay on a current state set to the moment of 245 model time units on a single (1) state in a set, the upper bound of a delay is open and bounded only by future horizon (see -F). Line 21 says that TRON is applying the input event on channel grasp it has just executed at time interval 1225896-1225940 microseconds which is mapped to model time interval [245..246) in Uppaal constraint encoding. The encoding [245..246) means a model time interval (122,123) as 245/2=122.5 (remainder shows that the constraint is strict, i.e. >122, and the point 122mtu is not included) and 246/2=123 which is strict as ")" in the log. The same mapping and encoding procedure applies to outputs on lines 22-25 which show that output events on channel level have variable values attached (0, 1, 2 and 3). The output is time-stamped right after it is registered in the driver. The inputs are time-stamped with two time-stamps: just before offering an input and right after the input is offered, to reflect an over-approximation and uncertainty on when exactly it was actually delivered at (remote) IUT.

Verdict Assignment and Diagnostics

At the end of testing TRON will issue a verdict, which is either PASSED, INCONCLUSIVE or FAILED. PASSED means that the timeout for testing has expired and no faulty behavior has been detected. Test may fail with verdict FAILED if IUT exposes the behavior which could not be mapped in the model of IUT, i.e. if IUT reported wrong output at wrong time (too early or too late) or IUT did not respond at all when it was required to respond with some output. In case of INCONCLUSIVE verdict, TRON is either 1) confused with the output observed from IUT, cannot map this output to the model of environment and hence does not know how to continue testing or 2) late for delivering an input in time as required by the model of environment. The second option can be very frequent on heavily loaded machines, broken schedulers (Windows tend to issue spurious timeouts even if timeout did not expire) while testing in real time using the host machine's clock. Also it is still not clear how to handle situations when TRON and IUT rely on different clocks which drift away from each other, hence we rely on assumption that TRON is operating on a correct (reference) clock.

TRON can also provide additional information on why the test ended up with verdict FAILED or INCONCLUSIVE if the bit-flag 8 is specified on -v option. The following is a typical output of such diagnostic information:

Short post-mortem analysis based on last good stateSet(3):

```
1)
```

( interface.touching switch.idle dimmer.PassiveUp user.busy graspAdapter._id26 ... )

interface.x>47, dimmer.x>260, user.z>52, graspAdapter.x>52, ...

on=1 iutLevel=5 OL=7 adapLevel=5 user.L=5

```
2)
```

( interface.holding switch.idle dimmer._id10 user.busy graspAdapter._id26 ... )

interface.x>=50, user.z>52, graspAdapter.x>52, releaseAdapter.x>162, ...

on=1 iutLevel=7 OL=7 adapLevel=5 user.L=5

```
3)
```

( interface.holding switch.idle dimmer.Up user.busy graspAdapter._id26 ... )

interface.x>=50, user.z>52, graspAdapter.x>52, releaseAdapter.x>162, #t>5937, ...

on=1 iutLevel=7 OL=7 adapLevel=7 user.L=5

```
  Options for input   : (empty)
```

  Options for output  : level@[11875..11894)

  Options for internal: starthold@[11875..13770), setLevel@[11875..11890)

```
  Options for delay   : ..13770)
```
```
  Last time-window    : [11987..11990)
```

Could not delay any more (to the last time-window).

Output expected: level(7)@0-0[11875..11894)

TEST FAILED: IUT failed to produce output in time

```
Time elapsed: 5993 tu = 59.939325s
```
```
Time    left: 994007 tu = 9940.060675s
```
```
Random  seed: 1163420344
```

AdapterConnection died: socket closed upon read

Line 31 says the following analysis is based only on the last good state (might be inaccurate if fault happened much earlier than observed) consisting of 3 symbolic states. Lines 32-43 enumerate the symbolic states (it can be very long, this is a shortened version of it), for example line 32 specifies the symbolic state number 1, line 33 says in which control locations the processes are, line 34 enumerates clock constraints and line 35 enumerates values of integer variables. Lines 44-47 reiterates what options TRON was facing just before test has terminated: line 44 says that there could be no inputs offered, line 45 says that according to model the output level is expected at model time interval (5937,5947) (as 11875/2=5937.5 and 11894/2=5947 in Uppaal encoding), line 46 enumerates internal transitions available in the model, line 47 specifies the longest possible delay until 6885mtu without observable input/output. Line 48 says that TRON was trying to compute the reachable symbolic state set for the interval (5993,5995), but according to line 49 it could not, as the resulting symbolic state set contained no states. Line 50 notes that there was level(7) output expected at (5937,5947) therefore the conclusion in line 51 is that IUT failed to produce output (in required time). Lines 52-53 show how long test was running and how much left to testing timeout in model time units and seconds. Line 54 shows the random seed used to start the pseudo-random number generator (see -X option). Line 55 contains spurious exception upon disposing SocketAdapter which can be safely ignored.

As of version 1.4 be aware of bug 369 in diagnosis.

Uppaal TRON

Testing Runtime

Command Line Options

Interpreting Messages

Verdict Assignment and Diagnostics