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_COMPONENT_SOLVER_H
      11             : #define MCRL2_PG_COMPONENT_SOLVER_H
      12             : 
      13             : #include "mcrl2/pg/SmallProgressMeasures.h"
      14             : #include "mcrl2/pg/DenseSet.h"
      15             : #include "mcrl2/pg/SCC.h"
      16             : 
      17             : /*! A solver that breaks down the game graph into strongly connected components.
      18             : 
      19             :     The individual components are then solved from bottom to top with a
      20             :     general solver.  Whenever a component is solved, its attractor set in the
      21             :     complete graph is computed, and the graph is decomposed again, in hopes of
      22             :     generating even smaller components.
      23             : */
      24             : class ComponentSolver : public ParityGameSolver
      25             : {
      26             : public:
      27             :     /*! Constructs a solver for the given `game` using the factory `pgsf` to
      28             :         create subsolver instances to solve subgames constructed for each
      29             :         strongly connected component found.
      30             : 
      31             :         When `max_depth` > 0, components identified in the main graph are
      32             :         recursively decomposed (up to the give depth) if it turns out they have
      33             :         been partially solved already (i.e. when some of their vertices lie in
      34             :         the attractor sets of winning regions identified earlier).
      35             :     */
      36             :     ComponentSolver( const ParityGame &game, ParityGameSolverFactory &pgsf,
      37             :                      int max_depth, const verti *vmap = 0, verti vmap_size = 0
      38             :                    );
      39             :     ~ComponentSolver();
      40             : 
      41             :     ParityGame::Strategy solve();
      42             : 
      43             : private:
      44             :     // SCC callback
      45             :     int operator()(const verti *vertices, std::size_t num_vertices);
      46             :     friend class SCC<ComponentSolver>;
      47             : 
      48             : protected:
      49             :     ParityGameSolverFactory  &pgsf_;        //!< Solver factory to use
      50             :     const int                max_depth_;    //!< Max. recusion depth
      51             :     const verti              *vmap_;        //!< Current vertex map
      52             :     const verti              vmap_size_;    //!< Size of vertex map
      53             :     ParityGame::Strategy     strategy_;     //!< Resulting strategy
      54             :     DenseSet<verti>          *winning_[2];  //!< Resulting winning sets
      55             : };
      56             : 
      57             : //! Factory class for ComponentSolver instances.
      58             : class ComponentSolverFactory : public ParityGameSolverFactory
      59             : {
      60             : public:
      61             :     //! \see ComponentSolver::ComponentSolver()
      62           0 :     ComponentSolverFactory(ParityGameSolverFactory &pgsf, int max_depth = 10)
      63           0 :         : pgsf_(pgsf), max_depth_(max_depth) { pgsf_.ref(); }
      64           0 :     ~ComponentSolverFactory() { pgsf_.deref(); }
      65             : 
      66             :     //! Return a new ComponentSolver instance.
      67             :     ParityGameSolver *create( const ParityGame &game,
      68             :         const verti *vertex_map, verti vertex_map_size );
      69             : 
      70             : protected:
      71             :     ParityGameSolverFactory &pgsf_;     //!< Factory used to create subsolvers
      72             :     const int max_depth_;               //!< Maximum recursion depth
      73             : };
      74             : 
      75             : #endif /* ndef MCRL2_PG_COMPONENT_SOLVER_H */