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 : }