diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index 2f5fd9af0..aa61ce8e7 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -32,7 +32,7 @@ #include #include #include -#include + namespace spot { @@ -607,9 +607,9 @@ namespace spot } twa_graph_ptr - tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation, - bool pretty_print, bool scc_opt, bool use_bisimulation, - bool complete, bool use_stutter) + tgba_determinisation(const const_twa_graph_ptr& a, + bool pretty_print, bool scc_opt, + bool use_bisimulation, bool use_stutter) { // Degeneralize twa_graph_ptr aut = spot::degeneralize_tba(a); @@ -729,12 +729,8 @@ namespace spot res->prop_deterministic(true); res->prop_state_acc(false); - if (bisimulation) - res = simulation(res); if (pretty_print) res->set_named_prop("state-names", print_debug(seen)); - if (complete) - spot::complete_here(res); return res; } } diff --git a/spot/twaalgos/determinize.hh b/spot/twaalgos/determinize.hh index 608846cc6..db9234b7b 100644 --- a/spot/twaalgos/determinize.hh +++ b/spot/twaalgos/determinize.hh @@ -25,10 +25,8 @@ namespace spot { SPOT_API twa_graph_ptr tgba_determinisation(const const_twa_graph_ptr& aut, - bool bisimulation = false, bool pretty_print = false, bool scc_opt = false, bool use_bisimulation = false, - bool complete = false, bool use_stutter = false); } diff --git a/tests/core/safra.cc b/tests/core/safra.cc index 2e6adf90e..05fca6157 100644 --- a/tests/core/safra.cc +++ b/tests/core/safra.cc @@ -20,15 +20,17 @@ #include #include -#include "spot/tl/parse.hh" // spot::parse_infix_psl -#include "spot/tl/formula.hh" // spot::formula -#include "spot/parseaut/public.hh" -#include "spot/twa/twagraph.hh" -#include "spot/twaalgos/degen.hh" -#include "spot/twaalgos/dot.hh" // print_dot -#include "spot/twaalgos/hoa.hh" // print_hoa -#include "spot/twaalgos/determinize.hh" -#include "spot/twaalgos/translate.hh" +#include // spot::parse_infix_psl +#include // spot::formula +#include +#include +#include +#include // print_dot +#include // print_hoa +#include +#include +#include +#include int help(); @@ -117,18 +119,23 @@ int main(int argc, char* argv[]) spot::translator trans(dict); trans.set_pref(spot::postprocessor::Deterministic); auto tmp = trans.run(f); - res = spot::tgba_determinisation(tmp, sim, pretty_print, scc_opt, - use_bisim, complete, use_stutter); + res = spot::tgba_determinisation(tmp, pretty_print, scc_opt, + use_bisim, use_stutter); } else if (in_hoa) { auto aut = spot::parse_aut(input, dict); if (aut->format_errors(std::cerr)) return 2; - res = tgba_determinisation(aut->aut, sim, pretty_print, scc_opt, - use_bisim, complete, use_stutter); + res = tgba_determinisation(aut->aut, pretty_print, scc_opt, + use_bisim, use_stutter); } - res->merge_edges(); + if (sim) + res = simulation(res); + else + res->merge_edges(); + if (complete) + spot::complete_here(res); if (out_hoa) {