From 744f54a0a83050529a6a556c51ce6000012099bf Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 21 May 2026 16:31:06 +0200 Subject: [PATCH 1/2] fix: replace assertion with output_scc_info call in main function Co-authored-by: Copilot --- src/main.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main.cpp b/src/main.cpp index 6eb728b..78cc54d 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -359,7 +359,7 @@ int main(int argc, char *argv[]) spot::print_hoa(std::cout, result); std::cout << "\n"; } else if (options.operation == "type") { - assert(false); + output_scc_info(aut); } else if (options.operation == "determinize") { spot::twa_graph_ptr result = kofola::determinize_tela(aut); From b8dfcb8ee8fcf386cba82047afcb1d78af874697 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 21 May 2026 21:51:36 +0200 Subject: [PATCH 2/2] fix: enhance output_scc_info to track IADACs and improve SCC checks Co-authored-by: Copilot --- src/main.cpp | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/src/main.cpp b/src/main.cpp index 78cc54d..4f21b3d 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -54,6 +54,9 @@ void output_scc_info(spot::twa_graph_ptr aut) unsigned num_max_iwcs_states = 0; unsigned num_acciwcs_states = 0; unsigned num_max_acciwcs_states = 0; + unsigned num_iadacs = 0; + unsigned num_iadacs_states = 0; + unsigned num_max_iadacs_states = 0; unsigned num_dacs = 0; unsigned num_dacs_states = 0; unsigned num_max_dacs_states = 0; @@ -78,21 +81,43 @@ void output_scc_info(spot::twa_graph_ptr aut) num_max_acciwcs_states = std::max(num_max_acciwcs_states, num); } - if (helpers::is_accepting_detscc(types, sc)) + if (!helpers::is_accepting_scc(types, sc)) + { + continue; + } + + // Keep category checks in the same order as complement partitioning. + if (helpers::is_accepting_weakscc(types, sc)) + { + continue; + } + if (helpers::is_accepting_initial_almost_detscc(types, sc)) + { + num_iadacs_states += num; + num_iadacs++; + num_max_iadacs_states = std::max(num_max_iadacs_states, num); + continue; + } + if (helpers::is_accepting_detscc(types, sc)) { num_dacs_states += num; num_dacs++; num_max_dacs_states = std::max(num_max_dacs_states, num); + continue; } if (helpers::is_accepting_nondetscc(types, sc)) { num_nacs_states += num; num_nacs++; num_max_nacs_states = std::max(num_max_nacs_states, num); + continue; } + + throw std::runtime_error("Invalid accepting SCC on the input"); } std::cout << "Number of IWCs: " << num_iwcs << " with " << num_iwcs_states << " states, in which max IWC with " << num_max_iwcs_states << " states\n"; std::cout << "Number of ACC_IWCs: " << num_acc_iwcs << " with " << num_acciwcs_states << " states, in which max IWC with " << num_max_acciwcs_states << " states\n"; + std::cout << "Number of IADACs: " << num_iadacs << " with " << num_iadacs_states << " states, in which max IADAC with " << num_max_iadacs_states << " states\n"; std::cout << "Number of DACs: " << num_dacs << " with " << num_dacs_states << " states, in which max DAC with " << num_max_dacs_states << " states\n"; std::cout << "Number of NACs: " << num_nacs << " with " << num_nacs_states << " states, in which max NAC with " << num_max_nacs_states << " states\n"; }