LCOV - code coverage report
Current view: top level - pg/include/mcrl2/pg - LinPredLiftingStrategy.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 22 0.0 %
Date: 2024-03-08 02:52:28 Functions: 0 4 0.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Copyright (c) 2009-2013 University of Twente
       2             : // Copyright (c) 2009-2013 Michael Weber <michaelw@cs.utwente.nl>
       3             : // Copyright (c) 2009-2013 Maks Verver <maksverver@geocities.com>
       4             : // Copyright (c) 2009-2013 Eindhoven University of Technology
       5             : //
       6             : // Distributed under the Boost Software License, Version 1.0.
       7             : // (See accompanying file LICENSE_1_0.txt or copy at
       8             : // http://www.boost.org/LICENSE_1_0.txt)
       9             : 
      10             : #ifndef MCRL2_PG_LINPRED_LIFTING_STRATEGY_H
      11             : #define MCRL2_PG_LINPRED_LIFTING_STRATEGY_H
      12             : 
      13             : #include "mcrl2/pg/SmallProgressMeasures.h"
      14             : 
      15             : /*! \ingroup LiftingStrategies
      16             : 
      17             :     A lifting strategy that combines the linear and predecessor lifting
      18             :     strategies: vertices are lifted in sequential order (like with the linear
      19             :     lifting strategy) but after a single pass over all vertices, only those
      20             :     vertices which had a successor lifted are (like with the predecessor lifting
      21             :     strategy).
      22             : 
      23             :     Intended for debugging, as it shouldn't really offer any benefits over
      24             :     predecessor lifting using a queue. Its main advantage is that the order in
      25             :     which vertices are lifted is more predictable.
      26             : */
      27             : class LinPredLiftingStrategy : public LiftingStrategy
      28             : {
      29             : public:
      30           0 :     LinPredLiftingStrategy( const ParityGame &game,
      31             :                             const SmallProgressMeasures &spm )
      32           0 :         : LiftingStrategy(), graph_(game.graph())
      33             :     {
      34             :         (void)spm;  // unused
      35           0 :         cur_queue.reserve(graph_.V());
      36           0 :         for (verti v = 0; v < graph_.V(); ++v) cur_queue.push_back(v);
      37           0 :         pos = cur_queue.begin();
      38           0 :     }
      39             : 
      40           0 :     void lifted(verti v)
      41             :     {
      42           0 :         for ( StaticGraph::const_iterator it = graph_.pred_begin(v);
      43           0 :               it != graph_.pred_end(v); ++it ) next_queue.push_back(*it);
      44           0 :     }
      45             : 
      46           0 :     verti next()
      47             :     {
      48           0 :         if (pos == cur_queue.end())
      49             :         {
      50           0 :             std::sort(next_queue.begin(), next_queue.end());
      51           0 :             next_queue.erase( std::unique(next_queue.begin(), next_queue.end()),
      52           0 :                               next_queue.end() );
      53           0 :             cur_queue.clear();
      54           0 :             cur_queue.swap(next_queue);
      55           0 :             pos = cur_queue.begin();
      56             :         }
      57           0 :         if (pos == cur_queue.end()) return NO_VERTEX;
      58           0 :         return *pos++;
      59             :     }
      60             : 
      61             : private:
      62             :     //! Graph for the game being solved.
      63             :     const StaticGraph &graph_;
      64             : 
      65             :     //! List of vertices to be lifted in the current pass.
      66             :     std::vector<verti> cur_queue;
      67             : 
      68             :     /*! List of vertices to be lifted in the next next pass.
      69             :         These are the predecessors of the vertices that have been successfully
      70             :         lifted during the current pass. */
      71             :     std::vector<verti> next_queue;
      72             : 
      73             :     /*! Iterator over `cur_queue` that points to the next vertex to be lifted
      74             :         in the current pass. */     
      75             :     std::vector<verti>::const_iterator pos; 
      76             : };
      77             : 
      78             : /*! \ingroup LiftingStrategies
      79             :     A factory class for LinPredLiftingStrategy instances. */
      80             : class LinPredLiftingStrategyFactory : public LiftingStrategyFactory
      81             : {
      82             : public:
      83             :     //! Return a new LinPredLiftingStrategy instance.
      84           0 :     LiftingStrategy *create( const ParityGame &game,
      85             :                              const SmallProgressMeasures &spm )
      86             :     {
      87           0 :         return new LinPredLiftingStrategy(game, spm);
      88             :     }
      89             : };
      90             : 
      91             : #endif /* ndef PREDECESSOR_LIFTING_STRATEGY_H_INCLUDED */

Generated by: LCOV version 1.14