LCOV - code coverage report
Current view: top level - pg/source - SmallProgressMeasures.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 308 0.0 %
Date: 2020-02-21 00:44:40 Functions: 0 32 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/SmallProgressMeasures.h"
      11             : #include "mcrl2/pg/attractor.h"
      12             : #include "mcrl2/pg/SCC.h"
      13             : 
      14             : #include <cstring>
      15             : 
      16           0 : LiftingStatistics::LiftingStatistics( const ParityGame &game,
      17           0 :                                       long long max_lifts )
      18           0 :     : lifts_attempted_(0), lifts_succeeded_(0), max_lifts_(max_lifts)
      19             : {
      20           0 :     vertex_stats_.resize(game.graph().V());
      21           0 : }
      22             : 
      23           0 : void LiftingStatistics::record_lift(verti v, bool success)
      24             : {
      25           0 :     assert(v == NO_VERTEX || v < vertex_stats_.size());
      26             : 
      27           0 :     ++lifts_attempted_;
      28           0 :     if (lifts_attempted_ == max_lifts_) Abortable::abort_all();
      29           0 :     if (v != NO_VERTEX) ++vertex_stats_[v].first;
      30           0 :     if (success)
      31             :     {
      32           0 :         ++lifts_succeeded_;
      33           0 :         if (v != NO_VERTEX) ++vertex_stats_[v].second;
      34             :     }
      35           0 : }
      36             : 
      37           0 : SmallProgressMeasures::SmallProgressMeasures(
      38             :         const ParityGame &game, ParityGame::Player player,
      39           0 :         LiftingStatistics *stats, const verti *vmap, verti vmap_size )
      40             :     : game_(game), p_(player), stats_(stats),
      41             :       vmap_(vmap), vmap_size_(vmap_size),
      42           0 :       strategy_(game.graph().V(), NO_VERTEX), dirty_(0)
      43             : {
      44           0 :     assert(p_ == 0 || p_ == 1);
      45             : 
      46             :     // Initialize SPM vector bounds
      47           0 :     len_ = (game_.d() + p_)/2;
      48           0 :     if (len_ < 1) len_ = 1;  // ensure Top is representable
      49           0 :     M_ = new verti[len_];
      50           0 :     for (std::size_t n = 0; n < len_; ++n)
      51             :     {
      52           0 :         std::size_t prio = 2*n + 1 - p_;
      53           0 :         M_[n] = (prio < game.d()) ? game_.cardinality(prio) + 1 : 0;
      54             :     }
      55           0 : }
      56             : 
      57           0 : void SmallProgressMeasures::initialize_loops()
      58             : {
      59           0 :     const verti V = game_.graph().V();
      60             : 
      61             :     // Initialize vertices won by the opponent to Top. This is designed to
      62             :     // work in conjunction with preprocess_game() which should have removed
      63             :     // the non-loop outgoing edges for such vertices.
      64             : 
      65             :     // N.B. The DecycleSolver and DeloopSolver make this obsolete, so if we
      66             :     //      always use those, this code may well be removed!
      67             : 
      68             :     // (Alternatively, the winning set propagation in Friedmann's two-sided
      69             :     //  approach sets these to top, but in the current implementation this
      70             :     //  is only done after iteration, not before!)
      71             : 
      72           0 :     verti cnt = 0;
      73           0 :     for (verti v = 0; v < V; ++v)
      74             :     {
      75           0 :         if ( game_.priority(v)%2 == 1 - p_ &&
      76           0 :              game_.graph().outdegree(v) == 1 &&
      77           0 :              *game_.graph().succ_begin(v) == v )
      78             :         {
      79           0 :             strategy_[v] = v;
      80           0 :             set_top(v);
      81           0 :             ++cnt;
      82             :         }
      83             :     }
      84           0 :     mCRL2log(mcrl2::log::debug) << "Initialized " << cnt
      85           0 :                                 << "vert" << (cnt == 1 ? "ex" : "ices") << " to top" << std::endl;
      86           0 : }
      87             : 
      88           0 : void SmallProgressMeasures::initialize_lifting_strategy(LiftingStrategy2 &ls)
      89             : {
      90           0 :     const verti V = game_.graph().V();
      91           0 :     if (!dirty_) dirty_ = new bool[V];
      92           0 :     for (verti v = 0; v < V; ++v)
      93             :     {
      94           0 :         if (is_top(v))
      95             :         {
      96             :             // strategy may not be valid for top vertices!
      97           0 :             dirty_[v] = false;
      98             :         }
      99             :         else
     100             :         {
     101           0 :             verti w = get_ext_succ(v, take_max(v));
     102           0 :             bool dirty = less_than(v, vec(w), compare_strict(v));
     103           0 :             strategy_[v] = w;
     104           0 :             dirty_[v]    = dirty;
     105           0 :             if (dirty) ls.push(v);
     106             :         }
     107             :     }
     108           0 : }
     109             : 
     110           0 : SmallProgressMeasures::~SmallProgressMeasures()
     111             : {
     112           0 :     delete[] M_;
     113           0 :     delete[] dirty_;
     114           0 : }
     115             : 
     116           0 : long long SmallProgressMeasures::solve_some( LiftingStrategy &ls,
     117             :                                              long long attempts )
     118             : {
     119           0 :     while (attempts > 0 && solve_one(ls).first != NO_VERTEX) --attempts;
     120           0 :     return attempts;
     121             : }
     122             : 
     123           0 : long long SmallProgressMeasures::solve_some( LiftingStrategy2 &ls,
     124             :                                              long long attempts )
     125             : {
     126           0 :     while (attempts > 0 && solve_one(ls) != NO_VERTEX) --attempts;
     127           0 :     return attempts;
     128             : }
     129             : 
     130           0 : std::pair<verti, bool> SmallProgressMeasures::solve_one(LiftingStrategy &ls)
     131             : {
     132           0 :     verti v = ls.next();
     133           0 :     if (v == NO_VERTEX) return std::make_pair(NO_VERTEX, false);
     134             : 
     135           0 :     bool success = false;
     136           0 :     if (!is_top(v))
     137             :     {
     138           0 :         verti w = get_ext_succ(v, take_max(v));
     139           0 :         if (lift_to(v, vec(w), compare_strict(v)))
     140             :         {
     141           0 :             ls.lifted(v);
     142           0 :             success = true;
     143             :         }
     144             :     }
     145           0 :     if (stats_ != NULL)
     146             :     {
     147           0 :         stats_->record_lift(vmap_ && v < vmap_size_ ? vmap_[v] : v, success);
     148             :     }
     149           0 :     return std::make_pair(v, success);
     150             : }
     151             : 
     152           0 : verti SmallProgressMeasures::solve_one(LiftingStrategy2 &ls)
     153             : {
     154           0 :     verti v = ls.pop();
     155           0 :     if (v == NO_VERTEX) return NO_VERTEX;
     156             : 
     157           0 :     assert(!is_top(v));
     158             : 
     159             :     #ifndef NDEBUG
     160             :     bool success =
     161             :     #endif // NDEBUG
     162           0 :     lift_to(v, vec(get_successor(v)), compare_strict(v));
     163           0 :     assert(success);
     164           0 :     dirty_[v] = false;
     165             :     // debug_print_vertex(v);
     166             : 
     167           0 :     for ( const verti *it  = game_.graph().pred_begin(v),
     168           0 :                       *end = game_.graph().pred_end(v); it != end; ++it )
     169             :     {
     170           0 :         verti u = *it;
     171           0 :         if (is_top(u)) continue;
     172             : 
     173             :         bool changed;
     174           0 :         if (!take_max(u))  // even-controlled vertex: minimize
     175             :         {
     176           0 :             if (get_successor(u) == v)  // minimum successor increased
     177             :             {
     178           0 :                 verti w = get_min_succ(u);
     179           0 :                 strategy_[u] = w;
     180           0 :                 changed = true;
     181             :             }
     182             :             else  // non-minimum successor increased -- no change!
     183             :             {
     184           0 :                 changed = false;
     185             :             }
     186             :         }
     187             :         else  // odd-controlled vertex: maximize
     188             :         {
     189           0 :             if (get_successor(u) == v)  // maximum successor increased
     190             :             {
     191           0 :                 changed = true;
     192             :             }
     193             :             else
     194           0 :             if (vector_cmp(vec(v), vec(get_successor(u)), len_) > 0)
     195             :             {   // maximum successor changed
     196           0 :                 strategy_[u] = v;
     197           0 :                 changed = true;
     198             :             }
     199             :             else  // non-maximum successor doesn't beat current maximum
     200             :             {
     201           0 :                 changed = false;
     202             :             }
     203             :         }
     204           0 :         if (changed)
     205             :         {
     206           0 :             if (is_dirty(u))
     207             :             {
     208           0 :                 ls.bump(u);
     209             :             }
     210             :             else
     211             :             {
     212           0 :                 bool carry = game_.priority(u)%2 != p_;
     213           0 :                 bool dirty = less_than(u, vec(get_successor(u)), carry);
     214           0 :                 if (dirty)
     215             :                 {
     216           0 :                     dirty_[u] = true;
     217           0 :                     ls.push(u);
     218             :                 }
     219             :             }
     220             :         }
     221             :     }
     222             : 
     223           0 :     if (stats_ != NULL)
     224             :     {
     225           0 :         stats_->record_lift(vmap_ && v < vmap_size_ ? vmap_[v] : v, true);
     226             :     }
     227           0 :     return v;
     228             : }
     229             : 
     230           0 : verti SmallProgressMeasures::get_strategy(verti v) const
     231             : {
     232           0 :     return (!is_top(v) && game_.player(v) == p_) ? get_min_succ(v) : NO_VERTEX;
     233             : }
     234             : 
     235           0 : void SmallProgressMeasures::get_strategy(ParityGame::Strategy &strat) const
     236             : {
     237           0 :     verti V = game_.graph().V();
     238           0 :     assert(strat.size() == V);
     239           0 :     for (verti v = 0; v < V; ++v)
     240             :     {
     241           0 :         verti w = get_strategy(v);
     242           0 :         if (w != NO_VERTEX) strat[v] = w;
     243             :     }
     244           0 : }
     245             : 
     246             : // Returns the same result as lift_to, but doesn't actually change anything:
     247           0 : bool SmallProgressMeasures::less_than(verti v, const verti vec2[], bool carry)
     248             : {
     249           0 :     if (is_top(v)) return false;
     250           0 :     if (is_top(vec2)) return true;
     251           0 :     int comparison = vector_cmp(vec(v), vec2, len(v));
     252           0 :     return comparison < 0 || (comparison <= 0 && carry);
     253             : }
     254             : 
     255           0 : bool SmallProgressMeasures::lift_to(verti v, const verti vec2[], bool carry)
     256             : {
     257           0 :     if (is_top(v)) return false;
     258             : 
     259           0 :     if (is_top(vec2))
     260             :     {
     261           0 :         set_top(v);
     262             :     }
     263             :     else
     264             :     {
     265           0 :         int comparison = vector_cmp(vec(v), vec2, len(v));
     266           0 :         if (comparison > 0 || (comparison >= 0 && !carry))  return false;
     267           0 :         set_vec(v, vec2, carry);
     268             :     }
     269           0 :     return true;
     270             : }
     271             : 
     272             : #if 0
     273             : void SmallProgressMeasures::debug_print_vertex(int v) const
     274             : {
     275             :     printf ( "%6d %c p=%d:", (int)v,
     276             :                 game_.player(v) == ParityGame::PLAYER_EVEN ? 'E' :
     277             :                 game_.player(v) == ParityGame::PLAYER_ODD  ? 'O' : '?',
     278             :                 (int)game_.priority(v) );
     279             :     if (is_top(v))
     280             :     {
     281             :         printf(" T");
     282             :     }
     283             :     else
     284             :     {
     285             :         for (int p = 0; p < game_.d(); ++p)
     286             :         {
     287             :             printf(" %d", (p%2 == p_) ? 0 : vec(v)[p/2]);
     288             :         }
     289             :     }
     290             :     printf("\n");
     291             : }
     292             : 
     293             : void SmallProgressMeasures::debug_print() const
     294             : {
     295             :     printf("M =");
     296             :     for (int p = 0; p < game_.d(); ++p) printf(" %d", (p%2 == p_) ? 0 : M_[p/2]);
     297             :     printf("\n");
     298             :     for (verti v = 0; v < game_.graph().V(); ++v) debug_print_vertex(v);
     299             : }
     300             : 
     301             : bool SmallProgressMeasures::verify_solution()
     302             : {
     303             :     const StaticGraph &graph = game_.graph();
     304             : 
     305             :     for (verti v = 0; v < graph.V(); ++v)
     306             :     {
     307             :         if (!is_top(v))
     308             :         {
     309             :             for (int p = 0; p < game_.d(); ++p)
     310             :             {
     311             :                 if (p%2 == p_) continue; /* this component is not stored */
     312             : 
     313             :                 /* Ensure vector values satisfy bounds */
     314             :                 if (vec(v)[p/2] >= M_[p/2])
     315             :                 {
     316             :                     printf( "%d-th component of SPM vector for vertex %d "
     317             :                             "out of bounds!\n", p, (int)v );
     318             :                     return false;
     319             :                 }
     320             : 
     321             :                 if (p > game_.priority(v) && vec(v)[p/2] != 0)
     322             :                 {
     323             :                     printf( "%d-th component of SPM vector for vertex %d "
     324             :                             "should be zero!\n", p/2, (int)v );
     325             :                     return false;
     326             :                 }
     327             :             }
     328             :         }
     329             : 
     330             :         bool all_ok = true, one_ok = false;
     331             :         for ( StaticGraph::const_iterator it = graph.succ_begin(v);
     332             :               it != graph.succ_end(v); ++it )
     333             :         {
     334             :             bool ok = is_top(v) ||
     335             :                       vector_cmp(v, *it, len(v)) >= compare_strict(v);
     336             :             one_ok = one_ok || ok;
     337             :             all_ok = all_ok && ok;
     338             :         }
     339             : 
     340             :         if (!(game_.player(v) == p_ ? one_ok : all_ok))
     341             :         {
     342             :             printf( "order constraint not satisfied for vertex %d with "
     343             :                     "priority %d and player %s!\n", v, game_.priority(v),
     344             :                 game_.player(v) == PLAYER_EVEN ? "even" :
     345             :                 game_.player(v) == PLAYER_ODD  ? "odd"  : "???" );
     346             :             return false;
     347             :         }
     348             :     }
     349             :     return true;
     350             : }
     351             : #endif
     352             : 
     353             : //
     354             : //  SmallProgressMeasuresSolver
     355             : //
     356             : 
     357           0 : SmallProgressMeasuresSolver::SmallProgressMeasuresSolver(
     358             :     const ParityGame &game, std::shared_ptr<LiftingStrategyFactory> lsf, bool alternate,
     359           0 :     LiftingStatistics *stats, const verti *vmap, verti vmap_size )
     360             :         : ParityGameSolver(game), lsf_(lsf), alternate_(alternate),
     361           0 :           stats_(stats), vmap_(vmap), vmap_size_(vmap_size)
     362           0 : {}
     363             : 
     364           0 : ParityGame::Strategy SmallProgressMeasuresSolver::solve()
     365             : {
     366           0 :     return alternate_ ? solve_alternate() : solve_normal();
     367             : }
     368             : 
     369           0 : ParityGame::Strategy SmallProgressMeasuresSolver::solve_normal()
     370             : {
     371           0 :     ParityGame::Strategy strategy(game_.graph().V(), NO_VERTEX);
     372           0 :     std::vector<verti> won_by_odd;
     373             : 
     374             :     {
     375           0 :         mCRL2log(mcrl2::log::verbose) << "Solving for Even..." << std::endl;
     376             :         DenseSPM spm( game(), PLAYER_EVEN,
     377           0 :                       stats_, vmap_, vmap_size_ );
     378           0 :         std::unique_ptr<LiftingStrategy> ls(lsf_->create(game_, spm));
     379           0 :         while (spm.solve_some(*ls) == 0)
     380             :         {
     381           0 :             if (aborted()) return ParityGame::Strategy();
     382             :         }
     383           0 :         spm.get_strategy(strategy);
     384           0 :         spm.get_winning_set( PLAYER_ODD,
     385             :             std::back_insert_iterator<std::vector<verti> >(won_by_odd) );
     386             : #ifdef DEBUG
     387             :         mCRL2log(mcrl2::log::verbose) << "Verifying small progress measures." << std::endl;
     388             :         assert(spm.verify_solution());
     389             : #endif
     390             :     }
     391             : 
     392           0 :     if (!won_by_odd.empty())
     393             :     {
     394             :         // Make a dual subgame of the vertices won by player Odd
     395           0 :         ParityGame subgame;
     396           0 :         mCRL2log(mcrl2::log::verbose) << "Constructing subgame of size "
     397           0 :                                       << won_by_odd.size() << " to solve for Odd..." << std::endl;
     398           0 :         subgame.make_subgame(game_, won_by_odd.begin(), won_by_odd.end(), true);
     399           0 :         subgame.compress_priorities();
     400             : 
     401             :         // Create vertex map to use:
     402           0 :         std::vector<verti> submap_data;
     403           0 :         verti *submap = &won_by_odd[0];
     404           0 :         std::size_t submap_size = won_by_odd.size();
     405           0 :         if (vmap_)
     406             :         {
     407           0 :             submap_data = won_by_odd;
     408           0 :             submap = &submap_data[0];
     409           0 :             merge_vertex_maps(submap, submap + submap_size, vmap_, vmap_size_);
     410             :         }
     411             : 
     412             :         // Second pass; solve subgame of vertices won by Odd:
     413           0 :         mCRL2log(mcrl2::log::verbose) << "Solving for Odd..." << std::endl;
     414             :         DenseSPM spm( subgame, PLAYER_ODD,
     415           0 :                       stats_, submap, submap_size );
     416           0 :         std::unique_ptr<LiftingStrategy> ls(lsf_->create(subgame, spm));
     417           0 :         while (spm.solve_some(*ls) == 0)
     418             :         {
     419           0 :             if (aborted()) return ParityGame::Strategy();
     420             :         }
     421           0 :         ParityGame::Strategy substrat(won_by_odd.size(), NO_VERTEX);
     422           0 :         spm.get_strategy(substrat);
     423           0 :         merge_strategies(strategy, substrat, won_by_odd);
     424             : #ifdef DEBUG
     425             :         mCRL2log(mcrl2::log::debug) << "Verifying small progress measures." << std::endl;
     426             :         assert(spm.verify_solution());
     427             : #endif
     428             :     }
     429             : 
     430           0 :     return strategy;
     431             : }
     432             : 
     433           0 : ParityGame::Strategy SmallProgressMeasuresSolver::solve_alternate()
     434             : {
     435             :     // Create two SPM and two lifting strategy instances:
     436           0 :     std::unique_ptr<SmallProgressMeasures> spm[2];
     437           0 :     spm[0].reset(new DenseSPM( game_, PLAYER_EVEN,
     438           0 :                                stats_, vmap_, vmap_size_ ));
     439           0 :     spm[1].reset(new DenseSPM( game_, PLAYER_ODD,
     440           0 :                                stats_, vmap_, vmap_size_ ));
     441             : 
     442             :     // Solve games alternatingly:
     443           0 :     int player = 0;
     444           0 :     bool half_solved = false;
     445           0 :     while (!half_solved)
     446             :     {
     447           0 :         mCRL2log(mcrl2::log::verbose) << "Switching to "
     448           0 :                                        << (player == 0 ? "normal" : "dual") << " game..." << std::endl;
     449           0 :         std::unique_ptr<LiftingStrategy> ls(lsf_->create(game_, *spm[player]));
     450             : 
     451             :         /* Note: work size should be large enough so that dumb strategies like
     452             :                  linear lifting are still able to detect termination! */
     453           0 :         for ( long long work = game_.graph().V(); work > 0 && !half_solved;
     454           0 :               work -= SmallProgressMeasures::work_size )
     455             :         {
     456           0 :             half_solved = spm[player]->solve_some(*ls) > 0;
     457           0 :             if (aborted()) return ParityGame::Strategy();
     458             :         }
     459             : 
     460           0 :         mCRL2log(mcrl2::log::verbose) << "Propagating solved vertices to other game..." << std::endl;
     461           0 :         spm[player]->get_winning_set( (ParityGame::Player)player,
     462           0 :                                       SetToTopIterator(*spm[1 - player]) );
     463           0 :         player = 1 - player;
     464             :     }
     465             : 
     466             :     // One game is solved; solve other game completely too:
     467           0 :     mCRL2log(mcrl2::log::verbose) << "Finishing " << (player == 0 ? "normal" : "dual") << "game..." << std::endl;
     468           0 :     std::unique_ptr<LiftingStrategy> ls(lsf_->create(game_, *spm[player]));
     469           0 :     while (spm[player]->solve_some(*ls) == 0)
     470             :     {
     471           0 :         if (aborted()) return ParityGame::Strategy();
     472             :     }
     473             : 
     474             :     // Retrieve combined strategies:
     475           0 :     ParityGame::Strategy strategy(game_.graph().V(), NO_VERTEX);
     476           0 :     spm[0]->get_strategy(strategy);
     477           0 :     spm[1]->get_strategy(strategy);
     478             : 
     479           0 :     return strategy;
     480             : }
     481             : 
     482           0 : void SmallProgressMeasuresSolver::preprocess_game(ParityGame &game)
     483             : {
     484           0 :     StaticGraph &graph = const_cast<StaticGraph&>(game.graph());  // HACK
     485           0 :     StaticGraph::edge_list obsolete_edges;
     486             : 
     487           0 :     for (verti v = 0; v < graph.V(); ++v)
     488             :     {
     489           0 :         if (graph.has_succ(v, v))
     490             :         {
     491             :             // Decide what to do with the edges:
     492           0 :             if ((int)game.priority(v)%2 == (int)game.player(v))
     493             :             {
     494             :                 // Self-edge is beneficial; remove other edges
     495           0 :                 for ( StaticGraph::const_iterator it = graph.succ_begin(v);
     496           0 :                       it != graph.succ_end(v); ++it )
     497             :                 {
     498           0 :                     if (*it != v)
     499             :                     {
     500           0 :                         obsolete_edges.push_back(std::make_pair(v, *it));
     501             :                     }
     502             :                 }
     503             :             }
     504             :             else
     505           0 :             if (graph.outdegree(v) > 1)
     506             :             {
     507             :                 // Self-edge is detrimental; remove it
     508           0 :                 obsolete_edges.push_back(std::make_pair(v, v));
     509             :             }
     510             :         }
     511             :     }
     512           0 :     graph.remove_edges(obsolete_edges);
     513           0 : }
     514             : 
     515             : 
     516             : //
     517             : //  SmallProgressMeasuresSolver2
     518             : //
     519             : 
     520           0 : SmallProgressMeasuresSolver2::SmallProgressMeasuresSolver2(
     521             :     const ParityGame &game, std::shared_ptr<LiftingStrategyFactory> lsf, bool alternate,
     522           0 :     LiftingStatistics *stats, const verti *vmap, verti vmap_size )
     523             :         : SmallProgressMeasuresSolver( game, lsf, alternate,
     524           0 :                                        stats, vmap, vmap_size)
     525             : {
     526           0 : }
     527             : 
     528           0 : ParityGame::Strategy SmallProgressMeasuresSolver2::solve_normal()
     529             : {
     530           0 :     ParityGame::Strategy strategy(game_.graph().V(), NO_VERTEX);
     531           0 :     std::vector<verti> won_by_odd;
     532             : 
     533             :     {
     534           0 :         mCRL2log(mcrl2::log::verbose) << "Solving for Even..." << std::endl;
     535             :         DenseSPM spm( game(), PLAYER_EVEN,
     536           0 :                       stats_, vmap_, vmap_size_ );
     537           0 :         std::unique_ptr<LiftingStrategy2> ls(lsf_->create2(game_, spm));
     538           0 :         spm.initialize_lifting_strategy(*ls);
     539           0 :         while (spm.solve_some(*ls) == 0)
     540             :         {
     541           0 :             if (aborted()) return ParityGame::Strategy();
     542             :         }
     543           0 :         spm.get_strategy(strategy);
     544           0 :         spm.get_winning_set( PLAYER_ODD,
     545             :             std::back_insert_iterator<std::vector<verti> >(won_by_odd) );
     546             : #ifdef DEBUG
     547             :         mCRL2log(mcrl2::log::debug) << "Verifying small progress measures." << std::endl;
     548             :         assert(spm.verify_solution());
     549             : #endif
     550             :     }
     551             : 
     552           0 :     if (!won_by_odd.empty())
     553             :     {
     554             :         // Make a dual subgame of the vertices won by player Odd
     555           0 :         ParityGame subgame;
     556           0 :         mCRL2log(mcrl2::log::verbose) << "Constructing subgame of size "
     557           0 :                                       << won_by_odd.size() << " to solve for Odd..." << std::endl;
     558           0 :         subgame.make_subgame(game_, won_by_odd.begin(), won_by_odd.end(), true);
     559           0 :         subgame.compress_priorities();
     560             : 
     561             :         // Create vertex map to use:
     562           0 :         std::vector<verti> submap_data;
     563           0 :         verti *submap = &won_by_odd[0];
     564           0 :         std::size_t submap_size = won_by_odd.size();
     565           0 :         if (vmap_)
     566             :         {
     567           0 :             submap_data = won_by_odd;
     568           0 :             submap = &submap_data[0];
     569           0 :             merge_vertex_maps(submap, submap + submap_size, vmap_, vmap_size_);
     570             :         }
     571             : 
     572             :         // Second pass; solve subgame of vertices won by Odd:
     573           0 :         mCRL2log(mcrl2::log::verbose) << "Solving for Odd..." << std::endl;
     574             :         DenseSPM spm( subgame, PLAYER_ODD,
     575           0 :                       stats_, submap, submap_size );
     576           0 :         std::unique_ptr<LiftingStrategy2> ls(lsf_->create2(subgame, spm));
     577           0 :         spm.initialize_lifting_strategy(*ls);
     578           0 :         while (spm.solve_some(*ls) == 0)
     579             :         {
     580           0 :             if (aborted()) return ParityGame::Strategy();
     581             :         }
     582           0 :         ParityGame::Strategy substrat(won_by_odd.size(), NO_VERTEX);
     583           0 :         spm.get_strategy(substrat);
     584           0 :         merge_strategies(strategy, substrat, won_by_odd);
     585             : #ifdef DEBUG
     586             :         mCRL2log(mcrl2::log::debug) << "Verifying small progress measures." << std::endl;
     587             :         assert(spm.verify_solution());
     588             : #endif
     589             :     }
     590             : 
     591           0 :     return strategy;
     592             : }
     593             : 
     594           0 : ParityGame::Strategy SmallProgressMeasuresSolver2::solve_alternate()
     595             : {
     596             :     // Create two SPM and two lifting strategy instances:
     597           0 :     std::unique_ptr<SmallProgressMeasures> spm[2];
     598           0 :     spm[0].reset(new DenseSPM( game_, PLAYER_EVEN,
     599           0 :                                stats_, vmap_, vmap_size_ ));
     600           0 :     spm[1].reset(new DenseSPM( game_, PLAYER_ODD,
     601           0 :                                stats_, vmap_, vmap_size_ ));
     602             : 
     603             :     // Solve games alternatingly:
     604           0 :     int player = 0;
     605           0 :     bool half_solved = false;
     606           0 :     while (!half_solved)
     607             :     {
     608           0 :         mCRL2log(mcrl2::log::verbose) << "Switching to " << (player == 0 ? "normal" : "dual") << " game..." << std::endl;
     609           0 :         std::unique_ptr<LiftingStrategy2> ls(lsf_->create2(game_, *spm[player]));
     610           0 :         spm[player]->initialize_lifting_strategy(*ls);
     611             : 
     612           0 :         for ( long long work = game_.graph().V(); work > 0 && !half_solved;
     613           0 :               work -= SmallProgressMeasures::work_size )
     614             :         {
     615           0 :             half_solved = spm[player]->solve_some(*ls) > 0;
     616           0 :             if (aborted()) return ParityGame::Strategy();
     617             :         }
     618             : 
     619           0 :         mCRL2log(mcrl2::log::verbose) << "Propagating solved vertices to other game..." << std::endl;
     620           0 :         spm[player]->get_winning_set( (ParityGame::Player)player,
     621           0 :                                       SetToTopIterator(*spm[1 - player]) );
     622           0 :         player = 1 - player;
     623             :     }
     624             : 
     625             :     // One game is solved; solve other game completely too:
     626           0 :     mCRL2log(mcrl2::log::verbose) << "Finishing " << (player == 0 ? "normal" : "dual") << " game..." << std::endl;
     627           0 :     std::unique_ptr<LiftingStrategy2> ls(lsf_->create2(game_, *spm[player]));
     628           0 :     spm[player]->initialize_lifting_strategy(*ls);
     629           0 :     while (spm[player]->solve_some(*ls) == 0)
     630             :     {
     631           0 :         if (aborted()) return ParityGame::Strategy();
     632             :     }
     633             : 
     634             :     // Retrieve combined strategies:
     635           0 :     ParityGame::Strategy strategy(game_.graph().V(), NO_VERTEX);
     636           0 :     spm[0]->get_strategy(strategy);
     637           0 :     spm[1]->get_strategy(strategy);
     638             : 
     639           0 :     return strategy;
     640             : }
     641             : 
     642             : 
     643             : //
     644             : //  SmallProgressMeasuresSolverFactory
     645             : //
     646             : 
     647           0 : SmallProgressMeasuresSolverFactory::SmallProgressMeasuresSolverFactory(
     648             :         std::shared_ptr<LiftingStrategyFactory> lsf, int version, bool alt,
     649           0 :         LiftingStatistics *stats )
     650           0 :     : lsf_(lsf), version_(version), alt_(alt), stats_(stats)
     651           0 : {}
     652             : 
     653           0 : ParityGameSolver *SmallProgressMeasuresSolverFactory::create(
     654             :     const ParityGame &game, const verti *vmap, verti vmap_size )
     655             : {
     656           0 :     assert(version_ == 1 || version_ == 2);
     657           0 :     if (version_ == 1)
     658             :     {
     659             :         return new SmallProgressMeasuresSolver(
     660           0 :             game, lsf_, alt_, stats_, vmap, vmap_size );
     661             :     }
     662           0 :     if (version_ == 2)
     663             :     {
     664             :         return new SmallProgressMeasuresSolver2(
     665           0 :             game, lsf_, alt_, stats_, vmap, vmap_size );
     666             :     }
     667           0 :     return 0;
     668             : }
     669             : 
     670             : //
     671             : //  DenseSPM
     672             : //
     673             : 
     674           0 : DenseSPM::DenseSPM( const ParityGame &game, ParityGame::Player player,
     675             :                     LiftingStatistics *stats,
     676           0 :                     const verti *vertex_map, verti vertex_map_size )
     677             :     : SmallProgressMeasures(game, player, stats, vertex_map, vertex_map_size),
     678           0 :       spm_(new verti[(std::size_t)len_*game.graph().V()]())
     679             : {
     680           0 :     initialize_loops();
     681           0 : }
     682             : 
     683           0 : DenseSPM::~DenseSPM()
     684             : {
     685           0 :     delete[] spm_;
     686           0 : }
     687             : 
     688           0 : void DenseSPM::set_vec(verti v, const verti src[], bool carry)
     689             : {
     690           0 :     verti *dst = &spm_[(std::size_t)len_*v];
     691           0 :     const int l = len(v);                   // l: vector length
     692           0 :     int k = l;                              // k: position of last overflow
     693           0 :     for (int n = l - 1; n >= 0; --n)
     694             :     {
     695           0 :         dst[n] = src[n] + carry;
     696           0 :         carry = (dst[n] >= M_[n]);
     697           0 :         if (carry) k = n;
     698             :     }
     699           0 :     while (k < l) dst[k++] = 0;
     700           0 :     if (carry) set_top(v);
     701           0 : }
     702             : 
     703           0 : void DenseSPM::set_vec_to_top(verti v)
     704             : {
     705           0 :     spm_[(std::size_t)len_*v] = NO_VERTEX;
     706           0 : }

Generated by: LCOV version 1.13