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_PARITY_GAME_SOLVER_H
      11             : #define MCRL2_PG_PARITY_GAME_SOLVER_H
      12             : 
      13             : #include "mcrl2/pg/ParityGame.h"
      14             : #include "mcrl2/pg/Abortable.h"
      15             : #include "mcrl2/pg/RefCounted.h"
      16             : 
      17             : /*! Merge a substrategy into a main strategy. Overwrites the existing strategy
      18             :     for all vertices with indices in vertex_map. */
      19             : void merge_strategies( std::vector<verti> &strategy,
      20             :                        const std::vector<verti> &substrat,
      21             :                        const std::vector<verti> &vertex_map );
      22             : 
      23             : /*! Merge two vertex maps. Values from begin to end are remapped using old_map,
      24             :     creating a new map, such that new_map[i] becomes old_map[new_map[i]] if
      25             :     new_map[i] < old_map_size or NO_VERTEX otherwise. */
      26             : template<class ForwardIterator>
      27             : void merge_vertex_maps( ForwardIterator begin, ForwardIterator end,
      28             :                         const verti *old_map, verti old_map_size );
      29             : 
      30             : /*! Abstract base class for parity game solvers: classes that encapsulate
      31             :     algorithms to compute the winning set and optimal strategies in a game. */
      32             : class ParityGameSolver : public Abortable, RefCounted
      33             : {
      34             : public:
      35           0 :     ParityGameSolver(const ParityGame &game)
      36           0 :         : game_(game) { };
      37           0 :     virtual ~ParityGameSolver() { };
      38             : 
      39             :     /*! Solve the game and return the strategies for both players. */
      40             :     virtual ParityGame::Strategy solve() = 0;
      41             : 
      42             :     /*! Return the parity game for this solver instance. */
      43           0 :     const ParityGame &game() const { return game_; }
      44             : 
      45             : protected:
      46             :     const ParityGame &game_;           //!< Game being solved
      47             : };
      48             : 
      49             : /*! Abstract base class for parity game solver factories. */
      50             : class ParityGameSolverFactory : public RefCounted
      51             : {
      52             : public:
      53           0 :     virtual ~ParityGameSolverFactory() { };
      54             : 
      55             :     /*! Create a parity game solver for the given game.
      56             :         \param vertex_map maps vertex indices from the given subgame to the
      57             :             main game. (This allows the SPM solver to correctly collect per-
      58             :             vertex lifting statistics even if the game is decomposed first.)
      59             :         \param vertex_map_size number of vertices mapped */
      60             :     virtual ParityGameSolver *create( const ParityGame &game,
      61             :         const verti *vertex_map = NULL, verti vertex_map_size = 0 ) = 0;
      62             : };
      63             : 
      64             : #include "ParityGameSolver_impl.h"
      65             : 
      66             : #endif /* ndef MCRL2_PG_PARITY_GAME_SOLVER_H */