add state comparisons

[adl]

Just so we don't forget this; in my interface I sometimes need to compare two states (for instance to put them in a std::map). Any total order is ok (e.g., lexicographical) with me.

[fredher]

I have defined tchecker::lexical_cmp over states, as well as ranges (see tchecker/utils/ordering.hh), tuple of locations, integer variables valuations, DBMs and offset DBMs (and zones as well).

Assume n1 and n2 are two node pointers (of type node_ptr_t in TChecker), invoking:

tchecker::lexical_cmp(*n1, *n2);

returns 0 if n1 and n2 are equal, <0 if n1 is smaller than n2 for lexical ordering (tuple of locations, then integer variable valuation, then zone) and >0 otherwise.

I have tried to build an std::set of nodes from the graph computed by covreach algorithm. Iterating over the set, I could display the nodes in lexical order.

[fredher]

I have implemented lexical ordering on nodes by providing functions:

tchecker::lexical_cmp(STATE const & s1, STATE const & s2);

for several kind of states (fsm, ta, zg, etc). These functions are all defined in namespace tchecker but in different files include/tchecker/XXX/details/state.hh.

The problem with this approach is that if you don't include the right ...details/state.hh file, you may end up using the wrong tchecker::lexical_cmp function silently (since type resolution works as soon as one tchecker::lexical_cmp is declared). This was the problem behind issue #41 .

To avoid this problem, I suggest to declare each tchecker::lexical_cmp function in a different state space, e.g.:

namespace ta {
  int lexical_cmp(ta::state_t const &, ta::state_t const &);
}

namespace zg {
  int lexical_cmp(zg::state_t const &, zg::state_t const &);
}

Namespaces will give a way to ensure that we are calling the expected function. This is compatible with the current usage of tchecker::lexical_cmp in TChecker.

Is this compatible with your usage of tchecker::lexical_cmp, in particular in tcltl?

[adl]

tcltl is not yet using lexical_cmp (this is on my todo list), so that change will not break anything.

(I confess I don't quite understand the issue. It's not clear to me how you can #include the wrong lexical_cmp if lexical_cmp is defined in the same file has the structure it compares. In any case, I would expect lexical_cmp to be defined at the same place as operator== and operator!= are.)

[fredher]

Thanks, I will move all lexical_cmp definitions under the appropriate namespaces.

The issue was the following:

• the method output of template class tchecker::covreach::dot_outputter_t (in file include/tchecker/algorithms/covreach/output.hh) was directly calling tchecker::lexical_cmp
• but there was no definition of tchecker::lexical_cmp in this file, as expected since the template class tchecker::covreach::dot_outputter_t is parametrized by the type of graph (hence the type of nodes), and the flavour of tchecker::lexical_cmp that shall be used can only be determined once the template class is instantiated.
• thus, the definition of tchecker::lexical_cmp was provided when template class tchecker::covreach::dot_outputter_t was instantiated in file include/tchecker/algorithms/covreach/run.hh. But there, the exact definition of tchecker::lexical_cmp was dependent on the order of #include directives in the file.
• it happened that the definition of tchecker::lexical_cmp for zone graph states was provided after the template class tchecker::covreach::dot_outputter_t was instantiated. The only definition of tchecker::lexical_cmp compatible with states of the zone graphs, that was known when the template class was instantiated, was the one provided for timed automata state.
• as a result, when comparing two states s1 and s2 of the zone graph with tchecker::lexical_cmp, we were using its definition for states of timed automata (in file include/tchecker/ta/details/state.hh). Thus we were only comparing the tuples of locations and the valuations of integer variables in s1 and s2, and we were ignoring their zones.

I know that you will enjoy the fact that it was solved by adding a template parameter to method output of class tchecker::covreach::dot_outputter_tto specify which total ordering on nodes should be used (in practice, which version of tchecker::lexical_cmp) :-)