-
Notifications
You must be signed in to change notification settings - Fork 17
Implementing a reachability algorithm using TChecker libraries v0.2
This tutorial shows how to use TChecker libraries to program a standard reachability algorithm for transition systems. 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 in TChecker. 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 is a node is accepting in A. In a first step we implement a simplified version of the algorithm without visited states. This algorithm terminates on acyclic timed automata. In a second step, we introduce memory management paradigms and implement the full algorithm. Then, we extend our implementation to output a certificate of (un-)satisfaction of P by A.
You first need to install TChecker. To that purpose, clone the repository and follow the installation instructions. Unfortunately current binary releases are not compatible with this tutorial.
The archive 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.txt, csmacd2.txt and
csmacd5.txt. Notice that the first implementations of the reachability
algorithm will only terminate on acyclic.txt but not on the two other files.
Moreover, the reachability check on csmacd5.txt takes a long time as the zone
graph for this example is very large. From directory build, run the program
./reach ../acyclic.txt. It should display the content of the file
acyclic.txt.
The program reach.cc (shown below) reads and parses its input file assuming 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. It uses two features from TChecker. The logging facility log of type tchecker::log_t is used to report errors and warnings by TChecker functions. Here, log has been built to report any message to the standard error file std::cerr. The program also uses the parsing function tchecker::parsing::parse_system_declaration(filename, log) that reads the file at filename and parse it. The file should follow the TChecker file format. Any error or warning is reported using log.
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::log_t log(&std::cerr);
tchecker::parsing::system_declaration_t const * sysdecl = nullptr;
try {
sysdecl = tchecker::parsing::parse_system_declaration(argv[1], log);
if (sysdecl == nullptr)
throw std::runtime_error("System declaration cannot be built");
std::cout << *sysdecl << std::endl;
}
catch (std::exception const & e) {
log.error(e.what());
}
delete sysdecl;
return 0;
}The Doxygen documentation of the TChecker API is available under you installation of TChecker in 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.
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 model is built from the system declaration. A model contains a representation of the system that is suitable for state-space computation, along with other informations required for state-space generation. For instance, in the example above, the model contains a parsed expression built from the string y==1 as well at its compilation into a bytecode that is interpreted by TChecker's virtual machine during state-space generation. The first step to build a zone graph consists in building a model from the system declaration. The following definition instantiates a model for a zone graph of a timed automaton from sysdecl. Any error or warning dues to attributes parsing is reported using log:
tchecker::zg::ta::model_t model(*sysdecl, log);We are now ready to build a zone graph from the model:
using zone_graph_t = tchecker::zg::ta::elapsed_extraLUplus_local_t;
zone_graph_t::ts_t ts(model);This program defines a variable ts which is a zone graph of the timed automaton defined in model. Several types of zone graphs are defined in the header file tchecker/zg/zg_ta.hh. Here, we choose to build a zone graph of type tchecker::zg::ta::elapsed_extraLUplus_local_t which is the state-of-the-art approach for timed automata reachability. We introduce the short name zone_graph_t to increase code readability.
TChecker introduces several interfaces to the zone graph. Here, we choose the transition system interface: zone_graph_t::ts_t (see also tchecker::zg::ts_t) which is the most convenient for implementing the reachability algorithm. TChecker also implements a low-level interface to zone graphs which is not discussed here (see tchecker::zg::zg_t for details). Here is the current version of our program:
#include <iostream>
#include "tchecker/parsing/parsing.hh"
#include "tchecker/utils/log.hh"
#include "tchecker/zg/zg_ta.hh"
int main(int argc, char * argv[])
{
if (argc != 2) {
std::cerr << "Usage: " << argv[0] << " filename " << std::endl;
return 1;
}
tchecker::log_t log(&std::cerr);
tchecker::parsing::system_declaration_t const * sysdecl = nullptr;
try {
sysdecl = tchecker::parsing::parse_system_declaration(argv[1], log);
if (sysdecl == nullptr)
throw std::runtime_error("System declaration cannot be built");
tchecker::zg::ta::model_t model(*sysdecl, log);
using zone_graph_t = tchecker::zg::ta::elapsed_extraLUplus_local_t;
zone_graph_t::ts_t ts(model);
std::cout << *sysdecl << std::endl;
}
catch (std::exception const & e) {
log.error(e.what());
}
delete sysdecl;
return 0;
}This program is available in file src/reach-1.cc.
The class for transition systems tchecker::ts::ts_t (file tchecker/ts/ts.hh) has four main methods:
tchecker::range_t<INITIAL_ITERATOR> initial();
enum tchecker::state_status_t initialize(STATE & s, TRANSITION & t, INITIAL_ITERATOR_VALUE const & v);
tchecker::range_t<OUTGOING_EDGES_ITERATOR> outgoing_edges(STATE const & s);
enum tchecker::state_status_t next(STATE & s, TRANSITION & t, OUTGOING_EDGES_ITERATOR_VALUE const & v);Capitalized names indicate template parameters to the class tchecker::ts::ts_t. There are two main parameters: STATE, the type of states, and TRANSITION, the type of transitions. There are two types of transitions in the class tchecker::ts::ts_t. Transitions of type TRANSITION are user-defined and are made available to the caller of the methods above. Depending on the type of transition system, the class TRANSITION provides access to the guard of the transitions, the clocks reset on the transition, etc. The class tchecker::ts::ts_t also manipulates transitions of type INITIAL_ITERATOR_VALUE and OUTGOING_EDGES_ITERATOR_VALUE. These two types are internal to TChecker and are not meant to be used, except as parameters of the methods above.
The method initial returns a range (a pair of iterators) of initial edges. And the method outgoing_edges returns a range of outgoing edges of a state s. Then, the method initialize computes a state s and an initial transition t from v. And the method next applies v on a state s (i.e. s becomes its successor along v) and it computes a transition t from v.
The exact content of states and transitions depends on the kind of transition system under consideration. In our example, a state of a zone graph (see tchecker::ta::zg::state_t) consists in a tuple of locations (one location for each process), a valuation of bounded integer variables, and a zone of clock valuations. Transitions (see tchecker::ta::zg::transition_t) provide access to the source state invariant, the target state invariant, the guard of the edge and the clocks reset on the edge.
The methods initialize and next return the status of state s after computation. The returned value is tchecker::STATE_OK when the state and the transition have been computed. Several errors may occur. For instance, the return value STATE_CLOCKS_GUARD_VIOLATED means that the transition from state s cannot be taken because its guard is not satisfied by any valuation in the zone of s. The possible return values are described in file tchecker/basictypes.hh.
The methods of the transition system interface tchecker::ts::ts_t do not allocate memory. They take pre-allocated states and transitions as inputs, and set their values according to the edge v. States and transitions must be allocated by the caller. TChecker provides state and transition allocators.
The reachability algorithm allocates and stores a lot of states. We will thus use a pool allocator that allocates block of states in a single allocation. The algorithm does not store any transition. Thus, we will use a singleton allocator for transitions. The class
tchecker::zg::ta::elapsed_extraLUplus_local_t not only defines a type of transition system ts_t, but also many related types, like the type of states state_t, the type of transitions transition_t, and types of allocators for states and transitions state_pool_allocator_t and transition_singleton_allocator_t. We introduce new type aliases for readablity:
using shared_state_t = zone_graph_t::shared_state_t;
using transition_t = zone_graph_t::transition_t;
using state_allocator_t = zone_graph_t::state_pool_allocator_t<shared_state_t>;
using transition_allocator_t = zone_graph_t::transition_singleton_allocator_t<transition_t>;TChecker pool allocators return objects (states, etc) equipped with a reference counter. For example, zone_graph_t::shared_state_t is a state of type zone_graph_t::state_tequipped with a reference counter. The reference counter is used for garbage collection. TChecker implements a garbage collector (see class tchecker::gc_t) that continuously scans the memory and releases the objects that are not referenced anymore. The garbage collector is simply created by:
tchecker::gc_t gc;We will later see that the class tchecker::gc_t has two methods start() and stop() to activate and deactivate garbage collection. But we should first instantiate the allocators of states and transitions. To that purprose, we build a transition system allocator:
using allocator_t = tchecker::ts::allocator_t<state_allocator_t, transition_allocator_t>;
allocator_t allocator(gc, std::make_tuple(model, 100000), std::tuple());Our allocator can allocate states (using a state_allocator_t instance) and transitions (using a transition_allocator_t instance). The first parameter gc is the garbage collector. It will be used to collect the memory allocated by allocator. The second parameter std::make_tuple(model, 100000) is a tuple of values used to construct the state allocator: the model, and the size of an allocation block of states, here 100000. The third parameter std::tuple() is a tuple of values used to construct the transition allocator (nothing here).
We can now review the new version of our program:
#include <iostream>
#include "tchecker/parsing/parsing.hh"
#include "tchecker/ts/allocators.hh"
#include "tchecker/utils/gc.hh"
#include "tchecker/utils/log.hh"
#include "tchecker/zg/zg_ta.hh"
int main(int argc, char * argv[])
{
if (argc != 2) {
std::cerr << "Usage: " << argv[0] << " filename " << std::endl;
return 1;
}
tchecker::log_t log(&std::cerr);
tchecker::parsing::system_declaration_t const * sysdecl = nullptr;
try {
sysdecl = tchecker::parsing::parse_system_declaration(argv[1], log);
if (sysdecl == nullptr)
throw std::runtime_error("System declaration cannot be built");
tchecker::zg::ta::model_t model(*sysdecl, log);
using zone_graph_t = tchecker::zg::ta::elapsed_extraLUplus_local_t;
zone_graph_t::ts_t ts(model);
using state_t = zone_graph_t::shared_state_t;
using transition_t = zone_graph_t::transition_t;
using state_allocator_t = zone_graph_t::state_pool_allocator_t<state_t>;
using transition_allocator_t = zone_graph_t::transition_singleton_allocator_t<transition_t>;
tchecker::gc_t gc;
using allocator_t = tchecker::ts::allocator_t<state_allocator_t, transition_allocator_t>;
allocator_t allocator(gc, std::make_tuple(model, 100000), std::tuple());
gc.start();
gc.stop();
std::cout << *sysdecl << std::endl;
}
catch (std::exception const & e) {
log.error(e.what());
}
delete sysdecl;
return 0;
}The call to gc.start() starts garbage collection for all allocators which are registered with gc (here, allocator). This starts a separate thread of execution that continuously scans the memory and that frees the objects that are not used anymore. When gc.stop() is called, the garbage collection thread is stopped.
The program above is available in file src/reach-2.cc.
To simplify, we first consider the case of acyclic timed automata: termination of the reachability algorithm is guaranteed without storing visited nodes. Our goal is to use the zone graph transition system ts and the states/transitions allocator to generates states. There is one last problem to solve before we an implement a first version of the algorithm. The methods initialize and next of the transition system ts may fail to compute the initial/next state. This is for instance the case when a transition is not fireable from a state. In order to avoid dealing with uncomputable states, TChecker implements the transition system builder tchecker::ts::builder_ok_t that only returns computable states (i.e. with status tchecker::STATE_OK). The class tchecker::ts::builder_ok_t comes with two main methods:
tchecker::range_t<tchecker::ts::builder_ok_t<TS, ALLOCATOR>::initial_iterator_t> initial();
tchecker::range_t<tchecker::ts::builder_ok_t<TS, ALLOCATOR>::outgoing_iterator_t> outgoing(state_ptr_t & s);The method initial returns a range (pair of iterators) of pairs (initial transition, initial state). The method outgoing returns the range of pairs (successor state, outgoing transition) of state s. The builder is simply built from the transition system and the allocator:
using builder_t = tchecker::ts::builder_ok_t<zone_graph_t::ts_t, allocator_t>;
builder_t builder(ts, allocator);To summarize, the main differences between builder and ts is that (1) builder allocates states and transitions, whereas ts does not allocate memory, and (2) builder only returns pairs of (transition, states) that are fireable (i.e. state has status tchecker::STATE_OK), whereas ts gives access to all the transitions, even those which are not fireable.
We are now ready to write a first version of the reachability algorithm (without visited states):
template <class TS, class ALLOCATOR>
void reachable(TS & ts, ALLOCATOR & allocator)
{
using builder_t = tchecker::ts::builder_ok_t<TS, ALLOCATOR>;
using state_ptr_t = typename builder_t::state_ptr_t;
using transition_ptr_t = typename builder_t::transition_ptr_t;
builder_t builder(ts, allocator);
std::stack<state_ptr_t> stack;
state_ptr_t state, next_state;
transition_ptr_t transition;
auto initial_range = builder.initial();
for (auto it = initial_range.begin(); ! it.at_end(); ++it) {
std::tie(state, transition) = *it;
stack.push(state);
}
while ( ! stack.empty() ) {
state = stack.top();
stack.pop();
auto outgoing_range = builder.outgoing(state);
for (auto it = outgoing_range.begin(); ! it.at_end(); ++it) {
std::tie(next_state, transition) = *it;
stack.push(next_state);
}
}
}This function is a direct translation of the algorithm where we ignore visited states and the predicate P. In the function main, we call reachable between the calls to gc.start() and gc.stop():
...
gc.start();
reachable(ts, allocator);
gc.stop();
...The full program is available in file src/reach-3.cc.
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.
We first add a definition of predicate P:
class P_t {
public:
P_t(tchecker::label_index_t const & index, std::string const & label)
{
try {
_label_id = index.key(label);
}
catch (...) {
_label_id = index.size() + 1;
}
}
template <class STATE_PTR>
bool operator() (STATE_PTR const & state)
{
for (auto const * loc : state->vloc())
for (tchecker::label_id_t id : loc->labels())
if (id == _label_id)
return true;
return false;
}
private:
tchecker::label_id_t _label_id;
};TChecker models contain an index of the labels defined in the system specification (all names appearing to the right of a labels: attribute). The predicate take a label index as a parameter, as well as label for which we check reachability. Then, it computes and stores in _label_id the index of label or a value corresponding to no label if label is not defined in the system declaration. The predicate defined by operator() checks if state is labelled by label. Recall that a state contains one location for each process in the system declaration. Hence, operator() ranges over all locations in the state, and all labels in the locations to check if state is labelled by label.
Now, we can modify the reachable function to stop as soon as a state satisfying predicate P is reached:
template <class TS, class ALLOCATOR, class PREDICATE>
bool reachable(TS & ts, ALLOCATOR & allocator, PREDICATE P)
{
using builder_t = tchecker::ts::builder_ok_t<TS, ALLOCATOR>;
using state_ptr_t = typename builder_t::state_ptr_t;
using transition_ptr_t = typename builder_t::transition_ptr_t;
builder_t builder(ts, allocator);
std::stack<state_ptr_t> stack;
state_ptr_t state, next_state;
transition_ptr_t transition;
auto initial_range = builder.initial();
for (auto it = initial_range.begin(); ! it.at_end(); ++it) {
std::tie(state, transition) = *it;
stack.push(state);
}
while ( ! stack.empty() ) {
state = stack.top();
stack.pop();
if (P(state))
return true;
auto outgoing_range = builder.outgoing(state);
for (auto it = outgoing_range.begin(); ! it.at_end(); ++it) {
std::tie(next_state, transition) = *it;
stack.push(next_state);
}
}
return false;
}The function reachable now takes an extra parameter P: the predicate to check. It returns a boolean value: true if a state satisfying P is reachable, false otherwise.
Finally, it remains to instantiate the class P_t in function main and pass it to function reachable. We modify the function main to make it accept two parameters on the command line: the file name, and the label to check. Then, before calling reachable, we build a predicate P of type P_t using the label index in model. We finally display the outcome of function reachable.
int main(int argc, char * argv[])
{
if (argc != 3) {
std::cerr << "Usage: " << argv[0] << " filename label" << std::endl;
return 1;
}
tchecker::log_t log(&std::cerr);
tchecker::parsing::system_declaration_t const * sysdecl = nullptr;
try {
sysdecl = tchecker::parsing::parse_system_declaration(argv[1], log);
if (sysdecl == nullptr)
throw std::runtime_error("System declaration cannot be built");
tchecker::zg::ta::model_t model(*sysdecl, log);
using zone_graph_t = tchecker::zg::ta::elapsed_extraLUplus_local_t;
zone_graph_t::ts_t ts(model);
using state_t = zone_graph_t::shared_state_t;
using transition_t = zone_graph_t::transition_t;
using state_allocator_t = zone_graph_t::state_pool_allocator_t<state_t>;
using transition_allocator_t = zone_graph_t::transition_singleton_allocator_t<transition_t>;
tchecker::gc_t gc;
using allocator_t = tchecker::ts::allocator_t<state_allocator_t, transition_allocator_t>;
allocator_t allocator(gc, std::make_tuple(model, 100000), std::tuple());
gc.start();
std::string label = argv[2];
P_t P(model.system().labels(), label);
if (reachable(ts, allocator, P))
std::cout << label << " is reachable" << std::endl;
else
std::cout << label << " is not reachable" << std::endl;
gc.stop();
}
catch (std::exception const & e) {
log.error(e.what());
}
delete sysdecl;
return 0;
}The full program is available in file src/reach-4.cc.
Our goal to to improve our implementation to ensure termination for all timed automata, not only acyclic ones. This requires to store the set of visited states.
A trivial solution to this problem is to use a standard implementation of sets, for instance std::unordered_set, to define a set of states in function reachable (with adequate parameters):
std::unordered_set<state_ptr_t> visited_states(...);Then, every time a state is generated, we first check if the state belongs to visited_states. If no, the state is pushed on stack and added to visited_states, if yes the state is ignored.
However, this solution is not satisfying since we are left with two objects: allocator and visited_states that share addresses in memory (pointers to states). In particular, we must ensure that the lifetime of allocator exceeds the lifetime of visited_states. Moreover, this solution does not scale well to more complex situations: for instance, if we want to build a reachability graph instead of only storing visited nodes.
So, we take another approach that consists in building a graph that encapsulates both the states allocator and the set of visited states. All the constraints concerning states lifetime management will be handled by the graph. To that purpose, we first define convenient type aliases:
using zone_graph_t = tchecker::zg::ta::elapsed_extraLUplus_local_t;
using state_t = zone_graph_t::shared_state_t;
using transition_t = zone_graph_t::transition_t;
using node_t = state_t;
using node_ptr_t = tchecker::intrusive_shared_ptr_t<node_t>;
using delegate_hash_t = tchecker::intrusive_shared_ptr_delegate_hash_t;
using delegate_equal_to_t = tchecker::intrusive_shared_ptr_delegate_equal_to_t;
using node_allocator_t = zone_graph_t::state_pool_allocator_t<node_t>;
using transition_allocator_t = zone_graph_t::transition_singleton_allocator_t<transition_t>;
using allocator_t = tchecker::ts::allocator_t<node_allocator_t, transition_allocator_t>;The novelty is that we have introduced a new type node_t. In TChecker, we make the following difference between states and nodes. States come from transition systems and only contain information that is relevant to the transition system. Then TChecker algorithms traverse transitions systems and build graphs to store relevant information, for instance reachable nodes, or a reachability graph. The nodes of the graph derives from states. They usually store extra informations along with the states, that are needed by the algorithms. As an example, our reachability algorithm builds the set of visited nodes (which is a graph). It could also build a reachability graph over the transition system (see later). We make a similar distinction between transition (from transition systems) and edges (from graphs).
Since the reachability algorithm does not need to store extra information along with states, the type node_t defined above is simply an alias for the type of states of the zone graph state_t. We then introduce the type node_ptr_t which corresponds to shared pointer on node_t using reference counters to track unused nodes.
The types delegate_hash_t and delegate_equal_to_t introduce hash function and equality predicate over shared pointers that respectively computes the hash code, and checks equality of objects pointed by shared objects. They will be used to implement the set of visited nodes.
Finally, the allocator type aliases are as before except that states have been renamed as nodes. Notice that state allocators can be used to allocate nodes, even in the case where nodes extends states.
We are now ready to introduce our graph:
class graph_t
: public tchecker::graph::find_graph_t<node_ptr_t, delegate_hash_t, delegate_equal_to_t>
{
public:
graph_t(tchecker::gc_t & gc, tchecker::zg::ta::model_t const & model, std::size_t block_size)
: _ts_allocator(gc, std::make_tuple(model, block_size), std::tuple())
{}
graph_t(graph_t const &) = delete;
graph_t(graph_t &&) = delete;
~graph_t()
{
_ts_allocator.destruct_all();
}
graph_t & operator= (graph_t const &) = delete;
graph_t & operator= (graph_t &&) = delete;
void destruct_all()
{
tchecker::graph::find_graph_t<node_ptr_t, delegate_hash_t, delegate_equal_to_t>::clear();
_ts_allocator.destruct_all();
}
void free_all()
{
tchecker::graph::find_graph_t<node_ptr_t, delegate_hash_t, delegate_equal_to_t>::clear();
_ts_allocator.free_all();
}
allocator_t & ts_allocator()
{
return _ts_allocator;
}
private:
allocator_t _ts_allocator;
};The class graph_t derives from tchecker::graph::find_graph_t that stores nodes and that can answer membership queries. Our class graph_t also owns an instance of the transition system allocator allocator_t. As explained above, the main goal of our class graph_t is to handle memory management since nodes are stored by both the allocator and the set of visited nodes. Unsurprisingly, the only methods that are defined by the class graph_t concern memory management. They ensure that the set of visited nodes is cleared before memory is freed.
Aside from memory management, the main functionalities offered by graph_t come from two methods of the class tchecker::graph::find_graph_t:
NODE_PTR const & find(NODE_PTR const & n);
bool add_node(NODE_PTR const & n);The method find returns a pointer to a node equal to n in the graph if it exists. It returns n otherwise. The method add_node is used to add a node to the graph.
We can now use our graph in function reachable to ensure termination of the reachability algorithm:
template <class TS, class ALLOCATOR, class GRAPH, class PREDICATE>
bool reachable(TS & ts, ALLOCATOR & allocator, GRAPH & g, PREDICATE P)
{
using builder_t = tchecker::ts::builder_ok_t<TS, ALLOCATOR>;
using node_ptr_t = typename builder_t::state_ptr_t;
using transition_ptr_t = typename builder_t::transition_ptr_t;
builder_t builder(ts, allocator);
std::stack<node_ptr_t> stack;
node_ptr_t node, next_node, found_node;
transition_ptr_t transition;
auto initial_range = builder.initial();
for (auto it = initial_range.begin(); ! it.at_end(); ++it) {
std::tie(node, transition) = *it;
found_node = g.find(node);
if (found_node != node)
continue;
g.add_node(node);
stack.push(node);
}
while ( ! stack.empty() ) {
node = stack.top();
stack.pop();
if (P(node))
return true;
auto outgoing_range = builder.outgoing(node);
for (auto it = outgoing_range.begin(); ! it.at_end(); ++it) {
std::tie(next_node, transition) = *it;
found_node = g.find(next_node);
if (found_node != next_node)
continue;
g.add_node(next_node);
stack.push(next_node);
}
}
return false;
}The function reachable takes a new parameter g: the graph. Each time a node is computed, we first check if this node can be found in g. If this is the case, the new node is simply ignored. Otherwise, the new node is added to the graph, and pushed onto the stack for exploration.
Finally, the function main needs to instantiate the a graph instead of an allocator. We use the method ts_allocator of class graph_t to provide the transition system allocator of the graph to the transition system builder.
int main(int argc, char * argv[])
{
if (argc != 3) {
std::cerr << "Usage: " << argv[0] << " filename label" << std::endl;
return 1;
}
tchecker::log_t log(&std::cerr);
tchecker::parsing::system_declaration_t const * sysdecl = nullptr;
try {
sysdecl = tchecker::parsing::parse_system_declaration(argv[1], log);
if (sysdecl == nullptr)
throw std::runtime_error("System declaration cannot be built");
tchecker::zg::ta::model_t model(*sysdecl, log);
zone_graph_t::ts_t ts(model);
tchecker::gc_t gc;
graph_t graph(gc, model, 100000);
gc.start();
std::string label = argv[2];
P_t P(model.system().labels(), label);
if (reachable(ts, graph.ts_allocator(), graph, P))
std::cout << label << " is reachable" << std::endl;
else
std::cout << label << " is not reachable" << std::endl;
gc.stop();
}
catch (std::exception const & e) {
log.error(e.what());
}
delete sysdecl;
return 0;
}The full program is available in src/reach-5.cc
Finally, we want to produce a certificate of (un-)reachability in the form of a reachability graph. The graph will contain a path from a root node to a node labelled by label when label is reachable. Otherwise, the graph will contain all the reachable nodes and edges between them. First, we extend our graph in order to store edges. Second, we modify the reachability algorithm to build the edges of the graph. Finally, the third step consists in outputting the graph that has been computed by function reachable.
The class tchecker::graph::directed::graph_t defines a graph that is capable of storing edges. It provides methods to add and remove edges, as well as methods to access the incoming and outgoing edges of a node. It does not store nodes, so we will use it in combination with tchecker::graph::find_graph_t to store the nodes and retrieve them. The directed graph tchecker::graph::directed::graph_t also introduces a type of edges which allow to access the source node and the target node of an edge, and a type of nodes. So the first step is to define the nodes and edges in our new graph. We put the definitions in a new namespace reach to avoid ambiguities.
using zone_graph_t = tchecker::zg::ta::elapsed_extraLUplus_local_t;
using state_t = zone_graph_t::state_t;
using transition_t = zone_graph_t::transition_t;
namespace reach {
template <class EDGE_PTR>
class node_impl_t : public state_t, public tchecker::graph::directed::node_t<EDGE_PTR> {
public:
template <class ... SARGS>
node_impl_t(SARGS && ... sargs) : state_t(std::forward<SARGS>(sargs)...)
{}
node_impl_t(reach::node_impl_t<EDGE_PTR> const &) = default;
node_impl_t(reach::node_impl_t<EDGE_PTR> &&) = default;
~node_impl_t() = default;
reach::node_impl_t<EDGE_PTR> & operator= (reach::node_impl_t<EDGE_PTR> const &) = default;
reach::node_impl_t<EDGE_PTR> & operator= (reach::node_impl_t<EDGE_PTR> &&) = default;
};
template <class NODE_PTR, class EDGE_PTR>
using edge_impl_t = tchecker::graph::directed::edge_t<NODE_PTR, EDGE_PTR>;
class node_t;
class edge_t;
using shared_node_t = tchecker::make_shared_t<reach::node_t>;
using node_ptr_t = tchecker::intrusive_shared_ptr_t<reach::shared_node_t>;
using shared_edge_t = tchecker::make_shared_t<reach::edge_t>;
using edge_ptr_t = tchecker::intrusive_shared_ptr_t<reach::shared_edge_t>;
class node_t : public reach::node_impl_t<reach::edge_ptr_t> {
public:
using reach::node_impl_t<reach::edge_ptr_t>::node_impl_t;
};
class edge_t : public reach::edge_impl_t<reach::node_ptr_t, reach::edge_ptr_t> {
public:
using reach::edge_impl_t<reach::node_ptr_t, reach::edge_ptr_t>::edge_impl_t;
};
} // end of namespace reachFirst observe that the type state_t is now an alias for zone_graph_t::state_t instead of zone_graph_t::shared_state_t. Recall that "shared" means that the state is equipped with a reference counter. The reference counter will now be placed in the node, and we will define a type shared_node_t later.
We first define a new class node_impl_t for node implementations. The main difference is that it is both a state_t and a node of a directed graph tchecker::graph::directed::node_t. It does not provide any functionality beyond those provided by these two classes. The edges implementation edge_impl_t is simply a type alias for edges of the directed graph tchecker::graph::directed::edge_t. Notice that we choose to not store the transitions on the edges: an edge will only allow to move from a node to its predecessor/successor node.
Nodes and edges will be allocated using pool allocators. We thus introduce shared_node_t and shared_edge_t that extend nodes and edges with a reference counter to allow garbage collection. We introduce pointers to shared nodes and shared edges. Finally, nodes node_t and edges edge_t are instantiation of node_impl_t and edge_impl_t with types properly instantiated. In the sequel, we will only use pointers to nodes node_ptr_t and edges edge_ptr_t.
TChecker pool allocators need to know the allocation size of objects. They do not use operator sizeof but specializations of the template tchecker::allocation_size_t. This enables to allocate more memory than the default size of the allocated objects. This is used in some applications for efficiency reasons. So, the next step is to specialize tchecker::allocation_size_t to our new types of nodes and edges. In our settings, we just need to allocate the exact size of the objects as returned by sizeof:
namespace tchecker {
template <>
class allocation_size_t<reach::node_t> {
public:
template <class ... ARGS>
static constexpr std::size_t alloc_size(ARGS && ... args)
{
return sizeof(reach::node_t);
}
};
template <>
class allocation_size_t<reach::edge_t> {
public:
template <class ... ARGS>
static constexpr std::size_t alloc_size(ARGS && ... args)
{
return sizeof(reach::edge_t);
}
};
} // end of namespace tcheckerIn the last step, we define the graph. As before, it owns a transition system allocator for nodes and transitions. It also derives from tchecker::graph::find_graph_t for storing nodes and answering membership queries. This new graph also derives from tchecker::graph::directed::graph_t to store edges. It also owns a pool allocator of edges. Finally, it also stores the list of root nodes to allow exploration of the graph.
using delegate_hash_t = tchecker::intrusive_shared_ptr_delegate_hash_t;
using delegate_equal_to_t = tchecker::intrusive_shared_ptr_delegate_equal_to_t;
using node_allocator_t = zone_graph_t::state_pool_allocator_t<reach::shared_node_t>;
using transition_allocator_t = zone_graph_t::transition_singleton_allocator_t<transition_t>;
using allocator_t = tchecker::ts::allocator_t<node_allocator_t, transition_allocator_t>;
namespace reach {
class graph_t
: private tchecker::graph::find_graph_t<reach::node_ptr_t, delegate_hash_t, delegate_equal_to_t>,
private tchecker::graph::directed::graph_t<reach::node_ptr_t, reach::edge_ptr_t>
{
public:
graph_t(tchecker::gc_t & gc, tchecker::zg::ta::model_t const & model, std::size_t block_size)
: _ts_allocator(gc, std::make_tuple(model, block_size), std::tuple()),
_edge_allocator(block_size, tchecker::allocation_size_t<reach::edge_t>::alloc_size())
{
_edge_allocator.enroll(gc);
}
graph_t(reach::graph_t const &) = delete;
graph_t(reach::graph_t &&) = delete;
~graph_t()
{
destruct_all();
}
reach::graph_t & operator= (reach::graph_t const &) = delete;
reach::graph_t & operator= (reach::graph_t &&) = delete;
void clear()
{
_root_nodes.clear();
tchecker::graph::find_graph_t<reach::node_ptr_t, delegate_hash_t, delegate_equal_to_t>::clear();
tchecker::graph::directed::graph_t<reach::node_ptr_t, reach::edge_ptr_t>::clear();
}
void destruct_all()
{
clear();
_edge_allocator.destruct_all();
_ts_allocator.destruct_all();
}
void free_all()
{
clear();
_edge_allocator.free_all();
_ts_allocator.free_all();
}
allocator_t & ts_allocator()
{
return _ts_allocator;
}
void add_node(reach::node_ptr_t const & n)
{
tchecker::graph::find_graph_t<reach::node_ptr_t, delegate_hash_t, delegate_equal_to_t>::add_node(n);
}
void add_root_node(reach::node_ptr_t const & n)
{
add_node(n);
_root_nodes.push_back(n);
}
void add_edge(reach::node_ptr_t const & src, reach::node_ptr_t const & tgt)
{
reach::edge_ptr_t edge = _edge_allocator.construct();
tchecker::graph::directed::graph_t<reach::node_ptr_t, reach::edge_ptr_t>::add_edge(src, tgt, edge);
}
reach::node_ptr_t const & find(reach::node_ptr_t const & n)
{
return tchecker::graph::find_graph_t<reach::node_ptr_t, delegate_hash_t, delegate_equal_to_t>::find(n);
}
using root_nodes_const_iterator_t = typename std::vector<reach::node_ptr_t>::const_iterator;
tchecker::range_t<root_nodes_const_iterator_t> root_nodes() const
{
return tchecker::make_range(_root_nodes.begin(), _root_nodes.end());
}
inline tchecker::range_t<typename tchecker::graph::directed::graph_t<reach::node_ptr_t, reach::edge_ptr_t>::outgoing_edges_iterator_t>
outgoing_edges(reach::node_ptr_t const & n) const
{
return tchecker::graph::directed::graph_t<reach::node_ptr_t, reach::edge_ptr_t>::outgoing_edges(n);
}
inline reach::node_ptr_t const & edge_src(reach::edge_ptr_t const & edge) const
{
return tchecker::graph::directed::graph_t<reach::node_ptr_t, reach::edge_ptr_t>::edge_src(edge);
}
inline reach::node_ptr_t const & edge_tgt(reach::edge_ptr_t const & edge) const
{
return tchecker::graph::directed::graph_t<reach::node_ptr_t, reach::edge_ptr_t>::edge_tgt(edge);
}
private:
std::vector<reach::node_ptr_t> _root_nodes;
allocator_t _ts_allocator;
tchecker::pool_t<reach::shared_edge_t> _edge_allocator;
};
} // end of namespace reachThe first main features of graph_t is that it abstracts memory management issues from the algorithm. The graph is responsible of emptying the data structures before the memory is freed by the allocators (see method clear, destruct_all and free_all).
The second important feature is that graph_t provides an interface to build the graph (see methods add_node, add_root_node and add_edge), as well as an interface to explore the graph (see methods root_nodes, outgoing_edges, edge_src and edge_tgt). This will allow to build the graph in function reachable, and to traverse it to display the certificate (see function output later).
Building the graph only requires a simple modification of function reachable:
template <class TS, class ALLOCATOR, class GRAPH, class PREDICATE>
bool reachable(TS & ts, ALLOCATOR & allocator, GRAPH & g, PREDICATE P)
{
using builder_t = tchecker::ts::builder_ok_t<TS, ALLOCATOR>;
using node_ptr_t = typename builder_t::state_ptr_t;
using transition_ptr_t = typename builder_t::transition_ptr_t;
builder_t builder(ts, allocator);
std::stack<node_ptr_t> stack;
node_ptr_t node, next_node, found_node;
transition_ptr_t transition;
auto initial_range = builder.initial();
for (auto it = initial_range.begin(); ! it.at_end(); ++it) {
std::tie(node, transition) = *it;
found_node = g.find(node);
if (found_node != node)
continue;
g.add_root_node(node);
stack.push(node);
}
while ( ! stack.empty() ) {
node = stack.top();
stack.pop();
if (P(node))
return true;
auto outgoing_range = builder.outgoing(node);
for (auto it = outgoing_range.begin(); ! it.at_end(); ++it) {
std::tie(next_node, transition) = *it;
found_node = g.find(next_node);
if (found_node == next_node) {
g.add_node(next_node);
stack.push(next_node);
}
g.add_edge(node, found_node);
}
}
return false;
}Now, each time we compute the successor node next_node of current node node, we add an edge from node to found_node, the node equivalent to next_node in the graph.
In order to output the reachability graph, we simply run a depth-first search from its root nodes. This is implemented using the interface provided by reach::graph_t:
namespace reach {
template <class NODE_OUPUTTER>
void output(std::ostream & os, reach::graph_t const & g, std::string const & name, NODE_OUTPUTTER & node_outputter)
{
std::stack<reach::node_ptr_t> stack;
std::unordered_set<reach::node_ptr_t, tchecker::instrusive_shared_ptr_hash_t> visited;
os << "digraph " << name << " {" << std::endl;
os << "node [shape=\"box\",style=\"rounded\"];" << std::endl;
auto root_nodes = g.root_nodes();
for (reach::node_ptr_t const & n : root_nodes) {
stack.push(n);
visited.insert(n);
}
while ( ! stack.empty() ) {
reach::node_ptr_t n = stack.top();
stack.pop();
os << "n" << n.ptr() << " [label=\"";
node_outputter.output(os, *n);
os << "\"]" << std::endl;
auto outgoing_edges = g.outgoing_edges(n);
for (reach::edge_ptr_t const & e : outgoing_edges) {
reach::node_ptr_t const & tgt = g.edge_tgt(e);
os << "n" << n.ptr() << " -> " << "n" << tgt.ptr() << std::endl;
if (visited.find(tgt) == visited.end()) {
stack.push(tgt);
visited.insert(tgt);
}
}
}
os << "}" << std::endl;
os.flush();
visited.clear();
}
} // end of namespace reachThe function reach::output takes as parameter an output stream os, the reachability graph g, the name of the model name and a node outputter node_ouputter. The node outputter will output the content of the node to os. For instance, in the case of node of the zone graph, it will output the tuple of locations, the valuation of the bounded integer variables and the zone. The exact type of node outputter depends on the type of nodes, and, more precisely, on the type of states from which the nodes derive. In our case, we will use a node outputter for nodes of the zone graph (see below).
The last step simply consists in calling function output in function main, once the reachability graph has been computed:
int main(int argc, char * argv[])
{
if (argc != 3) {
std::cerr << "Usage: " << argv[0] << " filename label" << std::endl;
return 1;
}
tchecker::log_t log(&std::cerr);
tchecker::parsing::system_declaration_t const * sysdecl = nullptr;
try {
sysdecl = tchecker::parsing::parse_system_declaration(argv[1], log);
if (sysdecl == nullptr)
throw std::runtime_error("System declaration cannot be built");
tchecker::zg::ta::model_t model(*sysdecl, log);
zone_graph_t::ts_t ts(model);
tchecker::gc_t gc;
reach::graph_t graph(gc, model, 100000);
tchecker::zg::ta::state_outputter_t node_outputter(model.vm_variables().intvars(model.system()).layout().index(),
model.vm_variables().clocks(model.system()).layout().index());
gc.start();
std::string label = argv[2];
P_t P(model.system().labels(), label);
if (reachable(ts, graph.ts_allocator(), graph, P))
std::cout << "#" << label << " is reachable" << std::endl;
else
std::cout << "#" << label << " is not reachable" << std::endl;
gc.stop();
reach::output(std::cout, graph, model.system().name(), node_outputter);
graph.free_all();
}
catch (std::exception const & e) {
log.error(e.what());
}
delete sysdecl;
return 0;
}We build a node outputter node_outputter for states of the zone graph, that is of type tchecker::zg::ta::state_outputter_t. Had our nodes contained extra informations with respect to states of the zone graph, we would have had to define a node outputter deriving from tchecker::zg::ta::state_outputter_t that would have output the state as well as the extra informations. Here, the state outputter is also suitable for our nodes.
Then, after function reachable has returned, we output the reachabilty graph to std::cout and that is it.
The full program is available in src/reach-6.txt. Running executable program reach-6, one not only get an answer to the reachability problem, but also a certificate of (un-)reachability as a reachable graph in the Graphviz DOT format. The Graphviz tool can be used to visualise the graphs generated by our program.