diff --git a/spot/twacube/cube.cc b/spot/twacube/cube.cc index 10f13f8db..d0c426b0c 100644 --- a/spot/twacube/cube.cc +++ b/spot/twacube/cube.cc @@ -34,9 +34,6 @@ namespace spot ++uint_size_; } - cubeset::~cubeset() - { } - cube cubeset::alloc() const { auto* res = new unsigned int[2*uint_size_]; diff --git a/spot/twacube/cube.hh b/spot/twacube/cube.hh index 6dda9c9e8..dcdecf6ab 100644 --- a/spot/twacube/cube.hh +++ b/spot/twacube/cube.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Developpement de +// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -77,14 +77,13 @@ namespace spot size_t nb_bits_; public: - // Some deleted constructor + // Some default/deleted constructor/destructors cubeset() = delete; + ~cubeset() = default; /// \brief Build the cubeset manager for \a aps variables cubeset(int aps); - virtual ~cubeset(); - /// \brief Allocate a new cube cube alloc() const; diff --git a/spot/twacube/twacube.cc b/spot/twacube/twacube.cc index 563698e92..26b4342d6 100644 --- a/spot/twacube/twacube.cc +++ b/spot/twacube/twacube.cc @@ -30,9 +30,6 @@ namespace spot { } - cstate::~cstate() - { } - unsigned cstate::label() { return id_; @@ -47,12 +44,6 @@ namespace spot cube_(cube), acc_(acc) { } - transition::~transition() - { } - - transition::transition() - { } - twacube::twacube(const std::vector aps): init_(0U), aps_(aps), cubeset_(aps.size()) { @@ -60,7 +51,7 @@ namespace spot twacube::~twacube() { - spot::cubeset cs = get_cubeset(); + const spot::cubeset cs = get_cubeset(); for (unsigned i = 1; i <= theg_.num_edges(); ++i) cs.release(theg_.edge_data(i).cube_); } diff --git a/spot/twacube/twacube.hh b/spot/twacube/twacube.hh index f35917265..0769b3e09 100644 --- a/spot/twacube/twacube.hh +++ b/spot/twacube/twacube.hh @@ -33,11 +33,12 @@ namespace spot class SPOT_API cstate { public: - cstate() {} + cstate() = default; cstate(const cstate& s) = delete; cstate(cstate&& s) noexcept; cstate(unsigned id); - virtual ~cstate(); + ~cstate() = default; + unsigned label(); private: unsigned id_; @@ -47,13 +48,14 @@ namespace spot class SPOT_API transition { public: - cube cube_; - acc_cond::mark_t acc_; - transition(); + transition() = default; transition(const transition& t) = delete; transition(transition&& t) noexcept; transition(const cube& cube, acc_cond::mark_t acc); - virtual ~transition(); + ~transition() = default; + + cube cube_; + acc_cond::mark_t acc_; }; /// \brief Class for iterators over transitions @@ -119,7 +121,7 @@ namespace spot const graph_t::state_storage_t& st_; ///< The underlying states }; - /// \brief Class for representign + /// \brief Class for representing a thread-safe twa. class SPOT_API twacube final: public std::enable_shared_from_this { public: