diff --git a/spot/kripke/kripke.hh b/spot/kripke/kripke.hh index d9eae2ab2..8edd0b7b0 100644 --- a/spot/kripke/kripke.hh +++ b/spot/kripke/kripke.hh @@ -58,7 +58,7 @@ namespace spot void recycle(SuccIterator*, unsigned tid); /// \brief This method allow to deallocate a given state. - const std::vector get_ap(); + const std::vector ap(); }; #ifndef SWIG @@ -84,7 +84,7 @@ namespace spot std::is_samesucc(State(), 0))>::value && std::is_samerecycle(nullptr, 0))>::value && std::is_same, - decltype(u->get_ap())>::value && + decltype(u->ap())>::value && std::is_samerecycle(nullptr, 0))>::value && // Check the SuccIterator diff --git a/spot/ltsmin/spins_kripke.hh b/spot/ltsmin/spins_kripke.hh index 1e20d3b13..f6e14bd0a 100644 --- a/spot/ltsmin/spins_kripke.hh +++ b/spot/ltsmin/spins_kripke.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement de +// Copyright (C) 2017, 2018, 2019, 2020 Laboratoire de Recherche et Développement de // l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -221,7 +221,7 @@ namespace spot void recycle(cspins_iterator* it, unsigned tid); /// \brief List the atomic propositions used by *this* kripke - const std::vector get_ap(); + const std::vector ap(); /// \brief The number of thread used by *this* kripke unsigned get_threads(); diff --git a/spot/ltsmin/spins_kripke.hxx b/spot/ltsmin/spins_kripke.hxx index 67697aca4..bafb6f641 100644 --- a/spot/ltsmin/spins_kripke.hxx +++ b/spot/ltsmin/spins_kripke.hxx @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de +// Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement de // l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -302,7 +302,7 @@ namespace spot } const std::vector - kripkecube::get_ap() + kripkecube::ap() { return aps_; } diff --git a/spot/mc/mc_instanciator.hh b/spot/mc/mc_instanciator.hh index 060e1ce6e..160117bb6 100644 --- a/spot/mc/mc_instanciator.hh +++ b/spot/mc/mc_instanciator.hh @@ -166,9 +166,9 @@ namespace spot algo == mc_algorithm::SWARMING) { SPOT_ASSERT(prop != nullptr); - SPOT_ASSERT(sys->get_ap().size() == prop->get_ap().size()); - for (unsigned int i = 0; i < sys->get_ap().size(); ++i) - SPOT_ASSERT(sys->get_ap()[i].compare(prop->get_ap()[i]) == 0); + SPOT_ASSERT(sys->ap().size() == prop->ap().size()); + for (unsigned int i = 0; i < sys->ap().size(); ++i) + SPOT_ASSERT(sys->ap()[i].compare(prop->ap()[i]) == 0); } switch (algo) diff --git a/spot/mc/utils.hh b/spot/mc/utils.hh index 7e708f87e..6124f55fa 100644 --- a/spot/mc/utils.hh +++ b/spot/mc/utils.hh @@ -55,7 +55,7 @@ namespace spot res_->new_state(); // Compute the reverse binder. - auto aps = this->sys_.get_ap(); + auto aps = this->sys_.ap(); for (unsigned i = 0; i < aps.size(); ++i) { auto k = res_->register_ap(aps[i]); @@ -72,7 +72,7 @@ namespace spot void edge(unsigned src, unsigned dst) { - cubeset cs(this->sys_.get_ap().size()); + cubeset cs(this->sys_.ap().size()); bdd cond = cube_to_bdd(this->todo.back().it->condition(), cs, reverse_binder_); res_->new_edge(src, dst, cond); @@ -345,7 +345,7 @@ namespace spot names_ = new std::vector(); int i = 0; - for (auto ap : this->twa_->get_ap()) + for (auto ap : this->twa_->ap()) { auto idx = res_->register_ap(ap); reverse_binder_[i++] = idx; diff --git a/spot/twacube/twacube.cc b/spot/twacube/twacube.cc index 11b822c07..9325f76b3 100644 --- a/spot/twacube/twacube.cc +++ b/spot/twacube/twacube.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Developpement de +// Copyright (C) 2015, 2016, 2018, 2020 Laboratoire de Recherche et Developpement de // l'EPITA (LRDE). // // This file is part of Spot, a model checking library. @@ -66,7 +66,7 @@ namespace spot return acc_; } - std::vector twacube::get_ap() const + std::vector twacube::ap() const { return aps_; } diff --git a/spot/twacube/twacube.hh b/spot/twacube/twacube.hh index b9732dbb6..3f2290d9e 100644 --- a/spot/twacube/twacube.hh +++ b/spot/twacube/twacube.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche +// Copyright (C) 2015, 2016, 2020 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -139,7 +139,7 @@ namespace spot acc_cond& acc(); /// \brief Returns the names of the atomic properties. - std::vector get_ap() const; + std::vector ap() const; /// \brief This method creates a new state. unsigned new_state(); diff --git a/spot/twacube_algos/convert.cc b/spot/twacube_algos/convert.cc index ba89ac97c..d376c673b 100644 --- a/spot/twacube_algos/convert.cc +++ b/spot/twacube_algos/convert.cc @@ -154,7 +154,7 @@ namespace spot // Grep bdd id for each atomic propositions std::vector bdds_ref; - for (auto& ap : twacube->get_ap()) + for (auto& ap : twacube->ap()) bdds_ref.push_back(res->register_ap(ap)); // Build all resulting states diff --git a/tests/core/twacube.cc b/tests/core/twacube.cc index fa4b57fe4..9e9b50892 100644 --- a/tests/core/twacube.cc +++ b/tests/core/twacube.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2015, 2016, 2018, 2020 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -52,7 +52,7 @@ int main() spot::print_dot(std::cout, tg, "A"); std::cout << "-----------\n" << *aut << "-----------\n"; - const std::vector& aps = aut->get_ap(); + const std::vector& aps = aut->ap(); unsigned int seed = 17; for (auto it = aut->succ(2); !it->done(); it->next()) { diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc index acf35c447..f2c91e833 100644 --- a/tests/ltsmin/modelcheck.cc +++ b/tests/ltsmin/modelcheck.cc @@ -470,7 +470,7 @@ static int checked_main() { std::vector aps = {}; if (propcube != nullptr) - aps = propcube->get_ap(); + aps = propcube->ap(); modelcube = spot::ltsmin_model::load(mc_options.model) .kripkecube(aps, deadf, mc_options.compress, mc_options.nb_threads);