Skip to content

relabel_bse: rework to simplify more patterns

Alexandre Duret-Lutz requested to merge adl/540 into next

Rework the way we compute and use cut-points to catch more patterns we can rewrite. Also Use BDDs to check if a Boolean sub-expression is false or true. Fixes issue #540 (closed).

  • spot/tl/relabel.hh: Update documentation
  • spot/tl/relabel.cc (relabel_bse): Rework.
  • tests/core/ltlfilt.test: Add more test cases.
  • tests/python/_mealy.ipynb: Update.
  • NEWS: Mention the change.

Merge request reports