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

ltl2aa: handle edge case in UConcat

Browse source 
If SERE recognizes false, then combined with UConcat the property is
always true.
This commit is contained in:
Antoine Martin 2022-09-30 01:32:01 +02:00
parent 2d11d907ef
commit 8abad2b4f7
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
spot/twaalgos/translate_aa.cc
View file

@ -328,6 +328,13 @@ namespace spot
const auto& dict = aut_->get_dict(); const auto& dict = aut_->get_dict();
twa_graph_ptr sere_aut = derive_finite_automaton_with_first(f[0], dict); twa_graph_ptr sere_aut = derive_finite_automaton_with_first(f[0], dict);
// DFA recognizes the empty language, so {0} []-> rhs is always true
unsigned ns = sere_aut->num_states();
bool has_accepting_state = false;
for (unsigned st = 0; st < ns && !has_accepting_state; ++st)
has_accepting_state = sere_aut->state_is_accepting(st);
if (!has_accepting_state)
return accepting_sink_;
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;
@ -361,7 +368,6 @@ namespace spot
}; };
aut_->copy_ap_of(sere_aut); aut_->copy_ap_of(sere_aut);
unsigned ns = sere_aut->num_states();
for (unsigned st = 0; st < ns; ++st) for (unsigned st = 0; st < ns; ++st)
{ {
register_state(st); register_state(st);