Skip to content
  • Alexandre Duret-Lutz's avatar
    ltl2tgba_fm: fix non-deterministic output · 4ea63f84
    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.
    * NEWS: Mention the fix.
    4ea63f84
To find the state of this project's repository at the time of any of these versions, check out the tags.