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 : 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 0 : 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) << "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) << "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 0 : }
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) << "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 0 : }
174 :
175 0 : const verti num_unsolved = V - (verti)solved_set.size();
176 0 : mCRL2log(mcrl2::log::verbose) << "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) << "Solving..." << std::endl;
210 0 : ParityGame::Strategy substrat = subsolver->solve();
211 0 : if (!substrat.empty())
212 : {
213 0 : mCRL2log(mcrl2::log::verbose) << "Merging strategies..." << std::endl;
214 0 : merge_strategies(strategy, substrat, unsolved);
215 : }
216 :
217 0 : return strategy;
218 0 : }
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 : }
|
