Skip to content

Using TChecker

Jump to bottom
Frédéric Herbreteau edited this page Sep 6, 2023 · 11 revisions

Foreword: this document describes how to use TChecker tools v0.3 and above. For previous versions of TChecker, please refer to the corresponding documentation.

TChecker is a verification tool for timed automata as well as a plateform for testing new algorithms. It implements several verification algorithms. This document describes how to invoke these algorithms using the command line tools. Currently, TChecker consists of four tools: tck-syntax, tck-simulate, tck-reach and tck-liveness. Running the tools with command-line option -h lists all available command-line options.

The workflow

The first step in order to use these tools consists in writing a model that complies with the TChecker input format. We recommend using the tool tck-syntax with option -c to check that the model is syntactically correct (please refer to The tool tck-syntax) below.

Please notice that TChecker input files consist in a list of declarations (of variables, processes, locations, edges, etc). Each of these declarations is terminated by an optional list of attributes. For instance, the declaration below defines an edge in process P from location r to location s, with event e. This declaration is terminated by a list of attributes: provided with value x<1, and foo with value bar. TChecker interprets the attribute provided as the guard of the edge (please refer to TChecker input format for details). However, foo is unknown and thus uninterpreted. TChecker does not have fixed list of valid attributes: it is valid to add new attributes like foo in order to use them in your own algorithms implemented in TChecker. However, as a result, a typo such as povided instead of provided is not detected as a syntax error by TChecker tools but as an unknown attribute that will be ignored by the algorithms that are currently implemented. Such misspelling can still be detected by running tck-syntax -c as the tool issues a warning for every attribute name that is unknown to TChecker.

edge:P:r:s:e{provided: x<1 : foo: bar}

Once a syntactically correct model has been written, it is generally a good idea to use the simulator tck-simulate to check that the model behaves as expected. It is particularly useful to check that synchronisations of events work as expected. Please, notice that events which do not appear in a synchronization occur asynchronously.

Finally, the verification tools tck-reach and tck-liveness can be used to assess that the model satisfies its specification.

The description of tools below correspond to the latest version of the tools in the repository. It may slightly differ to the version of the tools in the latest release. Each tool can be run with option -h to get a description of its features.

The tool tck-syntax

The tool tck-syntax implements several analysis on TChecker files: syntax check, model transformation, etc. Launching the tool with option -h yields the list of features:

Usage: ./src/tck-syntax [options] [file]
   -c          syntax check (timed automaton)
   -p          synchronized product
   -t          transform a system into dot graphviz file format
   -j          transform a system into json file format
   -o file     output file
   -d delim    delimiter string (default: _)
   -n name     name of synchronized process (default: P)
   -h          help
reads from standard input if file is not provided
  • Syntax check is performed when option -c is specified. tck-syntax checks that the input file contains a syntactically valid description of system of timed automata and reports all errors and warnings.
  • Model flattening (synchronized product) consists in transforming a model with several concurrent (timed) processes in an equivalent model with a single process (but the exact same runs). This feature is selected with option -p. Then, option -o selects the output file, option -n name sets the name of the resulting process, and option -d delim sets the delimiter used to build state and event names in the resulting process.
  • Options -t and -j allow to translate the TChecker model as a graphviz DOT file and as a JSON file respectively. The output file is specified with option -o.

The tool tck-simulate

The tool tck-simulate is a simulator of timed automata models. It can do randomized simulation as well as interactive simulation. It also outputs the simulation trace using the graphviz DOT file format if asked to.

Launching the tool with option -h lists the features implemented in the tool:

Usage: ./build/src/tck-simulate [options] [file]
   -1          one-step simulation (output initial or next states if combined with -s)
   -i          interactive simulation (default)
   --json      display states/transitions in JSON format
   -r N        randomized simulation, N steps
   -o file     output file for simulation trace (default: stdout)
   -s state    starting state, specified as a JSON object with keys vloc, intval and zone
               vloc: comma-separated list of location names (one per process), in-between < and >
               intval: comma-separated list of assignments (one per integer variable)
               zone: conjunction of clock-constraints (following TChecker expression syntax)
   -t          output simulation trace, incompatible with -1
   -h          help
reads from standard input if file is not provided

The tool tck-simulate can be used in one of three modes: interactive (-i), random (-r) and one-step (-1). These three options are mutually exclusive.

  • option -i selects interactive simulation. At each step, the simulator will display the initial/next states and let the user select the state she wants to proceed with. Notice that it is possible to use randomized selection at any time during the interactive simulation.
  • option -r selects reandomized simulation. This option takes the maximum number of simulation steps as parameter.
  • option -t asks tck-simulate to output the simulation trace. The simulator outputs the simulation trace using the graphviz DOT file format. By default, the trace is output to the standard output.
  • option -o specifies an output file for the trace. It is only useful in combination with option -t.
  • option -s permits to specify the starting state of the simulation. It should be specified following TChecker JSON format (see below).
  • options -1 and --json are provided to allow interaction of external tools with tck-simulate. Option --json tells the simulator to output initial states, as well as next states and transitions using JSON file format (see below). Option -1 selects the one-step simulation mode. If a starting state is specified with option -s, one-step simulation will output the list of next states and transitions of the specified state. Without option -s, the simulator displays the list of initial states.

Here are examples of the JSON file format used by tck-simulate. The list of initial states is output as an object with a single key initial.

{
    "initial": [
        {
            "state": {
                "intval": "id=0",
                "labels": "",
                "vloc": "<A,A,A,A>",
                "zone": "(x1==0 && x2==0 && x3==0 && x4==0 && x1==x2 && x1==x3 && x1==x4 && x2==x3 && x2==x4 && x3==x4)"
            },
            "status": 1,
            "transition": {
                "guard": "",
                "reset": "",
                "src_invariant": "",
                "tgt_invariant": "",
                "vedge": "<>"
            }
        }
    ]
}

Each entry in the list of initial states consists of an object with three keys state (the initial state), status (the status of the initial state, which is always 1 in the simulator) and transition (the initial transition).

The state is made of 4 values:

  • intval, the value of bounded integer variables (if any). It consists of a comma-separated list of assignments like id=0 is the example below.
  • labels, the list of labels (as specified in the model) in the initial state. The initial state in the exampel below has an empty list of labels "".
  • vloc, the vector of process locations. It consists of a comma-separated list of location names, one for each process, following the order of the processes in the model, in-between < and >. In the example below, the vector of locations is "<A,A,A,A>"
  • finally, zone specifies the initial zone, as (x1==0 && x2==0 && x3==0 && x4==0 && x1==x2 && x1==x3 && x1==x4 && x2==x3 && x2==x4 && x3==x4) in the example below.

The transition is made of 5 values:

  • guard, the guard of the transition
  • reset, the list of clock resets on the transition
  • src_invariant, the invariant of the source state of the transition.
  • tgt_invarant, the invariant of the target state of the transition.
  • vedge, the vector of process edges that are triggered on the transition.

In the case of initial transitions, src_invariant specifies the invariant on clocks in the initial states. All other components are empty.

Next states and transitions are listed as an object with two keys: current which specifies the current state (with the same informations as above), and next which yields the list of next states and transitions. Each entry in the next list follows the same format as initial states (see above). The source state of each transition is the current state. The next state is specified by the state part. The transition is given by the transition part. As before, status is always 1.

{
    "current": {
        "intval": "id=0",
        "labels": "",
        "vloc": "<A,A,A,A>",
        "zone": "(x1==0 && x2==0 && x3==0 && x4==0 && x1==x2 && x1==x3 && x1==x4 && x2==x3 && x2==x4 && x3==x4)"
    },
    "next": [
        {
            "state": {
                "intval": "id=0",
                "labels": "",
                "vloc": "<req,A,A,A>",
                "zone": "(x1==0 && 0<=x2 && 0<=x3 && 0<=x4 && x1-x2<=0 && x1-x3<=0 && x1-x4<=0 && x2==x3 && x2==x4 && x3==x4)"
            },
            "status": 1,
            "transition": {
                "guard": "",
                "reset": "x1=0",
                "src_invariant": "",
                "tgt_invariant": "x1<=10",
                "vedge": "<P1@tau>"
            }
        },
        {
            "state": {
                "intval": "id=0",
                "labels": "",
                "vloc": "<A,req,A,A>",
                "zone": "(0<=x1 && x2==0 && 0<=x3 && 0<=x4 && 0<=x1-x2 && x1==x3 && x1==x4 && x2-x3<=0 && x2-x4<=0 && x3==x4)"
            },
            "status": 1,
            "transition": {
                "guard": "",
                "reset": "x2=0",
                "src_invariant": "",
                "tgt_invariant": "x2<=10",
                "vedge": "<P2@tau>"
            }
        }
    ]
}

The state part of initial states or next states can be passed to tck-simulate with option -s. For instance:

tck-simulate -1 --json -s "{\"intval\":\"id=0\",\"labels\":\"\",\"vloc\":\"<A,A,A,A>\",\"zone\":\"(x1==0 && x2==0 && x3==0 && x4==0 && x1==x2 && x1==x3 && x1==x4 && x2==x3 && x2==x4 && x3==x4)\"}" foo.tck

Will perform one-step simulation for the model in file foo.tck, from the initial state above. It will output the list of next states and transitions as above (although the list has been truncated for readability). We used the model produced by exampels/fischer.sh 4 to produce the examples above.

The tool tck-reach

The tool tck-reach implements several reachability algorithms:

  • reach which is the standard reachability algorithm: depth-first search or breadth-first search on the abstract zone graph.
  • covreach which extends the previous algorithm with state covering w.r.t. zone inclusion. This is the standard algorithm for reachability analysis of timed automata, which is implemented in other tools like UPPAAL.
  • concur19 which implements the algorithm presented in: R. Govind, Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz: Revisiting Local Time Semantics for Networks of Timed Automata. CONCUR 2019: 16:1-16:15

Launching the tool with option -h yields a list of features:

Usage: ./build/src/tck-reach [options] [file]
   -a algorithm  reachability algorithm
          reach      standard reachability algorithm over the zone graph
          concur19   reachability algorithm with covering over the local-time zone graph
          covreach   reachability algorithm with covering over the zone graph
   -C type       type of certificate
          none       no certificate (default)
          graph      graph of explored state-space
          symbolic   symbolic run to a state with searched labels if any
          concrete   concrete run to a state with searched labels if any (only for reach and covreach)
   -h            help
   -l l1,l2,...  comma-separated list of searched labels
   -o out_file   output file for certificate (default is standard output)
   -s bfs|dfs    search order
   --block-size  size of allocation blocks
   --table-size  size of hash tables
reads from standard input if file is not provided
  • -a selects the reachability algorithm. This option is mandatory.
  • -C selects the type of reachability certificate. graph outputs a graph representation of the part of the state-space that has been explored. The other two choices symbolic and concrete produce a symbolic/concrete run when the specified labels (see -l) are reachable. It will not produce any certificate if the labels are not reachable (select graph instead). Notice that concrete is not implemented yet for algorithm concur19. CAUTION: choosing symbolic or concrete implies restricted covering in algorithms concur19 and covreach which may lead to bigger unreachability certificates, hence greater memory usage and running time.
  • -o file outputs the certificate in file. By default, the certificate, if required, is written on the standard output.
  • -l specifies a list of labels. The reachability algorithms search for a state that has all the specified labels. If no label is specified, the algorithms compute the entire state-space of the timed automaton.
  • -s selects a search order for the algorithms which can be either breadth-first search (bfs) or depth-first search (dfs)
  • --block-size specifies the size of allocation blocks. TChecker uses pool allocators and garbage collection. Increasing the size of allocation blocks results in allocating more objects (states, zones, etc) at a time. This may increase memory consumption by allocating more memory that actually needed, however, on this will decrease the number of garbage collections. Hence, we recommend to increase the size of allocation blocks for big models.
  • --table-size specifies the size of hash tables. The performances of TChecker rely on the absence of collisions in hash table. Thus, we recommend to increase the size of hash tables for big models.

The tool tck-liveness

The tool tck-liveness implements several liveness verification algorithms:

  • couvscc is based on Couvreur's SCC-decomposition based algorithm as described in Andreas Gaiser, Stefan Schwoon: Comparison of Algorithms for Checking Emptiness on Büchi Automata. MEMICS 2009
  • ndfs is the standard nested depth-first search algorithm with the optimisations presented in Andreas Gaiser, Stefan Schwoon: Comparison of Algorithms for Checking Emptiness on Büchi Automata. MEMICS 2009

Launching the tool with option -h yields a list of features:

Usage: ./build/src/tck-liveness [options] [file]
   -a algorithm  liveness algorithm
          couvscc    Couvreur's SCC-decomposition-based algorithm
                     search an accepting cycle that visits all labels
          ndfs       nested depth-first search algorithm over the zone graph
                     search an accepting cycle with a state with all labels
   -C type       type of certificate
          none       no certificate (default)
          graph      graph of explored state-space
          symbolic   symbolic lasso run with loop on labels (not for couvscc with mulitple labels)
   -h            help
   -l l1,l2,...  comma-separated list of accepting labels
   -o out_file   output file for certificate (default is standard output)
   --block-size  size of allocation blocks
   --table-size  size of hash tables
reads from standard input if file is not provided
  • -a selects the livenes verification algorithm. This option is mandatory.
  • -C asks for a certificate to be output. The certificate is a graph representation of the explored path of the state-space when graph is selected. Instead, symbolic outputs a lasso path that visits the specified labels (see -l) infinitely often. NB: symbolic is not implemented for algorithm couvscc with multiple labels, i.e. generalized Büchi conditions.
  • -o file outputs the certificate in file (if required).
  • -l specifies a list of labels. Notice, that labels are interpreted as a single Büchi condition for algorithm ndfs and as a generalized Büchi condition for algorithm couvscc. Hence, ndfs searches for a lasso run that visits a state with all labels infinitely often, whereas couvscc searches for a lasso path with all labels on the cycle (not necessarily on the same state). If no label is specified, the algorithms compute the entire state-space of the timed automaton.
  • --block-size specifies the size of allocation blocks. TChecker uses pool allocators and garbage collection. Increasing the size of allocation blocks results in allocating more objects (states, zones, etc) at a time. This may increase memory consumption by allocating more memory that actually needed, however, on this will decrease the number of garbage collections. Hence, we recommend to increase the size of allocation blocks for big models.
  • --table-size specifies the size of hash tables. The performances of TChecker rely on the absence of collisions in hash table. Thus, we recommend to increase the size of hash tables for big models.
Clone this wiki locally