alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twaalgos: ltl2tgba_fm: allow disabling SCC trim

Browse source
This commit is contained in:
Antoine Martin 2023-03-06 18:37:44 +01:00
parent b5f11f7366
commit 382c57923c
2 changed files with 13 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

16
spot/twaalgos/ltl2tgba_fm.cc
View file

@ -102,7 +102,7 @@ namespace spot
{ {
typedef twa_graph::namer<formula> namer; typedef twa_graph::namer<formula> namer;
public: public:
ratexp_to_dfa(translate_dict& dict); ratexp_to_dfa(translate_dict& dict, bool disable_scc_trimming = false);
std::vector<std::pair<bdd, formula>> succ(formula f); std::vector<std::pair<bdd, formula>> succ(formula f);
~ratexp_to_dfa(); ~ratexp_to_dfa();
@ -117,6 +117,7 @@ namespace spot
typedef robin_hood::unordered_node_map<formula, labelled_aut> f2a_t; typedef robin_hood::unordered_node_map<formula, labelled_aut> f2a_t;
std::vector<labelled_aut> automata_; std::vector<labelled_aut> automata_;
f2a_t f2a_; f2a_t f2a_;
bool disable_scc_trimming_;
}; };
// Helper dictionary. We represent formulae using BDDs to // 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) : 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 // The following code trims the automaton in a crude way by
// eliminating SCCs that are not coaccessible. It does not // eliminating SCCs that are not coaccessible. It does not
// actually remove the states, it simply marks the corresponding // actually remove the states, it simply marks the corresponding
@ -2181,7 +2189,7 @@ namespace spot
} }
twa_graph_ptr 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); f = negative_normal_form(f);
@ -2189,7 +2197,7 @@ namespace spot
twa_graph_ptr a = make_twa_graph(dict); twa_graph_ptr a = make_twa_graph(dict);
translate_dict d(a, s, false, false, false); 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); auto [dfa, namer, state] = sere2dfa.succ(f);

2
spot/twaalgos/ltl2tgba_fm.hh
View file

@ -91,5 +91,5 @@ namespace spot
bool label_with_ltl = false); bool label_with_ltl = false);
SPOT_API twa_graph_ptr 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);
} }