LCOV - code coverage report
Current view: top level - pg/include/mcrl2/pg - DecycleSolver.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 1 0.0 %
Date: 2024-03-08 02:52:28 Functions: 0 2 0.0 %
Legend: Lines: hit not hit

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

Generated by: LCOV version 1.14