Skip to content
  • Alexandre Duret-Lutz's avatar
    ltl2tgba_fm: Fix incorrect simplification of promises for M · 795c2f17
    Alexandre Duret-Lutz authored
    The bug was reported by Joachim Klein.
    
    * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::register_a_variable):
    Reduce P(a M b) to P(a & b), not to P(a).
    * src/tgbatest/ltlcross.test: Test Joachim's formula.
    * src/tgbatest/ltl2ta.test: Adjust some expected values.
    * NEWS: Mention the bug.
    795c2f17