From 3fb29ce1be1d046781afb1d69745b22758c8e88b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 17 Mar 2012 12:02:19 +0100 Subject: [PATCH] Typo: rename automata_ as aut_. * src/tgbaalgos/reachiter.hh, src/tgbaalgos/reachiter.cc, src/tgbaalgos/dotty.cc, src/tgbaalgos/dupexp.cc, src/tgbaalgos/lbtt.cc, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/save.cc, src/tgbaalgos/sccfilter.cc, src/tgba/tgbareduc.cc, src/evtgbaalgos/tgba2evtgba.cc, src/kripke/kripkeprint.cc: Rename automata_ as aut_. --- src/evtgbaalgos/tgba2evtgba.cc | 8 ++++---- src/kripke/kripkeprint.cc | 16 ++++++++-------- src/tgba/tgbareduc.cc | 8 ++++---- src/tgbaalgos/dotty.cc | 16 ++++++++-------- src/tgbaalgos/dupexp.cc | 6 +++--- src/tgbaalgos/lbtt.cc | 4 +++- src/tgbaalgos/neverclaim.cc | 18 +++++++++--------- src/tgbaalgos/reachiter.cc | 6 +++--- src/tgbaalgos/reachiter.hh | 4 ++-- src/tgbaalgos/reductgba_sim.cc | 10 +++++----- src/tgbaalgos/reductgba_sim_del.cc | 8 ++++---- src/tgbaalgos/save.cc | 14 +++++++------- src/tgbaalgos/sccfilter.cc | 6 +++--- 13 files changed, 63 insertions(+), 61 deletions(-) diff --git a/src/evtgbaalgos/tgba2evtgba.cc b/src/evtgbaalgos/tgba2evtgba.cc index 398a6fb20..d5d26d932 100644 --- a/src/evtgbaalgos/tgba2evtgba.cc +++ b/src/evtgbaalgos/tgba2evtgba.cc @@ -49,7 +49,7 @@ namespace spot start() { const rsymbol_set ss = - acc_to_symbol_set(automata_->all_acceptance_conditions()); + acc_to_symbol_set(aut_->all_acceptance_conditions()); for (rsymbol_set::const_iterator i = ss.begin(); i != ss.end(); ++i) res->declare_acceptance_condition(*i); } @@ -57,7 +57,7 @@ namespace spot virtual void process_state(const state* s, int n, tgba_succ_iterator*) { - std::string str = this->automata_->format_state(s); + std::string str = this->aut_->format_state(s); name_[n] = str; if (n == 1) res->set_init_state(str); @@ -90,7 +90,7 @@ namespace spot if (low == bddfalse) { const ltl::formula* v = - automata_->get_dict()->var_formula_map[bdd_var(one)]; + aut_->get_dict()->var_formula_map[bdd_var(one)]; res->add_transition(name_[in], to_string(v), ss, @@ -125,7 +125,7 @@ namespace spot if (low == bddfalse) { const ltl::formula* v = - automata_->get_dict()->acc_formula_map[bdd_var(one)]; + aut_->get_dict()->acc_formula_map[bdd_var(one)]; ss.insert(rsymbol(to_string(v))); break; } diff --git a/src/kripke/kripkeprint.cc b/src/kripke/kripkeprint.cc index eefb0046a..54525f421 100644 --- a/src/kripke/kripkeprint.cc +++ b/src/kripke/kripkeprint.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement // de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -42,11 +42,11 @@ namespace spot void process_state(const state* s, int, tgba_succ_iterator* si) { - const bdd_dict* d = automata_->get_dict(); + const bdd_dict* d = aut_->get_dict(); os_ << "\""; - escape_str(os_, automata_->format_state(s)); + escape_str(os_, aut_->format_state(s)); os_ << "\", \""; - const kripke* automata = down_cast (automata_); + const kripke* automata = down_cast (aut_); assert(automata); escape_str(os_, bdd_format_formula(d, automata->state_condition(s))); @@ -56,7 +56,7 @@ namespace spot { state* dest = si->current_state(); os_ << " \""; - escape_str(os_, automata_->format_state(dest)); + escape_str(os_, aut_->format_state(dest)); os_ << "\""; } os_ << ";\n"; @@ -89,10 +89,10 @@ namespace spot else notfirst = true; - const bdd_dict* d = automata_->get_dict(); - std::string cur = automata_->format_state(s); + const bdd_dict* d = aut_->get_dict(); + std::string cur = aut_->format_state(s); os_ << "S" << in_s << ", \""; - const kripke* automata = down_cast(automata_); + const kripke* automata = down_cast(aut_); assert(automata); escape_str(os_, bdd_format_formula(d, automata->state_condition(s))); diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc index df9424302..a014302ed 100644 --- a/src/tgba/tgbareduc.cc +++ b/src/tgba/tgbareduc.cc @@ -132,9 +132,9 @@ namespace spot void tgba_reduc::process_state(const spot::state* s, int, tgba_succ_iterator* si) { - spot::state* init = automata_->get_init_state(); + spot::state* init = aut_->get_init_state(); if (init->compare(s) == 0) - this->set_init_state(automata_->format_state(s)); + this->set_init_state(aut_->format_state(s)); init->destroy(); transition* t; @@ -152,8 +152,8 @@ namespace spot tgba_reduc::create_transition(const spot::state* source, const spot::state* dest) { - const std::string ss = automata_->format_state(source); - const std::string sd = automata_->format_state(dest); + const std::string ss = aut_->format_state(source); + const std::string sd = aut_->format_state(dest); tgba_explicit::state* s = tgba_explicit_string::add_state(ss); tgba_explicit::state* d = tgba_explicit_string::add_state(sd); diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 970d4ac91..f6be911f9 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -74,7 +74,7 @@ namespace spot si->first(); accepting = ((!si->done()) && (si->current_acceptance_conditions() == - automata_->all_acceptance_conditions())); + aut_->all_acceptance_conditions())); } } else @@ -83,8 +83,8 @@ namespace spot } os_ << " " << n << " " - << dd_->state_decl(automata_, s, n, si, - escape_str(automata_->format_state(s)), + << dd_->state_decl(aut_, s, n, si, + escape_str(aut_->format_state(s)), accepting) << '\n'; } @@ -94,13 +94,13 @@ namespace spot const state* out_s, int out, const tgba_succ_iterator* si) { std::string label = - bdd_format_formula(automata_->get_dict(), + bdd_format_formula(aut_->get_dict(), si->current_condition()) + "\n" - + bdd_format_accset(automata_->get_dict(), + + bdd_format_accset(aut_->get_dict(), si->current_acceptance_conditions()); - std::string s = automata_->transition_annotation(si); + std::string s = aut_->transition_annotation(si); if (!s.empty()) { if (*label.rbegin() != '\n') @@ -109,7 +109,7 @@ namespace spot } os_ << " " << in << " -> " << out << " " - << dd_->link_decl(automata_, in_s, in, out_s, out, si, + << dd_->link_decl(aut_, in_s, in, out_s, out, si, escape_str(label)) << '\n'; } diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc index b88127af8..16df587c1 100644 --- a/src/tgbaalgos/dupexp.cc +++ b/src/tgbaalgos/dupexp.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -53,9 +53,9 @@ namespace spot const tgba_succ_iterator* si) { std::ostringstream in_name; - in_name << "(#" << in << ") " << this->automata_->format_state(in_s); + in_name << "(#" << in << ") " << this->aut_->format_state(in_s); std::ostringstream out_name; - out_name << "(#" << out << ") " << this->automata_->format_state(out_s); + out_name << "(#" << out << ") " << this->aut_->format_state(out_s); tgba_explicit::transition* t = out_->create_transition(in_name.str(), out_name.str()); diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index e4dafe88e..7525554f8 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -124,7 +126,7 @@ namespace spot body_ << out - 1 << " "; acs_.split(body_, si->current_acceptance_conditions()); body_ << "-1 " << bdd_to_lbtt(si->current_condition(), - automata_->get_dict()) << std::endl; + aut_->get_dict()) << std::endl; } void diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 9bbb1d949..bcfdd11bc 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -58,7 +58,7 @@ namespace spot os_ << " */"; } os_ << '\n'; - init_ = automata_->get_init_state(); + init_ = aut_->get_init_state(); } void @@ -86,7 +86,7 @@ namespace spot // we just check the acceptance of the first transition. This // is not terribly efficient since we have to create the // iterator. - tgba_succ_iterator* it = automata_->succ_iter(s); + tgba_succ_iterator* it = aut_->succ_iter(s); it->first(); bool accepting = !it->done() && it->current_acceptance_conditions() == all_acc_conds_; @@ -111,7 +111,7 @@ namespace spot if (state_is_accepting(s)) { - tgba_succ_iterator* it = automata_->succ_iter(s); + tgba_succ_iterator* it = aut_->succ_iter(s); it->first(); if (it->done()) label = "accept_S" + ns; @@ -136,7 +136,7 @@ namespace spot void process_state(const state* s, int n, tgba_succ_iterator*) { - tgba_succ_iterator* it = automata_->succ_iter(s); + tgba_succ_iterator* it = aut_->succ_iter(s); it->first(); if (it->done()) { @@ -144,7 +144,7 @@ namespace spot os_ << " fi;\n"; os_ << get_state_label(s, n) << ":"; if (comments_) - os_ << " /* " << automata_->format_state(s) << " */"; + os_ << " /* " << aut_->format_state(s) << " */"; os_ << "\n if\n :: (0) -> goto " << get_state_label(s, n) << '\n'; fi_needed_ = true; @@ -163,7 +163,7 @@ namespace spot os_ << " fi;\n"; os_ << get_state_label(s, n) << ":"; if (comments_) - os_ << " /* " << automata_->format_state(s) << " */"; + os_ << " /* " << aut_->format_state(s) << " */"; os_ << "\n if\n"; fi_needed_ = true; } @@ -180,7 +180,7 @@ namespace spot { os_ << " :: ("; const ltl::formula* f = bdd_to_formula(si->current_condition(), - automata_->get_dict()); + aut_->get_dict()); to_spin_string(f, os_, true); f->destroy(); state* current = si->current_state(); diff --git a/src/tgbaalgos/reachiter.cc b/src/tgbaalgos/reachiter.cc index 03880dcc6..d386e7985 100644 --- a/src/tgbaalgos/reachiter.cc +++ b/src/tgbaalgos/reachiter.cc @@ -30,7 +30,7 @@ namespace spot ////////////////////////////////////////////////////////////////////// tgba_reachable_iterator::tgba_reachable_iterator(const tgba* a) - : automata_(a) + : aut_(a) { } @@ -51,7 +51,7 @@ namespace spot { int n = 0; start(); - state* i = automata_->get_init_state(); + state* i = aut_->get_init_state(); if (want_state(i)) add_state(i); seen[i] = ++n; @@ -60,7 +60,7 @@ namespace spot { assert(seen.find(t) != seen.end()); int tn = seen[t]; - tgba_succ_iterator* si = automata_->succ_iter(t); + tgba_succ_iterator* si = aut_->succ_iter(t); process_state(t, tn, si); for (si->first(); !si->done(); si->next()) { diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh index 6f516c6fb..f077db0bd 100644 --- a/src/tgbaalgos/reachiter.hh +++ b/src/tgbaalgos/reachiter.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -90,7 +90,7 @@ namespace spot const tgba_succ_iterator* si); protected: - const tgba* automata_; ///< The spot::tgba to explore. + const tgba* aut_; ///< The spot::tgba to explore. typedef Sgi::hash_map seen_map; diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc index 087d76ccd..03f499a58 100644 --- a/src/tgbaalgos/reductgba_sim.cc +++ b/src/tgbaalgos/reductgba_sim.cc @@ -291,7 +291,7 @@ namespace spot for (i1 = spoiler_vertice_.begin(); i1 != spoiler_vertice_.end(); ++i1) { - os << (*i1)->to_string(automata_); + os << (*i1)->to_string(aut_); ++n; if (n > 20) { @@ -311,7 +311,7 @@ namespace spot for (i2 = duplicator_vertice_.begin(); i2 != duplicator_vertice_.end(); ++i2) { - os << (*i2)->to_string(automata_); + os << (*i2)->to_string(aut_); ++n; if (n > 20) { @@ -404,7 +404,7 @@ namespace spot for (std::vector::iterator j = tgba_state_.begin(); j != tgba_state_.end(); ++j) { - si = automata_->succ_iter(*j); + si = aut_->succ_iter(*j); for (si->first(); !si->done(); si->next()) { @@ -485,7 +485,7 @@ namespace spot ->compare((*i)->get_spoiler_node()) == 0) { tgba_succ_iterator* si - = automata_->succ_iter((*j)->get_duplicator_node()); + = aut_->succ_iter((*j)->get_duplicator_node()); for (si->first(); !si->done(); si->next()) { s = si->current_state(); @@ -506,7 +506,7 @@ namespace spot ->compare((*i)->get_duplicator_node()) == 0) { tgba_succ_iterator* si - = automata_->succ_iter((*i)->get_spoiler_node()); + = aut_->succ_iter((*i)->get_spoiler_node()); for (si->first(); !si->done(); si->next()) { s = si->current_state(); diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc index 6ac08a572..d2df0a0f4 100644 --- a/src/tgbaalgos/reductgba_sim_del.cc +++ b/src/tgbaalgos/reductgba_sim_del.cc @@ -344,7 +344,7 @@ namespace spot int parity_game_graph_delayed::nb_set_acc_cond() { - return automata_->number_of_acceptance_conditions(); + return aut_->number_of_acceptance_conditions(); } // We build only node which are reachable @@ -393,7 +393,7 @@ namespace spot { assert(sn); - tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node()); + tgba_succ_iterator* si = aut_->succ_iter(sn->get_spoiler_node()); for (si->first(); !si->done(); si->next()) { @@ -439,7 +439,7 @@ namespace spot spoiler_node* , std::ostringstream& os) { - tgba_succ_iterator* si = automata_->succ_iter(dn->get_duplicator_node()); + tgba_succ_iterator* si = aut_->succ_iter(dn->get_duplicator_node()); for (si->first(); !si->done(); si->next()) { @@ -524,7 +524,7 @@ namespace spot { bool exist = false; - //bool l2a = (acc != automata_->all_acceptance_conditions()); + //bool l2a = (acc != aut_->all_acceptance_conditions()); spoiler_node_delayed* sn_n = new spoiler_node_delayed(sn, dn, acc, nb); diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index c30ed95b9..5169c3ae6 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement de -// l'Epita (LRDE) +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement +// de l'Epita (LRDE) // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -45,19 +45,19 @@ namespace spot start() { os_ << "acc ="; - print_acc(automata_->all_acceptance_conditions()) << ";\n"; + print_acc(aut_->all_acceptance_conditions()) << ";\n"; } void process_state(const state* s, int, tgba_succ_iterator* si) { - const bdd_dict* d = automata_->get_dict(); - std::string cur = escape_str(automata_->format_state(s)); + const bdd_dict* d = aut_->get_dict(); + std::string cur = escape_str(aut_->format_state(s)); for (si->first(); !si->done(); si->next()) { state* dest = si->current_state(); os_ << "\"" << cur << "\", \""; - escape_str(os_, automata_->format_state(dest)); + escape_str(os_, aut_->format_state(dest)); os_ << "\", \""; escape_str(os_, bdd_format_formula(d, si->current_condition())); os_ << "\","; @@ -72,7 +72,7 @@ namespace spot std::ostream& print_acc(bdd acc) { - const bdd_dict* d = automata_->get_dict(); + const bdd_dict* d = aut_->get_dict(); while (acc != bddfalse) { bdd cube = bdd_satone(acc); diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index cd4d92782..55f43ae2f 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -95,7 +95,7 @@ namespace spot const tgba_succ_iterator* si) { tgba_explicit::transition* t = - create_transition(this->automata_, out_, in_s, in, out_s, out); + create_transition(this->aut_, out_, in_s, in, out_s, out); out_->add_conditions(t, si->current_condition()); // Regardless of all_, do not output any acceptance condition