diff --git a/src/complement/complement_tela.cpp b/src/complement/complement_tela.cpp index b956f4c..9bef86c 100644 --- a/src/complement/complement_tela.cpp +++ b/src/complement/complement_tela.cpp @@ -25,6 +25,11 @@ #include #include #include +#include +#include +#include +#include +#include // standard library #include @@ -214,3 +219,52 @@ bool kofola::is_post_reduction_suitable(const spot::twa_graph_ptr& aut) { } return true; } + +spot::twa_graph_ptr kofola::spot_complement(const spot::twa_graph_ptr& aut) +{ + spot::twa_graph_ptr result = spot::complement(aut); + + if (!aut->is_existential() || is_universal(aut)) + { + spot::twa_graph_ptr res = spot::dualize(aut); + // There are cases with "t" acceptance that get converted to + // Büchi during completion, then dualized to co-Büchi, but the + // acceptance is still not used. Try to clean it up in this + // case. + if (aut->num_sets() == 0 || + // Also dualize removes sink states, but doesn't simplify + // the acceptance condition. + res->num_states() < aut->num_states()) + spot::cleanup_acceptance_here(res); + + return result; + } + if (spot::is_very_weak_automaton(aut)) + // Removing alternation may need more acceptance sets than Spot + // supports. When this happens res==nullptr and we fall back to + // determinization-based complementation. + if (spot::twa_graph_ptr res = spot::remove_alternation(spot::dualize(aut), false, + nullptr, false)) { + return result; + } + // Determinize + spot::option_map m; + + // In addition to the above options, the simulation-based + // optimization of the determinization is already restricted by + // the default values of simul-max and simul-trans-pruning. + // (See spot-x(7) for details.) + spot::postprocessor p(&m); + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic); + p.set_level(spot::postprocessor::Low); + + auto det = p.run(std::const_pointer_cast(aut)); + if (!det || !spot::is_universal(det)) + return nullptr; + + // Apply postprocessor to the dualized result if postp_l is specified + spot::twa_graph_ptr dualized = spot::dualize(det); + + return dualized; +} diff --git a/src/complement/complement_tela.hpp b/src/complement/complement_tela.hpp index f8f415b..8d705e8 100644 --- a/src/complement/complement_tela.hpp +++ b/src/complement/complement_tela.hpp @@ -36,6 +36,9 @@ spot::twa_graph_ptr complement_deterministic(const spot::twa_graph_ptr& aut); /// applies postprocessing to an automaton based on configuration parameters spot::twa_graph_ptr apply_postprocessing(const spot::twa_graph_ptr& aut, const spot::twa_graph_ptr& original_aut); +/// complements using Spot's built-in complement algorithm (essentially copy-paste from spot) +spot::twa_graph_ptr spot_complement(const spot::twa_graph_ptr& aut); + /// complements a TELA using the synchronous algorithm (cf. paper) spot::twa_graph_ptr complement_sync(const spot::twa_graph_ptr& aut); diff --git a/src/main.cpp b/src/main.cpp index 6eb728b..91fdf44 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -185,6 +185,7 @@ int process_args(int argc, char *argv[], kofola::options* params) // command args::Group operation_group(parser, "Operation:", args::Group::Validators::AtMostOne); args::Flag complement_flag(operation_group, "complement", "complement the inputs (default)", {"complement"}); + args::Flag spot_complement_flag(operation_group, "spot_complement", "complement the inputs using Spot", {"spot_complement"}); args::Flag det_flag(operation_group, "det", "determinize the inputs", {"det"}); args::Flag type_flag(operation_group, "type", "print out types of the inputs", {"type"}); args::Flag scc_types_flag(operation_group, "scc-types", "print out types of SCCs in the inputs", {"scc-types"}); @@ -249,6 +250,8 @@ int process_args(int argc, char *argv[], kofola::options* params) params->operation = "inclusion"; } else if (to_elev_flag) { params->operation = "elevatorization"; + } else if (spot_complement_flag) { + params->operation = "spot_complement"; } else { // default params->operation = "complement"; } @@ -358,6 +361,13 @@ int main(int argc, char *argv[]) spot::print_hoa(std::cout, result); std::cout << "\n"; + } else if(options.operation == "spot_complement") { + spot::twa_graph_ptr result = kofola::spot_complement(aut); + + if (result) { + spot::print_hoa(std::cout, result); + std::cout << "\n"; + } } else if (options.operation == "type") { assert(false); } else if (options.operation == "determinize") {