Implementing a reachability algorithm using TChecker libraries

Coding a reachability algorithm using TChecker libraries

Foreword: this version of the tutorial is for TChecker v0.6 and above. In case you want to use previous versions of TChecker, please refer to the tutorial up to v0.2. Notice that this tutorial is kept up-to-date with the latest version of TChecker (unless we forgot to!) so it may not compile with version older than the current one.

This tutorial shows how to use TChecker libraries to program a standard reachability algorithm for transition systems.

• Coding a reachability algorithm using TChecker libraries
  • The reachability algorithm
  • Before we start
  • Parsing TChecker input files
  • Building a zone graph from a system declaration
  • Transition systems
  • Implementation of the reachability algorithm
  • Adding predicate P for reachability checking
  • Building a (un-)reachability certificate
    • Abstract waiting containers
    • The reachability graph
    • Building the graph during reachability analysis
    • Outputting the reachability graph
  • Backward reachability

The reachability algorithm

Assume that s0 is the initial state of the transition system, and for each state s, succ(s) is the set of successors of state s. Finally, we assume a predicate P on states. The following algorithm decides if a finite transition system defined by s0 and succ can reach a state s such that P(s) is true.

push s0 on the stack
add s0 to the set of visited states
while (the stack is not empty) do
  let s be the top state on the stack
  pop the stack
  if P(s)
    return "P is satisfied"
  for each successor s' in succ(s) do
    if (s' is not in the set of visited states)
      push s' on the stack
      add s' to the set of visited states
    end
  end
end
return "P is not satisfied"

The goal of this tutorial is to implement the algorithm above using TChecker librairies. The transition system that we consider is a finitely abstracted zone graph of a timed automaton A. The states of this transition system are of the form (q,v,Z) for a state q of A, a valuation v of bounded integer variables and a zone Z of clock valuations. The predicate P checks if a node is accepting in A. In a first step we implement the algorithm above that checks for reachability of a state s that satisfies P. In a second step, we improve our implementation to output a certificate of (un-)reachability.

Before we start

You first need to install TChecker. To that purpose, clone the repository and follow the installation instructions.

The archive reachability-tutorial-v0.6.tar.gz contains the source files of the tutorial (in directory src). The file src/reach.cc is identical to src/reach-0.src and is the starting point of the tutorial. You can choose to update src/reach.cc to follow the steps of the tutorial, or simply look at the successive versions of the code in src/reach-0.cc, src/reach-1.cc, etc.

The project is built by entering directory build and running cmake ../src -DTCHECKER_PATH=??? where ??? should be replaced by the path to the directory where TChecker has been installed. You may need to specify extra options to cmake. In particular you may need to set CMAKE_PREFIX_PATH to help cmake find the right version of the compilation tools. Once cmake has succeeded, you can run command make from directory build. This will produce an executable for each source file.

The executable programs expects a file name as a parameter. Several TChecker example are provided in the archive: acyclic.tck, csmacd2.tck and csmacd5.tck. From directory build, run the program ./reach ../acyclic.tck. It should display the content of the file acyclic.tck.

Minor updates from the v0.3 tutorial are pointed out below

Parsing TChecker input files

The program reach.cc (shown below) parses its input file and checks that it contains a valid TChecker model. It builds a memory representation of the declarations in the file. The declarations are then output following the TChecker file format.

The program uses the parsing function tchecker::parsing::parse_system_declaration(filename) that reads the file at filename and parses it. The file should follow the TChecker file format. Any error or warning is reported to standard error output stream std::cerr. Outputting tchecker::log_error results in displaying an error header, as well as increasing the error counter. The function tchecker::log_error_count() allows to know how many errors have occurred, in particular when a file is parsed.

On success, the parsing function returns a pointer to a system declaration of type tchecker::parsing::system_declaration_t. This system declaration contains the list of all the declarations in the input file. Thus, the variable sysdecl is simply a memory representation of the input file. Then, the output operator << is used to display the system declaration on the standard output following the TChecker file format.

#include <iostream>

#include "tchecker/parsing/parsing.hh"
#include "tchecker/utils/log.hh"

int main(int argc, char * argv[])
{
  if (argc != 2) {
    std::cerr << "Usage: " << argv[0] << " filename " << std::endl;
    return 1;
  }

  tchecker::parsing::system_declaration_t const * sysdecl = nullptr;
  try {
    sysdecl = tchecker::parsing::parse_system_declaration(argv[1]);
    if (sysdecl == nullptr)
      throw std::runtime_error("System declaration cannot be built");
    std::cout << *sysdecl << std::endl;
  }
  catch (std::exception const & e) {
    std::cerr << tchecker::log_error << e.what() << std::endl;
  }
  delete sysdecl;

  return 0;
}

The Doxygen documentation of the TChecker API is available under you installation of TChecker in the directory share/doc/tchecker/html/index.html. All functions and classes used in this tutorial are described in the documentation.

The first version of our program displayed above is available in file src/reach-0.cc.

Building a zone graph from a system declaration

The next step is to obtain a zone graph of the timed automaton defined by the system declaration. The system declaration is a straightforward memory representation of the input file. In particular, this representation is not suitable for state-space computation algorithms. Building a suitable representation of the system involves a last step of parsing that we describe now.

TChecker models consists in a list of declarations. Some of the declarations have attributes, for instance:

edge:P:l1:l2:b{provided: y==1}

The edge declaration is parsed when the system declaration sysdecl is built. However, its list of attributes is not fully parsed: attributes are not interpreted during this phase. Attributes are meant as a way to extend the TChecker file format by providing extra information on the components in a system. There is no fixed list of attributes, and you can safely add your own attributes to any TChecker model with no impact on existing algorithms. The way attributes are interpreted depends on the transition system that is built from the system declaration. For instance, the attribute provided in the example above is interpreted as the guard of the edge. A complete list of reserved attributes is specified in TChecker input format documentation.

The attributes are parsed when a system is built from the system declaration. A system contains a representation of the input model that is suitable for state-space exploration, along with other informations required for state-space computation. For instance, in the example above, the system contains a parsed expression built from the string y==1 as well at its compilation into a bytecode that is interpreted by TChecker virtual machine during state-space computation. The first step to build a zone graph consists in building a system from the system declaration. The following definition instantiates a system that interprets the attributes of timed automata from sysdecl:

tchecker::ta::system_t system{*sysdecl};

Any error or warning due to attributes parsing is reported to the standard error output stream std::cerr.

We are now ready to build a zone graph from the system. Notice however that the zone graph keeps a shared pointer to the system. Hence, we need to slightly modify the declaration above to get a shared pointer to the system:

std::shared_ptr<tchecker::ta::system_t const> system = std::make_shared<tchecker::ta::system_t>(*sysdecl);

std::shared_ptr<tchecker::zg::zg_t>
zg{tchecker::zg::factory(system, tchecker::ts::SHARING, tchecker::zg::ELAPSED_SEMANTICS, tchecker::zg::EXTRA_LU_PLUS_LOCAL, block_size, table_size)};

This program defines a variable zg that is (a shared pointer to) the zone graph of the timed automaton in *system. There are several type of zone graphs that are parametrized by the semantcs (here ELAPSED_SEMANTICS) and the zone extrapolation used to ensure finiteness (here EXTRA_LU_PLUS_LOCAL). Please, refer to the file include/tchecker/zg/zg.hh for details. These are the standard semantics and extrapolations used in standard model-checkers for timed automata.

All the states and transitions allocated by the zone graph are automatically garbage collected. To that purpose, memory allocation is handled by pool allocators. The parameter block_size specifies the number of objects (states, transitions, etc) that are allocated in single allocation. The value of block_size is not relevant for this tutorial. In general, a higher value may lead to increased memory consumption, but greater garbage collection performance. The zone graph also makes use of internal hash table, which can be configured with parameter table_size, which sets the size of the table. Bigger values will reduce the risk of collisions at the cost of higher memory usage.

Finally, zone graphs can share states and transitions components (tuple of locations, zone, etc) to save (quite a lot of) memory. This is specified by the parameter tchecker::ts::SHARING.

From versions v0.3 to v0.5 there is no sharing_type parameter. Indeed, there was a specialized implementation of the zone graph, called tchecker::zg::sharing_zg_t which was not covered by this tutorial.

Here is the current version of our program (src/reach-1.cc from the archive):

#include <iostream>
#include <memory>

#include "tchecker/parsing/parsing.hh"
#include "tchecker/ta/system.hh"
#include "tchecker/utils/log.hh"
#include "tchecker/zg/zg.hh"

int main(int argc, char * argv[])
{
  if (argc != 2) {
    std::cerr << "Usage: " << argv[0] << " filename " << std::endl;
    return 1;
  }

  std::size_t const block_size = 10000;
  std::size_t const table_size = 65536;

  tchecker::parsing::system_declaration_t const * sysdecl = nullptr;
  try {
    sysdecl = tchecker::parsing::parse_system_declaration(argv[1]);
    if (sysdecl == nullptr)
      throw std::runtime_error("System declaration cannot be built");
    std::cout << *sysdecl << std::endl;

    std::shared_ptr<tchecker::ta::system_t const> system = std::make_shared<tchecker::ta::system_t>(*sysdecl);

    std::shared_ptr<tchecker::zg::zg_t> 
    zg{tchecker::zg::factory(system, tchecker::ts::SHARING, tchecker::zg::ELAPSED_SEMANTICS, tchecker::zg::EXTRA_LU_PLUS_LOCAL, block_size, table_size)};
  }
  catch (std::exception const & e) {
    std::cerr << tchecker::log_error << e.what() << std::endl;
  }
  delete sysdecl;

  return 0;
}

This program outputs the system declaration read from argv[1]. It also builds a zone graph, but it does not use it yet.

Transition systems

The class tchecker::zg::zg_t implements the transition system interface tchecker::ts::fwd_t in file include/tchecker/ts/fwd.hh. This interface provides several methods to perform forward reachability in the transition system. We will focus on two methods:

void initial(std::vector<sst_t> & v, tchecker::state_status_t mask);

void next(tchecker::zg::const_state_sptr_t const & s, std::vector<sst_t> & v, tchecker::state_status_t mask)

These two methods manipulate values of type tchecker::zg::zg_t::sst_t which are tuples <status, s, t> which consists in a state s, a transition t to state s and the status of state s. Both methods take a parameter mask that selects the states s which have status that match mask.

The method initial above adds all initial triples <status, s, t> to the vector v such that status matches mask. Initial transitions simulate initialisation of the state s. The method next adds to the vector v all successors <status, s', t> of state s such that status matches mask. The transition t contains informations on the transition from s to s', in particular, the set of system edges involved in the transition.

While computing the successors of a state s, the zone graph will consider all the transitions from s in the system. Some of these transitions may not be enabled from s due to bounded integer variables or due to clocks. For instance, consider the following edge in a system declaration:

edge:P:l0:l1:a{provided: i==0}

This edge is enabled from a state s0 with i=0, but disabled from a state s1 where i=1. The successor of state s0 computed by the zone graph zg will have status tchecker::STATE_OK, whereas the successor of state s1 will have status tchecker::STATE_INTVARS_GUARD_VIOLATED (see include/tchecker/basictypes.hh for a list of state status). The status of a state allows to get a diagnostic when a transition is disabled and is used by some algorithms. If the mask is set to tchecker::STATE_OK, the method next above only adds s0 to the vector v. If mask is set to tchecker::STATE_OK | tchecker::STATE_INTVARS_GUARD_VIOLATED then both s0 and s1 are added to v. We usually filter states with status tchecker::STATE_OK to only get actual initial and successor states. This is the default value.

The state and transition in triples <status, s, t> have type tchecker::zg::state_sptr_t and tchecker::zg::transition_sptr_t respectively. These are two types of shared pointers (i.e. tchecker::intrusive_shared_ptr_t<...>). Hence, all states and transitions computed by these two methods are allocated and deallocated automatically. Shared objects are alive until no other object point to them. The memory is reclamed when garbage collection occurs.

Implementation of the reachability algorithm

In order to implement the reachability algorithm presented above, we further need two containers: a list of waiting states that we need to explore, and a set of passed states that we have already explored. The waiting list will be implemented as a stack of states: std::stack<tchecker::zg::state_sptr_t> (we could as well have chosen a queue of states to implement a breadth-first state instead of a depth-first state).

The set of passed states requires more work. We will use a hash table of states as implemented by std::unordered_set. To that purpose, we need to provide two functors: one that computes the hash value of a state, and another one that checks if two states are equal. TChecker provides two functions that achieve our goals:

bool operator==(tchecker::zg::state_t const & s1, tchecker::zg::state_t const & s2);

std::size_t hash_value(tchecker::zg::state_t const & s);

We only need to encapsulate these functions into functors:

class state_sptr_hash_t {
public:
  std::size_t operator() (tchecker::zg::state_sptr_t const & s) const {
    return tchecker::zg::hash_value(*s);
  }
};

class state_sptr_equal_t {
public:
  bool operator() (tchecker::zg::state_sptr_t const & s1, tchecker::zg::state_sptr_t const & s2) const {
    return *s1 == *s2;
  }
};

We are now ready to implement our reachability algorithm:

void reach(tchecker::zg::zg_t & zg)
{
  std::stack<tchecker::zg::state_sptr_t> waiting;
  std::unordered_set<tchecker::zg::state_sptr_t, state_sptr_hash_t, state_sptr_equal_t> passed;
  std::vector<tchecker::zg::zg_t::sst_t> v;

  zg.initial(v);
  for (auto && [status, s, t] : v) {
    waiting.push(s);
    passed.insert(s);
  }
  v.clear();

  while (! waiting.empty()) {
    tchecker::zg::const_state_sptr_t s{waiting.top()};
    waiting.pop();

    zg.next(s, v);
    for (auto && [status, next_s, t] : v) {
      if (passed.find(next_s) == passed.end()) {
        waiting.push(next_s);
        passed.insert(next_s);
      }
    }
    v.clear();
  }
}

In the main function, we simply call the function reach. Notice that the function reach explores the entire state-space of the timed automaton. In the next section, we extend this function with reachability checking. The current version of our program is available in the file src/reach-2.cc from the archive.

NB: we could make our functors state_sptr_hash_t and state_sptr_equal_t more efficient. Indeed, we built our zone graph zg with sharing type tchecker::ts::SHARING. Hence, we could use function tchecker::zg::shared_equal_to instead of operator== and function tchecker::zg::shared_hash_value instead of function tchecker::zg::hash_value. These two functions compare pointers instead of pointed values, which is valid as each value (tuple of locations, zone, etc) is uniquely represented in memory with sharing type tchecker::ts::SHARING.

Adding predicate P for reachability checking

The standard way to specify reachability properties in TChecker is to label locations (using the attribute labels: in the system declaration), and to check for reachability of a state with a given set of labels. For instance, the declaration:

location:P:l2{labels: accepting}

defines a location l2 in process P that is labeled by accepting. The reachability checking algorithm will return true if we search for label accepting, and l2 is reachable.

In v0.3, the zone graph tchecker::zg::zg_t provides method:

bool satisfies(tchecker::zg::const_state_sptr_t const & s, boost::dynamic_bitset<> const & labels);

that checks if a state s satisfies a set of labels, i.e. if all labels appear in the locations in s. This method has been DEPRECATED

From v0.4, the class tchecker::zg::zg_t provides methods:

boost::dynamic_bitset<> labels(tchecker::zg::const_state_sptr_t const & s) const;
bool is_valid_final(tchecker::zg::const_state_sptr_t const & s) const;

that respectively: return the set of labels of state s, and check if state s is a valid final state. These two methods are defined in the interface tchecker::ts::inspector_t which is implemented by tchecker::zg::zg_t.

So, we define a function accepting that tells if a state s is accepting. We then use function accepting in our function reach to detect accepting states. Observe that we choose to interpret an empty set labels as non-accepting.

bool accepting(tchecker::zg::const_state_sptr_t const & s, tchecker::zg::zg_t const & zg,
               boost::dynamic_bitset<> const & labels)
{
  return !labels.none() && labels.is_subset_of(zg.labels(s)) && zg.is_valid_final(s);
}

bool reach(tchecker::zg::zg_t & zg, boost::dynamic_bitset<> const & labels)
{
  std::stack<tchecker::zg::state_sptr_t> waiting;
  std::unordered_set<tchecker::zg::state_sptr_t, state_sptr_hash_t, state_sptr_equal_t> passed;
  std::vector<tchecker::zg::zg_t::sst_t> v;

  zg.initial(v);
  for (auto && [status, s, t] : v) {
    waiting.push(s);
    passed.insert(s);
  }
  v.clear();

  while (! waiting.empty()) {
    tchecker::zg::const_state_sptr_t s{waiting.top()};
    waiting.pop();

    if (accepting(s, zg, labels))
      return true;

    zg.next(s, v);
    for (auto && [status, next_s, t] : v) {
      if (passed.find(next_s) == passed.end()) {
        waiting.push(next_s);
        passed.insert(next_s);
      }
    }
    v.clear();
  }

  return false;
}

Now, we modify the function main to build a set of accepting labels from a comma-separated string of labels (e.g. "a,b,c"). The class tchecker::syncprod::system_t provides a method labels that achieve this goal. We can call this method from our timed automaton system as follows:

boost::dynamic_bitset<> labels = system->as_syncprod_system().labels("accepting");

NB: all the labels in the string (as "accepting" above) must be defined in the system.

The current version of our program is available in the file src/reach-3.cc from the archive. In this file, the set of accepting labels is read from the command-line (i.e. argument argv[2]). An empty set of labels (i.e. "") leads to full state-space exploration. Calling: reach-3 on the file acyclic.tck with empty labels set "" returns Unreachable, whereas it returns Reachable with labels set "accepting".

Building a (un-)reachability certificate

So far, we have written a program that can check if a state with given set of labels is reachable in (the zone graph of) a timed automaton. We have checked that it yields the expected result on example acyclic.tck. However, it is very convenient to not only get a vedict of (un-)reachability but also a certificate. In this part, we show how to build a reachability graph that will either certify reachability (if it contains a path from the initial state to a state with all accepting labels), or unreachability (when the graph represents the entire state-space of the timed automaton and has no state with accepting labels).

Abstract waiting containers

We will also replace our waiting stack using waiting containers. While std::stack and std::queue come with incompatible interfaces, the class tchecker::waiting::waiting_t provides with an interface that abstracts the implementation of the container. To that purpose, the nodes of our graph must derive from tchecker::waiting::element_t to be stored in waiting containers.

The reachability graph

TChecker provides an implementation of a reachability graph as the class tchecker::graph::reachability::graph_t (in file include/tchecker/graph/reachability_graph.hh). We will now use this graph as a replacement for the set of passed states. To that purpose, we first need to define the type of nodes and edges in our reachability graph. A node will simply contain a state of the zone graph (a tchecker::zg::state_sptr_t). An edge will contain the set of system edges involved in the transition (a shared pointer to a vector of edges tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t const>). As for states before, we will also need to define a hash functor and an equality functor on nodes to implement our reachability graph.

Hence, nodes are defined by the class node_t as follows along with required functors that delegate the computation to the embeddded state:

class node_t : public tchecker::waiting::element_t {
public:
  node_t(tchecker::zg::state_sptr_t const & s) : _state(s) {}
  node_t(tchecker::zg::const_state_sptr_t const & s) : _state(s) {}
  tchecker::zg::const_state_sptr_t state_ptr() const { return _state; }
  tchecker::zg::state_t const & state() const { return *_state; }
private:
  tchecker::zg::const_state_sptr_t _state;
};

class node_hash_t {
public:
  std::size_t operator()(node_t const & n) const
  { 
    return hash_value(n.state());
  }
};

class node_equal_to_t {
public:
  bool operator()(node_t const & n1, node_t const & n2) const
  {
    return n1.state() == n2.state();
  }
};

The edges are defined by the class edge_t as follows. The edge is built from a transition of the zone graph. It keeps a shared pointer on the tuple of system edges involved in the transition:

class edge_t {
public:
  edge_t(tchecker::zg::transition_t const & t) : _vedge(t.vedge_ptr()) {}
  tchecker::vedge_t const & vedge() const { return *_vedge; }
  tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t const> vedge_ptr() const { return _vedge; }
private:
  tchecker::intrusive_shared_ptr_t<tchecker::shared_vedge_t const> _vedge;
};

We can now define our reachability graph from the class tchecker::graph::reachability::graph_t as follows:

class graph_t : public tchecker::graph::reachability::graph_t<node_t, edge_t, node_hash_t, node_equal_to_t> {
public:
  graph_t(std::shared_ptr<tchecker::zg::zg_t> const & zg, std::size_t block_size, std::size_t table_size, node_hash_t & node_hash, node_equal_to_t & node_equal)
  : tchecker::graph::reachability::graph_t<node_t, edge_t, node_hash_t, node_equal_to_t>(block_size, table_size, node_hash, node_equal),
    _zg(zg)
  {}

  virtual ~graph_t()
  {
    tchecker::graph::reachability::graph_t<node_t, edge_t, node_hash_t, node_equal_to_t>::clear();
  }

  using tchecker::graph::reachability::graph_t<node_t, edge_t, node_hash_t, node_equal_to_t>::attributes;

protected:
  virtual void attributes(node_t const & n, std::map<std::string, std::string> & m) const
  {
    _zg->attributes(n.state_ptr(), m);
  }

  virtual void attributes(edge_t const & e, std::map<std::string, std::string> & m) const
  {
    m["vedge"] = tchecker::to_string(e.vedge(), _zg->system().as_system_system());
  }

private:
  std::shared_ptr<tchecker::zg::zg_t> _zg;
};

The class tchecker::graph::reachability:;graph_t is an abstract class that leaves the two protected methods attributes undefined. These methods are used to output the graph. They shall add to the map m the list of attributes of nodes and edges respectively. Our class graph_t provides an implementation of these two methods in adequation with our nodes and edges. Our graph stores a shared pointer to the zone graph that is used by the methods attributes.

The parameters block_size and table_size of the constructor play the same role as before. They determine the size of allocation blocks, and the size of hash tables respectively.

The parameters node_hash and node_equal are a hash functor and a node equality predicate that are passed to the graph to detect equal nodes.

Our graph allocates and stores nodes and edges. All allocated nodes and edges are deallocated automatically. Notice that the destructor of the graph needs to clear the graph to remove all nodes and edges from containers before they are deallocated.

Building the graph during reachability analysis

We now need to update the function reach so that it builds the reachability graph while it performs reachability analysis:

std::tuple<bool, std::shared_ptr<graph_t>> 
reach(std::shared_ptr<tchecker::zg::zg_t> const & zg, boost::dynamic_bitset<> const & labels, std::size_t block_size, std::size_t table_size)
{
  using node_sptr_t = graph_t::node_sptr_t;
  using waiting_t = tchecker::waiting::waiting_t<node_sptr_t>;

  std::unique_ptr<waiting_t> waiting{tchecker::waiting::factory<node_sptr_t>(tchecker::waiting::STACK)};
  std::shared_ptr<graph_t> graph{new graph_t{zg, block_size, table_size}};

  std::vector<tchecker::zg::zg_t::sst_t> v;
  bool reachable = false;

  zg->initial(v);
  for (auto && [status, s, t] : v) {
    auto && [is_new_node, initial_node] = graph->add_node(s);
    if (is_new_node)
      waiting->insert(initial_node);
  }
  v.clear();

  while (! waiting->empty()) {
    node_sptr_t node = waiting->first();
    waiting->remove_first();

    if (accepting(node->state_ptr(), *zg, labels)) {
      reachable = true;
      break;
    }

    zg->next(node->state_ptr(), v);
    for (auto && [status, s, t] : v) {
      auto && [is_new_node, next_node] = graph->add_node(s);
      if (is_new_node)
        waiting->insert(next_node);
      graph->add_edge(node, next_node, *t);
    }
    v.clear();
  }

  return std::make_tuple(reachable, graph);
}

First observe that the function reach now returns a boolean that tells if the accepting state (according to labels) is reachable or not, as well as the reachability graph. Once again, we choosed to build a waiting stack but we could run a breadth-first search instead if a depth-first search by replacing tchecker::waiting::STACK by tchecker::waiting::QUEUE.

Notice that the class tchecker::graph::reachability::graph_t provides a method add_node that either returns the node in the graph that already stores state s if any, or that creates a new node that stores state s if no such node already exist in the graph. The flag is_new_node allows to differentiate the two behaviors: is_new_node is true when the node has juste been created, whereas it is false if the node already exists. The graph uses the two functors node_hash_t and node_equal_to_t to identify identical nodes.

Observe that we create a new edge in the graph for each transition t in the zone graph.

Outputting the reachability graph

Finally, in the function main, we need to output the reachability graph as a certificate of (un-)reachability of the accepting labels. To that purpose, TChecker provides the function tchecker::graph::dot_output:

template <class GRAPH, class NODE_LE, class EDGE_LE>
std::ostream & dot_output(std::ostream & os, GRAPH const & g, std::string const & name);

This function outputs a graph g to an output stream os following the graphviz DOT file format. It is parametrized by two functors: a total order on nodes, and a total order on edges, that are used to ensure that nodes and edges are always output in the same order. TChecker provides lexical comparator functions lexical_cmp for most types. We just need to encapsulate the functions calls in functors as follows:

class node_lexical_less_t {
public:
  bool operator()(graph_t::node_sptr_t const & n1,
                  graph_t::node_sptr_t const & n2) const
  {
    return tchecker::zg::lexical_cmp(n1->state(), n2->state()) < 0;
  }
};

class edge_lexical_less_t {
public:
  bool operator()(graph_t::edge_sptr_t const & e1,
                  graph_t::edge_sptr_t const & e2) const
  {
    return tchecker::lexical_cmp(e1->vedge(), e2->vedge()) < 0;
  }
};

Finally, we output the graph in the function main:

auto && [is_reachable, graph] = reach(zg, labels, block_size, table_size);

if (is_reachable)
  std::cout << "Reachable" << std::endl;
else
  std::cout << "Unreachable" << std::endl;

tchecker::graph::dot_output<graph_t, node_lexical_less_t, edge_lexical_less_t>(std::cout, *graph, "reachability_graph");

The full program is available in src/reach-4.cc from the archive. TChecker provides its own implementation of the reachability algorithm. We refer the reader to files include/tchecker/algorithms/reach/algorithm.hh, src/tck-reach/zg-reach.hh and src/tck-reach/zg-reach.cc for details.

Backward reachability

From version v0.6, TChecker provides backward state-space computation. The corresponding interface is defined in the file include/tchecker/ts/bwd.hh. The class tchecker::zg::zg_t implements this interface and allows to do backward state-space computation on the zone graph.

Our goal is to implement the following algorithm in TChecker, where F is a set of final states, and prev(s) returns the set of predecessor states of s in the transition system.

push every state in F on the stack
add all states in F in the set of visited states
while (the stack is not empty) do
  let s be the top state on the stack
  pop the stack
  if s is an initial state:
    return "final states are reachable"
  for each predecessor s' in prev(s) do
    if (s' is not in the set of visited states)
      push s' on the stack
      add s' to the set of visited states
    end
  end
end
return "final states are not reachable"

The code below is an implementation of the algorithm above using TChecker libraries. It performs a backward state-space exploration from a set of final states identified through a set of labels. As before, labels can be specified in TChecker input files using attribute labels: on states.

To keep the code simple, we use a stack for the set of waiting states, and an unordered set for the set of passed states. Exploration relies on two methods: tchecker::zg::zg_t::final and tchecker::zg::zg_t::prev that return the set of final states (according to labels) and the set of predecessor states in a zone graph. These methods are provided by the interface tchecker::ts::bwd.hh.

The algorithm terminates either when all the state-space has been visited, or when an initial state has been found. To that purpose, we use the method tchecker::zg::zg_t::is_initial.

bool bwd_reach(tchecker::zg::zg_t & zg, boost::dynamic_bitset<> const & labels)
{
  std::stack<tchecker::zg::state_sptr_t> waiting;
  std::unordered_set<tchecker::zg::state_sptr_t, state_sptr_hash_t, state_sptr_equal_t> passed;
  std::vector<tchecker::zg::zg_t::sst_t> v;

  zg.final(labels, v);
  for (auto && [status, s, t] : v) {
    waiting.push(s);
    passed.insert(s);
  }
  v.clear();

  while (! waiting.empty()) {
    tchecker::zg::const_state_sptr_t s{waiting.top()};
    waiting.pop();

    if (zg.is_initial(s))
        return true;

    zg.prev(s, v);
    for (auto && [status, prev_s, t] : v) {
      if (passed.find(prev_s) == passed.end()) {
        waiting.push(prev_s);
        passed.insert(prev_s);
      }
    }
    v.clear();
  }

  return false;
}

The full program is available in the file reach-b.cc. The set of final labels is computed from a comma-separated list of string using method
tchecker::ta::system_t::labels. Parsing and zone graph instantiation are performed as before. Notice that we do not need extrapolation to ensure termination of the algorithm.

As before, we can extend this program to build a certificate or (un)reachability, as a (backward) reachability graph. We leave this extension as an exercise for the reader.

Forward exploration of the state-space should be preferred over backward computation when possible. Indeed backward exploration is significantly more expensive. The computation of final states and previous states require to enumerate (almost) all possible discrete states of the automaton. The number of discrete states is exponential in the number of locations, the number of processes, and the domain of bounded integer variables.