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

* sanity/style.test: Catch misuses of Sgi::.

Browse source 
* tgba/tgbareduc.hh, tgbaalgos/reductgba_sim.cc,
tgbaalgos/reductgba_sim.hh, tgbaalgos/reductgba_sim_del.cc: Fix them.
This commit is contained in:
Alexandre Duret-Lutz 2005-05-25 08:56:15 +00:00
parent 64d5de8fe1
commit 35aa277164
6 changed files with 56 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,3 +1,9 @@
2005-05-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
* sanity/style.test: Catch misuses of Sgi::.
* tgba/tgbareduc.hh, tgbaalgos/reductgba_sim.cc,
tgbaalgos/reductgba_sim.hh, tgbaalgos/reductgba_sim_del.cc: Fix them.
2005-05-16 Denis Poitrenaud <dp@src.lip6.fr> 2005-05-16 Denis Poitrenaud <dp@src.lip6.fr>
* src/ltlvisit/syntimpl.cc: Fix a typo. * src/ltlvisit/syntimpl.cc: Fix a typo.

6
src/sanity/style.test
View file

@ -146,6 +146,12 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
grep '[^a-zA-Z0-9_](\*[a-zA-Z0-9_]*)\.' $tmp && grep '[^a-zA-Z0-9_](\*[a-zA-Z0-9_]*)\.' $tmp &&
diag 'Use "x->y", not "(*x).y"' diag 'Use "x->y", not "(*x).y"'
grep 'std::hash' $tmp &&
diag 'use Sgi:: for hash and hash_map'
grep 'Sgi::[^h]' $tmp &&
diag 'Sgi:: is for hash and hash_map only'
res=`perl -ne '$/ = undef; res=`perl -ne '$/ = undef;
print "$&\n" print "$&\n"
while /if \((.*)(\s*==\s*0)?\)\s*delete(\[\])?\s+\1;(?!\s+else)/g' $tmp` while /if \((.*)(\s*==\s*0)?\)\s*delete(\[\])?\s+\1;(?!\s+else)/g' $tmp`

8
src/tgba/tgbareduc.hh
View file

@ -31,12 +31,12 @@
namespace spot namespace spot
{ {
typedef Sgi::pair<const spot::state*, const spot::state*> state_couple; typedef std::pair<const spot::state*, const spot::state*> state_couple;
typedef Sgi::vector<state_couple*> simulation_relation; typedef std::vector<state_couple*> simulation_relation;
/* /*
typedef Sgi::vector<state_couple*> direct_simulation_relation; typedef std::vector<state_couple*> direct_simulation_relation;
typedef Sgi::vector<state_couple*> delayed_simulation_relation; typedef std::vector<state_couple*> delayed_simulation_relation;
*/ */
class direct_simulation_relation: public simulation_relation class direct_simulation_relation: public simulation_relation

46
src/tgbaalgos/reductgba_sim.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -97,13 +97,13 @@ namespace spot
spoiler_node::set_win() spoiler_node::set_win()
{ {
bool change = not_win; bool change = not_win;
for (Sgi::vector<spoiler_node*>::iterator i = lnode_succ->begin(); for (std::vector<spoiler_node*>::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i) i != lnode_succ->end(); ++i)
{ {
not_win |= (*i)->not_win; not_win |= (*i)->not_win;
} }
if (change != not_win) if (change != not_win)
for (Sgi::vector<spoiler_node*>::iterator i = lnode_pred->begin(); for (std::vector<spoiler_node*>::iterator i = lnode_pred->begin();
i != lnode_pred->end(); ++i) i != lnode_pred->end(); ++i)
(*i)->set_win(); (*i)->set_win();
@ -195,14 +195,14 @@ namespace spot
else else
{ {
not_win = true; not_win = true;
for (Sgi::vector<spoiler_node*>::iterator i = lnode_succ->begin(); for (std::vector<spoiler_node*>::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i) i != lnode_succ->end(); ++i)
{ {
not_win &= (*i)->not_win; not_win &= (*i)->not_win;
} }
} }
if (change != not_win) if (change != not_win)
for (Sgi::vector<spoiler_node*>::iterator i = lnode_pred->begin(); for (std::vector<spoiler_node*>::iterator i = lnode_pred->begin();
i != lnode_pred->end(); ++i) i != lnode_pred->end(); ++i)
(*i)->set_win(); (*i)->set_win();
@ -292,8 +292,8 @@ namespace spot
void void
parity_game_graph::print(std::ostream& os) parity_game_graph::print(std::ostream& os)
{ {
Sgi::vector<spoiler_node*>::iterator i1; std::vector<spoiler_node*>::iterator i1;
Sgi::vector<duplicator_node*>::iterator i2; std::vector<duplicator_node*>::iterator i2;
int n = 0; int n = 0;
@ -359,8 +359,8 @@ namespace spot
parity_game_graph::~parity_game_graph() parity_game_graph::~parity_game_graph()
{ {
Sgi::vector<spoiler_node*>::iterator i1; std::vector<spoiler_node*>::iterator i1;
Sgi::vector<duplicator_node*>::iterator i2; std::vector<duplicator_node*>::iterator i2;
for (i1 = spoiler_vertice_.begin(); for (i1 = spoiler_vertice_.begin();
i1 != spoiler_vertice_.end(); ++i1) i1 != spoiler_vertice_.end(); ++i1)
@ -392,18 +392,18 @@ namespace spot
parity_game_graph_direct::build_graph() parity_game_graph_direct::build_graph()
{ {
tgba_succ_iterator* si = 0; tgba_succ_iterator* si = 0;
typedef Sgi::pair<bdd, bdd> couple_bdd; typedef std::pair<bdd, bdd> couple_bdd;
couple_bdd *p = 0; couple_bdd *p = 0;
Sgi::vector<couple_bdd*>* trans = 0; std::vector<couple_bdd*>* trans = 0;
bool exist = false; bool exist = false;
spot::state* s = 0; spot::state* s = 0;
for (Sgi::vector<const state*>::iterator i = tgba_state_.begin(); for (std::vector<const state*>::iterator i = tgba_state_.begin();
i != tgba_state_.end(); ++i) i != tgba_state_.end(); ++i)
{ {
// spoiler node are all state couple (i,j) // spoiler node are all state couple (i,j)
for (Sgi::vector<const state*>::iterator j = tgba_state_.begin(); for (std::vector<const state*>::iterator j = tgba_state_.begin();
j != tgba_state_.end(); ++j) j != tgba_state_.end(); ++j)
{ {
spoiler_node* n1 = new spoiler_node(*i, spoiler_node* n1 = new spoiler_node(*i,
@ -414,8 +414,8 @@ namespace spot
// duplicator node are all state couple where // duplicator node are all state couple where
// the first state i are reachable. // the first state i are reachable.
trans = new Sgi::vector<couple_bdd*>; trans = new std::vector<couple_bdd*>;
for (Sgi::vector<const state*>::iterator j = tgba_state_.begin(); for (std::vector<const state*>::iterator j = tgba_state_.begin();
j != tgba_state_.end(); ++j) j != tgba_state_.end(); ++j)
{ {
si = automata_->succ_iter(*j); si = automata_->succ_iter(*j);
@ -434,7 +434,7 @@ namespace spot
// If an other predecessor of i has the same label p // If an other predecessor of i has the same label p
// to reach i, then we don't compute the duplicator node. // to reach i, then we don't compute the duplicator node.
exist = false; exist = false;
for (Sgi::vector<couple_bdd*>::iterator v for (std::vector<couple_bdd*>::iterator v
= trans->begin(); = trans->begin();
v != trans->end(); ++v) v != trans->end(); ++v)
{ {
@ -448,7 +448,7 @@ namespace spot
{ {
// We build all the state couple with the label p. // We build all the state couple with the label p.
trans->push_back(p); trans->push_back(p);
for (Sgi::vector<const state*>::iterator s for (std::vector<const state*>::iterator s
= tgba_state_.begin(); = tgba_state_.begin();
s != tgba_state_.end(); ++s) s != tgba_state_.end(); ++s)
{ {
@ -470,7 +470,7 @@ namespace spot
} }
delete si; delete si;
} }
Sgi::vector<couple_bdd*>::iterator i2; std::vector<couple_bdd*>::iterator i2;
for (i2 = trans->begin(); i2 != trans->end(); ++i2) for (i2 = trans->begin(); i2 != trans->end(); ++i2)
{ {
delete *i2; delete *i2;
@ -487,10 +487,10 @@ namespace spot
spot::state* s = 0; spot::state* s = 0;
// for each couple of (spoiler, duplicator) // for each couple of (spoiler, duplicator)
for (Sgi::vector<spoiler_node*>::iterator i for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i) = spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i)
{ {
for (Sgi::vector<duplicator_node*>::iterator j for (std::vector<duplicator_node*>::iterator j
= duplicator_vertice_.begin(); = duplicator_vertice_.begin();
j != duplicator_vertice_.end(); ++j) j != duplicator_vertice_.end(); ++j)
{ {
@ -547,13 +547,13 @@ namespace spot
while (change) while (change)
{ {
change = false; change = false;
for (Sgi::vector<duplicator_node*>::iterator i for (std::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin(); = duplicator_vertice_.begin();
i != duplicator_vertice_.end(); ++i) i != duplicator_vertice_.end(); ++i)
{ {
change |= (*i)->set_win(); change |= (*i)->set_win();
} }
for (Sgi::vector<spoiler_node*>::iterator i for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin(); = spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i) i != spoiler_vertice_.end(); ++i)
{ {
@ -569,7 +569,7 @@ namespace spot
state_couple* p = 0; state_couple* p = 0;
seen_map::iterator j; seen_map::iterator j;
for (Sgi::vector<spoiler_node*>::iterator i for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin(); = spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i) i != spoiler_vertice_.end(); ++i)
{ {

8
src/tgbaalgos/reductgba_sim.hh
View file

@ -86,9 +86,9 @@ namespace spot
class spoiler_node; class spoiler_node;
class duplicator_node; class duplicator_node;
typedef Sgi::vector<spoiler_node*> sn_v; typedef std::vector<spoiler_node*> sn_v;
typedef Sgi::vector<duplicator_node*> dn_v; typedef std::vector<duplicator_node*> dn_v;
typedef Sgi::vector<const state*> s_v; typedef std::vector<const state*> s_v;
/// \brief Parity game graph which compute a simulation relation. /// \brief Parity game graph which compute a simulation relation.
class parity_game_graph : public tgba_reachable_iterator_breadth_first class parity_game_graph : public tgba_reachable_iterator_breadth_first
@ -297,7 +297,7 @@ namespace spot
/// Vector which contain all the sub-set of the set /// Vector which contain all the sub-set of the set
/// of acceptance condition. /// of acceptance condition.
typedef Sgi::vector<bdd> bdd_v; typedef std::vector<bdd> bdd_v;
bdd_v sub_set_acc_cond_; bdd_v sub_set_acc_cond_;
/// Return the number of acceptance condition. /// Return the number of acceptance condition.

26
src/tgbaalgos/reductgba_sim_del.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -35,7 +35,7 @@ namespace spot
static bdd all_acc_cond = bddfalse; static bdd all_acc_cond = bddfalse;
static Sgi::vector<bool*> bool_v; static std::vector<bool*> bool_v;
//static int nb_node = 0; //static int nb_node = 0;
@ -505,7 +505,7 @@ namespace spot
duplicator_node_delayed* dn_n duplicator_node_delayed* dn_n
= new duplicator_node_delayed(sn, dn, acc, label, nb); = new duplicator_node_delayed(sn, dn, acc, label, nb);
for (Sgi::vector<duplicator_node*>::iterator i for (std::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin(); = duplicator_vertice_.begin();
i != duplicator_vertice_.end(); ++i) i != duplicator_vertice_.end(); ++i)
{ {
@ -536,7 +536,7 @@ namespace spot
spoiler_node_delayed* sn_n spoiler_node_delayed* sn_n
= new spoiler_node_delayed(sn, dn, acc, nb); = new spoiler_node_delayed(sn, dn, acc, nb);
for (Sgi::vector<spoiler_node*>::iterator i for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin(); = spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i) i != spoiler_vertice_.end(); ++i)
{ {
@ -564,32 +564,32 @@ namespace spot
if (this->nb_set_acc_cond() > 1) if (this->nb_set_acc_cond() > 1)
{ {
for (Sgi::vector<duplicator_node*>::iterator i for (std::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin(); = duplicator_vertice_.begin();
i != duplicator_vertice_.end(); ++i) i != duplicator_vertice_.end(); ++i)
{ {
/* /*
for (Sgi::vector<duplicator_node*>::iterator i2 for (std::vector<duplicator_node*>::iterator i2
= duplicator_vertice_.begin(); = duplicator_vertice_.begin();
i2 != duplicator_vertice_.end(); ++i2) i2 != duplicator_vertice_.end(); ++i2)
dynamic_cast<duplicator_node_delayed*>(*i2)->seen_ = false; dynamic_cast<duplicator_node_delayed*>(*i2)->seen_ = false;
for (Sgi::vector<spoiler_node*>::iterator i3 for (std::vector<spoiler_node*>::iterator i3
= spoiler_vertice_.begin(); = spoiler_vertice_.begin();
i3 != spoiler_vertice_.end(); ++i3) i3 != spoiler_vertice_.end(); ++i3)
dynamic_cast<spoiler_node_delayed*>(*i3)->seen_ = false; dynamic_cast<spoiler_node_delayed*>(*i3)->seen_ = false;
*/ */
dynamic_cast<duplicator_node_delayed*>(*i)->set_lead_2_acc_all(); dynamic_cast<duplicator_node_delayed*>(*i)->set_lead_2_acc_all();
} }
for (Sgi::vector<spoiler_node*>::iterator i for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin(); = spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i) i != spoiler_vertice_.end(); ++i)
{ {
/* /*
for (Sgi::vector<duplicator_node*>::iterator i2 for (std::vector<duplicator_node*>::iterator i2
= duplicator_vertice_.begin(); = duplicator_vertice_.begin();
i2 != duplicator_vertice_.end(); ++i2) i2 != duplicator_vertice_.end(); ++i2)
dynamic_cast<duplicator_node_delayed*>(*i2)->seen_ = false; dynamic_cast<duplicator_node_delayed*>(*i2)->seen_ = false;
for (Sgi::vector<spoiler_node*>::iterator i3 for (std::vector<spoiler_node*>::iterator i3
= spoiler_vertice_.begin(); = spoiler_vertice_.begin();
i3 != spoiler_vertice_.end(); ++i3) i3 != spoiler_vertice_.end(); ++i3)
dynamic_cast<spoiler_node_delayed*>(*i3)->seen_ = false; dynamic_cast<spoiler_node_delayed*>(*i3)->seen_ = false;
@ -606,13 +606,13 @@ namespace spot
{ {
//std::cout << "lift::change = true" << std::endl; //std::cout << "lift::change = true" << std::endl;
change = false; change = false;
for (Sgi::vector<duplicator_node*>::iterator i for (std::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin(); = duplicator_vertice_.begin();
i != duplicator_vertice_.end(); ++i) i != duplicator_vertice_.end(); ++i)
{ {
change |= (*i)->set_win(); change |= (*i)->set_win();
} }
for (Sgi::vector<spoiler_node*>::iterator i for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin(); = spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i) i != spoiler_vertice_.end(); ++i)
{ {
@ -634,7 +634,7 @@ namespace spot
return rel; return rel;
*/ */
for (Sgi::vector<spoiler_node*>::iterator i for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin(); = spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i) i != spoiler_vertice_.end(); ++i)
{ {