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

Correct CAR when we use apply_to_Buchi

Browse source 
* spot/twaalgos/car.cc: Correct the colors producted in apply_to_Buchi.
This commit is contained in:
Florian Renkin 2020-02-24 14:58:11 +01:00
parent a62241376f
commit f4c201c980
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/twaalgos/car.cc
View file

@ -686,7 +686,7 @@ public:
names->push_back(new_car.to_string( names->push_back(new_car.to_string(
is_streett_to_buchi ? Streett_to_Buchi : Rabin_to_Buchi)); is_streett_to_buchi ? Streett_to_Buchi : Rabin_to_Buchi));
} }
auto g = sub_automaton->get_graph(); auto g = buchi->get_graph();
for (unsigned s = 0; s < buchi->num_states(); ++s) for (unsigned s = 0; s < buchi->num_states(); ++s)
{ {
unsigned b = g.state_storage(s).succ; unsigned b = g.state_storage(s).succ;
@ -701,7 +701,7 @@ public:
dst = { (*init_states)[e.dst], e.dst, perm_t() }; dst = { (*init_states)[e.dst], e.dst, perm_t() };
unsigned src_state = car2num[src], unsigned src_state = car2num[src],
dst_state = car2num[dst]; dst_state = car2num[dst];
auto col = ((int) acc.min_set()) - 1; int col = ((int) acc.max_set()) - 1;
if (col > (int) max_free_color) if (col > (int) max_free_color)
throw std::runtime_error("CAR needs more sets"); throw std::runtime_error("CAR needs more sets");
auto& e2 = sub_automaton->get_graph().edge_storage(b); auto& e2 = sub_automaton->get_graph().edge_storage(b);