From 9f63bb663741bafd803660c9e569c71f5b1d385f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 31 Mar 2011 19:39:44 +0200 Subject: [PATCH] Introduct a down_cast macro. * src/misc/casts.hh: New file. * src/misc/Makefile.am: Add it. * iface/dve2/dve2.cc, iface/gspn/gspn.cc, iface/gspn/ssp.cc, src/evtgba/explicit.cc, src/evtgba/product.cc, src/misc/casts.hh, src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.cc, src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc, src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim_del.cc: Use down_cast when appropriate. --- ChangeLog | 18 ++++++++++ iface/dve2/dve2.cc | 8 ++--- iface/gspn/gspn.cc | 8 ++--- iface/gspn/ssp.cc | 55 +++++++++++++++--------------- src/evtgba/explicit.cc | 10 +++--- src/evtgba/product.cc | 10 +++--- src/misc/Makefile.am | 9 +++-- src/misc/casts.hh | 40 ++++++++++++++++++++++ src/tgba/state.hh | 1 + src/tgba/statebdd.cc | 4 ++- src/tgba/taatgba.cc | 8 ++--- src/tgba/taatgba.hh | 4 +-- src/tgba/tgbabddconcrete.cc | 8 ++--- src/tgba/tgbaexplicit.cc | 14 ++++---- src/tgba/tgbaexplicit.hh | 2 +- src/tgba/tgbakvcomplement.cc | 6 ++-- src/tgba/tgbaproduct.cc | 14 ++++---- src/tgba/tgbasafracomplement.cc | 10 +++--- src/tgba/tgbasgba.cc | 12 +++---- src/tgba/tgbatba.cc | 14 ++++---- src/tgba/tgbaunion.cc | 12 +++---- src/tgba/wdbacomp.cc | 12 +++---- src/tgbaalgos/ndfs_result.hxx | 2 +- src/tgbaalgos/reductgba_sim.cc | 4 +-- src/tgbaalgos/reductgba_sim_del.cc | 32 ++++++++--------- 25 files changed, 193 insertions(+), 124 deletions(-) create mode 100644 src/misc/casts.hh diff --git a/ChangeLog b/ChangeLog index 674d9d00f..1a4a511bf 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,21 @@ +2011-03-31 Alexandre Duret-Lutz + + Introduct a down_cast macro. + + * src/misc/casts.hh: New file. + * src/misc/Makefile.am: Add it. + * iface/dve2/dve2.cc, iface/gspn/gspn.cc, iface/gspn/ssp.cc, + src/evtgba/explicit.cc, src/evtgba/product.cc, src/misc/casts.hh, + src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/taatgba.cc, + src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.cc, + src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh, + src/tgba/tgbakvcomplement.cc, src/tgba/tgbaproduct.cc, + src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc, + src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc, + src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reductgba_sim.cc, + src/tgbaalgos/reductgba_sim_del.cc: Use down_cast when + appropriate. + 2011-03-31 Alexandre Duret-Lutz Cosmetics. diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index 57ec1cbf6..e6607c78e 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -107,7 +107,7 @@ namespace spot { if (this == other) return 0; - const dve2_state* o = dynamic_cast(other); + const dve2_state* o = down_cast(other); assert(o); if (hash_value < o->hash_value) return -1; @@ -650,7 +650,7 @@ namespace spot succ_iter(const state* local_state, const state*, const tgba*) const { - const dve2_state* s = dynamic_cast(local_state); + const dve2_state* s = down_cast(local_state); assert(s); // This may also compute successors in state_condition_last_cc @@ -682,7 +682,7 @@ namespace spot bdd state_condition(const state* st) const { - const dve2_state* s = dynamic_cast(st); + const dve2_state* s = down_cast(st); assert(s); return compute_state_condition(s); } @@ -690,7 +690,7 @@ namespace spot virtual std::string format_state(const state *st) const { - const dve2_state* s = dynamic_cast(st); + const dve2_state* s = down_cast(st); assert(s); std::stringstream res; diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc index 2fea20c1c..85c12652e 100644 --- a/iface/gspn/gspn.cc +++ b/iface/gspn/gspn.cc @@ -51,7 +51,7 @@ namespace spot virtual int compare(const state* other) const { - const state_gspn* o = dynamic_cast(other); + const state_gspn* o = down_cast(other); assert(o); return reinterpret_cast(o->get_state()) - reinterpret_cast(get_state()); @@ -389,7 +389,7 @@ namespace spot const state* global_state, const tgba* global_automaton) const { - const state_gspn* s = dynamic_cast(local_state); + const state_gspn* s = down_cast(local_state); assert(s); (void) global_state; (void) global_automaton; @@ -402,7 +402,7 @@ namespace spot bdd tgba_gspn::compute_support_conditions(const spot::state* state) const { - const state_gspn* s = dynamic_cast(state); + const state_gspn* s = down_cast(state); assert(s); return data_->state_conds(s); } @@ -434,7 +434,7 @@ namespace spot std::string tgba_gspn::format_state(const state* state) const { - const state_gspn* s = dynamic_cast(state); + const state_gspn* s = down_cast(state); assert(s); char* str; int err = print_state(s->get_state(), &str); diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index db0c062f5..5f90d9741 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -74,13 +74,14 @@ namespace spot virtual int compare(const state* other) const { - const state_gspn_ssp* o = dynamic_cast(other); + const state_gspn_ssp* o = down_cast(other); assert(o); - int res = (reinterpret_cast(o->left()) - - reinterpret_cast(left())); - if (res != 0) - return res; - return right_->compare(o->right()); + if (o->left() == left()) + return right_->compare(o->right()); + if (o->left() < left()) + return -1; + else + return 1; } virtual size_t @@ -349,7 +350,7 @@ namespace spot const state* global_state, const tgba* global_automaton) const { - const state_gspn_ssp* s = dynamic_cast(state_); + const state_gspn_ssp* s = down_cast(state_); assert(s); (void) global_state; (void) global_automaton; @@ -485,7 +486,7 @@ namespace spot std::string tgba_gspn_ssp::format_state(const state* state) const { - const state_gspn_ssp* s = dynamic_cast(state); + const state_gspn_ssp* s = down_cast(state); assert(s); char* str; State gs = s->left(); @@ -512,7 +513,7 @@ namespace spot state* tgba_gspn_ssp::project_state(const state* s, const tgba* t) const { - const state_gspn_ssp* s2 = dynamic_cast(s); + const state_gspn_ssp* s2 = down_cast(s); assert(s2); if (t == this) return s2->clone(); @@ -681,7 +682,7 @@ namespace spot virtual numbered_state_heap::state_index find(const state* s) const { - const state_gspn_ssp* s_ = dynamic_cast(s); + const state_gspn_ssp* s_ = down_cast(s); const void* cont = container_(s_->left()); contained_map::const_iterator i = contained.find(cont); if (i != contained.end()) @@ -695,9 +696,9 @@ namespace spot for (j = l.begin(); j != l.end(); ++j) { const state_gspn_ssp* old_state = - dynamic_cast(*j); + down_cast(*j); const state_gspn_ssp* new_state = - dynamic_cast(s); + down_cast(s); assert(old_state); assert(new_state); @@ -756,7 +757,7 @@ namespace spot virtual numbered_state_heap::state_index_p find(const state* s) { - const state_gspn_ssp* s_ = dynamic_cast(s); + const state_gspn_ssp* s_ = down_cast(s); const void* cont = container_(s_->left()); contained_map::const_iterator i = contained.find(cont); if (i != contained.end()) @@ -770,9 +771,9 @@ namespace spot for (j = l.begin(); j != l.end(); ++j) { const state_gspn_ssp* old_state = - dynamic_cast(*j); + down_cast(*j); const state_gspn_ssp* new_state = - dynamic_cast(s); + down_cast(s); assert(old_state); assert(new_state); @@ -875,7 +876,7 @@ namespace spot { h[s] = index; - const state_gspn_ssp* s_ = dynamic_cast(s); + const state_gspn_ssp* s_ = down_cast(s); State sg = s_->left(); if (sg) { @@ -1058,7 +1059,7 @@ namespace spot get_contained_map_size() const { return - dynamic_cast(ecs_->h)->contained.size(); + down_cast(ecs_->h)->contained.size(); } // If a new state includes an older state, we may have to add new @@ -1069,14 +1070,14 @@ namespace spot find_state(const state* s) { typedef numbered_state_heap_ssp_semi::hash_type hash_type; - hash_type& h = dynamic_cast(ecs_->h)->h; + hash_type& h = down_cast(ecs_->h)->h; typedef numbered_state_heap_ssp_semi::contained_map contained_map; typedef numbered_state_heap_ssp_semi::f_map f_map; typedef numbered_state_heap_ssp_semi::state_list state_list; const contained_map& contained = - dynamic_cast(ecs_->h)->contained; + down_cast(ecs_->h)->contained; - const state_gspn_ssp* s_ = dynamic_cast(s); + const state_gspn_ssp* s_ = down_cast(s); const void* cont = container_(s_->left()); contained_map::const_iterator i = contained.find(cont); @@ -1092,9 +1093,9 @@ namespace spot for (j = l.begin(); j != l.end(); ++j) { const state_gspn_ssp* old_state = - dynamic_cast(*j); + down_cast(*j); const state_gspn_ssp* new_state = - dynamic_cast(s); + down_cast(s); assert(old_state); assert(new_state); @@ -1106,9 +1107,9 @@ namespace spot for (j = l.begin(); j != l.end(); ++j) { const state_gspn_ssp* old_state = - dynamic_cast(*j); + down_cast(*j); const state_gspn_ssp* new_state = - dynamic_cast(s); + down_cast(s); assert(old_state); assert(new_state); @@ -1279,7 +1280,7 @@ namespace spot static_cast (&couvreur99_check_shy_semi_ssp::get_inclusion_count); - //dynamic_cast(ecs_->h)->stats = this; + //down_cast(ecs_->h)->stats = this; } private: @@ -1296,7 +1297,7 @@ namespace spot get_inclusion_count() const { return - dynamic_cast(ecs_->h)->inclusions; + down_cast(ecs_->h)->inclusions; }; @@ -1304,7 +1305,7 @@ namespace spot get_contained_map_size() const { return - dynamic_cast(ecs_->h)->contained.size(); + down_cast(ecs_->h)->contained.size(); } virtual numbered_state_heap::state_index_p diff --git a/src/evtgba/explicit.cc b/src/evtgba/explicit.cc index 446624498..ac4da8c48 100644 --- a/src/evtgba/explicit.cc +++ b/src/evtgba/explicit.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 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. @@ -35,7 +37,7 @@ namespace spot state_evtgba_explicit::compare(const spot::state* other) const { const state_evtgba_explicit* o = - dynamic_cast(other); + down_cast(other); assert(o); return o->get_state() - get_state(); } @@ -179,7 +181,7 @@ namespace spot evtgba_explicit::succ_iter(const spot::state* s) const { const state_evtgba_explicit* u = - dynamic_cast(s); + down_cast(s); assert(u); return new evtgba_explicit_iterator_fw(&u->get_state()->out); } @@ -188,7 +190,7 @@ namespace spot evtgba_explicit::pred_iter(const spot::state* s) const { const state_evtgba_explicit* u = - dynamic_cast(s); + down_cast(s); assert(u); return new evtgba_explicit_iterator_fw(&u->get_state()->in); } @@ -197,7 +199,7 @@ namespace spot evtgba_explicit::format_state(const spot::state* s) const { const state_evtgba_explicit* u = - dynamic_cast(s); + down_cast(s); assert(u); sn_map::const_iterator i = state_name_map_.find(u->get_state()); assert(i != state_name_map_.end()); diff --git a/src/evtgba/product.cc b/src/evtgba/product.cc index 63ef1575f..f9d2ce073 100644 --- a/src/evtgba/product.cc +++ b/src/evtgba/product.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Développement de +// l'Epita (LRDE) // Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), @@ -64,7 +66,7 @@ namespace spot compare(const state* other) const { const evtgba_product_state* s = - dynamic_cast(other); + down_cast(other); assert(s); assert(s->n_ == n_); for (int i = 0; i < n_; ++i) @@ -404,7 +406,7 @@ namespace spot evtgba_product::succ_iter(const state* st) const { const evtgba_product_state* s = - dynamic_cast(st); + down_cast(st); assert(s); int n = op_.size(); @@ -420,7 +422,7 @@ namespace spot evtgba_product::pred_iter(const state* st) const { const evtgba_product_state* s = - dynamic_cast(st); + down_cast(st); assert(s); int n = op_.size(); @@ -436,7 +438,7 @@ namespace spot evtgba_product::format_state(const state* st) const { const evtgba_product_state* s = - dynamic_cast(st); + down_cast(st); int n = op_.size(); std::string res = "<" + op_[0]->format_state(s->nth(0)); diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index 573bf3d02..93c2834af 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -1,6 +1,8 @@ -## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), -## département Systèmes Répartis Coopératifs (SRC), Université Pierre -## et Marie Curie. +## Copyright (C) 2011 Laboratoire de Recherche et Développement +## de l'Epita (LRDE). +## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +## Paris 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. ## @@ -29,6 +31,7 @@ misc_HEADERS = \ bddalloc.hh \ bddlt.hh \ bddop.hh \ + casts.hh \ escape.hh \ freelist.hh \ hash.hh \ diff --git a/src/misc/casts.hh b/src/misc/casts.hh new file mode 100644 index 000000000..e973e7ef3 --- /dev/null +++ b/src/misc/casts.hh @@ -0,0 +1,40 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_MISC_CASTS_HH +# define SPOT_MISC_CASTS_HH + + +// We usually write code like +// subclass* i = down_cast(m); +// assert(i); +// ... use i ... +// When NDEBUG is set, the down_cast is a fast static_cast +// and the assert has no effect. +// Otherwise, the down_cast is a dynamic_cast and may return 0 +// on error, which the assert catches. + +#if NDEBUG +# define down_cast static_cast +#else +# define down_cast dynamic_cast +#endif + +#endif // SPOT_MISC_CASTS_HH diff --git a/src/tgba/state.hh b/src/tgba/state.hh index 318510f8f..6692189f0 100644 --- a/src/tgba/state.hh +++ b/src/tgba/state.hh @@ -29,6 +29,7 @@ #include #include #include +#include "misc/casts.hh" namespace spot { diff --git a/src/tgba/statebdd.cc b/src/tgba/statebdd.cc index 092ea6c5c..99794a8eb 100644 --- a/src/tgba/statebdd.cc +++ b/src/tgba/statebdd.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -32,7 +34,7 @@ namespace spot // This method should not be called to compare states from different // automata, and all states from the same automaton will use the same // state class. - const state_bdd* o = dynamic_cast(other); + const state_bdd* o = down_cast(other); assert(o); return o->as_bdd().id() - state_.id(); } diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc index dcd73b19e..53cd55b9f 100644 --- a/src/tgba/taatgba.cc +++ b/src/tgba/taatgba.cc @@ -70,7 +70,7 @@ namespace spot const spot::state* global_state, const tgba* global_automaton) const { - const spot::state_set* s = dynamic_cast(state); + const spot::state_set* s = down_cast(state); assert(s); (void) global_state; (void) global_automaton; @@ -104,7 +104,7 @@ namespace spot bdd taa_tgba::compute_support_conditions(const spot::state* s) const { - const spot::state_set* se = dynamic_cast(s); + const spot::state_set* se = down_cast(s); assert(se); const state_set* ss = se->get_state(); @@ -120,7 +120,7 @@ namespace spot bdd taa_tgba::compute_support_variables(const spot::state* s) const { - const spot::state_set* se = dynamic_cast(s); + const spot::state_set* se = down_cast(s); assert(se); const state_set* ss = se->get_state(); @@ -146,7 +146,7 @@ namespace spot int state_set::compare(const spot::state* other) const { - const state_set* o = dynamic_cast(other); + const state_set* o = down_cast(other); assert(o); const taa_tgba::state_set* s1 = get_state(); diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index 0ee0ebe3d..2ab039659 100644 --- a/src/tgba/taatgba.hh +++ b/src/tgba/taatgba.hh @@ -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). // // This file is part of Spot, a model checking library. @@ -227,7 +227,7 @@ namespace spot /// e.g. like {string_1,...,string_n}. virtual std::string format_state(const spot::state* s) const { - const spot::state_set* se = dynamic_cast(s); + const spot::state_set* se = down_cast(s); assert(se); const state_set* ss = se->get_state(); return format_state_set(ss); diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index 3e45cc202..c13f33d10 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -98,7 +98,7 @@ namespace spot const state* global_state, const tgba* global_automaton) const { - const state_bdd* s = dynamic_cast(local_state); + const state_bdd* s = down_cast(local_state); assert(s); bdd succ_set = data_.relation & s->as_bdd(); // If we are in a product, inject the local conditions of @@ -115,7 +115,7 @@ namespace spot bdd tgba_bdd_concrete::compute_support_conditions(const state* st) const { - const state_bdd* s = dynamic_cast(st); + const state_bdd* s = down_cast(st); assert(s); return bdd_relprod(s->as_bdd(), data_.relation, data_.notvar_set); } @@ -123,7 +123,7 @@ namespace spot bdd tgba_bdd_concrete::compute_support_variables(const state* st) const { - const state_bdd* s = dynamic_cast(st); + const state_bdd* s = down_cast(st); assert(s); bdd succ_set = data_.relation & s->as_bdd(); // bdd_support must be called BEFORE bdd_exist @@ -144,7 +144,7 @@ namespace spot std::string tgba_bdd_concrete::format_state(const state* state) const { - const state_bdd* s = dynamic_cast(state); + const state_bdd* s = down_cast(state); assert(s); return bdd_format_set(get_dict(), s->as_bdd()); } diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index c074caada..e305c526b 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -88,7 +88,7 @@ namespace spot int state_explicit::compare(const spot::state* other) const { - const state_explicit* o = dynamic_cast(other); + const state_explicit* o = down_cast(other); assert(o); // Do not simply return "o - this", it might not fit in an int. if (o < this) @@ -222,7 +222,7 @@ namespace spot const spot::state* global_state, const tgba* global_automaton) const { - const state_explicit* s = dynamic_cast(state); + const state_explicit* s = down_cast(state); assert(s); (void) global_state; (void) global_automaton; @@ -233,7 +233,7 @@ namespace spot bdd tgba_explicit::compute_support_conditions(const spot::state* in) const { - const state_explicit* s = dynamic_cast(in); + const state_explicit* s = down_cast(in); assert(s); const state_explicit::transitions_t& st = s->successors; @@ -247,7 +247,7 @@ namespace spot bdd tgba_explicit::compute_support_variables(const spot::state* in) const { - const state_explicit* s = dynamic_cast(in); + const state_explicit* s = down_cast(in); assert(s); const state_explicit::transitions_t& st = s->successors; @@ -304,7 +304,7 @@ namespace spot std::string tgba_explicit_string::format_state(const spot::state* s) const { - const state_explicit* se = dynamic_cast(s); + const state_explicit* se = down_cast(s); assert(se); sn_map::const_iterator i = state_name_map_.find(se); assert(i != state_name_map_.end()); @@ -332,7 +332,7 @@ namespace spot std::string tgba_explicit_formula::format_state(const spot::state* s) const { - const state_explicit* se = dynamic_cast(s); + const state_explicit* se = down_cast(s); assert(se); sn_map::const_iterator i = state_name_map_.find(se); assert(i != state_name_map_.end()); @@ -357,7 +357,7 @@ namespace spot std::string tgba_explicit_number::format_state(const spot::state* s) const { - const state_explicit* se = dynamic_cast(s); + const state_explicit* se = down_cast(s); assert(se); sn_map::const_iterator i = state_name_map_.find(se); assert(i != state_name_map_.end()); diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 9ab757beb..a8f3df0c4 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -206,7 +206,7 @@ namespace spot const label& get_label(const spot::state* s) const { - const state_explicit* se = dynamic_cast(s); + const state_explicit* se = down_cast(s); assert(se); return get_label(se); } diff --git a/src/tgba/tgbakvcomplement.cc b/src/tgba/tgbakvcomplement.cc index 7c5a5b228..29c20fec1 100644 --- a/src/tgba/tgbakvcomplement.cc +++ b/src/tgba/tgbakvcomplement.cc @@ -137,7 +137,7 @@ namespace spot state_kv_complement::compare(const state* o) const { const state_kv_complement* other = - dynamic_cast(o); + down_cast(o); if (other == 0) return 1; @@ -632,7 +632,7 @@ namespace spot const tgba*) const { const state_kv_complement* state = - dynamic_cast(local_state); + down_cast(local_state); assert(state); return new tgba_kv_complement_succ_iterator(automaton_, @@ -650,7 +650,7 @@ namespace spot tgba_kv_complement::format_state(const state* state) const { const state_kv_complement* s = - dynamic_cast(state); + down_cast(state); assert(s); std::ostringstream ss; ss << "{ set: {" << std::endl; diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 27637dd09..92573ec60 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -49,7 +49,7 @@ namespace spot int state_product::compare(const state* other) const { - const state_product* o = dynamic_cast(other); + const state_product* o = down_cast(other); assert(o); int res = left_->compare(o->left()); if (res != 0) @@ -353,7 +353,7 @@ namespace spot const tgba* global_automaton) const { const state_product* s = - dynamic_cast(local_state); + down_cast(local_state); assert(s); // If global_automaton is not specified, THIS is the root of a @@ -381,7 +381,7 @@ namespace spot bdd tgba_product::compute_support_conditions(const state* in) const { - const state_product* s = dynamic_cast(in); + const state_product* s = down_cast(in); assert(s); bdd lsc = left_->support_conditions(s->left()); bdd rsc = right_->support_conditions(s->right()); @@ -391,7 +391,7 @@ namespace spot bdd tgba_product::compute_support_variables(const state* in) const { - const state_product* s = dynamic_cast(in); + const state_product* s = down_cast(in); assert(s); bdd lsc = left_->support_variables(s->left()); bdd rsc = right_->support_variables(s->right()); @@ -407,7 +407,7 @@ namespace spot std::string tgba_product::format_state(const state* state) const { - const state_product* s = dynamic_cast(state); + const state_product* s = down_cast(state); assert(s); return (left_->format_state(s->left()) + " * " @@ -417,7 +417,7 @@ namespace spot state* tgba_product::project_state(const state* s, const tgba* t) const { - const state_product* s2 = dynamic_cast(s); + const state_product* s2 = down_cast(s); assert(s2); if (t == this) return s2->clone(); @@ -443,7 +443,7 @@ namespace spot tgba_product::transition_annotation(const tgba_succ_iterator* t) const { const tgba_succ_iterator_product* i = - dynamic_cast(t); + down_cast(t); assert(i); std::string left = left_->transition_annotation(i->left_); std::string right = right_->transition_annotation(i->right_); diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index 0e4fd053e..e40161a0e 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -917,7 +917,7 @@ namespace spot { if (other == this) return 0; - const state_complement* s = dynamic_cast(other); + const state_complement* s = down_cast(other); if (s == 0) return 1; #if TRANSFORM_TO_TBA @@ -1189,7 +1189,7 @@ namespace spot { const safra_tree_automaton* a = static_cast(safra_); const state_complement* s = - dynamic_cast(local_state); + down_cast(local_state); assert(s); safra_tree_automaton::automaton_t::const_iterator tr = a->automaton.find(const_cast(s->get_safra())); @@ -1282,7 +1282,7 @@ namespace spot tgba_safra_complement::format_state(const state* state) const { const state_complement* s = - dynamic_cast(state); + down_cast(state); assert(s); return s->to_string(); } @@ -1311,7 +1311,7 @@ namespace spot tgba_safra_complement::compute_support_conditions(const state* state) const { const safra_tree_automaton* a = static_cast(safra_); - const state_complement* s = dynamic_cast(state); + const state_complement* s = down_cast(state); assert(s); typedef safra_tree_automaton::automaton_t::const_iterator auto_it; typedef safra_tree_automaton::transition_list::const_iterator trans_it; @@ -1331,7 +1331,7 @@ namespace spot tgba_safra_complement::compute_support_variables(const state* state) const { const safra_tree_automaton* a = static_cast(safra_); - const state_complement* s = dynamic_cast(state); + const state_complement* s = down_cast(state); assert(s); typedef safra_tree_automaton::automaton_t::const_iterator auto_it; typedef safra_tree_automaton::transition_list::const_iterator trans_it; diff --git a/src/tgba/tgbasgba.cc b/src/tgba/tgbasgba.cc index 051cea4f8..cbdbb629e 100644 --- a/src/tgba/tgbasgba.cc +++ b/src/tgba/tgbasgba.cc @@ -67,7 +67,7 @@ namespace spot compare(const state* other) const { const state_sgba_proxy* o = - dynamic_cast(other); + down_cast(other); assert(o); int res = s_->compare(o->real_state()); if (res != 0) @@ -198,7 +198,7 @@ namespace spot const tgba* global_automaton) const { const state_sgba_proxy* s = - dynamic_cast(local_state); + down_cast(local_state); assert(s); tgba_succ_iterator* it = a_->succ_iter(s->real_state(), @@ -216,7 +216,7 @@ namespace spot std::string tgba_sgba_proxy::format_state(const state* state) const { - const state_sgba_proxy* s = dynamic_cast(state); + const state_sgba_proxy* s = down_cast(state); assert(s); std::string a; if (!emulate_acc_cond_) @@ -248,7 +248,7 @@ namespace spot tgba_sgba_proxy::state_acceptance_conditions(const state* state) const { const state_sgba_proxy* s = - dynamic_cast(state); + down_cast(state); assert(s); if (emulate_acc_cond_) return acceptance_condition_; @@ -259,7 +259,7 @@ namespace spot tgba_sgba_proxy::compute_support_conditions(const state* state) const { const state_sgba_proxy* s = - dynamic_cast(state); + down_cast(state); assert(s); if (emulate_acc_cond_) @@ -271,7 +271,7 @@ namespace spot tgba_sgba_proxy::compute_support_variables(const state* state) const { const state_sgba_proxy* s = - dynamic_cast(state); + down_cast(state); assert(s); if (emulate_acc_cond_) diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 2c728f9e1..6eb19351d 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -80,7 +80,7 @@ namespace spot virtual int compare(const state* other) const { - const state_tba_proxy* o = dynamic_cast(other); + const state_tba_proxy* o = down_cast(other); assert(o); int res = s_->compare(o->real_state()); if (res != 0) @@ -334,7 +334,7 @@ namespace spot const tgba* global_automaton) const { const state_tba_proxy* s = - dynamic_cast(local_state); + down_cast(local_state); assert(s); tgba_succ_iterator* it = a_->succ_iter(s->real_state(), @@ -374,7 +374,7 @@ namespace spot std::string tgba_tba_proxy::format_state(const state* state) const { - const state_tba_proxy* s = dynamic_cast(state); + const state_tba_proxy* s = down_cast(state); assert(s); std::string a = bdd_format_accset(get_dict(), s->acceptance_cond()); if (a != "") @@ -385,7 +385,7 @@ namespace spot state* tgba_tba_proxy::project_state(const state* s, const tgba* t) const { - const state_tba_proxy* s2 = dynamic_cast(s); + const state_tba_proxy* s2 = down_cast(s); assert(s2); if (t == this) return s2->clone(); @@ -409,7 +409,7 @@ namespace spot tgba_tba_proxy::compute_support_conditions(const state* state) const { const state_tba_proxy* s = - dynamic_cast(state); + down_cast(state); assert(s); return a_->support_conditions(s->real_state()); } @@ -418,7 +418,7 @@ namespace spot tgba_tba_proxy::compute_support_variables(const state* state) const { const state_tba_proxy* s = - dynamic_cast(state); + down_cast(state); assert(s); return a_->support_variables(s->real_state()); } @@ -481,7 +481,7 @@ namespace spot tgba_sba_proxy::state_is_accepting(const state* state) const { const state_tba_proxy* s = - dynamic_cast(state); + down_cast(state); assert(s); return bddtrue == s->acceptance_cond(); } diff --git a/src/tgba/tgbaunion.cc b/src/tgba/tgbaunion.cc index 1f5c8301c..3089a3b0b 100644 --- a/src/tgba/tgbaunion.cc +++ b/src/tgba/tgbaunion.cc @@ -45,7 +45,7 @@ namespace spot int state_union::compare(const state* other) const { - const state_union* o = dynamic_cast(other); + const state_union* o = down_cast(other); assert(o); // Initial state if (!o->left() && !o->right()) @@ -278,7 +278,7 @@ namespace spot { (void) global_state; (void) global_automaton; - const state_union* s = dynamic_cast(local_state); + const state_union* s = down_cast(local_state); assert(s); tgba_succ_iterator_union* res = 0; // Is it the initial state ? @@ -323,7 +323,7 @@ namespace spot bdd tgba_union::compute_support_conditions(const state* in) const { - const state_union* s = dynamic_cast(in); + const state_union* s = down_cast(in); assert(s); if (!s->left() && !s->right()) return (left_->support_conditions(left_->get_init_state()) @@ -337,7 +337,7 @@ namespace spot bdd tgba_union::compute_support_variables(const state* in) const { - const state_union* s = dynamic_cast(in); + const state_union* s = down_cast(in); assert(s); if (!s->left() && !s->right()) return (left_->support_variables(left_->get_init_state()) @@ -357,7 +357,7 @@ namespace spot std::string tgba_union::format_state(const state* target_state) const { - const state_union* s = dynamic_cast(target_state); + const state_union* s = down_cast(target_state); assert(s); if (!s->left() && !s->right()) { @@ -375,7 +375,7 @@ namespace spot state* tgba_union::project_state(const state* s, const tgba* t) const { - const state_union* s2 = dynamic_cast(s); + const state_union* s2 = down_cast(s); assert(s2); // We can't project the initial state of our union. if (!s2->left() && !s2->right()) diff --git a/src/tgba/wdbacomp.cc b/src/tgba/wdbacomp.cc index 345ed775a..0e81ad9d8 100644 --- a/src/tgba/wdbacomp.cc +++ b/src/tgba/wdbacomp.cc @@ -58,7 +58,7 @@ namespace spot compare(const state* other) const { const state_wdba_comp_proxy* o = - dynamic_cast(other); + down_cast(other); assert(o); const state* oo = o->real_state(); if (s_ == 0) @@ -195,7 +195,7 @@ namespace spot const tgba* global_automaton = 0) const { const state_wdba_comp_proxy* s = - dynamic_cast(local_state); + down_cast(local_state); assert(s); const state* o = s->real_state(); @@ -216,7 +216,7 @@ namespace spot format_state(const state* ostate) const { const state_wdba_comp_proxy* s = - dynamic_cast(ostate); + down_cast(ostate); assert(s); const state* rs = s->real_state(); if (rs) @@ -229,7 +229,7 @@ namespace spot project_state(const state* s, const tgba* t) const { const state_wdba_comp_proxy* s2 = - dynamic_cast(s); + down_cast(s); assert(s2); if (t == this) return s2->clone(); @@ -253,7 +253,7 @@ namespace spot compute_support_conditions(const state* ostate) const { const state_wdba_comp_proxy* s = - dynamic_cast(ostate); + down_cast(ostate); assert(s); const state* rs = s->real_state(); if (rs) @@ -265,7 +265,7 @@ namespace spot virtual bdd compute_support_variables(const state* ostate) const { const state_wdba_comp_proxy* s = - dynamic_cast(ostate); + down_cast(ostate); assert(s); const state* rs = s->real_state(); if (rs) diff --git a/src/tgbaalgos/ndfs_result.hxx b/src/tgbaalgos/ndfs_result.hxx index 07b6cb87b..560558d12 100644 --- a/src/tgbaalgos/ndfs_result.hxx +++ b/src/tgbaalgos/ndfs_result.hxx @@ -82,7 +82,7 @@ namespace spot acss_states() const { // all visited states are in the state space search - return dynamic_cast(this)->h_.size(); + return static_cast(this)->h_.size(); } }; diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc index e9c5ece0b..cdbe2a241 100644 --- a/src/tgbaalgos/reductgba_sim.cc +++ b/src/tgbaalgos/reductgba_sim.cc @@ -234,8 +234,8 @@ namespace spot duplicator_node::compare(spoiler_node* n) { return (this->spoiler_node::compare(n) && - (label_ == dynamic_cast(n)->get_label()) && - (acc_ == dynamic_cast(n)->get_acc())); + (label_ == static_cast(n)->get_label()) && + (acc_ == static_cast(n)->get_acc())); } bdd diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc index 38c837f7e..6ac08a572 100644 --- a/src/tgbaalgos/reductgba_sim_del.cc +++ b/src/tgbaalgos/reductgba_sim_del.cc @@ -89,18 +89,18 @@ namespace spot if (i != lnode_succ->end()) { tmpmax = - dynamic_cast(*i)->get_progress_measure(); - if (dynamic_cast(*i)->get_lead_2_acc_all()) + static_cast(*i)->get_progress_measure(); + if (static_cast(*i)->get_lead_2_acc_all()) tmpmaxwin = tmpmax; ++i; } for (; i != lnode_succ->end(); ++i) { tmp = - dynamic_cast(*i)->get_progress_measure(); + static_cast(*i)->get_progress_measure(); if (tmp > tmpmax) tmpmax = tmp; - if (dynamic_cast(*i)->get_lead_2_acc_all() && + if (static_cast(*i)->get_lead_2_acc_all() && (tmp > tmpmaxwin)) tmpmaxwin = tmp; } @@ -126,7 +126,7 @@ namespace spot { return (this->spoiler_node::compare(n) && (acceptance_condition_visited_ == - dynamic_cast(n)-> + static_cast(n)-> get_acceptance_condition_visited())); } @@ -193,7 +193,7 @@ namespace spot seen_ = true; for (sn_v::iterator i = lnode_succ->begin(); i != lnode_succ->end(); ++i) - dynamic_cast(*i)->set_lead_2_acc_all(acc); + static_cast(*i)->set_lead_2_acc_all(acc); } else { @@ -246,17 +246,17 @@ namespace spot if (i != lnode_succ->end()) { tmpmin = - dynamic_cast(*i)->get_progress_measure(); - if (dynamic_cast(*i)->get_lead_2_acc_all()) + static_cast(*i)->get_progress_measure(); + if (static_cast(*i)->get_lead_2_acc_all()) tmpminwin = tmpmin; ++i; } for (; i != lnode_succ->end(); ++i) { - tmp = dynamic_cast(*i)->get_progress_measure(); + tmp = static_cast(*i)->get_progress_measure(); if (tmp < tmpmin) tmpmin = tmp; - if (dynamic_cast(*i)->get_lead_2_acc_all() && + if (static_cast(*i)->get_lead_2_acc_all() && (tmp > tmpminwin)) tmpminwin = tmp; } @@ -333,7 +333,7 @@ namespace spot for (sn_v::iterator i = lnode_succ->begin(); i != lnode_succ->end(); ++i) lead_2_acc_all_ - |= dynamic_cast(*i)->set_lead_2_acc_all(acc); + |= static_cast(*i)->set_lead_2_acc_all(acc); } return lead_2_acc_all_; } @@ -398,7 +398,7 @@ namespace spot for (si->first(); !si->done(); si->next()) { bdd btmp = si->current_acceptance_conditions() | - dynamic_cast(sn)-> + static_cast(sn)-> get_acceptance_condition_visited(); s_v::iterator i1; @@ -505,7 +505,7 @@ namespace spot { exist = true; delete dn_n; - dn_n = dynamic_cast(*i); + dn_n = static_cast(*i); break; } } @@ -536,7 +536,7 @@ namespace spot { exist = true; delete sn_n; - sn_n = dynamic_cast(*i); + sn_n = static_cast(*i); break; } } @@ -590,9 +590,9 @@ namespace spot = spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i) { - if ((dynamic_cast(*i)->get_progress_measure() + if ((static_cast(*i)->get_progress_measure() < nb_spoiler_loose_ + 1) && - (dynamic_cast(*i) + (static_cast(*i) ->get_acceptance_condition_visited() == bddfalse)) { p = new state_couple((*i)->get_spoiler_node(),