Alexandre Duret-Lutz authored
The ltl_to_tgba_fm() translation function was using a hash_map of maps (ugh!) to merge transitions on output. However recent libstd++ changed the implementation of hash_map (a.k.a. unordered_map) causing transitions to be output in a different order. This implementation-dependent order caused the ltl2ta.test to fail because the BA->TA transformation can produce TA of different sizes if you simply change the order of transitions in the input BA! This does not sound like a nice property for the BA->TA transformation, but Ala Eddine isn't sure how to fix it yet. In the meantime, this patch makes sure ltl_to_tgba_fm() will return the same output regardless of the implementation of hash_map. The ltl2ta.test failure has been observed with g++ 4.9.2 on Arch Linux, and with gcc-snapshot (5.0.0 20141016) on Debian. * src/tgbaalgos/ltl2tgba_fm.cc: Rewrite the transition merging using a std::vector and std::sort instead of nested maps tables. * src/tgbatest/ltl2ta.test: Adjust sizes to the new order. * NEWS: Mention the fix.11aa708a
To find the state of this project's repository at the time of any of these versions, check out the tags.