From a577850eb3419c2993b2bd91e9091cac9ad83e87 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 20 Dec 2012 17:18:56 +0100 Subject: [PATCH] Address several issues reported by cppcheck all over the place. * src/bin/common_finput.cc, src/tgbaalgos/lbtt.cc: Use !empty() instead of size() > 0. * src/bin/ltl2tgta.cc, src/kripke/kripkeexplicit.cc, src/tgbatest/complementation.cc: Avoid useless assignments. * src/bin/ltlcross.cc: Correct mistaken assignment inside assert(). * src/evtgba/symbol.hh, src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh, src/tgba/tgbasafracomplement.cc (operator=): Do not return a const reference. * src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/product.cc, src/evtgbatest/product.cc: Check indices before using them, not after. * src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh, src/tgbatest/randtgba.cc: Pass constant strings by reference. * src/kripke/kripkeprint.cc, src/tgbaalgos/simulation.cc: Remove a useless operation. * src/ltlvisit/simplify.cc: Remove a duplicate condition. * src/misc/formater.hh: Remove unused attribute. * src/misc/modgray.cc: Initialize done_ in the constructor. * src/saba/explicitstateconjunction.cc, src/saba/explicitstateconjunction.hh (operator=): Fix prototype. * src/saba/sabacomplementtgba.cc: Remove unused default constructor. * src/ta/taexplicit.cc, src/ta/taproduct.cc, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh, src/taalgos/emptinessta.cc, src/taalgos/minimize.cc, src/taalgos/reachiter.cc, src/taalgos/tgba2ta.cc, src/tgbaalgos/cutscc.cc: Use C++ casts, and ++it instead of it++. * src/taalgos/dotty.cc, src/tgbatest/ltl2tgba.cc: Refine the scope of variables. * src/tgba/tgbakvcomplement.hh (bdd_order): Always initialize bdd_. * src/tgba/tgbasgba.cc, src/tgba/wdbacomp.cc: Use the initialization line to initialize all members. --- src/bin/common_finput.cc | 2 +- src/bin/ltl2tgta.cc | 11 +++---- src/bin/ltlcross.cc | 6 ++-- src/evtgba/symbol.hh | 2 +- src/evtgbatest/ltl2evtgba.cc | 2 +- src/evtgbatest/product.cc | 9 ++--- src/kripke/kripkeexplicit.cc | 9 +++-- src/kripke/kripkeexplicit.hh | 2 +- src/kripke/kripkeprint.cc | 2 +- src/ltlvisit/simplify.cc | 3 +- src/misc/formater.hh | 1 - src/misc/modgray.cc | 7 ++-- src/saba/explicitstateconjunction.cc | 7 ++-- src/saba/explicitstateconjunction.hh | 5 +-- src/saba/sabacomplementtgba.cc | 9 ++--- src/ta/taexplicit.cc | 49 +++++++++++++++------------- src/ta/taproduct.cc | 2 +- src/ta/tgtaproduct.cc | 6 ++-- src/ta/tgtaproduct.hh | 7 +--- src/taalgos/dotty.cc | 7 ++-- src/taalgos/emptinessta.cc | 7 ++-- src/taalgos/minimize.cc | 2 +- src/taalgos/reachiter.cc | 5 +-- src/taalgos/tgba2ta.cc | 16 ++++----- src/tgba/tgbabddcoredata.cc | 2 +- src/tgba/tgbabddcoredata.hh | 2 +- src/tgba/tgbakvcomplement.hh | 9 ++--- src/tgba/tgbasafracomplement.cc | 6 ++-- src/tgba/tgbasgba.cc | 5 ++- src/tgba/wdbacomp.cc | 3 +- src/tgbaalgos/cutscc.cc | 11 +++---- src/tgbaalgos/lbtt.cc | 4 +-- src/tgbaalgos/simulation.cc | 1 - src/tgbatest/complementation.cc | 3 +- src/tgbatest/ltl2tgba.cc | 10 +++--- src/tgbatest/randtgba.cc | 6 ++-- 36 files changed, 117 insertions(+), 123 deletions(-) diff --git a/src/bin/common_finput.cc b/src/bin/common_finput.cc index fb7298f4d..711bcd57f 100644 --- a/src/bin/common_finput.cc +++ b/src/bin/common_finput.cc @@ -94,7 +94,7 @@ job_processor::process_string(const std::string& input, spot::ltl::parse_error_list pel; const spot::ltl::formula* f = parse_formula(input, pel); - if (!f || pel.size() > 0) + if (!f || !pel.empty()) { if (filename) error_at_line(0, 0, filename, linenum, "parse error:"); diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc index cdf7a42fb..5a7bffd4a 100644 --- a/src/bin/ltl2tgta.cc +++ b/src/bin/ltl2tgta.cc @@ -199,12 +199,11 @@ namespace if (ta_type != TGTA) { - spot::ta* testing_automaton = 0; - testing_automaton = tgba_to_ta(aut, ap_set, - type == spot::postprocessor::BA, - opt_with_artificial_initial_state, - opt_single_pass_emptiness_check, - opt_with_artificial_livelock); + spot::ta* testing_automaton = + tgba_to_ta(aut, ap_set, type == spot::postprocessor::BA, + opt_with_artificial_initial_state, + opt_single_pass_emptiness_check, + opt_with_artificial_livelock); if (level != spot::postprocessor::Low) { spot::ta* testing_automaton_nm = testing_automaton; diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index e4c64489e..df3f0013e 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -744,7 +744,7 @@ namespace states_in_acc(neg, sspace, s); bool res = s.size() == states; state_set::iterator it; - for (it = s.begin(); it != s.end(); it++) + for (it = s.begin(); it != s.end(); ++it) (*it)->destroy(); return res; } @@ -1001,7 +1001,7 @@ print_stats_csv(const char* filename) unsigned ntrans = translators.size(); unsigned rounds = vstats.size(); - assert(rounds = formulas.size()); + assert(rounds == formulas.size()); *out << "\"formula\", \"tool\", "; statistics::fields(*out); @@ -1039,7 +1039,7 @@ print_stats_json(const char* filename) unsigned ntrans = translators.size(); unsigned rounds = vstats.size(); - assert(rounds = formulas.size()); + assert(rounds == formulas.size()); *out << "{\n \"tools\": [\n \""; spot::escape_str(*out, translators[0]); diff --git a/src/evtgba/symbol.hh b/src/evtgba/symbol.hh index 7855e5138..07b83170a 100644 --- a/src/evtgba/symbol.hh +++ b/src/evtgba/symbol.hh @@ -83,7 +83,7 @@ namespace spot return s_; } - const rsymbol& + rsymbol& operator=(const rsymbol& rs) { if (this != &rs) diff --git a/src/evtgbatest/ltl2evtgba.cc b/src/evtgbatest/ltl2evtgba.cc index cb3003a19..8182e2617 100644 --- a/src/evtgbatest/ltl2evtgba.cc +++ b/src/evtgbatest/ltl2evtgba.cc @@ -58,7 +58,7 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* unobservables = new spot::ltl::atomic_prop_set; - while (argv[formula_index][0] == '-' && formula_index < argc) + while (formula_index < argc && argv[formula_index][0] == '-') { if (!strcmp(argv[formula_index], "-d")) { diff --git a/src/evtgbatest/product.cc b/src/evtgbatest/product.cc index 32c7e08bf..d5bdcc932 100644 --- a/src/evtgbatest/product.cc +++ b/src/evtgbatest/product.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -47,7 +48,7 @@ main(int argc, char** argv) bool dotty = false; int filename_index = 1; - while (argv[filename_index][0] == '-' && filename_index < argc) + while (filename_index < argc && argv[filename_index][0] == '-') { if (!strcmp(argv[filename_index], "-d")) debug = true; diff --git a/src/kripke/kripkeexplicit.cc b/src/kripke/kripkeexplicit.cc index f6318c37e..e84bf80e3 100644 --- a/src/kripke/kripkeexplicit.cc +++ b/src/kripke/kripkeexplicit.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. @@ -153,7 +153,7 @@ namespace spot { dict_->unregister_all_my_variables(this); std::map::iterator it; - for (it = ns_nodes_.begin(); it != ns_nodes_.end(); it++) + for (it = ns_nodes_.begin(); it != ns_nodes_.end(); ++it) { state_kripke* del_me = it->second; delete del_me; @@ -195,7 +195,7 @@ namespace spot } bdd - kripke_explicit::state_condition(const std::string name) const + kripke_explicit::state_condition(const std::string& name) const { std::map::const_iterator it; it = ns_nodes_.find(name); @@ -247,13 +247,12 @@ namespace spot void kripke_explicit::add_transition(std::string source, std::string dest) { - state_kripke* neo = 0; std::map::iterator destination = ns_nodes_.find(dest); if (ns_nodes_.find(dest) == ns_nodes_.end()) { - neo = new state_kripke; + state_kripke* neo = new state_kripke; add_state(dest, neo); add_transition(source, neo); } diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh index 420bd6248..7d4e26810 100644 --- a/src/kripke/kripkeexplicit.hh +++ b/src/kripke/kripkeexplicit.hh @@ -131,7 +131,7 @@ namespace spot /// \brief Get the condition on the state bdd state_condition(const state* s) const; /// \brief Get the condition on the state - bdd state_condition(const std::string) const; + bdd state_condition(const std::string&) const; /// \brief Return the name of the state. std::string format_state(const state*) const; diff --git a/src/kripke/kripkeprint.cc b/src/kripke/kripkeprint.cc index 5f04dde1e..564cd611d 100644 --- a/src/kripke/kripkeprint.cc +++ b/src/kripke/kripkeprint.cc @@ -1,3 +1,4 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement // de l'Epita (LRDE) // @@ -88,7 +89,6 @@ namespace spot notfirst = true; const bdd_dict* d = aut_->get_dict(); - std::string cur = aut_->format_state(s); os_ << "S" << in_s << ", \""; const kripke* automata = down_cast(aut_); assert(automata); diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index af393a40f..1282cf765 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -2388,7 +2388,6 @@ namespace spot && (op != multop::AndNLM) && (op != multop::OrRat) && (op != multop::Concat) - && (op != multop::Concat) && (op != multop::Fusion)) { bool is_and = op == multop::And; @@ -2442,7 +2441,7 @@ namespace spot else if (c_->implication_neg(*f1, *f2, is_and)) { for (multop::vec::iterator j = res->begin(); - j != res->end(); j++) + j != res->end(); ++j) if (*j) (*j)->destroy(); delete res; diff --git a/src/misc/formater.hh b/src/misc/formater.hh index 41c8dff9d..0f3d83fd7 100644 --- a/src/misc/formater.hh +++ b/src/misc/formater.hh @@ -180,7 +180,6 @@ namespace spot std::vector call_; protected: std::ostream* output_; - const char* pos_; }; } diff --git a/src/misc/modgray.cc b/src/misc/modgray.cc index 1cae48e7e..0941ac995 100644 --- a/src/misc/modgray.cc +++ b/src/misc/modgray.cc @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -24,7 +27,7 @@ namespace spot loopless_modular_mixed_radix_gray_code:: loopless_modular_mixed_radix_gray_code(int n) - : n_(n), a_(0), f_(0), m_(0), s_(0), non_one_radixes_(0) + : n_(n), done_(false), a_(0), f_(0), m_(0), s_(0), non_one_radixes_(0) { } diff --git a/src/saba/explicitstateconjunction.cc b/src/saba/explicitstateconjunction.cc index ae688cd77..191ec4196 100644 --- a/src/saba/explicitstateconjunction.cc +++ b/src/saba/explicitstateconjunction.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -34,7 +35,7 @@ namespace spot { } - explicit_state_conjunction* + explicit_state_conjunction& explicit_state_conjunction::operator=(const explicit_state_conjunction& o) { if (this != &o) @@ -42,7 +43,7 @@ namespace spot this->~explicit_state_conjunction(); new (this) explicit_state_conjunction(&o); } - return this; + return *this; } explicit_state_conjunction::~explicit_state_conjunction() diff --git a/src/saba/explicitstateconjunction.hh b/src/saba/explicitstateconjunction.hh index a5e6d8304..c1ca963f1 100644 --- a/src/saba/explicitstateconjunction.hh +++ b/src/saba/explicitstateconjunction.hh @@ -1,4 +1,5 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -37,7 +38,7 @@ namespace spot explicit_state_conjunction(const explicit_state_conjunction* other); virtual ~explicit_state_conjunction(); - explicit_state_conjunction* operator=(const explicit_state_conjunction& o); + explicit_state_conjunction& operator=(const explicit_state_conjunction& o); /// \name Iteration //@{ diff --git a/src/saba/sabacomplementtgba.cc b/src/saba/sabacomplementtgba.cc index c2be02e1c..1c9aae374 100644 --- a/src/saba/sabacomplementtgba.cc +++ b/src/saba/sabacomplementtgba.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -68,10 +69,6 @@ namespace spot bdd condition_; }; - saba_state_complement_tgba::saba_state_complement_tgba() - { - } - saba_state_complement_tgba::saba_state_complement_tgba(shared_state state, rank_t rank, bdd condition) diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index 32750c267..37c39655b 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -151,7 +151,7 @@ namespace spot bool transition_found = false; for (it_trans = trans_by_condition->begin(); (it_trans - != trans_by_condition->end() && !transition_found); it_trans++) + != trans_by_condition->end() && !transition_found); ++it_trans) { transition_found = ((*it_trans)->dest == t->dest); if (transition_found) @@ -240,7 +240,7 @@ namespace spot int state_ta_explicit::compare(const spot::state* other) const { - const state_ta_explicit* o = down_cast (other); + const state_ta_explicit* o = down_cast(other); assert(o); int compare_value = tgba_state_->compare(o->tgba_state_); @@ -286,7 +286,8 @@ namespace spot state_ta_explicit* dest = (*it_trans)->dest; bool is_stuttering_transition = (get_tgba_condition() == (dest)->get_tgba_condition()); - bool dest_is_livelock_accepting = dest->is_livelock_accepting_state(); + bool dest_is_livelock_accepting = + dest->is_livelock_accepting_state(); //Before deleting stuttering transitions, propaged back livelock //and initial state's properties @@ -329,7 +330,7 @@ namespace spot // We don't destroy the transitions in the state's destructor because // they are not cloned. if (trans != 0) - for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++) + for (it_trans = trans->begin(); it_trans != trans->end(); ++it_trans) { delete *it_trans; } @@ -369,9 +370,9 @@ namespace spot ta_explicit::~ta_explicit() { ta::states_set_t::iterator it; - for (it = states_set_.begin(); it != states_set_.end(); it++) + for (it = states_set_.begin(); it != states_set_.end(); ++it) { - state_ta_explicit* s = down_cast (*it); + state_ta_explicit* s = down_cast(*it); s->free_transitions(); s->get_tgba_state()->destroy(); @@ -388,14 +389,13 @@ namespace spot std::pair add_state_to_ta = states_set_.insert(s); - return static_cast (*add_state_to_ta.first); + return static_cast(*add_state_to_ta.first); } void ta_explicit::add_to_initial_states_set(state* state, bdd condition) { - state_ta_explicit * s = down_cast (state); - assert(s); + state_ta_explicit* s = down_cast(state); s->set_initial_state(true); if (condition == bddfalse) condition = get_state_condition(s); @@ -403,15 +403,17 @@ namespace spot initial_states_set_.insert(s); if (get_artificial_initial_state() != 0) if (add_state.second) - create_transition((state_ta_explicit*) get_artificial_initial_state(), - condition, bddfalse, s); - + { + state_ta_explicit* i = + down_cast(get_artificial_initial_state()); + create_transition(i, condition, bddfalse, s); + } } void ta_explicit::delete_stuttering_and_hole_successors(spot::state* s) { - state_ta_explicit * state = down_cast (s); + state_ta_explicit * state = down_cast(s); assert(state); state->delete_stuttering_and_hole_successors(); if (state->is_initial_state()) @@ -421,7 +423,8 @@ namespace spot void ta_explicit::create_transition(state_ta_explicit* source, bdd condition, - bdd acceptance_conditions, state_ta_explicit* dest, bool add_at_beginning) + bdd acceptance_conditions, + state_ta_explicit* dest, bool add_at_beginning) { state_ta_explicit::transition* t = new state_ta_explicit::transition; t->dest = dest; @@ -442,7 +445,7 @@ namespace spot ta_explicit::get_state_condition(const spot::state* initial_state) const { const state_ta_explicit* sta = - down_cast (initial_state); + down_cast(initial_state); assert(sta); return sta->get_tgba_condition(); } @@ -450,7 +453,7 @@ namespace spot bool ta_explicit::is_accepting_state(const spot::state* s) const { - const state_ta_explicit* sta = down_cast (s); + const state_ta_explicit* sta = down_cast(s); assert(sta); return sta->is_accepting_state(); } @@ -458,7 +461,7 @@ namespace spot bool ta_explicit::is_initial_state(const spot::state* s) const { - const state_ta_explicit* sta = down_cast (s); + const state_ta_explicit* sta = down_cast(s); assert(sta); return sta->is_initial_state(); } @@ -466,7 +469,7 @@ namespace spot bool ta_explicit::is_livelock_accepting_state(const spot::state* s) const { - const state_ta_explicit* sta = down_cast (s); + const state_ta_explicit* sta = down_cast(s); assert(sta); return sta->is_livelock_accepting_state(); } @@ -474,7 +477,7 @@ namespace spot ta_succ_iterator* ta_explicit::succ_iter(const spot::state* state) const { - const state_ta_explicit* s = down_cast (state); + const state_ta_explicit* s = down_cast(state); assert(s); return new ta_explicit_succ_iterator(s); } @@ -482,7 +485,7 @@ namespace spot ta_succ_iterator* ta_explicit::succ_iter(const spot::state* state, bdd condition) const { - const state_ta_explicit* s = down_cast (state); + const state_ta_explicit* s = down_cast(state); assert(s); return new ta_explicit_succ_iterator(s, condition); } @@ -502,7 +505,7 @@ namespace spot std::string ta_explicit::format_state(const spot::state* s) const { - const state_ta_explicit* sta = down_cast (s); + const state_ta_explicit* sta = down_cast(s); assert(sta); if (sta->get_tgba_condition() == bddtrue) @@ -517,11 +520,11 @@ namespace spot ta_explicit::delete_stuttering_transitions() { ta::states_set_t::iterator it; - for (it = states_set_.begin(); it != states_set_.end(); it++) + for (it = states_set_.begin(); it != states_set_.end(); ++it) { const state_ta_explicit* source = - static_cast (*it); + static_cast(*it); state_ta_explicit::transitions* trans = source->get_transitions(); state_ta_explicit::transitions::iterator it_trans; diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc index 39bf3d43e..9113ecd5d 100644 --- a/src/ta/taproduct.cc +++ b/src/ta/taproduct.cc @@ -288,7 +288,7 @@ namespace spot ta_init_states_set = ta_->get_initial_states_set(); } - for (it = ta_init_states_set.begin(); it != ta_init_states_set.end(); it++) + for (it = ta_init_states_set.begin(); it != ta_init_states_set.end(); ++it) { if ((artificial_initial_state != 0) || (kripke_init_state_condition diff --git a/src/ta/tgtaproduct.cc b/src/ta/tgtaproduct.cc index dc7284be7..2466fe3c0 100644 --- a/src/ta/tgtaproduct.cc +++ b/src/ta/tgtaproduct.cc @@ -1,3 +1,4 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2012 Laboratoire de Recherche et Developpement // de l Epita (LRDE). // @@ -64,8 +65,9 @@ namespace spot fixed_size_pool* p = const_cast (&pool_); - return new tgta_succ_iterator_product(s, (const kripke*) left_, - (const tgta *) right_, p); + return new tgta_succ_iterator_product(s, + down_cast(left_), + down_cast(right_), p); } //////////////////////////////////////////////////////////// diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh index 507cfae8e..33860213c 100644 --- a/src/ta/tgtaproduct.hh +++ b/src/ta/tgtaproduct.hh @@ -36,7 +36,6 @@ namespace spot class tgta_product : public tgba_product { public: - tgta_product(const kripke* left, const tgta* right); virtual state* @@ -45,8 +44,6 @@ namespace spot virtual tgba_succ_iterator* succ_iter(const state* local_state, const state* global_state = 0, const tgba* global_automaton = 0) const; - - }; /// \brief Iterate over the successors of a product computed on the fly. @@ -100,9 +97,7 @@ namespace spot bdd current_condition_; bdd current_acceptance_conditions_; bdd kripke_source_condition; - state * kripke_current_dest_state; - - + state* kripke_current_dest_state; }; } diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc index a23ba2249..698f74645 100644 --- a/src/taalgos/dotty.cc +++ b/src/taalgos/dotty.cc @@ -1,3 +1,4 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2010, 2012 Laboratoire de Recherche et Developpement // de l Epita (LRDE). // @@ -40,8 +41,6 @@ namespace spot { os_ << "digraph G {" << std::endl; - int n = 0; - artificial_initial_state_ = t_automata_->get_artificial_initial_state(); ta::states_set_t init_states_set; @@ -55,10 +54,10 @@ namespace spot } else { + int n = 0; init_states_set = t_automata_->get_initial_states_set(); - for (it = init_states_set.begin(); - it != init_states_set.end(); it++) + it != init_states_set.end(); ++it) { bdd init_condition = t_automata_->get_state_condition(*it); std::string label = bdd_format_formula(t_automata_->get_dict(), diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index 039dcbe25..cf59352b0 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -1,5 +1,6 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -360,7 +361,7 @@ namespace spot } std::set::const_iterator it; - for (it = liveset_dest.begin(); it != liveset_dest.end(); it++) + for (it = liveset_dest.begin(); it != liveset_dest.end(); ++it) { const state* succ = (*it); if (heuristic_livelock_detection(succ, h, h_livelock_root, @@ -442,7 +443,7 @@ namespace spot const ta::states_set_t init_states_set = a_->get_initial_states_set(); ta::states_set_t::const_iterator it; - for (it = init_states_set.begin(); it != init_states_set.end(); it++) + for (it = init_states_set.begin(); it != init_states_set.end(); ++it) { state* init_state = (*it); ta_init_it_.push(init_state); diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index 7f064a63a..09cf699f9 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -205,7 +205,7 @@ namespace spot spot::state* artificial_initial_state = ta_->get_artificial_initial_state(); - for (it = states_set.begin(); it != states_set.end(); it++) + for (it = states_set.begin(); it != states_set.end(); ++it) { const state* s = (*it); diff --git a/src/taalgos/reachiter.cc b/src/taalgos/reachiter.cc index 579d5c8f2..256bffbe4 100644 --- a/src/taalgos/reachiter.cc +++ b/src/taalgos/reachiter.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement // de l Epita (LRDE). // // @@ -66,7 +67,7 @@ namespace spot init_states_set = t_automata_->get_initial_states_set(); } - for (it = init_states_set.begin(); it != init_states_set.end(); it++) + for (it = init_states_set.begin(); it != init_states_set.end(); ++it) { state* init_state = (*it); if (want_state(init_state)) diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index bed729472..e9b561265 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -76,7 +76,7 @@ namespace spot state_ta_explicit::transitions* transitions_to_livelock_states = new state_ta_explicit::transitions; - for (it = states_set.begin(); it != states_set.end(); it++) + for (it = states_set.begin(); it != states_set.end(); ++it) { state_ta_explicit* source = static_cast (*it); @@ -122,8 +122,8 @@ namespace spot { state_ta_explicit::transitions::iterator it_trans; - for (it_trans = transitions_to_livelock_states->begin(); it_trans - != transitions_to_livelock_states->end(); it_trans++) + for (it_trans = transitions_to_livelock_states->begin(); + it_trans != transitions_to_livelock_states->end(); ++it_trans) { if (artificial_livelock_accepting_state != 0) { @@ -147,7 +147,7 @@ namespace spot } delete transitions_to_livelock_states; - for (it = states_set.begin(); it != states_set.end(); it++) + for (it = states_set.begin(); it != states_set.end(); ++it) { state_ta_explicit* state = static_cast (*it); @@ -196,7 +196,7 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata, ta::states_set_t::const_iterator it; ta::states_set_t init_states = testing_automata->get_initial_states_set(); - for (it = init_states.begin(); it != init_states.end(); it++) + for (it = init_states.begin(); it != init_states.end(); ++it) { state* init_state = (*it); init_set.push(init_state); @@ -610,7 +610,7 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata, // adapt a GTA to remove acceptance conditions from states ta::states_set_t states_set = ta->get_states_set(); ta::states_set_t::iterator it; - for (it = states_set.begin(); it != states_set.end(); it++) + for (it = states_set.begin(); it != states_set.end(); ++it) { state_ta_explicit* state = static_cast (*it); @@ -621,7 +621,7 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata, state_ta_explicit::transitions::iterator it_trans; for (it_trans = trans->begin(); it_trans != trans->end(); - it_trans++) + ++it_trans) { (*it_trans)->acceptance_conditions = ta->all_acceptance_conditions(); @@ -674,7 +674,7 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata, bdd bdd_stutering_transition = bdd_setxor(first_state_condition, first_state_condition); - for (it = states_set.begin(); it != states_set.end(); it++) + for (it = states_set.begin(); it != states_set.end(); ++it) { state_ta_explicit* state = static_cast (*it); diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index 8dd362cf6..cc5c78165 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/src/tgba/tgbabddcoredata.cc @@ -90,7 +90,7 @@ namespace spot assert(dict == right.dict); } - const tgba_bdd_core_data& + tgba_bdd_core_data& tgba_bdd_core_data::operator=(const tgba_bdd_core_data& copy) { if (this != ©) diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index e612f61a5..759c60294 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/src/tgba/tgbabddcoredata.hh @@ -134,7 +134,7 @@ namespace spot tgba_bdd_core_data(const tgba_bdd_core_data& left, const tgba_bdd_core_data& right); - const tgba_bdd_core_data& operator=(const tgba_bdd_core_data& copy); + tgba_bdd_core_data& operator=(const tgba_bdd_core_data& copy); /// \brief Update the variable sets to take a new pair of variables into /// account. diff --git a/src/tgba/tgbakvcomplement.hh b/src/tgba/tgbakvcomplement.hh index d514cb8a4..5cc38614c 100644 --- a/src/tgba/tgbakvcomplement.hh +++ b/src/tgba/tgbakvcomplement.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -30,7 +31,7 @@ namespace spot { public: bdd_ordered() - : order_(0) + : bdd_(0), order_(0) {}; bdd_ordered(int bdd_, unsigned order_) @@ -77,7 +78,7 @@ namespace spot /// \endverbatim /// /// The original automaton is used as a States-based Generalized - /// Büchi Automaton. + /// Büchi Automaton. /// /// The construction is done on-the-fly, by the /// \c tgba_kv_complement_succ_iterator class. diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index efa926937..812bff971 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -1,3 +1,4 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // @@ -104,7 +105,7 @@ namespace spot safra_tree(const subset_t& nodes, safra_tree* p, int n); ~safra_tree(); - const safra_tree& operator=(const safra_tree& other); + safra_tree& operator=(const safra_tree& other); int compare(const safra_tree* other) const; size_t hash() const; @@ -177,7 +178,7 @@ namespace spot (*i)->destroy(); } - const safra_tree& + safra_tree& safra_tree::operator=(const safra_tree& other) { if (this != &other) @@ -816,7 +817,6 @@ namespace spot void print_safra_automaton(safra_tree_automaton* a) { - safra_tree_automaton::automaton_t node_list = a->automaton; typedef safra_tree_automaton::automaton_t::reverse_iterator automaton_cit; typedef safra_tree_automaton::transition_list::const_iterator diff --git a/src/tgba/tgbasgba.cc b/src/tgba/tgbasgba.cc index 6cbbdeceb..763311bb6 100644 --- a/src/tgba/tgbasgba.cc +++ b/src/tgba/tgbasgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -101,9 +101,8 @@ namespace spot } tgba_sgba_proxy_succ_iterator(tgba_succ_iterator* it, bdd acc) - : it_(it), emulate_acc_cond_(true) + : it_(it), emulate_acc_cond_(true), acceptance_condition_(acc) { - acceptance_condition_ = acc; } virtual diff --git a/src/tgba/wdbacomp.cc b/src/tgba/wdbacomp.cc index 54e87af36..f55e66a8e 100644 --- a/src/tgba/wdbacomp.cc +++ b/src/tgba/wdbacomp.cc @@ -166,9 +166,8 @@ namespace spot { public: tgba_wdba_comp_proxy(const tgba* a) - : a_(a) + : a_(a), the_acceptance_cond_(a->all_acceptance_conditions()) { - the_acceptance_cond_ = a->all_acceptance_conditions(); if (the_acceptance_cond_ == bddfalse) { int v = get_dict() diff --git a/src/tgbaalgos/cutscc.cc b/src/tgbaalgos/cutscc.cc index b4bd28778..bf1f00231 100644 --- a/src/tgbaalgos/cutscc.cc +++ b/src/tgbaalgos/cutscc.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2011 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -38,7 +39,7 @@ namespace spot std::string cur_format = a->format_state(cur); std::set::iterator it; // Check if we have at least one accepting SCC. - for (it = s.begin(); it != s.end() && !m.accepting(*it); it++) + for (it = s.begin(); it != s.end() && !m.accepting(*it); ++it) continue; assert(it != s.end()); tovisit.push(cur); @@ -89,10 +90,8 @@ namespace spot hash_type::iterator it2; // Free visited states. - for (it2 = seen.begin(); it2 != seen.end(); it2++) - { + for (it2 = seen.begin(); it2 != seen.end(); ++it2) (*it2)->destroy(); - } return sub_a; } diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index bc65d2048..a8360f80b 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -218,7 +218,7 @@ namespace spot std::getline(is, guard); ltl::parse_error_list pel; const ltl::formula* f = parse_lbt(guard, pel, env); - if (!f || pel.size() > 0) + if (!f || !pel.empty()) { error += "failed to parse guard: " + guard; if (f) @@ -301,7 +301,7 @@ namespace spot std::getline(is, guard); ltl::parse_error_list pel; const ltl::formula* f = parse_lbt(guard, pel, env); - if (!f || pel.size() > 0) + if (!f || !pel.empty()) { error += "failed to parse guard: " + guard; if (f) diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 1875b8421..95213567f 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -286,7 +286,6 @@ namespace spot // We run through the map bdd/list, and we update // the previous_class_ with the new data. - it_bdd = used_var_.begin(); for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); it != bdd_lstate_.end(); ++it) diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 1892ee354..6a4c4af40 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -160,10 +160,9 @@ int main(int argc, char* argv[]) else if (print_formula) { spot::tgba* a; - const spot::ltl::formula* f1 = 0; spot::ltl::parse_error_list p1; - f1 = spot::ltl::parse(file, p1); + const spot::ltl::formula* f1 = spot::ltl::parse(file, p1); if (spot::ltl::format_parse_errors(std::cerr, file, p1)) return 2; diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 934b20602..0a5fbc005 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -360,12 +360,10 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* unobservables = 0; spot::tgba* system = 0; - const spot::tgba* product = 0; const spot::tgba* product_to_free = 0; spot::bdd_dict* dict = new spot::bdd_dict(); spot::timer_map tm; bool use_timer = false; - bool assume_sba = false; bool reduction_dir_sim = false; bool reduction_rev_sim = false; bool reduction_iterated_sim = false; @@ -892,6 +890,7 @@ main(int argc, char** argv) const spot::tgba* to_free = 0; const spot::tgba* to_free2 = 0; spot::tgba* a = 0; + bool assume_sba = false; if (from_file) { @@ -1198,10 +1197,8 @@ main(int argc, char** argv) if (ta_opt) { - spot::ta* testing_automaton = 0; - tm.start("conversion to TA"); - testing_automaton + spot::ta* testing_automaton = tgba_to_ta(a, atomic_props_set_bdd, degeneralize_opt == DegenSBA, opt_with_artificial_initial_state, opt_single_pass_emptiness_check, @@ -1286,7 +1283,8 @@ main(int argc, char** argv) if (system) { - product = product_to_free = a = new spot::tgba_product(system, a); + const spot::tgba* product = product_to_free = a = + new spot::tgba_product(system, a); assume_sba = false; diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 7b70ca5ac..2520f47a6 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -311,7 +311,7 @@ struct stat_collector std::ostream& display(std::ostream& os, - const alg_1stat_map& m, const std::string title, + const alg_1stat_map& m, const std::string& title, bool total = true) const { std::ios::fmtflags old = os.flags(); @@ -418,7 +418,7 @@ ar_stats_type mar_stats; // ... about minimized accepting runs. void -print_ar_stats(ar_stats_type& ar_stats, const std::string s) +print_ar_stats(ar_stats_type& ar_stats, const std::string& s) { std::ios::fmtflags old = std::cout.flags(); std::cout << std::endl << s << std::endl; @@ -818,7 +818,7 @@ main(int argc, char** argv) const char** i = default_algos; while (*i) { - ec_algo a = { *i++, 0 }; + ec_algo a = { *(i++), 0 }; ec_algos.push_back(a); } }