diff --git a/src/ta/ta.hh b/src/ta/ta.hh index 75b49962b..553bfacf5 100644 --- a/src/ta/ta.hh +++ b/src/ta/ta.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2010, 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Developpement de l Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -25,7 +25,6 @@ #include #include "misc/bddlt.hh" #include "tgba/tgba.hh" -#include "tgba/bdddict.hh" namespace spot { @@ -78,10 +77,11 @@ namespace spot { protected: acc_cond acc_; + bdd_dict_ptr dict_; public: ta(const bdd_dict_ptr& d) - : acc_(d) + : dict_(d) { } @@ -138,7 +138,7 @@ namespace spot bdd_dict_ptr get_dict() const { - return acc_.get_dict(); + return dict_; } /// \brief Format the state as a string for printing. diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index 8af7e0646..c7fbf35a6 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -23,7 +23,7 @@ # include # include # include -# include "bdddict.hh" +# include # include "ltlenv/defaultenv.hh" namespace spot @@ -191,8 +191,8 @@ namespace spot } }; - acc_cond(const bdd_dict_ptr& dict, unsigned n_sets = 0) - : d_(dict), num_(0U), all_(0U) + acc_cond(unsigned n_sets = 0) + : num_(0U), all_(0U) { add_sets(n_sets); } @@ -206,11 +206,6 @@ namespace spot { } - const bdd_dict_ptr& get_dict() const - { - return d_; - } - unsigned add_sets(unsigned num) { if (num == 0) @@ -426,7 +421,6 @@ namespace spot return r; } - bdd_dict_ptr d_; unsigned num_; mark_t::value_t all_; }; diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index f917aa35b..8d6aafa54 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement de +// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et Developpement 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 @@ -28,7 +28,7 @@ namespace spot { tgba::tgba(const bdd_dict_ptr& d) : iter_cache_(nullptr), - acc_(d), + dict_(d), last_support_conditions_input_(0) { props = 0U; diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 16dcd3769..37d4b2503 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2011, 2013, 2014, 2015 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. @@ -25,6 +25,7 @@ #include "fwd.hh" #include "acc.hh" +#include "bdddict.hh" #include #include #include @@ -473,7 +474,7 @@ namespace spot tgba(const bdd_dict_ptr& d); // Any iterator returned via release_iter. mutable tgba_succ_iterator* iter_cache_; - + bdd_dict_ptr dict_; public: #ifndef SWIG @@ -577,7 +578,7 @@ namespace spot /// different formula), or simply when printing. bdd_dict_ptr get_dict() const { - return acc_.get_dict(); + return dict_; } /// \brief Format the state as a string for printing. diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index a82fc9e47..b08e84978 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -339,7 +339,7 @@ namespace spot if (num < acc_.num_sets()) { acc_.~acc_cond(); - new (&acc_) acc_cond(get_dict()); + new (&acc_) acc_cond; } acc_.add_sets(num - acc_.num_sets()); prop_single_acc_set(num == 1); diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index ab0999494..26167dcbd 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -246,7 +246,7 @@ namespace spot struct dict { dict(const const_tgba_ptr& a) - : aut(a), cacc(a->get_dict()) + : aut(a) { } diff --git a/src/tgbatest/acc.cc b/src/tgbatest/acc.cc index e24919cef..1bc97e565 100644 --- a/src/tgbatest/acc.cc +++ b/src/tgbatest/acc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement +// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -36,8 +36,7 @@ void check(spot::acc_cond& ac, spot::acc_cond::mark_t m) int main() { - auto d = spot::make_bdd_dict(); - spot::acc_cond ac(d, 4); + spot::acc_cond ac(4); auto m1 = ac.marks({0, 2}); auto m2 = ac.marks({0, 3}); @@ -62,10 +61,10 @@ int main() check(ac, m2 & m3); check(ac, ac.comp(m2 & m3)); - spot::acc_cond ac2(d, ac.num_sets()); + spot::acc_cond ac2(ac.num_sets()); check(ac2, m3); - spot::acc_cond ac3(d, ac.num_sets() + ac2.num_sets()); + spot::acc_cond ac3(ac.num_sets() + ac2.num_sets()); std::cout << ac.num_sets() << " + " << ac2.num_sets() << " = " << ac3.num_sets() << '\n'; auto m5 = ac3.join(ac, m2, ac2, m3); @@ -85,7 +84,7 @@ int main() }; std::cout << '\n'; - spot::acc_cond ac4(d); + spot::acc_cond ac4; check(ac4, ac4.all_sets()); check(ac4, ac4.comp(ac4.all_sets())); @@ -104,4 +103,3 @@ int main() } } -