diff --git a/ChangeLog b/ChangeLog index 7dc7d4dab..ab420218e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,9 @@ +2005-06-06 Alexandre Duret-Lutz + + * src/tgbaalgos/reductgba_sim_del.cc + (parity_game_graph_delayed::get_relation): Disable for generalized + automata, it's wrong. + 2005-05-25 Alexandre Duret-Lutz * src/tgbaalgos/reductgba_sim_del.cc diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh index ce166a2e0..bb33e70aa 100644 --- a/src/tgbaalgos/reductgba_sim.hh +++ b/src/tgbaalgos/reductgba_sim.hh @@ -69,8 +69,7 @@ namespace spot int opt = -1); /// Compute a delayed simulation relation on state of tgba \a f. - // FIXME: This method is correct but it builds sometime (when there are more - // than one acceptance condition) only a part of the simulation relation. + /// \bug Does not work for generalized automata. delayed_simulation_relation* get_delayed_relation_simulation(const tgba* a, std::ostream& os, int opt = -1); diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc index 3890ca387..88e03e489 100644 --- a/src/tgbaalgos/reductgba_sim_del.cc +++ b/src/tgbaalgos/reductgba_sim_del.cc @@ -28,6 +28,7 @@ namespace spot /// The one priority is represent by a \a acceptance_condition_visited_ /// which differ of bddfalse. /// This spoiler node are looser for the duplicator. + /// FIXME: get rid of these ugly globals static int nb_spoiler_loose_; static int nb_spoiler; @@ -549,48 +550,7 @@ namespace spot void parity_game_graph_delayed::lift() { - // Before the lift we compute each vertices - // to know if he belong to a all accepting cycle - // of the graph. - - if (this->nb_set_acc_cond() > 1) - { - for (std::vector::iterator i - = duplicator_vertice_.begin(); - i != duplicator_vertice_.end(); ++i) - { - /* - for (std::vector::iterator i2 - = duplicator_vertice_.begin(); - i2 != duplicator_vertice_.end(); ++i2) - dynamic_cast(*i2)->seen_ = false; - for (std::vector::iterator i3 - = spoiler_vertice_.begin(); - i3 != spoiler_vertice_.end(); ++i3) - dynamic_cast(*i3)->seen_ = false; - */ - dynamic_cast(*i)->set_lead_2_acc_all(); - } - for (std::vector::iterator i - = spoiler_vertice_.begin(); - i != spoiler_vertice_.end(); ++i) - { - /* - for (std::vector::iterator i2 - = duplicator_vertice_.begin(); - i2 != duplicator_vertice_.end(); ++i2) - dynamic_cast(*i2)->seen_ = false; - for (std::vector::iterator i3 - = spoiler_vertice_.begin(); - i3 != spoiler_vertice_.end(); ++i3) - dynamic_cast(*i3)->seen_ = false; - */ - dynamic_cast(*i)->set_lead_2_acc_all(); - } - } - // Jurdzinski's algorithm - //int iter = 0; bool change = true; while (change) @@ -620,10 +580,11 @@ namespace spot state_couple* p = 0; seen_map::iterator j; - /* - if (this->nb_set_acc_cond() > 1) + // This does not work for generalized automata. A tarjan-like + // algorithm is required to tell whether a state can lead to an + // acceptance cycle. + if (this->nb_set_acc_cond() > 1) return rel; - */ for (std::vector::iterator i = spoiler_vertice_.begin();