Skip to content
  • Maximilien Colange's avatar
    Improve ltlsynt interface · 1da0afba
    Maximilien Colange authored
    To ease debugging and testing, ltlsynt can output the synthesized
    strategy as an automaton, not just an aiger circuit.
    Also, its exit code has been changed to something meaningful.
    
    * bin/ltlsynt.cc: Various improvements: options, exit code, code style
    * spot/twaalgos/aiger.hh, spot/twaalgos/aiger.cc,
      spot/twaalgos/Makefile.am: Move the aiger printer to separate files
    * tests/core/ltlsynt.test: Clean up and update test file
    * tests/Makefile.am: Add the test file to the test suite
    * NEWS: document the new aiger printer
    * doc/org/concepts.org: document the named property "synthesis-outputs",
      used by print_aiger
    1da0afba