LCOV - code coverage report
Current view: top level - pg/source - DecycleSolver.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 99 0.0 %
Date: 2020-02-21 00:44:40 Functions: 0 11 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             : #include "mcrl2/pg/DecycleSolver.h"
      11             : #include "mcrl2/pg/attractor.h"
      12             : 
      13             : /*! This helper class searches for cycles of a fixed priority in subgames
      14             :     controlled entirely by the corresponding player. */
      15           0 : struct CycleFinder
      16             : {
      17             :     /*! Construct an instance for the subgame of `game` induced by `mapping`,
      18             :         looking for cycles of dominant priority `prio`. */
      19             :     CycleFinder( const ParityGame &game, std::size_t prio,
      20             :                  const std::vector<verti> &mapping );
      21             : 
      22             :     /*! Search for minimum-priority cycles and vertices in their attractor sets,
      23             :         and update `strategy`, `done_set` and `done_queue` accordingly.
      24             :         Takes O(E) time. */
      25             :     void run( ParityGame::Strategy &strategy,
      26             :               DenseSet<verti> &done_set, std::deque<verti> &done_queue );
      27             : 
      28             :     // SCC callback
      29             :     int operator()(const verti *scc, std::size_t scc_size);
      30             : 
      31             : private:
      32             :     priority_t                  prio_;          //!< selected priority
      33             :     const std::vector<verti>    &mapping_;      //!< priority induced vertex set
      34             :     ParityGame                  subgame_;       //!< priority induced subgame
      35             :     DenseSet<verti>             winning_set_;   //!< winning set of the subgame
      36             :     std::deque<verti>           winning_queue_; //!< queue of winning vertices
      37             :     ParityGame::Strategy        substrat_;      //!< current winning strategy
      38             : };
      39             : 
      40           0 : CycleFinder::CycleFinder( const ParityGame &game,
      41           0 :                           std::size_t prio, const std::vector<verti> &mapping )
      42           0 :     : prio_(prio), mapping_(mapping), winning_set_(0, (verti)mapping.size()),
      43           0 :       winning_queue_(), substrat_(mapping.size(), NO_VERTEX)
      44             : {
      45           0 :     subgame_.make_subgame(game, mapping.begin(), mapping.end(), false);
      46           0 : }
      47             : 
      48           0 : void CycleFinder::run( ParityGame::Strategy &strategy,
      49             :     DenseSet<verti> &done_set, std::deque<verti> &done_queue )
      50             : {
      51             :     // Identify key vertices which are part of the winning set:
      52           0 :     decompose_graph(subgame_.graph(), *this);
      53             : 
      54           0 :     if (!winning_queue_.empty())
      55             :     {
      56             :         // Extend to attractor in subgame. This guarantees the strategy indeed
      57             :         // leads to cycles of priority prio_:
      58           0 :         make_attractor_set( subgame_, (ParityGame::Player)(prio_%2),
      59             :                             winning_set_, winning_queue_, substrat_ );
      60             : 
      61             :         // Map computed winning set and strategy back to global game:
      62           0 :         for ( DenseSet<verti>::const_iterator it = winning_set_.begin();
      63           0 :               it != winning_set_.end(); ++it )
      64             :         {
      65           0 :             verti v = mapping_[*it];
      66           0 :             verti w = substrat_[*it];
      67           0 :             if (w != NO_VERTEX) w = mapping_[w];
      68           0 :             strategy[v] = w;
      69           0 :             assert(!done_set.count(v));
      70           0 :             done_set.insert(v);
      71           0 :             done_queue.push_back(v);
      72             :         }
      73             :     }
      74           0 : }
      75             : 
      76           0 : int CycleFinder::operator()(const verti *scc, std::size_t scc_size)
      77             : {
      78             :     // Search for a vertex with minimum priority, with a successor in the SCC:
      79           0 :     for (std::size_t i = 0; i < scc_size; ++i)
      80             :     {
      81           0 :         verti v = scc[i];
      82           0 :         if (subgame_.priority(v) == prio_)
      83             :         {
      84             :             // Search for an edge inside the component:
      85             :             // FIXME: complexity analysis? has_succ is not constant time!
      86           0 :             for (std::size_t j = 0; j < scc_size; ++j)
      87             :             {
      88           0 :                 verti w = scc[j];
      89           0 :                 if (subgame_.graph().has_succ(v, w))
      90             :                 {
      91           0 :                     if (subgame_.player(v) == static_cast<int>(prio_%2))
      92             :                     {
      93           0 :                         substrat_[v] = w;
      94             :                     }
      95           0 :                     winning_set_.insert(v);
      96           0 :                     winning_queue_.push_back(v);
      97           0 :                     return 0;  // continue enumerating SCCs
      98             :                 }
      99             :             }
     100           0 :             assert(scc_size == 1);
     101             :         }
     102             :     }
     103           0 :     return 0;  // continue enumerating SCCs
     104             : }
     105             : 
     106           0 : DecycleSolver::DecycleSolver(
     107             :     const ParityGame &game, ParityGameSolverFactory &pgsf,
     108           0 :     const verti *vmap, verti vmap_size )
     109           0 :     : ParityGameSolver(game), pgsf_(pgsf), vmap_(vmap), vmap_size_(vmap_size)
     110             : {
     111           0 :     pgsf_.ref();
     112           0 : }
     113             : 
     114           0 : DecycleSolver::~DecycleSolver()
     115             : {
     116           0 :     pgsf_.deref();
     117           0 : }
     118             : 
     119           0 : ParityGame::Strategy DecycleSolver::solve()
     120             : {
     121           0 :     mCRL2log(mcrl2::log::verbose, "DecycleSolver") << "Searching for winner-controlled cycles..." << std::endl;
     122             : 
     123           0 :     const verti V = game_.graph().V();
     124           0 :     ParityGame::Strategy strategy(V, NO_VERTEX);
     125           0 :     DenseSet<verti> solved_set(0, V);
     126             : 
     127             :     // Find owner-controlled cycles for every priority value:
     128           0 :     for (priority_t prio = 0; prio < game_.d(); ++prio)
     129             :     {
     130           0 :         verti old_size = solved_set.size();
     131             : 
     132             :         // Find set of unsolved vertices with priority >= prio
     133           0 :         std::vector<verti> mapping;
     134           0 :         for (verti v = 0; v < V; ++v)
     135             :         {
     136           0 :             if ( solved_set.count(v) == 0 &&
     137           0 :                  game_.priority(v) >= prio &&
     138           0 :                  ( game_.player(v) == static_cast<int>(prio%2) ||
     139           0 :                    game_.graph().outdegree(v) == 1 ) )
     140             :             {
     141           0 :                 mapping.push_back(v);
     142             :             }
     143             :         }
     144             : 
     145             :         // Find (attractor set of) winning cycles in subgame:
     146           0 :         std::deque<verti> solved_queue;
     147           0 :         CycleFinder cf(game_, prio, mapping);
     148           0 :         cf.run(strategy, solved_set, solved_queue);
     149             : 
     150             :         // Extend to attractor set in the global game:
     151           0 :         make_attractor_set( game_, (ParityGame::Player)(prio%2),
     152             :                             solved_set, solved_queue, strategy );
     153             : 
     154           0 :         verti new_size = solved_set.size();
     155           0 :         if (old_size < new_size)
     156             :         {
     157           0 :             mCRL2log(mcrl2::log::verbose, "DecycleSolver") << "Identified " << new_size - old_size
     158           0 :                                                            << " vertices in " << prio << "-dominated cycles" << std::endl;
     159             :         }
     160             : 
     161             :         // Early out: if all vertices are solved, it is pointless to continue.
     162           0 :         if (new_size == V) return strategy;
     163             :     }
     164             : 
     165           0 :     if (solved_set.empty())
     166             :     {
     167             :         // Don't construct a subgame if it is identical to the input game:
     168           0 :         mCRL2log(mcrl2::log::verbose, "DecycleSolver") << "No suitable cycles found! Solving..." << std::endl;
     169             :         std::unique_ptr<ParityGameSolver> subsolver(
     170           0 :             pgsf_.create(game_, vmap_, vmap_size_) );
     171           0 :         subsolver->solve().swap(strategy);
     172           0 :         return strategy;
     173             :     }
     174             : 
     175           0 :     const verti num_unsolved = V - (verti)solved_set.size();
     176           0 :     mCRL2log(mcrl2::log::verbose, "DecycleSolver") << "Creating subgame with " << num_unsolved
     177           0 :                                                    << " vertices remaining..." << std::endl;
     178             : 
     179             :     // Gather remaining unsolved vertices:
     180           0 :     std::vector<verti> unsolved;
     181           0 :     unsolved.reserve(num_unsolved);
     182           0 :     for (verti v = 0; v < V; ++v)
     183             :     {
     184           0 :         if (!solved_set.count(v)) unsolved.push_back(v);
     185             :     }
     186           0 :     assert(!unsolved.empty() && unsolved.size() == num_unsolved);
     187             : 
     188             :     // Construct subgame for the unsolved part:
     189           0 :     ParityGame subgame;
     190           0 :     subgame.make_subgame(game_, unsolved.begin(), unsolved.end(), true);
     191             : 
     192             :     // Construct solver:
     193           0 :     std::vector<verti> submap;  // declared here so it survives subsolver
     194           0 :     std::unique_ptr<ParityGameSolver> subsolver;
     195           0 :     if (vmap_size_ > 0)
     196             :     {
     197             :         // Need to create merged vertex map:
     198           0 :         submap = unsolved;
     199           0 :         merge_vertex_maps(submap.begin(), submap.end(), vmap_, vmap_size_);
     200           0 :         subsolver.reset(
     201           0 :             pgsf_.create(subgame, &submap[0], submap.size()) );
     202             :     }
     203             :     else
     204             :     {
     205           0 :         subsolver.reset(
     206           0 :             pgsf_.create(subgame, &unsolved[0], unsolved.size()) );
     207             :     }
     208             : 
     209           0 :     mCRL2log(mcrl2::log::verbose, "DecycleSolver") << "Solving..." << std::endl;
     210           0 :     ParityGame::Strategy substrat = subsolver->solve();
     211           0 :     if (!substrat.empty())
     212             :     {
     213           0 :         mCRL2log(mcrl2::log::verbose, "DecycleSolver") << "Merging strategies..." << std::endl;
     214           0 :         merge_strategies(strategy, substrat, unsolved);
     215             :     }
     216             : 
     217           0 :     return strategy;
     218             : }
     219             : 
     220           0 : ParityGameSolver *DecycleSolverFactory::create( const ParityGame &game,
     221             :         const verti *vertex_map, verti vertex_map_size )
     222             : {
     223           0 :     return new DecycleSolver(game, pgsf_, vertex_map, vertex_map_size);
     224           0 : }

Generated by: LCOV version 1.13