Line data    Source code

       1             : // Author(s): Jan Friso Groote
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file lts/detail/embedded_list.h
      10             : 
      11             : #ifndef _EMBEDDED_LIST_H
      12             : #define _EMBEDDED_LIST_H
      13             : 
      14             : #include <cassert>
      15             : #include <vector>
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace lts
      20             : {
      21             : namespace detail
      22             : {
      23             : 
      24             : // The list type below embeds a list in existing data structures. 
      25             : // For instance if elements are stored in a vector, and should also
      26             : // be linked in a particular order in a list this data structure can be 
      27             : // used.
      28             : //
      29             : // For this purpose to each data structure that must be put in an embedded
      30             : // list the embedded_list_node must be added to the data structure. 
      31             : //
      32             : // From that point on the embedded_list data type can be used to construct
      33             : // an embedded list. The data structure, once created will not require
      34             : // extra memory. 
      35             : 
      36             : // prototype.
      37             : template < class TYPE > class embedded_list;
      38             : 
      39             : template <class TYPE>
      40             : class embedded_list_node
      41             : {
      42             :  
      43             :   template < class T > friend class embedded_list;
      44             : 
      45             :   protected:
      46             :      TYPE* m_next;  // Points to the next element in the list. The nullptr if it does not exist.
      47             :      TYPE* m_prev;  // Points to the current element in the list. The nullptr if it does not exist.
      48             : };
      49             : 
      50             : 
      51             : template < class TYPE >
      52             : class embedded_list
      53             : {
      54             :   protected:
      55             :     TYPE* m_first;   // Points to the last element of the list. nulllptr if not valid.
      56             :     TYPE* m_last;    // Points to the first element of the list
      57             :     std::size_t m_size;   // The number of elements in the list.
      58             : 
      59             :   protected:
      60             : 
      61        5527 :     bool check_this_embedded_list() const
      62             :     {
      63        5527 :       std::size_t count_up=0;
      64      176317 :       for(TYPE* walker=m_first; walker!=nullptr && count_up<=m_size ; walker=walker->m_next)
      65             :       {
      66      170790 :         count_up++;
      67             :       }
      68             : 
      69        5527 :       std::size_t count_down=0;
      70      176317 :       for(TYPE* walker=m_last; walker!=nullptr && count_down<=m_size ; walker=walker->m_prev)
      71             :       {
      72      170790 :         count_down++;
      73             :       }
      74             : 
      75        5527 :       return m_size==count_up && m_size==count_down;
      76             :     }
      77             : 
      78        1627 :     bool check_presence(const TYPE& e) const
      79             :     {
      80       30893 :       for(TYPE* walker=m_first; walker!=nullptr; walker=walker->m_next)
      81             :       {
      82       30893 :         if (walker==&e)
      83             :         {
      84        1627 :           return true;
      85             :         }
      86             :       }
      87           0 :       return false;
      88             :     }
      89             : 
      90             : 
      91             : 
      92             :   public:
      93             :     
      94             :     // Constructor.
      95         774 :     embedded_list()
      96         774 :       : m_first(nullptr), m_last(nullptr), m_size(0)
      97         774 :     {}
      98             : 
      99             :     // Copy constructor.
     100             :     embedded_list(const embedded_list& other) = default;
     101             : 
     102             :     // Assignment.
     103             :     embedded_list& operator=(const embedded_list& other) = default;
     104             : 
     105             :     // get the size
     106        3166 :     std::size_t size() const
     107             :     {
     108        3166 :       return m_size;
     109             :     }
     110             : 
     111             :     // Get the first element of the list.
     112         108 :     TYPE& front() 
     113             :     {
     114         108 :       assert(m_size>0);
     115         108 :       return *m_first;
     116             :     }
     117             : 
     118             :     // Get the last element of the list.
     119          36 :     TYPE& back() 
     120             :     {
     121          36 :       assert(m_size>0);
     122          36 :       return *m_last;
     123             :     }
     124             : 
     125             :     // Insert an element at the end of the list. Note that the element e is changed.
     126        2895 :     void push_back(TYPE& e)
     127             :     {
     128        2895 :       if (m_first==nullptr)
     129             :       {
     130         433 :         assert(m_last==nullptr && m_size==0);
     131         433 :         m_first= &e;
     132         433 :         e.m_prev= nullptr;
     133             :       }
     134             :       else 
     135             :       {
     136        2462 :         assert(m_last!=nullptr && m_size>0);
     137        2462 :         e.m_prev=m_last;
     138        2462 :         m_last->m_next=&e;
     139             :       }
     140        2895 :       e.m_next=nullptr;
     141        2895 :       m_last= &e;
     142        2895 :       m_size++;
     143        2895 :       assert(check_this_embedded_list());
     144        2895 :     }
     145             : 
     146             :     // Insert an element at the begining of the list. Note that the element e is changed.
     147             :     void push_front(TYPE& e)
     148             :     {
     149             :       if (m_last==nullptr)
     150             :       {
     151             :         assert(m_first==nullptr && m_size==0);
     152             :         m_last= &e;
     153             :         e.m_next= nullptr;
     154             :       }
     155             :       else 
     156             :       {
     157             :         assert(m_first!=nullptr && m_size>0);
     158             :         e.m_next=m_first;
     159             :         m_first->m_prev=&e;
     160             :       }
     161             :       e.m_prev=nullptr;
     162             :       m_first= &e;
     163             :       m_size++;
     164             :       assert(check_this_embedded_list());
     165             :     }
     166             : 
     167             :     // Erase this element from the list. The list is adapted such that it does not contain
     168             :     // element e anymore. Postcondition: The previous and next pointer in e are invalid. 
     169        1627 :     void erase(TYPE& e)
     170             :     {
     171        1627 :       assert(check_presence(e));
     172        1627 :       if (e.m_next==nullptr)
     173             :       {
     174         203 :         assert(&e==m_last);
     175         203 :         m_last=e.m_prev;
     176             :       }
     177             :       else
     178             :       {
     179        1424 :         assert(e.m_next->m_prev!=nullptr);
     180        1424 :         e.m_next->m_prev = e.m_prev;
     181             :       }
     182             : 
     183        1627 :       if (e.m_prev==nullptr)
     184             :       {
     185         816 :         assert(&e==m_first);
     186         816 :         m_first=e.m_next;
     187             :       }
     188             :       else
     189             :       {
     190         811 :         assert(e.m_prev->m_next!=nullptr);
     191         811 :         e.m_prev->m_next = e.m_next;
     192             :       }
     193             : 
     194        1627 :       e.m_next= nullptr;
     195        1627 :       e.m_prev= nullptr;
     196             : 
     197        1627 :       m_size--;
     198             : 
     199        1627 :       assert(check_this_embedded_list());
     200        1627 :     }
     201             : 
     202         331 :     void clear() 
     203             :     {
     204         331 :       m_first=nullptr;
     205         331 :       m_last=nullptr;
     206         331 :       m_size=0;
     207         331 :     }
     208             : 
     209             :     /* Append the list l to the current list.  
     210             :        After this operation the list l is replaced by the empty list
     211             :        to prevent unwanted sharing of lists.  */
     212             :        
     213          56 :     void append(embedded_list& l)
     214             :     {
     215          56 :       if (l.size()==0)
     216             :       {
     217           0 :         return;
     218             :       }
     219             : 
     220          56 :       if (m_size==0)
     221             :       {
     222          37 :         *this=l;
     223             :       }
     224             :       else
     225             :       {
     226          19 :         m_last->m_next=l.m_first;
     227          19 :         l.m_first->m_prev=m_last;
     228          19 :         m_last=l.m_last;
     229          19 :         m_size=m_size+l.m_size;
     230             :       }
     231             :       // Explicitly invalidate l.
     232          56 :       l.m_first=nullptr;
     233          56 :       l.m_last=nullptr;
     234          56 :       l.m_size=0;
     235             :       
     236          56 :       assert(check_this_embedded_list());
     237             :     }
     238             : 
     239             :     class iterator 
     240             :     {
     241             :       protected:
     242             :         TYPE* m_ptr;
     243             : 
     244             :       public:
     245             :         
     246        2473 :         iterator(TYPE* p)
     247        2473 :          : m_ptr(p)
     248        2473 :         {}
     249             : 
     250             :         // Prefix increment
     251        3082 :         iterator operator++() 
     252             :         {
     253        3082 :           iterator old=*this;
     254        3082 :           m_ptr=m_ptr->m_next;
     255        3082 :           return old;
     256             :         }
     257             :         
     258             :         // Postfix increment
     259        1061 :         iterator operator++(int) 
     260             :         {
     261        1061 :           m_ptr=m_ptr->m_next;
     262        1061 :           return *this;
     263             :         }
     264             : 
     265             :         // Dereference of the iterator. 
     266        4143 :         TYPE& operator*() 
     267             :         {
     268        4143 :           return *m_ptr;
     269             :         }
     270             : 
     271             :         // Dereference of the iterator. 
     272         600 :         TYPE* operator->() 
     273             :         {
     274         600 :           return m_ptr;
     275             :         }
     276             : 
     277             :        // Equality operator on iterators.
     278        5200 :        bool operator ==(const iterator& other) const
     279             :        {
     280        5200 :          return m_ptr==other.m_ptr;
     281             :        }
     282             :        // Inequality operator on iterators.
     283        5200 :        bool operator !=(const iterator& other) const
     284             :        {
     285        5200 :          return !(*this==other);
     286             :        }
     287             :         
     288             :     };
     289             : 
     290         949 :     iterator begin() const
     291             :     {
     292         949 :       assert(check_this_embedded_list());
     293         949 :       return m_first;
     294             :     }
     295             : 
     296        1524 :     iterator end() const
     297             :     {
     298        1524 :       return nullptr;
     299             :     }
     300             :     
     301             : };
     302             : 
     303             : } // end namespace detail
     304             : } // end namespace lts
     305             : } // end namespace mcrl2
     306             : #endif //_EMBEDDED_LIST_H