incorrect usage of spot::acc_cond::mark_t::value_t and problem with future Spot version

[adl]

I think there are some misconceptions in the source of LTL3TELA, and those are partly due to the way things were named in Spot.

Spot defines a type spot::acc_cond::mark_t that is used to hold a set of acceptance set numbers (e.g. as {1,4,5}). This type is for instance used to label each transition with the set of acceptance sets the transition belongs to. (In papers and comments we usually call the set numbers ❶,❹,❺... "marks", but mark_t does not represent one mark, it is a set of marks.)

Now mark_t has to implement all set operations (union m1|m2, intersection m1&m2, membership test m.has(3), etc.) in a quite efficient way, so it is implemented as a bit vector. The current type representing that bit vector happens to be publicly accessible as spot::acc_cond::mark_t::value_t and was equal to unsigned int in Spot versions up to 2.5.x. This is also why Spot only supports up to 32 acceptance sets: it actually supports as many bits you can fit in an unsigned int.

In the upcoming Spot 2.6, Maximilien (@bosonnoir) improved the mark_t implementation so that we can augment the number of supported sets at compile-time, this is basically done by changing the value of mark_t::value_t. That means mark_t::value_t should not be unsigned int anymore (even in the default setting where we still support only 32 sets), but that type really should not have been public in the first place.

Now ltl3tela unfortunately has an unexpected usage of these types. It uses spot::acc_cond::mark_t::value_t to represent one set number, and even build many std::set<spot::acc_cond::mark_t::value_t> to represents sets of marks. This is much slower than using spot::acc_cond::mark_t to represent a set of marks, and now it does not work with our new bit vector implementation (not unsigned int anymore).

As a consequence Maxiilien is reworking this code to preserve some kind of backward compatibility for ltl3tela. In the upcoming Spot 2.6 mark_t::value_t will still be defined as unsigned, but only in the default setting where Spot is still restricted to 32 acceptance sets. This typedef will be marked as deprecated, so you should expect warnings all over the place when compiling ltl3tela, and the implementation of mark_t will not use value_t at all (it will use our new bitvector implementation). When Spot is compiled with more that 32 acceptance sets, mark_t::value_t will simply not be defined.

A very crude fix of ltl3tela to avoid all the warnings is to run:

perl -i -pe 's/spot::acc_cond::mark_t::value_t/unsigned/g' *.?pp

but that will make the code a lot less readable. You probably want some typedef unsigned acc_mark; and use acc_mark instead of spot::acc_cond::mark_t::value_t everywhere. Also as I'v said above, you'd gain a lot by replacing std::set<spot::acc_cond::mark_t::value_t> by spot::acc_cond::mark_t, but that requires some careful update of all the code that manipulate these sets.

[adl]

Current warnings look as follows. ltl3tela still compiles.

g++ -std=c++14 -o ltl3tela alternating.cpp nondeterministic.cpp automaton.cpp utils.cpp main.cpp -lspot -lbddx
In file included from alternating.hpp:23:0,
                 from alternating.cpp:21:
automaton.hpp:48:35: warning: 'spot::internal::_32acc<true>::value_t' is deprecated: mark_t no longer relies on unsigned, stop using value_t [-Wdeprecated-declarations]
  std::set<spot::acc_cond::mark_t::value_t> marks;
                                   ^~~~~~~
In file included from automaton.hpp:32:0,
                 from alternating.hpp:23,
                 from alternating.cpp:21:
/usr/include/spot/twa/acc.hh:43:24: note: declared here
       typedef unsigned value_t;
                        ^~~~~~~
In file included from alternating.hpp:23:0,
                 from alternating.cpp:21:
automaton.hpp:87:108: warning: 'spot::internal::_32acc<true>::value_t' is deprecated: mark_t no longer relies on unsigned, stop using value_t [-Wdeprecated-declarations]
  int dominates(Edge* other, std::set<unsigned> o1, std::set<unsigned> o2, std::set<spot::acc_cond::mark_t::value_t> inf_marks) const;
                                                                                                            ^~~~~~~
In file included from automaton.hpp:32:0,
                 from alternating.hpp:23,
                 from alternating.cpp:21:
/usr/include/spot/twa/acc.hh:43:24: note: declared here
       typedef unsigned value_t;
                        ^~~~~~~
In file included from alternating.hpp:23:0,
                 from alternating.cpp:21:
automaton.hpp:88:62: warning: 'spot::internal::_32acc<true>::value_t' is deprecated: mark_t no longer relies on unsigned, stop using value_t [-Wdeprecated-declarations]
  int dominates(Edge* other, std::set<spot::acc_cond::mark_t::value_t> inf_marks) const;
                                                              ^~~~~~~
In file included from automaton.hpp:32:0,
                 from alternating.hpp:23,
                 from alternating.cpp:21:
/usr/include/spot/twa/acc.hh:43:24: note: declared here
       typedef unsigned value_t;
                        ^~~~~~~
[...]

[jurajmajor]

Hi Alexandre, I have now replaced spot::acc_cond::mark_t::value_t with an alias for unsigned so you can remove your compatibility layer. I'll leave this issue open until I rewrite (hopefully soon) the code to use the efficient mark_t interface. Thank you.