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