Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/pbes/parity_game_generator.h
10 : /// \brief A class for generating a parity game from a pbes.
11 :
12 : #ifndef MCRL2_PBES_PARITY_GAME_GENERATOR_H
13 : #define MCRL2_PBES_PARITY_GAME_GENERATOR_H
14 :
15 : #include "mcrl2/pbes/algorithms.h"
16 : #include "mcrl2/pbes/detail/bes_equation_limit.h"
17 : #include "mcrl2/pbes/join.h"
18 : #include "mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h"
19 : #include <iomanip>
20 :
21 : namespace mcrl2
22 : {
23 :
24 : namespace pbes_system
25 : {
26 :
27 : /// \brief Class for generating a BES from a PBES. This BES can be interpreted as
28 : /// a graph corresponding to a parity game problem. The proposition variables
29 : /// of the BES correspond to the vertices of the graph.
30 : /// An interface to the graph is provided in which the vertices correspond to
31 : /// integer values. The values are in the range [0, 1, ..., n], i.e. there are
32 : /// no holes in the sequence.
33 : /// Each vertex is labeled with a priority value, which is the
34 : /// block nesting depth of the proposition variable in the BES.
35 : class parity_game_generator
36 : {
37 : protected:
38 : /// \brief Substitution function type used by the PBES rewriter.
39 : typedef data::rewriter::substitution_type substitution_function;
40 :
41 : /// \brief Mark whether initialization has been initialized.
42 : /// Needed to properly cope with virtual inheritance!
43 : bool m_initialized;
44 :
45 : /// \brief The PBES that is being solved.
46 : pbes& m_pbes;
47 :
48 : /// \brief Data rewriter.
49 : data::rewriter datar;
50 :
51 : /// \brief PBES rewriter.
52 : pbes_system::enumerate_quantifiers_rewriter R;
53 :
54 : /// \brief Maps propositional variables to corresponding PBES equations.
55 : std::map<core::identifier_string, std::vector<pbes_equation>::const_iterator > m_pbes_equation_index;
56 :
57 : /// \brief Maps propositional variables to corresponding priorities.
58 : std::map<core::identifier_string, std::size_t> m_priorities;
59 :
60 : /// \brief Maps PBES closed expressions to corresponding BES variables.
61 : std::map<pbes_expression, std::size_t> m_pbes_expression_index;
62 :
63 : /// \brief Contains intermediate results of the BES that is being generated.
64 : /// m_bes[i] represents a BES equation corresponding to BES variable i.
65 : /// m_bes[i].first is the right hand side of the BES equation
66 : /// m_bes[i].second is the block nesting depth of the corresponding PBES variable
67 : std::vector<std::pair<pbes_expression, std::size_t> > m_bes;
68 :
69 : /// \brief Determines what kind of BES equations are generated for true and false.
70 : bool m_true_false_dependencies;
71 :
72 : /// \brief True if it is a min-parity game.
73 : bool m_is_min_parity_game;
74 :
75 : /// \brief The maximum priority value of the game.
76 : std::size_t m_max_priority = 0;
77 :
78 : /// \brief Adds a BES equation for a given PBES expression, if it not already exists.
79 : /// \param t A PBES expression
80 : /// \param priority A positive integer
81 : /// \return The index of a BES equation corresponding to the given PBES expression.
82 : /// If no equation exists for the expression, a new one is added.
83 183 : std::size_t add_bes_equation(pbes_expression t, std::size_t priority)
84 : {
85 : std::size_t result;
86 :
87 183 : mCRL2log(log::trace) << "Adding equation for " << t << std::endl;
88 :
89 : // TODO: can this insertion be done more efficiently?
90 183 : auto i = m_pbes_expression_index.find(t);
91 183 : if (i != m_pbes_expression_index.end())
92 : {
93 33 : result = i->second;
94 : }
95 : else
96 : {
97 150 : std::size_t p = m_pbes_expression_index.size();
98 150 : m_pbes_expression_index[t] = p;
99 150 : if (is_propositional_variable_instantiation(t))
100 : {
101 108 : priority = m_priorities[atermpp::down_cast<propositional_variable_instantiation>(t).name()];
102 : }
103 150 : m_bes.emplace_back(t, priority);
104 150 : detail::check_bes_equation_limit(m_bes.size());
105 150 : mCRL2log(log::status) << print_equation_count(m_bes.size());
106 150 : result = p;
107 : }
108 :
109 183 : return result;
110 : }
111 :
112 : /// \brief Generates a substitution function for the pbesinst rewriter.
113 : /// \param v A sequence of data variables
114 : /// \param e A sequence of data expressions
115 : /// \param sigma The result.
116 1834 : void make_substitution(const data::variable_list& v, const data::data_expression_list& e, substitution_function& sigma) const
117 : {
118 1834 : assert(v.size() == e.size());
119 1834 : data::variable_list::iterator i = v.begin();
120 1834 : data::data_expression_list::iterator j = e.begin();
121 7400 : for (; i != v.end(); ++i, ++j)
122 : {
123 5566 : sigma[*i] = *j;
124 : }
125 1834 : }
126 :
127 998 : pbes_expression expand_rhs(const pbes_expression& psi)
128 : {
129 : // expand the right hand side if needed
130 998 : if (is_propositional_variable_instantiation(psi))
131 : {
132 968 : const auto& psi1 = atermpp::down_cast<propositional_variable_instantiation>(psi);
133 968 : const pbes_equation& pbes_eqn = *m_pbes_equation_index[psi1.name()];
134 968 : substitution_function sigma;
135 968 : make_substitution(pbes_eqn.variable().parameters(), psi1.parameters(), sigma);
136 968 : mCRL2log(log::trace) << "Expanding right hand side " << pbes_eqn.formula() << " into " << std::flush;
137 968 : pbes_expression result = R(pbes_eqn.formula(), sigma);
138 968 : R.clear_identifier_generator();
139 968 : mCRL2log(log::trace) << result << std::endl;
140 968 : return result;
141 968 : }
142 30 : return psi;
143 : }
144 :
145 : /// \brief Compute equation index map.
146 21 : void compute_equation_index_map()
147 : {
148 :
149 72 : for (std::vector<pbes_equation>::const_iterator i = m_pbes.equations().begin(); i != m_pbes.equations().end(); ++i)
150 : {
151 51 : m_pbes_equation_index[i->variable().name()] = i;
152 : }
153 21 : }
154 :
155 : /// \brief Compute priorities of PBES propositional variables.
156 21 : void compute_priorities(const std::vector<pbes_equation>& equations)
157 : {
158 21 : fixpoint_symbol sigma = fixpoint_symbol::nu();
159 21 : std::size_t priority = 0;
160 72 : for (const auto& equation: equations)
161 : {
162 51 : if (equation.symbol() == sigma)
163 : {
164 30 : m_priorities[equation.variable().name()] = priority;
165 : }
166 : else
167 : {
168 21 : sigma = equation.symbol();
169 21 : m_priorities[equation.variable().name()] = ++priority;
170 : }
171 : }
172 :
173 21 : m_max_priority = (priority % 2 == 0 ? priority : priority + 1);
174 :
175 : // If it is a max-priority game, adjust the priorities
176 21 : if (!m_is_min_parity_game)
177 : {
178 : // Choose an even upperbound max_priority
179 0 : if (m_max_priority == 0)
180 : {
181 0 : m_max_priority = 2;
182 : }
183 0 : for (auto& i: m_priorities)
184 : {
185 0 : i.second = m_max_priority - i.second;
186 : }
187 : // Add BES equations for true and false with priorities 0 and 1.
188 0 : add_bes_equation(true_(), m_max_priority);
189 0 : add_bes_equation(false_(), m_max_priority - 1);
190 : }
191 : else
192 : {
193 : // Add BES equations for true and false with priorities 0 and 1.
194 21 : add_bes_equation(true_(), 0);
195 21 : add_bes_equation(false_(), 1);
196 : }
197 21 : }
198 :
199 : // prints the BES equation with left hand side 'index' and right hand side 'rhs'
200 : virtual
201 0 : std::string print_bes_equation(std::size_t index, const std::set<std::size_t>& rhs)
202 : {
203 0 : std::ostringstream out;
204 0 : const std::pair<pbes_expression, std::size_t>& eqn = m_bes[index];
205 0 : const std::size_t priority = eqn.second;
206 0 : out << (priority % 2 == 1 ? "mu Y" : "nu Y") << index << " = ";
207 0 : std::string op = (get_operation(index) == PGAME_AND ? " && " : " || ");
208 0 : for (auto i = rhs.begin(); i != rhs.end(); ++i)
209 : {
210 0 : out << (i == rhs.begin() ? "" : op) << "Y" << *i;
211 : }
212 0 : out << " (priority = " << priority << ")" << std::endl;
213 0 : return out.str();
214 0 : }
215 :
216 : /// \brief Prints a log message for every step-th equation
217 18 : std::string print_equation_count(std::size_t size, std::size_t step = 1000) const
218 : {
219 18 : if (size > 0 && (size % step == 0 || (size < 1000 && size % 100 == 0)))
220 : {
221 0 : std::ostringstream out;
222 0 : out << "Generated " << size << " BES equations" << std::endl;
223 0 : return out.str();
224 0 : }
225 18 : return "";
226 : }
227 :
228 : virtual
229 2182 : void initialize_generation()
230 : {
231 2182 : if (m_initialized)
232 : {
233 2161 : return;
234 : }
235 : else
236 : {
237 : // Nothing to be done for an empty PBES.
238 21 : if (m_pbes.equations().empty())
239 : {
240 0 : return;
241 : }
242 :
243 : // Normalize the pbes, since the parity game generator currently doesn't handle negation and implication.
244 21 : pbes_system::algorithms::normalize(m_pbes);
245 :
246 21 : compute_equation_index_map();
247 21 : compute_priorities(m_pbes.equations());
248 :
249 : // Add a BES equation for the initial state.
250 21 : propositional_variable_instantiation phi = get_initial_state();
251 21 : add_bes_equation(phi, m_priorities[phi.name()]);
252 :
253 21 : m_initialized = true;
254 21 : }
255 : }
256 :
257 : public:
258 : /// \brief The operation type of the vertices.
259 : enum operation_type { PGAME_OR, PGAME_AND };
260 :
261 : /// \brief Constructor.
262 : /// \param p A PBES
263 : /// \param true_false_dependencies If true, nodes are generated for the values <tt>true</tt> and <tt>false</tt>.
264 : /// \param is_min_parity If true a min-parity game is produced, otherwise a max-parity game
265 : /// \param rewrite_strategy Strategy to use for the data rewriter
266 21 : explicit parity_game_generator(pbes& p, bool true_false_dependencies = false, bool is_min_parity = true, data::rewriter::strategy rewrite_strategy = data::jitty)
267 21 : :
268 21 : m_initialized(false),
269 21 : m_pbes(p),
270 21 : datar(p.data(), mcrl2::data::used_data_equation_selector(p.data(), pbes_system::find_function_symbols(p), p.global_variables(), false), rewrite_strategy),
271 21 : R(datar, p.data()),
272 21 : m_true_false_dependencies(true_false_dependencies),
273 42 : m_is_min_parity_game(is_min_parity)
274 : {
275 21 : pbes_system::algorithms::instantiate_global_variables(p);
276 21 : }
277 :
278 21 : virtual ~parity_game_generator() = default;
279 :
280 : /// \brief Returns the (rewritten) initial state.
281 : /// \return the initial state rewritten by R
282 15 : virtual propositional_variable_instantiation get_initial_state()
283 : {
284 15 : return atermpp::down_cast<propositional_variable_instantiation>(R(m_pbes.initial_state()));
285 : }
286 :
287 : /// \brief Returns the vertex type.
288 : /// \param index A positive integer
289 : /// \return PGAME_AND if the corresponding BES equation is a conjunction,
290 : /// PGAME_OR if it is a disjunction.
291 : virtual
292 123 : operation_type get_operation(std::size_t index)
293 : {
294 123 : initialize_generation();
295 :
296 123 : assert(index < m_bes.size());
297 123 : const pbes_expression& phi = m_bes[index].first;
298 123 : return get_expression_operation(phi);
299 : }
300 :
301 : /// \brief Returns the vertex type.
302 : /// \param phi A PBES expression
303 : /// \return PGAME_AND if the expression is a conjunction,
304 : /// PGAME_OR if it is a disjunction.
305 : virtual
306 137 : operation_type get_expression_operation(const pbes_expression& phi)
307 : {
308 137 : if (is_and(phi))
309 : {
310 33 : return PGAME_AND;
311 : }
312 104 : else if (is_or(phi))
313 : {
314 3 : return PGAME_OR;
315 : }
316 101 : else if (is_propositional_variable_instantiation(phi))
317 : {
318 72 : return PGAME_OR;
319 : }
320 29 : else if (is_true(phi))
321 : {
322 13 : return PGAME_AND;
323 : }
324 16 : else if (is_false(phi))
325 : {
326 16 : return PGAME_OR;
327 : }
328 0 : else if (is_forall(phi))
329 : {
330 0 : return PGAME_AND;
331 : }
332 0 : else if (is_exists(phi))
333 : {
334 0 : return PGAME_OR;
335 : }
336 0 : else if (is_data(phi))
337 : {
338 0 : return PGAME_OR;
339 : }
340 0 : throw(std::runtime_error("Error in parity_game_generator: unexpected operation " + pbes_system::pp(phi)));
341 : }
342 :
343 : /// \brief Returns the priority of a vertex.
344 : /// The priority of the first equation is 0 if it is a maximal fixpoint,
345 : /// and 1 if it is a minimal fixpoint.
346 : /// \param index A positive integer
347 : /// \return The block nesting depth of the variable in the BES.
348 : virtual
349 177 : std::size_t get_priority(std::size_t index)
350 : {
351 177 : initialize_generation();
352 :
353 177 : assert(index < m_bes.size());
354 177 : return m_bes[index].second;
355 : }
356 :
357 : /// \brief Returns the vertices for which a solution is requested.
358 : /// By default a set containing the values 0, 1 and 2 is returned, corresponding
359 : /// to the expressions true, false and the initial state of the PBES.
360 : /// \return A set of indices corresponding to proposition variables of the generated BES.
361 : virtual
362 12 : std::set<std::size_t> get_initial_values()
363 : {
364 12 : initialize_generation();
365 :
366 12 : std::set<std::size_t> result;
367 12 : if (!m_pbes.equations().empty())
368 : {
369 12 : result.insert(0); // equation 0 corresponds with the value true
370 12 : result.insert(1); // equation 1 corresponds with the value false
371 12 : result.insert(2); // equation 2 corresponds with the initial state
372 : }
373 12 : return result;
374 0 : }
375 :
376 : /// \brief Returns the successors of a vertex in the graph.
377 : /// \param index A positive integer
378 : /// \return The indices of the proposition variables that appear in the
379 : /// right hand side of the BES equation of the given index.
380 : virtual
381 132 : std::set<std::size_t> get_dependencies(std::size_t index)
382 : {
383 132 : initialize_generation();
384 :
385 132 : assert(index < m_bes.size());
386 :
387 132 : std::set<std::size_t> result;
388 :
389 132 : std::pair<pbes_expression, std::size_t>& eqn = m_bes[index];
390 132 : pbes_expression& psi = eqn.first;
391 132 : const std::size_t priority = eqn.second;
392 :
393 132 : mCRL2log(log::debug) << std::endl << "Generating equation for expression " << psi << std::endl;
394 :
395 : // expand the right hand side if needed
396 132 : psi = expand_rhs(psi);
397 :
398 : // top_flatten
399 132 : if (is_propositional_variable_instantiation(psi))
400 : {
401 68 : result.insert(add_bes_equation(psi, m_priorities[atermpp::down_cast<propositional_variable_instantiation>(psi).name()]));
402 : }
403 64 : else if (is_and(psi))
404 : {
405 69 : for (const pbes_expression& term: split_and(psi))
406 : {
407 46 : auto prio = is_or(term) ? (m_is_min_parity_game ? m_max_priority : 0) : priority;
408 46 : result.insert(add_bes_equation(term, prio));
409 23 : }
410 : }
411 41 : else if (is_or(psi))
412 : {
413 9 : for (const pbes_expression& term: split_or(psi))
414 : {
415 6 : auto prio = is_and(term) ? (m_is_min_parity_game ? m_max_priority : 0) : priority;
416 6 : result.insert(add_bes_equation(term, prio));
417 3 : }
418 : }
419 38 : else if (is_true(psi))
420 : {
421 16 : if (m_true_false_dependencies)
422 : {
423 16 : auto i = m_pbes_expression_index.find(true_());
424 16 : assert(i != m_pbes_expression_index.end());
425 16 : result.insert(i->second);
426 : }
427 : }
428 22 : else if (is_false(psi))
429 : {
430 22 : if (m_true_false_dependencies)
431 : {
432 22 : auto i = m_pbes_expression_index.find(false_());
433 22 : assert(i != m_pbes_expression_index.end());
434 22 : result.insert(i->second);
435 : }
436 : }
437 : else
438 : {
439 0 : std::ostringstream out;
440 0 : out << "Error in parity_game_generator: unexpected expression " << psi << "\n" << atermpp::aterm(psi);
441 0 : throw(std::runtime_error(out.str()));
442 0 : }
443 132 : mCRL2log(log::debug) << print_bes_equation(index, result);
444 132 : return result;
445 0 : }
446 :
447 : /// \brief Prints the mapping from BES variables to the corresponding PBES expressions.
448 : virtual
449 0 : void print_variable_mapping()
450 : {
451 0 : mCRL2log(log::info) << "--- variable mapping ---" << std::endl;
452 0 : std::map<std::size_t, pbes_expression> m;
453 0 : for (auto& i: m_pbes_expression_index)
454 : {
455 0 : m[i.second] = i.first;
456 : }
457 0 : for (auto& i: m)
458 : {
459 0 : mCRL2log(log::info) << std::setw(4) << i.first << " " << i.second << std::endl;
460 : }
461 0 : mCRL2log(log::info) << "--- priorities ---" << std::endl;
462 0 : for (auto& i: m_priorities)
463 : {
464 0 : mCRL2log(log::info) << core::pp(i.first) << " " << i.second << std::endl;
465 : }
466 0 : }
467 : };
468 :
469 : } // namespace pbes_system
470 :
471 : } // namespace mcrl2
472 :
473 : #endif // MCRL2_PBES_PARITY_GAME_GENERATOR_H
|
