Skip to content
  • Alexandre Duret-Lutz's avatar
    simplify: fix related to event_univ handling · 8968bf6c
    Alexandre Duret-Lutz authored
    Fixes #260.  Reported by František Blahoudek.
    
    The simplification F(f)|q = F(f|q), where q designates an event_univ
    formula, was not always applied because of a couple of issue: (1) the
    mospliter was ignoring event_univ unless favor_event_univ was set, (2)
    when processing formulas from res_EventUniv they were not put back
    into res_F or res_G to be subject to the F/G rules.
    
    * spot/tl/simplify.cc: Improve handling of the above points.
    * tests/core/reduccmp.test: Adjust and add test case.
    * tests/core/ltl2tgba2.test, tests/python/atva16-fig2a.ipynb: Adjust.
    8968bf6c