LCOV - code coverage report
Current view: top level - pg/include/mcrl2/pg - PredecessorLiftingStrategy.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 2 0.0 %
Date: 2024-03-08 02:52:28 Functions: 0 2 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_PREDECESSOR_LIFTING_STRATEGY_H
      11             : #define MCRL2_PG_PREDECESSOR_LIFTING_STRATEGY_H
      12             : 
      13             : #include "mcrl2/pg/SmallProgressMeasures.h"
      14             : 
      15             : /*! \ingroup LiftingStrategies
      16             :  
      17             :     A simple lifting strategy that puts all nodes in a queue, then takes them
      18             :     out one at a time; whenever a node is successfully lifted, its predecessors
      19             :     are put back in the queue as they may need to be lifted too.
      20             : 
      21             :     This strategy requires predecessor edges to be stored in the game graph.
      22             : 
      23             :     The queue can operate as a true queue or as a stack; the latter may result
      24             :     in better locality of reference and/or fewer unsuccessful lifting attempts.
      25             :     (This has not been tested.)
      26             : 
      27             :     (The Multi-Core Solver for Parity Games paper contains a description of
      28             :      a "work list approach" that is similar.)
      29             : */
      30             : 
      31             : class PredecessorLiftingStrategy : virtual public LiftingStrategy,
      32             :                                    virtual public LiftingStrategy2
      33             : {
      34             : public:
      35             :     /*! Construct a new predecessor lifting strategy instance.
      36             : 
      37             :         If `stack` is set to true, vertices are removed in last-in-first-out
      38             :         order (instead of the default first-in-first-out order).
      39             :     */
      40             :     PredecessorLiftingStrategy(
      41             :         const ParityGame &game, const SmallProgressMeasures &spm, bool stack,
      42             :         int version );
      43             :     ~PredecessorLiftingStrategy();
      44             : 
      45             :     bool stack() const { return stack_; }
      46             : 
      47             :     // v1 API
      48             :     void lifted(verti v);
      49             :     verti next();
      50             : 
      51             :     // v2 API
      52             :     void push(verti v);
      53             :     verti pop();
      54           0 :     void bump(verti /*vertex*/) { }
      55             : 
      56             : private:
      57             :     const SmallProgressMeasures &spm_;
      58             :     const bool stack_;
      59             :     bool *queued_;
      60             :     verti *queue_;
      61             :     std::size_t queue_size_, queue_capacity_, queue_begin_, queue_end_;
      62             : };
      63             : 
      64             : /*! \ingroup LiftingStrategies
      65             :     Factory class for PredecessorLiftingStrategy instances. */
      66             : class PredecessorLiftingStrategyFactory : public LiftingStrategyFactory
      67             : {
      68             : public:
      69           0 :     PredecessorLiftingStrategyFactory(bool stack = false) : stack_(stack) { };
      70             : 
      71             :     bool supports_version(int version);
      72             :     LiftingStrategy *create( const ParityGame &game,
      73             :                              const SmallProgressMeasures &spm );
      74             :     LiftingStrategy2 *create2( const ParityGame &game,
      75             :                                const SmallProgressMeasures &spm );
      76             : 
      77             : private:
      78             :     const bool stack_;
      79             : };
      80             : 
      81             : #endif /* ndef MCRL2_PG_PREDECESSOR_LIFTING_STRATEGY_H */

Generated by: LCOV version 1.14