diff --git a/src/priv/Makefile.am b/src/priv/Makefile.am index 9bcb75b4a..0fd46aefc 100644 --- a/src/priv/Makefile.am +++ b/src/priv/Makefile.am @@ -24,6 +24,7 @@ noinst_HEADERS = \ acccompl.hh \ accconv.hh \ bddalloc.hh \ + countstates.hh \ freelist.hh noinst_LTLIBRARIES = libpriv.la @@ -31,6 +32,7 @@ libpriv_la_SOURCES = \ acccompl.cc \ accconv.cc \ bddalloc.cc \ + countstates.cc \ freelist.cc diff --git a/src/priv/countstates.cc b/src/priv/countstates.cc new file mode 100644 index 000000000..2eec96252 --- /dev/null +++ b/src/priv/countstates.cc @@ -0,0 +1,41 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013 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 3 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 this program. If not, see . + +#include "countstates.hh" +#include "tgba/tgbaexplicit.hh" +#include "tgbaalgos/stats.hh" + +namespace spot +{ + unsigned count_states(const tgba* a) + { + const sba_explicit_number* se = + dynamic_cast(a); + if (se) + return se->num_states(); + const tgba_explicit_number* te = + dynamic_cast(a); + if (te) + return te->num_states(); + tgba_statistics st = stats_reachable(a); + return st.states; + } + + +} diff --git a/src/priv/countstates.hh b/src/priv/countstates.hh new file mode 100644 index 000000000..03437bbd0 --- /dev/null +++ b/src/priv/countstates.hh @@ -0,0 +1,29 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013 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 3 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 this program. If not, see . + +#ifndef SPOT_PRIV_COUNTSTATES_HH +# define SPOT_PRIV_COUNTSTATES_HH + +namespace spot +{ + class tgba; + unsigned count_states(const tgba* a); +} + +#endif // SPOT_PRIV_COUNTSTATES_HH diff --git a/src/saba/sabacomplementtgba.cc b/src/saba/sabacomplementtgba.cc index 1c9aae374..a786125c3 100644 --- a/src/saba/sabacomplementtgba.cc +++ b/src/saba/sabacomplementtgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -28,7 +28,7 @@ #include "misc/hashfunc.hh" #include "ltlast/formula.hh" #include "ltlast/constant.hh" -#include "tgbaalgos/stats.hh" +#include "priv/countstates.hh" #include "sabacomplementtgba.hh" #include "explicitstateconjunction.hh" @@ -376,10 +376,7 @@ namespace spot int v = get_dict() ->register_acceptance_variable(ltl::constant::true_instance(), this); the_acceptance_cond_ = bdd_ithvar(v); - { - spot::tgba_statistics a_size = spot::stats_reachable(automaton_); - nb_states_ = a_size.states; - } + nb_states_ = count_states(automaton_); } saba_complement_tgba::~saba_complement_tgba() diff --git a/src/tgba/tgbakvcomplement.cc b/src/tgba/tgbakvcomplement.cc index 808437ba2..07e930a16 100644 --- a/src/tgba/tgbakvcomplement.cc +++ b/src/tgba/tgbakvcomplement.cc @@ -29,7 +29,7 @@ #include "misc/hashfunc.hh" #include "ltlast/formula.hh" #include "ltlast/constant.hh" -#include "tgbaalgos/stats.hh" +#include "priv/countstates.hh" namespace spot { @@ -601,10 +601,7 @@ namespace spot int v = get_dict() ->register_acceptance_variable(ltl::constant::true_instance(), this); the_acceptance_cond_ = bdd_ithvar(v); - { - spot::tgba_statistics a_size = spot::stats_reachable(automaton_); - nb_states_ = a_size.states; - } + nb_states_ = count_states(automaton_); get_acc_list(); } diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 3df72d895..5f37f80e5 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -45,7 +46,7 @@ #include "tgbaalgos/scc.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/bfssteps.hh" -#include "tgbaalgos/stats.hh" +#include "priv/countstates.hh" namespace spot { @@ -535,7 +536,7 @@ namespace spot // This corresponds to the algorithm in Fig. 1 of "Efficient // minimization of deterministic weak omega-automata" written by - // Christof Löding and published in Information Processing + // Christof Löding and published in Information Processing // Letters 79 (2001) pp 105--109. // We also keep track of whether an SCC is useless @@ -554,7 +555,7 @@ namespace spot unsigned k = (scc_count | 1) + 1; // SCC are numbered in topological order - // (but in the reverse order as Löding's) + // (but in the reverse order as Löding's) for (unsigned m = 0; m < scc_count; ++m) { bool is_useless = true; @@ -628,8 +629,8 @@ namespace spot if (reject_bigger) { // Abort if min_aut_f has more states than aut_f. - tgba_statistics orig_size = stats_reachable(aut_f); - if (orig_size.states < min_aut_f->num_states()) + unsigned orig_states = count_states(aut_f); + if (orig_states < min_aut_f->num_states()) { delete min_aut_f; return const_cast(aut_f); diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index df70a2abe..cb3768063 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -22,26 +22,13 @@ #include "simulation.hh" #include "sccfilter.hh" #include "degen.hh" -#include "stats.hh" #include "stripacc.hh" #include #include "misc/optionmap.hh" +#include "priv/countstates.hh" namespace spot { - unsigned count_states(const tgba* a) - { - const sba_explicit_number* se = - dynamic_cast(a); - if (se) - return se->num_states(); - const tgba_explicit_number* te = - dynamic_cast(a); - if (te) - return te->num_states(); - tgba_statistics st = stats_reachable(a); - return st.states; - } postprocessor::postprocessor(const option_map* opt) : type_(TGBA), pref_(Small), level_(High),