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

* src/tgbaalgos/reductgba_sim_del.cc

Browse source 
(parity_game_graph_delayed::get_relation): Disable for generalized
automata, it's wrong.
This commit is contained in:
Alexandre Duret-Lutz 2005-06-06 13:53:56 +00:00
parent fc4f4f7288
commit 8a5fd909b3
3 changed files with 12 additions and 46 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,3 +1,9 @@
2005-06-06 Alexandre Duret-Lutz <adl@src.lip6.fr>
* 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 <adl@src.lip6.fr> 2005-05-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/reductgba_sim_del.cc * src/tgbaalgos/reductgba_sim_del.cc

3
src/tgbaalgos/reductgba_sim.hh
View file

@ -69,8 +69,7 @@ namespace spot
int opt = -1); int opt = -1);
/// Compute a delayed simulation relation on state of tgba \a f. /// Compute a delayed simulation relation on state of tgba \a f.
// FIXME: This method is correct but it builds sometime (when there are more /// \bug Does not work for generalized automata.
// than one acceptance condition) only a part of the simulation relation.
delayed_simulation_relation* get_delayed_relation_simulation(const tgba* a, delayed_simulation_relation* get_delayed_relation_simulation(const tgba* a,
std::ostream& os, std::ostream& os,
int opt = -1); int opt = -1);

47
src/tgbaalgos/reductgba_sim_del.cc
View file

@ -28,6 +28,7 @@ namespace spot
/// The one priority is represent by a \a acceptance_condition_visited_ /// The one priority is represent by a \a acceptance_condition_visited_
/// which differ of bddfalse. /// which differ of bddfalse.
/// This spoiler node are looser for the duplicator. /// This spoiler node are looser for the duplicator.
/// FIXME: get rid of these ugly globals
static int nb_spoiler_loose_; static int nb_spoiler_loose_;
static int nb_spoiler; static int nb_spoiler;
@ -549,48 +550,7 @@ namespace spot
void void
parity_game_graph_delayed::lift() 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<duplicator_node*>::iterator i
= duplicator_vertice_.begin();
i != duplicator_vertice_.end(); ++i)
{
/*
for (std::vector<duplicator_node*>::iterator i2
= duplicator_vertice_.begin();
i2 != duplicator_vertice_.end(); ++i2)
dynamic_cast<duplicator_node_delayed*>(*i2)->seen_ = false;
for (std::vector<spoiler_node*>::iterator i3
= spoiler_vertice_.begin();
i3 != spoiler_vertice_.end(); ++i3)
dynamic_cast<spoiler_node_delayed*>(*i3)->seen_ = false;
*/
dynamic_cast<duplicator_node_delayed*>(*i)->set_lead_2_acc_all();
}
for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i)
{
/*
for (std::vector<duplicator_node*>::iterator i2
= duplicator_vertice_.begin();
i2 != duplicator_vertice_.end(); ++i2)
dynamic_cast<duplicator_node_delayed*>(*i2)->seen_ = false;
for (std::vector<spoiler_node*>::iterator i3
= spoiler_vertice_.begin();
i3 != spoiler_vertice_.end(); ++i3)
dynamic_cast<spoiler_node_delayed*>(*i3)->seen_ = false;
*/
dynamic_cast<spoiler_node_delayed*>(*i)->set_lead_2_acc_all();
}
}
// Jurdzinski's algorithm // Jurdzinski's algorithm
//int iter = 0;
bool change = true; bool change = true;
while (change) while (change)
@ -620,10 +580,11 @@ namespace spot
state_couple* p = 0; state_couple* p = 0;
seen_map::iterator j; seen_map::iterator j;
/* // 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) if (this->nb_set_acc_cond() > 1)
return rel; return rel;
*/
for (std::vector<spoiler_node*>::iterator i for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin(); = spoiler_vertice_.begin();