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_DECYCLE_SOLVER_H 11 : #define MCRL2_PG_DECYCLE_SOLVER_H 12 : 13 : #include "mcrl2/pg/SmallProgressMeasures.h" 14 : #include "mcrl2/pg/DenseSet.h" 15 : #include "mcrl2/pg/SCC.h" 16 : 17 : /*! A partial solver that efficiently solves cycles controlled by a single 18 : player. 19 : 20 : Specifically, it removes all i-dominated cycles controlled by player p for 21 : all values of i and p where i%2 == p, including the vertices in their 22 : attractor sets, and then calls a general solver to solve the remaining 23 : subgame. 24 : 25 : This is a generalization of the DeloopSolver, which is limited to detecting 26 : cycles of length 1. The only downside to using the DecycleSolver is that it 27 : is slower. 28 : 29 : \see DeloopSolver 30 : */ 31 : class DecycleSolver : public ParityGameSolver 32 : { 33 : public: 34 : DecycleSolver( const ParityGame &game, ParityGameSolverFactory &pgsf, 35 : const verti *vmap, verti vmap_size ); 36 : ~DecycleSolver(); 37 : 38 : ParityGame::Strategy solve(); 39 : 40 : protected: 41 : ParityGameSolverFactory &pgsf_; //!< Solver factory to use 42 : const verti *vmap_; //!< Current vertex map 43 : const verti vmap_size_; //!< Size of vertex map 44 : }; 45 : 46 : //! A factory class for DecycleSolver instances. 47 : class DecycleSolverFactory : public ParityGameSolverFactory 48 : { 49 : public: 50 : DecycleSolverFactory(ParityGameSolverFactory &pgsf) 51 : : pgsf_(pgsf) { pgsf_.ref(); } 52 0 : ~DecycleSolverFactory() { pgsf_.deref(); } 53 : 54 : //! Return a new DecycleSolver instance. 55 : ParityGameSolver *create( const ParityGame &game, 56 : const verti *vertex_map, verti vertex_map_size ); 57 : 58 : protected: 59 : ParityGameSolverFactory &pgsf_; //!< Factory used to create subsolvers 60 : }; 61 : 62 : #endif /* ndef MCRL2_PG_DECYCLE_SOLVER_H */