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 */