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_RECURSIVE_SOLVER_H
      11             : #define MCRL2_PG_RECURSIVE_SOLVER_H
      12             : 
      13             : #include "mcrl2/utilities/logger.h"
      14             : #include "mcrl2/pg/ParityGameSolver.h"
      15             : 
      16             : /*! Provides a view of a strategy corresponding to a subset of the vertex set.
      17             :     Note that elements of the substrategy can be written to, and the underlying
      18             :     global strategy is then updated accordingly, transparently mapping local
      19             :     to global vertex indices. */
      20             : class Substrategy
      21             : {
      22             : private:
      23             :     friend class Reference;
      24             : 
      25             :     class Reference
      26             :     {
      27             :     public:
      28           0 :         Reference(Substrategy &s, verti v) : substrat_(s), v_(s.global(v)) { }
      29             : 
      30           0 :         Reference &operator=(verti w)
      31             :         {
      32           0 :             if (w != NO_VERTEX) w = substrat_.global(w);
      33           0 :             substrat_.strategy_[v_] = w;
      34           0 :             return *this;
      35             :         }
      36             : 
      37             :     private:
      38             :         Substrategy &substrat_;
      39             :         verti v_;
      40             :     };
      41             : 
      42             : public:
      43             :     //! Constructs a strategy for all the vertices in a global strategy.
      44           0 :     Substrategy(ParityGame::Strategy &strategy)
      45           0 :         : strategy_(strategy)
      46             :     {
      47           0 :     }
      48             : 
      49             :     //! Constructs a substrategy from an existing (sub)strategy and vertex map.
      50           0 :     Substrategy(const Substrategy &substrat, std::vector<verti> vmap)
      51           0 :         : strategy_(substrat.strategy_)
      52             :     {
      53           0 :         global_.resize(vmap.size());
      54           0 :         for (std::size_t i = 0; i < global_.size(); ++i)
      55             :         {
      56           0 :             global_[i] = substrat.global(vmap[i]);
      57             :         }
      58           0 :     }
      59             : 
      60             :     //! Swaps this substrategy ovbect with another.
      61           0 :     void swap(Substrategy &other)
      62             :     {
      63           0 :         strategy_.swap(other.strategy_);
      64           0 :         global_.swap(other.global_);
      65           0 :     }
      66             : 
      67             :     //! Returns a write-only reference to the strategy for vertex `v`.
      68           0 :     Reference operator[](verti v)
      69             :     {
      70           0 :         return Reference(*this, v);
      71             :     }
      72             : 
      73             :     //! Returns the winner for vertex `v` assuming it is controlled by `p`.
      74           0 :     ParityGame::Player winner(verti v, ParityGame::Player p)
      75             :     {
      76           0 :         if (strategy_[global(v)] == NO_VERTEX) p = opponent(p);
      77           0 :         return p;
      78             :     }
      79             : 
      80             :     //! Maps local to global vertex index
      81           0 :     verti global(verti v) const
      82             :     {
      83           0 :         return global_.empty() ? v : global_[v];
      84             :     }
      85             : 
      86             : private:
      87             :     //! Reference to the global strategy
      88             :     ParityGame::Strategy &strategy_;
      89             : 
      90             :     //! Mapping from local to global vertex indices, or empty for identity.
      91             :     std::vector<verti> global_;
      92             : };
      93             : 
      94             : /*! Returns the first inversion of parity, i.e. the least priority `p` such that
      95             :     some vertices exist with priorities p and q, where q < p and q%2 != p%2.
      96             :     If there are no inversions, game.d() is returned instead. */
      97             : int first_inversion(const ParityGame &game);
      98             : 
      99             : 
     100             : /*! Parity game solver implementing Zielonka's recursive algorithm. */
     101             : class RecursiveSolver : public ParityGameSolver
     102             : {
     103             : public:
     104             :     RecursiveSolver(const ParityGame &game);
     105             :     ~RecursiveSolver();
     106             : 
     107             :     ParityGame::Strategy solve();
     108             : 
     109             : private:
     110             :     /*! Solves a subgame recursively, or returns false if solving is aborted. */
     111             :     bool solve(ParityGame &game, Substrategy &strat);
     112             : };
     113             : 
     114             : //! Factory object for RecursiveSolver instances.
     115             : class RecursiveSolverFactory : public ParityGameSolverFactory
     116             : {
     117             :     //! Returns a new ResuriveSolver instance.
     118             :     ParityGameSolver *create( const ParityGame &game,
     119             :         const verti *vertex_map, verti vertex_map_size );
     120             : };
     121             : 
     122             : #endif /* ndef MCRL2_PG_RECURSIVE_SOLVER_H */