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.84595883
To find the state of this project's repository at the time of any of these versions, check out the tags.