Skip to content

fix: replace assertion with output_scc_info call in main function #24

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
vhavlena merged 2 commits into from
May 21, 2026
Merged

fix: replace assertion with output_scc_info call in main function #24

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
744f54a
fix: replace assertion with output_scc_info call in main function
vhavlena May 21, 2026
b8dfcb8
fix: enhance output_scc_info to track IADACs and improve SCC checks
vhavlena May 21, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 27 additions & 2 deletions src/main.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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";
}
Expand Down Expand Up @@ -359,7 +384,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);

Expand Down
Loading