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

translate_aa: Factorize sere translation choice

Browse source 
* spot/twaalgos/translate_aa.cc: Here.
This commit is contained in:
Antoine Martin 2025-10-10 16:49:34 +02:00
parent e53bd32631
commit 514ef110f2
1 changed files with 16 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

48
spot/twaalgos/translate_aa.cc
View file

@ -34,6 +34,20 @@ namespace spot
{ {
namespace namespace
{ {
twa_graph_ptr sere_aa_translate(formula f, const bdd_dict_ptr& dict)
{
// old bdd method
if (sere_aa_translation_options() == 0)
return sere_to_tgba(f, dict, true);
// derivation
if (sere_aa_translation_options() == 1)
return derive_finite_automaton_with_first(f, dict);
// linear form
return expand_finite_automaton(f, dict, exp_opts::expand_opt::None);
}
struct ltl_to_aa_builder struct ltl_to_aa_builder
{ {
ltl_to_aa_builder(twa_graph_ptr aut, unsigned accepting_sink) ltl_to_aa_builder(twa_graph_ptr aut, unsigned accepting_sink)
@ -289,22 +303,7 @@ namespace spot
{ {
unsigned rhs_init = recurse(f[1]); unsigned rhs_init = recurse(f[1]);
const auto& dict = aut_->get_dict(); const auto& dict = aut_->get_dict();
twa_graph_ptr sere_aut; twa_graph_ptr sere_aut = sere_aa_translate(f[0], dict);
if (sere_aa_translation_options() == 0)
{
// old bdd method
sere_aut = sere_to_tgba(f[0], dict, true);
}
else if (sere_aa_translation_options() == 1)
{
// derivation
sere_aut = derive_finite_automaton_with_first(f[0], dict);
}
else
{
// linear form
sere_aut = expand_finite_automaton(f[0], dict, exp_opts::expand_opt::None);
}
// TODO: this should be a std::vector<bool> ! // TODO: this should be a std::vector<bool> !
std::vector<unsigned> acc_states; std::vector<unsigned> acc_states;
@ -345,22 +344,7 @@ namespace spot
{ {
unsigned rhs_init = recurse(f[1]); unsigned rhs_init = recurse(f[1]);
const auto& dict = aut_->get_dict(); const auto& dict = aut_->get_dict();
twa_graph_ptr sere_aut; twa_graph_ptr sere_aut = sere_aa_translate(f[0], dict);
if (sere_aa_translation_options() == 0)
{
// old bdd method
sere_aut = sere_to_tgba(f[0], dict, true);
}
else if (sere_aa_translation_options() == 1)
{
// derivation
sere_aut = derive_finite_automaton_with_first(f[0], dict);
}
else
{
// linear form
sere_aut = expand_finite_automaton(f[0], dict, exp_opts::expand_opt::None);
}
// DFA recognizes the empty language, so {0} []-> rhs is always true // DFA recognizes the empty language, so {0} []-> rhs is always true
unsigned ns = sere_aut->num_states(); unsigned ns = sere_aut->num_states();