Skip to main content.

This page’s menu:

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]
  -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:

Interpreting Messages

Here is the beginning of output from smart lamp demo:

  1. UPPAAL TRON 1.4 Beta 2 using UPPAAL 4.1.0 (rev. 2765), October 2006
  2. Compiled with g++-4.1.2 -Wall -DNDEBUG -O2    -DBOOST_DISABLE_THREADS
  3. Copyright (c) 1995 - 2006, Uppsala University and Aalborg University.
  4. All rights reserved.
  5. Options for the UPPAAL engine:
  6.   Search order is breadth first
  7.   Using no space optimisation
  8.   State space representation uses minimal constraint systems
  9.   Observation uncertainties: 0, 0, 0, 0 (microseconds).
  10.   Future precomputation: closure(300 mtu).
  11.   Input delay extended by: 0
  12.   OS scheduler: non-real-time.
  13. socket connect: Connection refused
  14. (* 9 tries left *)
  15.   Environment processes: user.
  16.   Timeunit: 10000us
  17.   Timeout: 1000000mtu
  18.   Inputs: grasp(), release()
  19.   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:

  1. TEST: delay to [245.. on 1
  2. TEST: grasp()@1225896-1225940 at [245..246) on 1
  3. TEST: level(0)@1771740 at [353..356) on 5
  4. TEST: level(1)@2752912 at [549..552) on 3
  5. TEST: level(2)@3777576 at [755..756) on 3
  6. TEST: level(3)@4798399 at [959..960) on 3
  7. TEST: delay to [1153.. on 3
  8. TEST: delay to [1159.. on 3
  9. TEST: release()@5798049-5798094 at [1159..1162) on 3
  10. TEST: delay to [1169.. on 13
  11. 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:

  1. Short post-mortem analysis based on last good stateSet(3):
  2. 1)
  3. ( interface.touching switch.idle dimmer.PassiveUp user.busy graspAdapter._id26 ... )
  4. interface.x>47, dimmer.x>260, user.z>52, graspAdapter.x>52, ...
  5. on=1 iutLevel=5 OL=7 adapLevel=5 user.L=5
  6. 2)
  7. ( interface.holding switch.idle dimmer._id10 user.busy graspAdapter._id26 ... )
  8. interface.x>=50, user.z>52, graspAdapter.x>52, releaseAdapter.x>162, ...
  9. on=1 iutLevel=7 OL=7 adapLevel=5 user.L=5
  10. 3)
  11. ( interface.holding switch.idle dimmer.Up user.busy graspAdapter._id26 ... )
  12. interface.x>=50, user.z>52, graspAdapter.x>52, releaseAdapter.x>162, #t>5937, ...
  13. on=1 iutLevel=7 OL=7 adapLevel=7 user.L=5
  14.   Options for input   : (empty)
  15.   Options for output  : level@[11875..11894)
  16.   Options for internal: starthold@[11875..13770), setLevel@[11875..11890)
  17.   Options for delay   : ..13770)
  18.   Last time-window    : [11987..11990)
  19. Could not delay any more (to the last time-window).
  20. Output expected: level(7)@0-0[11875..11894)
  21. TEST FAILED: IUT failed to produce output in time
  22. Time elapsed: 5993 tu = 59.939325s
  23. Time    left: 994007 tu = 9940.060675s
  24. Random  seed: 1163420344
  25. 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.