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

ltl2aa: share dict between sere and final aut

Browse source
This commit is contained in:
Antoine Martin 2022-09-06 16:07:28 +02:00
parent c1a0b5aa46
commit 85b8717c05
3 changed files with 18 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

10
spot/tl/derive.cc
View file

@ -203,9 +203,9 @@ namespace spot
} }
twa_graph_ptr twa_graph_ptr
derive_finite_automaton_with_first(formula f, bool deterministic) derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
bool deterministic)
{ {
auto bdd_dict = make_bdd_dict();
auto aut = make_twa_graph(bdd_dict); auto aut = make_twa_graph(bdd_dict);
aut->prop_state_acc(true); aut->prop_state_acc(true);
@ -403,9 +403,11 @@ namespace spot
} }
twa_graph_ptr twa_graph_ptr
derive_automaton_with_first(formula f, bool deterministic) derive_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
bool deterministic)
{ {
auto finite = derive_finite_automaton_with_first(f, deterministic); auto finite = derive_finite_automaton_with_first(f, bdd_dict,
deterministic);
return from_finite(finite); return from_finite(finite);
} }

6
spot/tl/derive.hh
View file

@ -39,13 +39,15 @@ namespace spot
derive_automaton(formula f, bool deterministic = true); derive_automaton(formula f, bool deterministic = true);
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
derive_automaton_with_first(formula f, bool deterministic = true); derive_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
bool deterministic = true);
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
derive_finite_automaton(formula f, bool deterministic = true); derive_finite_automaton(formula f, bool deterministic = true);
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
derive_finite_automaton_with_first(formula f, bool deterministic = true); derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
bool deterministic = true);
SPOT_API formula SPOT_API formula
rewrite_and_nlm(formula f); rewrite_and_nlm(formula f);

10
spot/twaalgos/translate_aa.cc
View file

@ -39,6 +39,11 @@ namespace spot
{ {
} }
~ltl_to_aa_builder()
{
aut_->get_dict()->unregister_all_my_variables(this);
}
twa_graph_ptr aut_; twa_graph_ptr aut_;
unsigned accepting_sink_; unsigned accepting_sink_;
internal::univ_dest_mapper<twa_graph::graph_t> uniq_; internal::univ_dest_mapper<twa_graph::graph_t> uniq_;
@ -241,9 +246,9 @@ namespace spot
{ {
// FIXME: combine out edges with rhs ! // FIXME: combine out edges with rhs !
//unsigned rhs_init = recurse(f[1]); //unsigned rhs_init = recurse(f[1]);
twa_graph_ptr sere_aut = derive_finite_automaton_with_first(f[0]); const auto& dict = aut_->get_dict();
twa_graph_ptr sere_aut = derive_finite_automaton_with_first(f[0], dict);
const auto& dict = sere_aut->get_dict();
std::map<unsigned, unsigned> old_to_new; std::map<unsigned, unsigned> old_to_new;
std::map<unsigned, int> state_to_var; std::map<unsigned, int> state_to_var;
@ -271,6 +276,7 @@ namespace spot
return p.first->second; return p.first->second;
}; };
aut_->copy_ap_of(sere_aut);
unsigned ns = sere_aut->num_states(); unsigned ns = sere_aut->num_states();
for (unsigned st = 0; st < ns; ++st) for (unsigned st = 0; st < ns; ++st)
{ {