LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - queue.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 41 0.0 %
Date: 2020-07-11 00:44:39 Functions: 0 8 0.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg
       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             : #ifndef MCRL2_LTS_DETAIL_QUEUE_H
      10             : #define MCRL2_LTS_DETAIL_QUEUE_H
      11             : 
      12             : #include <cassert>
      13             : #include <deque>
      14             : #include "mcrl2/utilities/logger.h"
      15             : 
      16             : namespace mcrl2
      17             : {
      18             : namespace lts
      19             : {
      20             : 
      21             : template <class T>
      22           0 : class queue
      23             : {
      24             :   protected:
      25             :     std::deque <T> queue_get;
      26             :     std::deque <T> queue_put;
      27             :     std::size_t queue_size_max;        // This is the maximal allowed size of a queue.
      28             :     std::size_t queue_put_count_extra; // This represents the number of elements that
      29             :                                        // did not fit in the put queue.
      30             : 
      31           0 :     bool add_to_full_queue(const T& state)
      32             :     {
      33             :       /* We wish that every state has equal chance of being in the queue.
      34             :        * Let N be the size of the queue and M the number of states from which
      35             :        * we can choose. (Note that N <= M; otherwise every state is simply in
      36             :        * the queue. We show that addition of state i, with N < i <= M, should
      37             :        * be done with chance N/i and at random in the queue. With induction
      38             :        * on the difference between M-N we show that doing so leads to a
      39             :        * uniform distribution (i.e. every state has chance N/M of being in the
      40             :        * queue):
      41             :        *
      42             :        * M-N = 0:   Trivial.
      43             :        * M-N = k+1: We added the last state, M, with probability N/M, so we
      44             :        *            need only consider the other states. Before adding state M
      45             :        *            they are in the queue with probability N/(M-1) (by
      46             :        *            induction) and if the last state is added, they are still
      47             :        *            in the queue afterwards with probability 1-1/N. So:
      48             :        *
      49             :        *              N/(M-1) ( N/M ( 1 - 1/N ) + ( 1 - N/M ) )
      50             :        *            =
      51             :        *              N/(M-1) ( N/M (N-1)/N + (M-N)/M )
      52             :        *            =
      53             :        *              N/(M-1) ( (N-1)/M + (M-N)/M )
      54             :        *            =
      55             :        *              N/(M-1) (M-1)/M
      56             :        *            =
      57             :        *              N/M
      58             :        *
      59             :        *
      60             :        * Here we have that N = queue_size and
      61             :        * i = queue_put_count + queue_put_count_extra.
      62             :        */
      63             : 
      64           0 :       assert(queue_size_max == queue_put.size());
      65           0 :       queue_put_count_extra++;
      66           0 :       if ((rand() % (queue_put.size() + queue_put_count_extra)) < queue_put.size())
      67             :       {
      68           0 :         std::size_t pos = rand() % queue_put.size();
      69           0 :         queue_put[pos]=state;
      70             :       }
      71           0 :       return false;
      72             :     }
      73             : 
      74             :   public:
      75           0 :     queue() :
      76           0 :       queue_size_max(std::numeric_limits<size_t>::max()),
      77           0 :       queue_put_count_extra(0)
      78             :     {
      79           0 :     }
      80             : 
      81             :     std::size_t max_size() const
      82             :     {
      83             :       return queue_size_max;
      84             :     }
      85             : 
      86           0 :     void set_max_size(std::size_t max_size)
      87             :     {
      88           0 :       queue_size_max = max_size;
      89           0 :       if (queue_put.size() > queue_size_max)
      90             :       {
      91           0 :         queue_put.resize(queue_size_max);
      92           0 :         mCRL2log(log::warning) << "Resizing put queue loses elements." << std::endl;
      93             :       }
      94           0 :       if (queue_get.size() > queue_size_max)
      95             :       {
      96           0 :         queue_get.resize(queue_size_max);
      97           0 :         mCRL2log(log::warning) << "Resizing get queue loses elements." << std::endl;
      98             :       }
      99           0 :     }
     100             : 
     101             :     /// \brief Add state to queue, if there is place. Return whether insertion led to an increase of the queue.
     102             :     /// \details If the queue is full, it is randomly decided whether the element is inserted, and if so
     103             :     ///          which element is replaced. This is done such that all elements have a uniform probability of
     104             :     ///          being inserted. 
     105           0 :     bool add_to_queue(const T& state)
     106             :     {
     107           0 :       if (queue_put.size() >= queue_size_max)
     108             :       {
     109           0 :         assert(queue_put.size() == queue_size_max);
     110           0 :         return add_to_full_queue(state);
     111             :       }
     112             : 
     113           0 :       assert(queue_put_count_extra==0);
     114           0 :       queue_put.push_back(state);
     115           0 :       return true;
     116             :     }
     117             : 
     118           0 :     T get_from_queue()
     119             :     {
     120           0 :       if (remaining() == 0)
     121             :       {
     122           0 :         return T();
     123             :       }
     124             :       else
     125             :       {
     126           0 :         T result = queue_get.front();
     127           0 :         queue_get.pop_front();
     128           0 :         return result;
     129             :       }
     130             :     }
     131             : 
     132           0 :     std::size_t remaining()
     133             :     {
     134           0 :       return queue_get.size();
     135             :     }
     136             : 
     137           0 :     void swap_queues()
     138             :     {
     139           0 :       queue_get.swap(queue_put);
     140           0 :       queue_put.clear();
     141           0 :       queue_put_count_extra = 0;
     142           0 :     }
     143             : };
     144             : 
     145             : }
     146             : 
     147             : }
     148             : 
     149             : #endif // MCRL2_LTS_DETAIL_QUEUE_H

Generated by: LCOV version 1.13