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_DELOOP_SOLVER_H
      11             : #define MCRL2_PG_DELOOP_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 identifies vertices with loops which are won by their owner
      18             :     (i.e. when the owner corresponds with the parity of the vertex priority)
      19             :     and removes their attractor sets from the game to obtain a loop-less reduced
      20             :     game that is then solved with a new solver.
      21             : 
      22             :     This REQUIRES that the game graph has been preprocessed with
      23             :     SmallProgressMeasures::preprocess_game()!
      24             : 
      25             :     Compared to the DecycleSolver, this preprocessor is faster but weaker.
      26             : 
      27             :     \see DecycleSolver
      28             : */
      29             : class DeloopSolver : public ParityGameSolver
      30             : {
      31             : public:
      32             :     DeloopSolver( const ParityGame &game, ParityGameSolverFactory &pgsf,
      33             :                   const verti *vmap, verti vmap_size );
      34             :     ~DeloopSolver();
      35             : 
      36             :     ParityGame::Strategy solve();
      37             : 
      38             : private:
      39             :     // SCC callback
      40             :     int operator()(const verti *vertices, std::size_t num_vertices);
      41             :     friend class SCC<DeloopSolver>;
      42             : 
      43             : protected:
      44             :     ParityGameSolverFactory &pgsf_;       //!< Solver factory to use
      45             :     const verti             *vmap_;       //!< Current vertex map
      46             :     const verti             vmap_size_;   //!< Size of vertex map
      47             : };
      48             : 
      49             : //! A factory class for DeloopSolver instances.
      50             : class DeloopSolverFactory : public ParityGameSolverFactory
      51             : {
      52             : public:
      53             :     DeloopSolverFactory(ParityGameSolverFactory &pgsf)
      54             :         : pgsf_(pgsf) { pgsf_.ref(); }
      55           0 :     ~DeloopSolverFactory() { pgsf_.deref(); }
      56             : 
      57             :     //! Create a new DeloopSolver instance.
      58             :     ParityGameSolver *create( const ParityGame &game,
      59             :         const verti *vertex_map, verti vertex_map_size );
      60             : 
      61             : protected:
      62             :     ParityGameSolverFactory &pgsf_;     //!< Factory used to create subsolvers
      63             : };
      64             : 
      65             : #endif /* ndef MCRL2_PG_DELOOP_SOLVER_H */