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 450f38f74d
commit bc61b7c30b
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;
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);
~ratexp_to_dfa();
@ -117,6 +117,7 @@ namespace spot
typedef robin_hood::unordered_node_map<formula, labelled_aut> f2a_t;
std::vector<labelled_aut> 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);

2
spot/twaalgos/ltl2tgba_fm.hh
View file

@ -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);
}