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             : #include "mcrl2/pg/attractor_impl.h"
      11             : #include "mcrl2/pg/DenseSet.h"
      12             : #include "mcrl2/pg/RecursiveSolver.h"
      13             : 
      14             : /*! Returns the complement of a vertex set.
      15             : 
      16             :     This function returns a vector of increasing vertex indices between 0 and
      17             :     V (exclusive) where 0 <= v < V is in the result iff. it is not included in
      18             :     the set s.
      19             : */
      20           0 : static std::vector<verti> get_complement(verti V, const DenseSet<verti> &s)
      21             : {
      22           0 :     std::vector<verti> res;
      23           0 :     verti n = V - s.size();
      24           0 :     res.reserve(n);
      25           0 :     DenseSet<verti>::const_iterator it = s.begin(), end = s.end();
      26           0 :     verti v = 0;
      27           0 :     while (it != end)
      28             :     {
      29           0 :         verti w = *it;
      30           0 :         while (v < w) res.push_back(v++);
      31           0 :         ++v;
      32           0 :         ++it;
      33             :     }
      34           0 :     while (v < V) res.push_back(v++);
      35           0 :     assert(n == (verti)res.size());
      36           0 :     return res;
      37           0 : }
      38             : 
      39             : /*! Returns the first inversion in parity for priorities occurring in the given
      40             :     game; i.e. the least value 'p` such that there is a priority `q` such that
      41             :     cardinality(q) > 0 && cardinality(p) > 0 && q < p && q%2 != p%2.
      42             : 
      43             :     If there are no inversions, the priority limit, d, is returned instead. */
      44           0 : int first_inversion(const ParityGame &game)
      45             : {
      46           0 :     int d = game.d();
      47           0 :     int q = 0;
      48           0 :     while (q < d && game.cardinality(q) == 0) ++q;
      49           0 :     int p = q + 1;
      50           0 :     while (p < d && game.cardinality(p) == 0) p += 2;
      51           0 :     return p < d ? p : d;
      52             : }
      53             : 
      54           0 : RecursiveSolver::RecursiveSolver(const ParityGame &game)
      55           0 :     : ParityGameSolver(game)
      56             : {
      57           0 : }
      58             : 
      59           0 : RecursiveSolver::~RecursiveSolver()
      60             : {
      61           0 : }
      62             : 
      63           0 : ParityGame::Strategy RecursiveSolver::solve()
      64             : {
      65           0 :     ParityGame game;
      66           0 :     game.assign(game_);
      67           0 :     ParityGame::Strategy strategy(game.graph().V(), NO_VERTEX);
      68           0 :     Substrategy substrat(strategy);
      69           0 :     if (!solve(game, substrat)) strategy.clear();
      70           0 :     return strategy;
      71           0 : }
      72             : 
      73             : /* Implementation note: the recursive solver might use either a DenseSet or
      74             :    a std::set to store vertex sets (which are passed to make_attractor_set).
      75             :    The former is faster when the size of these sets is large, but requires O(V)
      76             :    time and memory to initialize, which is costly when these sets are small.
      77             : 
      78             :    It seems that the benefit of faster lookups during attractor set computation
      79             :    usually tips the balance in favor of the DenseSet.
      80             : 
      81             :    Note that hash sets cannot readily be used because get_complement() expects
      82             :    iterators to produce the set contents in-order.
      83             : */
      84             : 
      85           0 : bool RecursiveSolver::solve(ParityGame &game, Substrategy &strat)
      86             : {
      87           0 :     if (aborted()) return false;
      88             : 
      89             :     std::size_t prio;
      90           0 :     while ((prio = first_inversion(game)) < game.d())
      91             :     {
      92           0 :         mCRL2log(mcrl2::log::debug) <<"prio=" << prio << std::endl;
      93             : 
      94           0 :         const StaticGraph &graph = game.graph();
      95           0 :         const verti V = graph.V();
      96           0 :         std::vector<verti> unsolved;
      97             : 
      98             :         // Compute attractor set of minimum priority vertices:
      99             :         {
     100           0 :             ParityGame::Player player = (ParityGame::Player)((prio - 1)%2);
     101             :             //std::set<verti> min_prio_attr;
     102           0 :             DenseSet<verti> min_prio_attr(0, V);
     103           0 :             for (verti v = 0; v < V; ++v)
     104             :             {
     105           0 :                 if (game.priority(v) < prio) min_prio_attr.insert(v);
     106             :             }
     107           0 :             mCRL2log(mcrl2::log::debug) <<"|min_prio|=" << min_prio_attr.size() << std::endl;
     108           0 :             assert(!min_prio_attr.empty());
     109           0 :             make_attractor_set_2(game, player, min_prio_attr, strat);
     110           0 :             mCRL2log(mcrl2::log::debug) << "|min_prio_attr|=" << min_prio_attr.size() << std::endl;
     111           0 :             if (min_prio_attr.size() == V) break;
     112           0 :             get_complement(V, min_prio_attr).swap(unsolved);
     113           0 :         }
     114             : 
     115             :         // Solve vertices not in the minimum priority attractor set:
     116             :         {
     117           0 :             ParityGame subgame;
     118           0 :             subgame.make_subgame(game, unsolved.begin(), unsolved.end(),
     119             :                                  true, StaticGraph::EDGE_PREDECESSOR);
     120           0 :             Substrategy substrat(strat, unsolved);
     121           0 :             if (!solve(subgame, substrat)) return false;
     122             : 
     123             :             // Compute attractor set of all vertices won by the opponent:
     124           0 :             ParityGame::Player opponent = (ParityGame::Player)(prio%2);
     125             :             //std::set<verti> lost_attr;
     126           0 :             DenseSet<verti> lost_attr(0, V);
     127           0 :             for ( std::vector<verti>::const_iterator it = unsolved.begin();
     128           0 :                   it != unsolved.end(); ++it )
     129             :             {
     130           0 :                 if (strat.winner(*it, game.player(*it)) == opponent)
     131             :                 {
     132           0 :                     lost_attr.insert(*it);
     133             :                 }
     134             :             }
     135           0 :             mCRL2log(mcrl2::log::debug) << "|lost|=" << lost_attr.size() << std::endl;
     136           0 :             if (lost_attr.empty()) break;
     137           0 :             make_attractor_set_2(game, opponent, lost_attr, strat);
     138           0 :             mCRL2log(mcrl2::log::debug) << "|lost_attr|=" << lost_attr.size() << std::endl;
     139           0 :             get_complement(V, lost_attr).swap(unsolved);
     140           0 :         }
     141             : 
     142             :         // Repeat with subgame of which vertices won by odd have been removed:
     143             :         {
     144           0 :             ParityGame subgame;
     145           0 :             subgame.make_subgame(game, unsolved.begin(), unsolved.end(),
     146             :                                  true, StaticGraph::EDGE_PREDECESSOR);
     147           0 :             Substrategy substrat(strat, unsolved);
     148           0 :             strat.swap(substrat);
     149           0 :             game.swap(subgame);
     150           0 :         }
     151           0 :     }
     152             : 
     153             :     // If we get here, then the opponent's winning set was empty; the strategy
     154             :     // for most vertices has already been initialized, except for those with
     155             :     // minimum priority. Since the whole game is won by the current player, it
     156             :     // suffices to pick an arbitrary successor for these vertices:
     157           0 :     const StaticGraph &graph = game.graph();
     158           0 :     const verti V = graph.V();
     159           0 :     if (graph.edge_dir() & StaticGraph::EDGE_SUCCESSOR)
     160             :     {
     161           0 :         for (verti v = 0; v < V; ++v)
     162             :         {
     163           0 :             if (game.priority(v) < prio)
     164             :             {
     165           0 :                 if (game.player(v) == game.priority(v)%2)
     166             :                 {
     167           0 :                     strat[v] = *graph.succ_begin(v);
     168             :                 }
     169             :                 else
     170             :                 {
     171           0 :                     strat[v] = NO_VERTEX;
     172             :                 }
     173             :             }
     174             :         }
     175             :     }
     176             :     else
     177             :     {
     178             :         // NOTE: this assumes the graph is a proper game graph!
     179             :         // If there are min. priority vertices without any successors, we won't
     180             :         // be able to find them this way!
     181           0 :         for (verti w = 0; w < V; ++w)
     182             :         {
     183           0 :             for (StaticGraph::const_iterator it = graph.pred_begin(w);
     184           0 :                 it != graph.pred_end(w); ++it)
     185             :             {
     186           0 :                 const verti v = *it;
     187             : 
     188           0 :                 if (game.priority(v) < prio)
     189             :                 {
     190           0 :                     if (game.player(v) == game.priority(v)%2)
     191             :                     {
     192           0 :                         strat[v] = w;
     193             :                     }
     194             :                     else
     195             :                     {
     196           0 :                         strat[v] = NO_VERTEX;
     197             :                     }
     198             :                 }
     199             :             }
     200             :         }
     201             :     }
     202           0 :     return true;
     203             : }
     204             : 
     205           0 : ParityGameSolver *RecursiveSolverFactory::create( const ParityGame &game,
     206             :         const verti *vertex_map, verti vertex_map_size )
     207             : {
     208             :     (void)vertex_map;       // unused
     209             :     (void)vertex_map_size;  // unused
     210             : 
     211           0 :     return new RecursiveSolver(game);
     212             : }