diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 838db28be..dd7bb9182 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -102,7 +102,7 @@ namespace spot { typedef twa_graph::namer namer; public: - ratexp_to_dfa(translate_dict& dict); + ratexp_to_dfa(translate_dict& dict, bool disable_scc_trimming = false); std::vector> succ(formula f); ~ratexp_to_dfa(); @@ -117,6 +117,7 @@ namespace spot typedef robin_hood::unordered_node_map f2a_t; std::vector automata_; f2a_t f2a_; + bool disable_scc_trimming_; }; // Helper dictionary. We represent formulae using BDDs to @@ -902,8 +903,9 @@ namespace spot } - ratexp_to_dfa::ratexp_to_dfa(translate_dict& dict) + ratexp_to_dfa::ratexp_to_dfa(translate_dict& dict, bool disable_scc_trimming) : dict_(dict) + , disable_scc_trimming_(disable_scc_trimming) { } @@ -956,6 +958,12 @@ namespace spot } } + if (disable_scc_trimming_) + { + automata_.emplace_back(a, namer); + return labelled_aut(a, namer); + } + // The following code trims the automaton in a crude way by // eliminating SCCs that are not coaccessible. It does not // actually remove the states, it simply marks the corresponding @@ -2181,7 +2189,7 @@ namespace spot } twa_graph_ptr - sere_to_tgba(formula f, const bdd_dict_ptr& dict) + sere_to_tgba(formula f, const bdd_dict_ptr& dict, bool disable_scc_trimming) { f = negative_normal_form(f); @@ -2189,7 +2197,7 @@ namespace spot twa_graph_ptr a = make_twa_graph(dict); translate_dict d(a, s, false, false, false); - ratexp_to_dfa sere2dfa(d); + ratexp_to_dfa sere2dfa(d, disable_scc_trimming); auto [dfa, namer, state] = sere2dfa.succ(f); diff --git a/spot/twaalgos/ltl2tgba_fm.hh b/spot/twaalgos/ltl2tgba_fm.hh index 7dba4aee0..51de038e1 100644 --- a/spot/twaalgos/ltl2tgba_fm.hh +++ b/spot/twaalgos/ltl2tgba_fm.hh @@ -91,5 +91,5 @@ namespace spot bool label_with_ltl = false); SPOT_API twa_graph_ptr - sere_to_tgba(formula f, const bdd_dict_ptr& dict); + sere_to_tgba(formula f, const bdd_dict_ptr& dict, bool disable_scc_trimming = false); }