• Alexandre Duret-Lutz's avatar
    restructure the complementation code · 06d3bc67
    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
ltl2dstar4.test 2.35 KB