LCOV - code coverage report
Current view: top level - pg/source - DeloopSolver.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 61 0.0 %
Date: 2024-03-08 02:52:28 Functions: 0 5 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/DeloopSolver.h"
      11             : #include "mcrl2/pg/attractor.h"
      12             : 
      13           0 : DeloopSolver::DeloopSolver(
      14             :     const ParityGame &game, ParityGameSolverFactory &pgsf,
      15           0 :     const verti *vmap, verti vmap_size )
      16           0 :     : ParityGameSolver(game), pgsf_(pgsf), vmap_(vmap), vmap_size_(vmap_size)
      17             : {
      18           0 :     pgsf_.ref();
      19           0 : }
      20             : 
      21           0 : DeloopSolver::~DeloopSolver()
      22             : {
      23           0 :     pgsf_.deref();
      24           0 : }
      25             : 
      26           0 : ParityGame::Strategy DeloopSolver::solve()
      27             : {
      28           0 :     const verti V = game_.graph().V();
      29           0 :     ParityGame::Strategy strategy(V, NO_VERTEX);
      30             : 
      31           0 :     mCRL2log(mcrl2::log::verbose) << "Searching for winning loops..." << std::endl;
      32           0 :     DenseSet<verti> solved(0, V);
      33           0 :     for (int player = 0; player < 2; ++player)
      34             :     {
      35           0 :         verti old_solved = (verti)solved.size();
      36           0 :         std::deque<verti> winning;
      37           0 :         for (verti v = 0; v < V; ++v)
      38             :         {
      39           0 :             if ( static_cast<int>(game_.priority(v)%2) == player &&
      40           0 :                  game_.graph().outdegree(v) == 1 &&
      41           0 :                  *game_.graph().succ_begin(v) == v )
      42             :             {
      43           0 :                 assert(solved.count(v) == 0);
      44           0 :                 strategy[v] = game_.player(v) == player ? v : NO_VERTEX;
      45           0 :                 winning.push_back(v);
      46           0 :                 solved.insert(v);
      47             :             }
      48             :         }
      49             : 
      50             :         // Compute attractor set and associated strategy:
      51           0 :         for ( std::deque<verti>::const_iterator it = winning.begin();
      52           0 :                 it != winning.end(); ++it ) solved.insert(*it);
      53           0 :         make_attractor_set( game_, (ParityGame::Player)player,
      54             :                             solved, winning, strategy );
      55             : 
      56           0 :         verti num_solved = (verti)solved.size() - old_solved;
      57           0 :         mCRL2log(mcrl2::log::verbose) << "Found " << num_solved << " vertices won by " << (player == 0 ? "Even" : "Odd" ) << std::endl;
      58           0 :     }
      59             : 
      60           0 :     std::vector<verti> unsolved;
      61           0 :     ParityGame subgame;
      62           0 :     std::vector<verti> submap;  // must survive subsolver!
      63           0 :     std::unique_ptr<ParityGameSolver> subsolver;
      64           0 :     ParityGame::Strategy substrat;
      65             : 
      66           0 :     if (solved.empty())
      67             :     {
      68             :         // Don't construct a subgame if it is identical to the input game:
      69           0 :         mCRL2log(mcrl2::log::verbose) << "Solving game." << std::endl;
      70           0 :         subsolver.reset(pgsf_.create(game_, vmap_, vmap_size_));
      71           0 :         strategy = subsolver->solve();
      72             :     }
      73             :     else
      74           0 :     if (solved.size() != V)
      75             :     {
      76           0 :         const verti num_unsolved = V - (verti)solved.size();
      77           0 :         mCRL2log(mcrl2::log::verbose) << "Creating subgame with " << num_unsolved << " vertices remaining..." << std::endl;
      78             : 
      79             :         // Create game with remaining unsolved vertices:
      80           0 :         unsolved.reserve(num_unsolved);
      81           0 :         for (verti v = 0; v < V; ++v)
      82             :         {
      83           0 :             if (solved.count(v) == 0) unsolved.push_back(v);
      84             :         }
      85           0 :         assert(!unsolved.empty() && unsolved.size() == num_unsolved);
      86             : 
      87           0 :         subgame.make_subgame(game_, unsolved.begin(), unsolved.end(), true);
      88             : 
      89             :         // Construct solver:
      90           0 :         if (vmap_size_ > 0)
      91             :         {
      92             :             // Need to create merged vertex map:
      93           0 :             submap = unsolved;
      94           0 :             merge_vertex_maps(submap.begin(), submap.end(), vmap_, vmap_size_);
      95           0 :             subsolver.reset(pgsf_.create(subgame, &submap[0], submap.size()));
      96             :         }
      97             :         else
      98             :         {
      99           0 :             subsolver.reset(pgsf_.create(subgame, &unsolved[0], unsolved.size()));
     100             :         }
     101             : 
     102           0 :         mCRL2log(mcrl2::log::verbose) << "Solving..." << std::endl;
     103           0 :         substrat = subsolver->solve();
     104           0 :         if (!substrat.empty())
     105             :         {
     106           0 :             mCRL2log(mcrl2::log::verbose) << "Merging strategies..." << std::endl;
     107           0 :             merge_strategies(strategy, substrat, unsolved);
     108             :         }
     109             :     }
     110             : 
     111           0 :     return strategy;
     112           0 : }
     113             : 
     114           0 : ParityGameSolver *DeloopSolverFactory::create( const ParityGame &game,
     115             :         const verti *vertex_map, verti vertex_map_size )
     116             : {
     117           0 :     return new DeloopSolver(game, pgsf_, vertex_map, vertex_map_size);
     118             : }

Generated by: LCOV version 1.14