Skip to content

ltlsynt: detect APs with constant polarity

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

This implements the first point of issue #529 (closed).

  • spot/tl/apcollect.cc, spot/tl/apcollect.hh (collect_litterals): New function.
  • bin/ltlsynt.cc: Implement the --polarity option, use collect_litterals() to simplify the specification, finally patch the game, Mealy, or Aiger output.
  • spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh: Take a relabeling_map has argument to specify extra APs.
  • tests/core/ltlsynt.test, tests/core/ltlsynt2.test: Adjust test cases.

Merge request reports