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 d410435adc
commit 2c4f85f687
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

@ -107,7 +107,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::tuple<const_twa_graph_ptr, const namer*, const state*> std::tuple<const_twa_graph_ptr, const namer*, const state*>
succ(formula f); succ(formula f);
~ratexp_to_dfa(); ~ratexp_to_dfa();
@ -122,6 +122,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
@ -907,8 +908,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)
{ {
} }
@ -961,6 +963,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
@ -2222,7 +2230,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);
@ -2230,7 +2238,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

@ -90,5 +90,5 @@ namespace spot
const output_aborter* aborter = nullptr); const output_aborter* aborter = nullptr);
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);
} }