From 4b96ea93082b75d30c70aaa0182176ee069dae00 Mon Sep 17 00:00:00 2001 From: OndrejAlexaj Date: Thu, 23 Apr 2026 19:19:49 +0000 Subject: [PATCH 1/4] add: spot complementation procedure called from kofola and provide postprocessing level changing parameter --- README.md | 1 + src/complement/complement_tela.cpp | 76 +++++++++++++++++++++++++++++- src/complement/complement_tela.hpp | 3 ++ src/main.cpp | 15 +++++- 4 files changed, 91 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index f612724..7745d5b 100644 --- a/README.md +++ b/README.md @@ -85,6 +85,7 @@ The complementation and the inclusion checking might be adjusted by the followin | `sh-break` | `yes`,`no` | Enable shared breakpoint across partial algorithms; when `yes` partial algorithms that support shared breakpoints propagate a common breakpoint across partitions | | `tela_det_alg` | `inductive`, `dnf-tela` | Algorithm selection for complementing deterministic TELA components (default `dnf-tela`) | | `sd_ind_sh_break` | `yes`, `no` | Shared breakpoint for inductive TELA procedure (assumes `tela_det_alg=inductive`) | +| `postp_l` | `low`, `medium`, `high` | postprocessing level applied to the result of complementation (used for both - spot's and kofola's implementation) ## Testing diff --git a/src/complement/complement_tela.cpp b/src/complement/complement_tela.cpp index b956f4c..2654993 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 @@ -59,8 +64,19 @@ spot::twa_graph_ptr kofola::apply_postprocessing(const spot::twa_graph_ptr& aut, if(is_post_reduction_suitable(original_aut)) { if(result->num_states() < 2000) { p_post.set_type(spot::postprocessor::GeneralizedBuchi); - } - p_post.set_level(spot::postprocessor::Low); + } + + // Set postprocessor level based on postp_l parameter + auto pp_level = spot::postprocessor::Low; + auto level_it = kofola::OPTIONS.params.find("postp_l"); + if (level_it != kofola::OPTIONS.params.end()) { + if (level_it->second == "high") { + pp_level = spot::postprocessor::High; + } else if (level_it->second == "medium") { + pp_level = spot::postprocessor::Medium; + } + } + p_post.set_level(pp_level); result = p_post.run(result); } @@ -214,3 +230,59 @@ 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); + + // Set postprocessor level based on params + auto level_it = kofola::OPTIONS.params.find("postp_l"); + if (level_it != kofola::OPTIONS.params.end()) { + auto pp_level = spot::postprocessor::Low; + if (level_it->second == "high") { + pp_level = spot::postprocessor::High; + } else if (level_it->second == "medium") { + pp_level = spot::postprocessor::Medium; + } + p.set_level(pp_level); + } + auto det = p.run(std::const_pointer_cast(aut)); + if (!det || !spot::is_universal(det)) + return nullptr; + + return spot::dualize(det); +} 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..735c428 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"}); @@ -199,8 +200,8 @@ int process_args(int argc, char *argv[], kofola::options* params) args::Flag debug_flag(misc_group, "debug", "output debugging information", {'d', "debug"}); args::ValueFlag params_flag(misc_group, "params", "string with ';'-separated parameters of the form 'key=value' " - "(or just 'key' for yes/no flags), e.g. for inclusion, " - "'early_sim=yes;early_plus_sim=yes;dir_sim=yes;gfee=yes;'", + "(or just 'key' for yes/no flags), e.g. 'postp_l=high;' for postprocessor level, " + "or for inclusion 'early_sim=yes;early_plus_sim=yes;dir_sim=yes;gfee=yes;'", {"params"}); try { @@ -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"; } @@ -337,6 +340,7 @@ int main(int argc, char *argv[]) return EXIT_SUCCESS; } + // kofola's complementation for (const std::string& input_filename : options.filenames) { spot::parsed_aut_ptr parsed_aut = nullptr; try { @@ -358,6 +362,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") { From b5264fc468f1e56d51e1e36ba44beae9abf57ef1 Mon Sep 17 00:00:00 2001 From: OndrejAlexaj Date: Thu, 23 Apr 2026 20:47:30 +0000 Subject: [PATCH 2/4] move postprocessing from input to output in the spot impl in kofola --- src/complement/complement_tela.cpp | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/src/complement/complement_tela.cpp b/src/complement/complement_tela.cpp index 2654993..2ecfeb9 100644 --- a/src/complement/complement_tela.cpp +++ b/src/complement/complement_tela.cpp @@ -268,21 +268,29 @@ spot::twa_graph_ptr kofola::spot_complement(const spot::twa_graph_ptr& aut) spot::postprocessor p(&m); p.set_type(spot::postprocessor::Generic); p.set_pref(spot::postprocessor::Deterministic); + p.set_level(spot::postprocessor::Low); - // Set postprocessor level based on params + 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); + auto level_it = kofola::OPTIONS.params.find("postp_l"); if (level_it != kofola::OPTIONS.params.end()) { + spot::postprocessor p_post; + p_post.set_type(spot::postprocessor::Generic); + auto pp_level = spot::postprocessor::Low; if (level_it->second == "high") { pp_level = spot::postprocessor::High; } else if (level_it->second == "medium") { pp_level = spot::postprocessor::Medium; } - p.set_level(pp_level); + p_post.set_level(pp_level); + dualized = p_post.run(dualized); } - auto det = p.run(std::const_pointer_cast(aut)); - if (!det || !spot::is_universal(det)) - return nullptr; - return spot::dualize(det); + return dualized; } From e629d4800cd087b3f41f6dbe5c01474eefd4da8e Mon Sep 17 00:00:00 2001 From: OndrejAlexaj Date: Thu, 23 Apr 2026 21:16:02 +0000 Subject: [PATCH 3/4] remove flag for controlling postproc level --- README.md | 1 - src/complement/complement_tela.cpp | 28 +--------------------------- src/main.cpp | 4 ++-- 3 files changed, 3 insertions(+), 30 deletions(-) diff --git a/README.md b/README.md index 7745d5b..f612724 100644 --- a/README.md +++ b/README.md @@ -85,7 +85,6 @@ The complementation and the inclusion checking might be adjusted by the followin | `sh-break` | `yes`,`no` | Enable shared breakpoint across partial algorithms; when `yes` partial algorithms that support shared breakpoints propagate a common breakpoint across partitions | | `tela_det_alg` | `inductive`, `dnf-tela` | Algorithm selection for complementing deterministic TELA components (default `dnf-tela`) | | `sd_ind_sh_break` | `yes`, `no` | Shared breakpoint for inductive TELA procedure (assumes `tela_det_alg=inductive`) | -| `postp_l` | `low`, `medium`, `high` | postprocessing level applied to the result of complementation (used for both - spot's and kofola's implementation) ## Testing diff --git a/src/complement/complement_tela.cpp b/src/complement/complement_tela.cpp index 2ecfeb9..56e49fa 100644 --- a/src/complement/complement_tela.cpp +++ b/src/complement/complement_tela.cpp @@ -65,18 +65,7 @@ spot::twa_graph_ptr kofola::apply_postprocessing(const spot::twa_graph_ptr& aut, if(result->num_states() < 2000) { p_post.set_type(spot::postprocessor::GeneralizedBuchi); } - - // Set postprocessor level based on postp_l parameter - auto pp_level = spot::postprocessor::Low; - auto level_it = kofola::OPTIONS.params.find("postp_l"); - if (level_it != kofola::OPTIONS.params.end()) { - if (level_it->second == "high") { - pp_level = spot::postprocessor::High; - } else if (level_it->second == "medium") { - pp_level = spot::postprocessor::Medium; - } - } - p_post.set_level(pp_level); + p_post.set_level(spot::postprocessor::Low); result = p_post.run(result); } @@ -277,20 +266,5 @@ spot::twa_graph_ptr kofola::spot_complement(const spot::twa_graph_ptr& aut) // Apply postprocessor to the dualized result if postp_l is specified spot::twa_graph_ptr dualized = spot::dualize(det); - auto level_it = kofola::OPTIONS.params.find("postp_l"); - if (level_it != kofola::OPTIONS.params.end()) { - spot::postprocessor p_post; - p_post.set_type(spot::postprocessor::Generic); - - auto pp_level = spot::postprocessor::Low; - if (level_it->second == "high") { - pp_level = spot::postprocessor::High; - } else if (level_it->second == "medium") { - pp_level = spot::postprocessor::Medium; - } - p_post.set_level(pp_level); - dualized = p_post.run(dualized); - } - return dualized; } diff --git a/src/main.cpp b/src/main.cpp index 735c428..74148e4 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -200,8 +200,8 @@ int process_args(int argc, char *argv[], kofola::options* params) args::Flag debug_flag(misc_group, "debug", "output debugging information", {'d', "debug"}); args::ValueFlag params_flag(misc_group, "params", "string with ';'-separated parameters of the form 'key=value' " - "(or just 'key' for yes/no flags), e.g. 'postp_l=high;' for postprocessor level, " - "or for inclusion 'early_sim=yes;early_plus_sim=yes;dir_sim=yes;gfee=yes;'", + "(or just 'key' for yes/no flags), e.g. for inclusion, " + "'early_sim=yes;early_plus_sim=yes;dir_sim=yes;gfee=yes;'", {"params"}); try { From 587f05f3bd0a8d5c93d99f9f81b901c8bac24557 Mon Sep 17 00:00:00 2001 From: OndrejAlexaj Date: Thu, 23 Apr 2026 21:17:29 +0000 Subject: [PATCH 4/4] polish --- src/complement/complement_tela.cpp | 2 +- src/main.cpp | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/complement/complement_tela.cpp b/src/complement/complement_tela.cpp index 56e49fa..9bef86c 100644 --- a/src/complement/complement_tela.cpp +++ b/src/complement/complement_tela.cpp @@ -64,7 +64,7 @@ spot::twa_graph_ptr kofola::apply_postprocessing(const spot::twa_graph_ptr& aut, if(is_post_reduction_suitable(original_aut)) { if(result->num_states() < 2000) { p_post.set_type(spot::postprocessor::GeneralizedBuchi); - } + } p_post.set_level(spot::postprocessor::Low); result = p_post.run(result); diff --git a/src/main.cpp b/src/main.cpp index 74148e4..91fdf44 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -340,7 +340,6 @@ int main(int argc, char *argv[]) return EXIT_SUCCESS; } - // kofola's complementation for (const std::string& input_filename : options.filenames) { spot::parsed_aut_ptr parsed_aut = nullptr; try {