-
Alexandre Duret-Lutz authored
The previous code was sometime doing the work of remove_fin() in addition to complementing the acceptance conditions. This separate the two operations clearly. Also the specialized code for complementing weak automata is now a specialized code for remove_fin() on weak automata. * src/twaalgos/dtgbacomp.hh, src/twaalgos/dtgbacomp.cc: Rename as ... * src/twaalgos/complement.hh, src/twaalgos/complement.cc: ... these. * src/twaalgos/Makefile.am: Adjust. * src/twaalgos/complement.hh (dtgba_complement): Rename as ... (dtwa_complement): ... this, and restrict the purpose to completion and accetance complementation. Further acceptance simplification can be done with remove_fin() and to_generalized_buchi(). * src/twaalgos/remfin.cc (remove_fin): Specialize handling of weak automata using the code that was originally in dtgba_complement(). Also mark the output as state-based when the input has to Inf. * src/twaalgos/postproc.cc, src/twaalgos/postproc.hh: Make sure scc_filter is always called after to_generalized_buchi(). * bench/stutter/stutter_invariance_randomgraph.cc, src/bin/ltlcross.cc, src/tests/ikwiad.cc, src/twaalgos/minimize.cc, src/twaalgos/powerset.cc, src/twaalgos/stutter.cc: Adjust usage. * src/tests/dstar.test, src/tests/ltl2dstar4.test, src/tests/remfin.test: Adjust expected outputs. * wrap/python/spot_impl.i: Export dtwa_complement().
06d3bc67