simplify: fix related to event_univ handling

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.
This commit is contained in:
Alexandre Duret-Lutz 2017-05-08 10:28:13 +02:00
parent 19aae6f9cf
commit 845958834f
5 changed files with 113 additions and 123 deletions

4
NEWS
View file

@ -93,6 +93,10 @@ New in spot 2.3.3.dev (not yet released)
- ltldo and ltlcross could leave temporary files behind when
aborting on error.
- The LTL simplifcation rule that turns F(f)|q into F(f|q)
when q is a subformula that is both eventual and universal
was documented but not applied in some forgotten cases.
Backward-incompatible changes:
- spot::acc_cond::mark_t::operator bool() has been marked as