• Alexandre Duret-Lutz's avatar
    print_hoa: output all registered APs · 1c2c914d
    Alexandre Duret-Lutz authored
    Also introduce twa::unregister_ap() and twa_graph::remove_unused_ap()
    so that the methods where this behavior is expected can be fixed.
    
    And fix ltsmin::kripke() which did not register APs.
    
    Part of #170.
    
    * spot/twaalgos/hoa.cc: Use apvars() to print all registerd APs.
    Throw an exception when printing automata using unregistered APs.
    * spot/ltsmin/ltsmin.cc: Call register_ap().
    * spot/twa/twa.cc, spot/twa/twa.hh, spot/twa/twagraph.cc,
    spot/twa/twagraph.hh (twa::unregister_ap, twa_graph::remove_unused_ap):
    New methods.
    * spot/tl/exclusive.cc, spot/twaalgos/postproc.cc,
    spot/twaalgos/remprop.cc, spot/twaalgos/relabel.cc: Use them.
    * tests/core/maskacc.test, tests/core/maskkeep.test,
    tests/core/strength.test: Adjust expected results.
    * NEWS: Mention those changes.
    1c2c914d
twagraph.cc 9.26 KB