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/solve_structure_graph.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_SOLVE_STRUCTURE_GRAPH_H
13 : #define MCRL2_PBES_SOLVE_STRUCTURE_GRAPH_H
14 :
15 : #include "mcrl2/atermpp/standard_containers/vector.h"
16 : #include "mcrl2/data/join.h"
17 : #include "mcrl2/lts/lts_algorithm.h"
18 : #include "mcrl2/pbes/pbes_equation_index.h"
19 : #include "mcrl2/pbes/pbessolve_attractors.h"
20 :
21 : namespace mcrl2 {
22 :
23 : namespace pbes_system {
24 :
25 : inline
26 67 : std::tuple<std::size_t, std::size_t, vertex_set> get_minmax_rank(const structure_graph& G)
27 : {
28 67 : std::size_t min_rank = (std::numeric_limits<std::size_t>::max)();
29 67 : std::size_t max_rank = 0;
30 67 : std::vector<structure_graph::index_type> M; // vertices with minimal rank
31 67 : std::size_t N = G.all_vertices().size();
32 :
33 3478 : for (std::size_t vi = 0; vi < N; vi++)
34 : {
35 3411 : if (!G.contains(vi))
36 : {
37 1555 : continue;
38 : }
39 1856 : const auto& v = G.find_vertex(vi);
40 1856 : if (v.rank <= min_rank)
41 : {
42 850 : if (v.rank < min_rank)
43 : {
44 69 : M.clear();
45 69 : min_rank = v.rank;
46 : }
47 850 : M.push_back(vi);
48 : }
49 1856 : if (v.rank > max_rank)
50 : {
51 76 : max_rank = v.rank;
52 : }
53 : }
54 201 : return std::make_tuple(min_rank, max_rank, vertex_set(N, M.begin(), M.end()));
55 67 : }
56 :
57 : /// \brief Guesses if a pbes has counter example information
58 : inline
59 : bool has_counter_example_information(const pbes& pbesspec)
60 : {
61 : std::regex re("Z(neg|pos)_(\\d+)_.*");
62 : std::smatch match;
63 : for (const pbes_equation& eqn: pbesspec.equations())
64 : {
65 : std::string X = eqn.variable().name();
66 : if (std::regex_match(X, match, re))
67 : {
68 : return true;
69 : }
70 : }
71 : return false;
72 : }
73 :
74 : class solve_structure_graph_algorithm
75 : {
76 : protected:
77 : // do a sanity check on the computed strategy
78 : bool check_strategy = false;
79 :
80 : bool use_toms_optimization = false;
81 :
82 : // find a successor of u
83 : static structure_graph::index_type succ(const structure_graph& G, structure_graph::index_type u)
84 : {
85 : for (structure_graph::index_type v: G.successors(u))
86 : {
87 : return v;
88 : }
89 : return undefined_vertex();
90 : }
91 :
92 : // find a successor of u in U, or a random one if no successor in U exists
93 : static inline
94 53 : structure_graph::index_type succ(const structure_graph& G, structure_graph::index_type u, const vertex_set& U)
95 : {
96 53 : auto result = undefined_vertex();
97 53 : for (structure_graph::index_type v: G.successors(u))
98 : {
99 1 : if (U.contains(v))
100 : {
101 1 : return v;
102 : }
103 0 : result = v;
104 55 : }
105 52 : return result;
106 : }
107 :
108 : public:
109 : // computes solve_recursive(G \ A)
110 : inline
111 191 : std::pair<vertex_set, vertex_set> solve_recursive(structure_graph& G, const vertex_set& A)
112 : {
113 191 : auto exclude = G.exclude() | A.include();
114 191 : std::swap(G.exclude(), exclude);
115 191 : auto result = solve_recursive(G);
116 191 : std::swap(G.exclude(), exclude);
117 382 : return result;
118 191 : }
119 :
120 : protected:
121 : // pre: G does not contain nodes with decoration true or false.
122 : //
123 : // N.B. If use_toms_optimization is true, then the oomputed strategy may be incorrect.
124 : // So this flag should only be used to compute the solution.
125 : inline
126 220 : std::pair<vertex_set, vertex_set> solve_recursive(structure_graph& G)
127 : {
128 220 : mCRL2log(log::debug) << "\n --- solve_recursive input ---\n" << G << std::endl;
129 220 : std::size_t N = G.extent();
130 :
131 220 : if (G.is_empty())
132 : {
133 306 : return { vertex_set(N), vertex_set(N) };
134 : }
135 :
136 67 : auto q = get_minmax_rank(G);
137 67 : std::size_t m = std::get<0>(q);
138 67 : const vertex_set& U = std::get<2>(q);
139 :
140 67 : std::size_t alpha = m % 2; // 0 = disjunctive, 1 = conjunctive
141 :
142 : // set strategy
143 883 : for (structure_graph::index_type ui: U.vertices())
144 : {
145 816 : const auto& u = G.find_vertex(ui);
146 816 : if (u.decoration == alpha)
147 : {
148 : // auto v = succ(G, ui); // N.B. this may lead to a wrong strategy!
149 53 : auto v = succ(G, ui, U);
150 53 : if (v != undefined_vertex())
151 : {
152 1 : global_strategy<structure_graph>(G).set_strategy(ui, v);
153 : // mCRL2log(log::debug) << "set initial strategy for node " << ui << " to " << v << std::endl;
154 : }
155 : }
156 : }
157 :
158 : // // optimization
159 : // std::size_t h = std::get<1>(q);
160 : // if (h == m)
161 : // {
162 : // if (m % 2 == 0)
163 : // {
164 : // return { make_vertex_set(G), vertex_set(N) };
165 : // }
166 : // else
167 : // {
168 : // return { vertex_set(N), make_vertex_set(G) };
169 : // }
170 : // }
171 :
172 268 : vertex_set W[2] = { vertex_set(N), vertex_set(N) };
173 402 : vertex_set W_1[2];
174 :
175 67 : vertex_set A = attr_default(G, U, alpha);
176 67 : std::tie(W_1[0], W_1[1]) = solve_recursive(G, A);
177 :
178 67 : if (use_toms_optimization)
179 : {
180 : // More efficient than Zielonka, because some recursive calls are skipped.
181 : // As a consequence, the computed strategy may be wrong.
182 38 : vertex_set B = attr_default(G, W_1[1 - alpha], 1 - alpha);
183 38 : if (W_1[1 - alpha].size() == B.size())
184 : {
185 33 : W[alpha] = set_union(A, W_1[alpha]);
186 33 : W[1 - alpha] = B;
187 : }
188 : else
189 : {
190 5 : std::tie(W[0], W[1]) = solve_recursive(G, B);
191 5 : W[1 - alpha] = set_union(W[1 - alpha], B);
192 : }
193 38 : }
194 : else
195 : {
196 : // Original Zielonka version
197 29 : if (W_1[1 - alpha].is_empty())
198 : {
199 22 : W[alpha] = set_union(A, W_1[alpha]);
200 22 : W[1 - alpha].clear();
201 : }
202 : else
203 : {
204 7 : vertex_set B = attr_default(G, W_1[1 - alpha], 1 - alpha);
205 7 : std::tie(W[0], W[1]) = solve_recursive(G, B);
206 7 : W[1 - alpha] = set_union(W[1 - alpha], B);
207 7 : }
208 : }
209 :
210 67 : mCRL2log(log::debug) << "\n --- solution for solve_recursive input ---\n" << G;
211 67 : mCRL2log(log::debug) << " W0 = " << W[0] << std::endl;
212 67 : mCRL2log(log::debug) << " W1 = " << W[1] << std::endl;
213 67 : assert(W[0].size() + W[1].size() + G.exclude().count() == N);
214 67 : return { W[0], W[1] };
215 536 : }
216 :
217 : // Handles nodes with decoration true or false.
218 : inline
219 141 : std::pair<vertex_set, vertex_set> solve_recursive_extended(structure_graph& G)
220 : {
221 141 : mCRL2log(log::debug) << "\n --- solve_recursive_extended input ---\n" << G << std::endl;
222 :
223 141 : std::size_t N = G.extent();
224 141 : vertex_set Vconj(N);
225 141 : vertex_set Vdisj(N);
226 :
227 : // find vertices Vconj with decoration false and Vdisj with decoration true
228 4149 : for (std::size_t vi = 0; vi < N; vi++)
229 : {
230 4008 : if (!G.contains(vi))
231 : {
232 0 : continue;
233 : }
234 4008 : const auto& v = G.find_vertex(vi);
235 4008 : if (v.decoration == structure_graph::d_false)
236 : {
237 587 : Vconj.insert(vi);
238 : }
239 3421 : else if (v.decoration == structure_graph::d_true)
240 : {
241 80 : Vdisj.insert(vi);
242 : }
243 : }
244 :
245 : // extend Vconj and Vdisj
246 141 : if (!Vconj.is_empty())
247 : {
248 74 : Vconj = attr_default(G, Vconj, 1);
249 : }
250 141 : if (!Vdisj.is_empty())
251 : {
252 45 : Vdisj = attr_default(G, Vdisj, 0);
253 : }
254 :
255 : // default case
256 141 : if (Vconj.is_empty() && Vdisj.is_empty())
257 : {
258 29 : return solve_recursive(G);
259 : }
260 : else
261 : {
262 112 : vertex_set Wconj(N);
263 112 : vertex_set Wdisj(N);
264 112 : vertex_set Vunion = set_union(Vconj, Vdisj);
265 112 : std::tie(Wdisj, Wconj) = solve_recursive(G, Vunion);
266 224 : return std::make_pair(set_union(Wdisj, Vdisj), set_union(Wconj, Vconj));
267 112 : }
268 141 : }
269 :
270 46 : static void insert_edge(structure_graph::vertex_vector& V, structure_graph::index_type ui, structure_graph::index_type vi)
271 : {
272 : using utilities::detail::contains;
273 46 : structure_graph::vertex& u = V[ui];
274 46 : structure_graph::vertex& v = V[vi];
275 46 : if (!contains(u.successors, vi))
276 : {
277 46 : u.successors.push_back(vi);
278 46 : v.predecessors.push_back(ui);
279 : }
280 46 : }
281 :
282 4 : void check_solve_recursive_solution(const structure_graph& G, bool is_disjunctive, const vertex_set& Wdisj, const vertex_set& Wconj)
283 : {
284 : using utilities::detail::contains;
285 :
286 4 : mCRL2log(log::debug) << "\n--- CHECK STRATEGY ---" << std::endl;
287 4 : log_vertex_set(G, Wconj, "Wconj");
288 4 : log_vertex_set(G, Wdisj, "Wdisj");
289 :
290 : typedef structure_graph::vertex vertex;
291 4 : structure_graph::index_type init = G.initial_vertex();
292 :
293 : // V contains the vertices of G, but not the edges
294 4 : structure_graph::vertex_vector V = G.all_vertices();
295 120 : for (vertex& v: V)
296 : {
297 116 : v.successors.clear();
298 116 : v.predecessors.clear();
299 : }
300 :
301 4 : std::set<structure_graph::index_type> todo = { init };
302 4 : std::set<structure_graph::index_type> done;
303 :
304 49 : while (!todo.empty())
305 : {
306 45 : structure_graph::index_type u = *todo.begin();
307 45 : todo.erase(todo.begin());
308 45 : done.insert(u);
309 45 : if ((is_disjunctive && G.decoration(u) == structure_graph::d_disjunction) || (!is_disjunctive && G.decoration(u) == structure_graph::d_conjunction))
310 : {
311 : // explore only the strategy edge
312 20 : structure_graph::index_type v = G.strategy(u);
313 20 : insert_edge(V, u, v);
314 20 : if (v != undefined_vertex() && !contains(done, v))
315 : {
316 19 : todo.insert(v);
317 : }
318 : }
319 : else
320 : {
321 : // explore all outgoing edges
322 51 : for (structure_graph::index_type v: G.successors(u))
323 : {
324 26 : insert_edge(V, u, v);
325 26 : if (!contains(done, v))
326 : {
327 26 : todo.insert(v);
328 : }
329 25 : }
330 : }
331 : }
332 :
333 4 : vertex_set Wconj1;
334 4 : vertex_set Wdisj1;
335 :
336 8 : structure_graph Gcopy(V, G.initial_vertex(), G.exclude());
337 4 : std::tie(Wdisj1, Wconj1) = solve_recursive_extended(Gcopy);
338 : bool is_disjunctive1;
339 4 : if (Wdisj1.contains(G.initial_vertex()))
340 : {
341 2 : is_disjunctive1 = true;
342 : }
343 2 : else if (Wconj1.contains(G.initial_vertex()))
344 : {
345 2 : is_disjunctive1 = false;
346 : }
347 : else
348 : {
349 0 : throw mcrl2::runtime_error("No solution found!!!");
350 : }
351 4 : if (is_disjunctive != is_disjunctive1)
352 : {
353 0 : log_vertex_set(Gcopy, Wconj1, "Wconj1");
354 0 : log_vertex_set(Gcopy, Wdisj1, "Wdisj1");
355 0 : throw mcrl2::runtime_error("check_solve_recursive_solution failed!");
356 : }
357 4 : }
358 :
359 : public:
360 135 : explicit solve_structure_graph_algorithm(bool check_strategy_ = false, bool use_toms_optimization_ = false)
361 135 : : check_strategy(check_strategy_),
362 135 : use_toms_optimization(use_toms_optimization_)
363 135 : {}
364 :
365 : inline
366 137 : bool solve(structure_graph& G)
367 : {
368 137 : mCRL2log(log::verbose) << "Solving parity game..." << std::endl;
369 137 : mCRL2log(log::debug) << G << std::endl;
370 137 : assert(G.extent() > 0);
371 137 : assert(G.is_defined());
372 137 : auto W = solve_recursive_extended(G);
373 : bool is_disjunctive;
374 137 : if (W.first.contains(G.initial_vertex()))
375 : {
376 59 : is_disjunctive = true;
377 : }
378 78 : else if (W.second.contains(G.initial_vertex()))
379 : {
380 78 : is_disjunctive = false;
381 : }
382 : else
383 : {
384 0 : throw mcrl2::runtime_error("No solution found!!!");
385 : }
386 137 : if (check_strategy)
387 : {
388 4 : check_solve_recursive_solution(G, is_disjunctive, W.first, W.second);
389 : }
390 137 : return is_disjunctive;
391 137 : }
392 : };
393 :
394 : class lps_solve_structure_graph_algorithm: public solve_structure_graph_algorithm
395 : {
396 : protected:
397 : static lps::specification create_counter_example_lps(structure_graph& G, const std::set<structure_graph::index_type>& V, const lps::specification& lpsspec, const pbes& p, const pbes_equation_index& p_index)
398 : {
399 : lps::specification result = lpsspec;
400 : result.process().action_summands().clear();
401 : result.process().deadlock_summands().clear();
402 : auto& action_summands = result.process().action_summands();
403 : std::regex re("Z(neg|pos)_(\\d+)_.*");
404 : std::size_t n = lpsspec.process().process_parameters().size();
405 :
406 : for (structure_graph::index_type vi: V)
407 : {
408 : const auto& v = G.find_vertex(vi);
409 : if (is_propositional_variable_instantiation(v.formula()))
410 : {
411 : // The variable Z below should be a reference, but this leads to crashes with the GCC compiler (March 2022).
412 : // JFG: I think this is a GCC problem, which may resolve itself in due time.
413 : const auto Z = atermpp::down_cast<propositional_variable_instantiation>(v.formula());
414 : std::string Zname = Z.name();
415 : std::smatch match;
416 : if (std::regex_match(Zname, match, re))
417 : {
418 : std::size_t summand_index = std::stoul(match[2]);
419 : if (summand_index >= lpsspec.process().action_summands().size())
420 : {
421 : throw mcrl2::runtime_error("Counter-example cannot be reconstructed from this LPS. Did you supply the correct file?");
422 : }
423 : lps::action_summand summand = lpsspec.process().action_summands()[summand_index];
424 : std::size_t equation_index = p_index.index(Z.name());
425 : const pbes_equation& eqn = p.equations()[equation_index];
426 : const data::variable_list& d = eqn.variable().parameters();
427 : data::variable_vector d1(d.begin(), d.end());
428 :
429 : const data::data_expression_list& e = Z.parameters();
430 : data::data_expression_vector e1(e.begin(), e.end());
431 :
432 : data::data_expression_vector condition;
433 : data::assignment_vector next_state_assignments;
434 : std::size_t m = d.size() - 2 * n;
435 :
436 : for (std::size_t i = 0; i < n; i++)
437 : {
438 : condition.push_back(data::equal_to(d1[i], e1[i]));
439 : next_state_assignments.emplace_back(d1[i], e1[n + m + i]);
440 : }
441 :
442 : process::action_vector actions;
443 : std::size_t index = 0;
444 : for (const process::action& a: summand.multi_action().actions())
445 : {
446 : process::action a1(a.label(), data::data_expression_list(e1.begin() + n + index, e1.begin() + n + index + a.arguments().size()));
447 : actions.push_back(a1);
448 : index = index + a.arguments().size();
449 : }
450 :
451 : summand.summation_variables() = data::variable_list();
452 : summand.condition() = data::join_and(condition.begin(), condition.end());
453 : summand.multi_action() = lps::multi_action(process::action_list(actions.begin(), actions.end()),summand.multi_action().time());
454 : summand.assignments() = data::assignment_list(next_state_assignments.begin(), next_state_assignments.end());
455 :
456 : action_summands.push_back(summand);
457 : }
458 : }
459 : }
460 : return result;
461 : }
462 :
463 : public:
464 : lps_solve_structure_graph_algorithm() = default;
465 :
466 : /// \brief Solve a pbes for some equation, while constructing a counter example or wittness based on the accompanying linear process.
467 : /// \param G A structure graph.
468 : /// \param lpsspec The original LPS that was used to create the PBES.
469 : /// \param p The pbes to be solved.
470 : /// \param p_index The index of the pbes equation to be solved.
471 : /// \return A boolean indicating the solution and a linear process that represents the counter example.
472 : std::pair<bool, lps::specification> solve_with_counter_example(structure_graph& G, const lps::specification& lpsspec, const pbes& p, const pbes_equation_index& p_index)
473 : {
474 : if (!lpsspec.global_variables().empty())
475 : {
476 : throw mcrl2::runtime_error("solve_with_counter_example requires an LPS without global variables.");
477 : }
478 : if (!p.global_variables().empty())
479 : {
480 : throw mcrl2::runtime_error("solve_with_counter_example requires a PBES without global variables.");
481 : }
482 :
483 : mCRL2log(log::verbose) << "Solving parity game..." << std::endl;
484 : vertex_set Wconj;
485 : vertex_set Wdisj;
486 : std::tie(Wdisj, Wconj) = solve_recursive_extended(G);
487 : structure_graph::index_type init = G.initial_vertex();
488 :
489 : mCRL2log(log::verbose) << "Extracting evidence..." << std::endl;
490 : std::set<structure_graph::index_type> W = extract_minimal_structure_graph(G, init, Wdisj, Wconj);
491 : return { Wdisj.contains(init), create_counter_example_lps(G, W, lpsspec, p, p_index) };
492 : }
493 : };
494 :
495 : class lts_solve_structure_graph_algorithm: public solve_structure_graph_algorithm
496 : {
497 : protected:
498 : // Removes all transitions from ltsspec, except the ones in transition_indices.
499 : // After that, the unreachable parts of the LTS are removed.
500 : static inline
501 : void filter_transitions(lts::lts_lts_t& ltsspec, const std::set<std::size_t>& transition_indices)
502 : {
503 : // remove transitions
504 : const auto& lts_transitions = ltsspec.get_transitions();
505 : std::vector<lts::transition> transitions;
506 : for (std::size_t i: transition_indices)
507 : {
508 : if (i >= lts_transitions.size())
509 : {
510 : throw mcrl2::runtime_error("Counter-example cannot be reconstructed from this LTS. Did you supply the correct file?");
511 : }
512 : transitions.push_back(lts_transitions[i]);
513 : }
514 : ltsspec.get_transitions() = transitions;
515 :
516 : // remove unreachable states
517 : lts::reachability_check(ltsspec, true);
518 : }
519 :
520 : // modifies ltsspec
521 : static inline
522 : void create_counter_example_lts(structure_graph& G, const std::set<structure_graph::index_type>& V, lts::lts_lts_t& ltsspec)
523 : {
524 : std::regex re("Z(neg|pos)_(\\d+)_.*");
525 :
526 : std::set<std::size_t> transition_indices;
527 : for (structure_graph::index_type vi: V)
528 : {
529 : const auto& v = G.find_vertex(vi);
530 : if (is_propositional_variable_instantiation(v.formula()))
531 : {
532 : const propositional_variable_instantiation& Z = atermpp::down_cast<propositional_variable_instantiation>(v.formula());
533 : std::string Zname = Z.name();
534 : std::smatch match;
535 : if (std::regex_match(Zname, match, re))
536 : {
537 : std::size_t transition_index = std::stoul(match[2]);
538 : transition_indices.insert(transition_index);
539 : }
540 : }
541 : }
542 : filter_transitions(ltsspec, transition_indices);
543 : }
544 :
545 : public:
546 : lts_solve_structure_graph_algorithm() = default;
547 :
548 : /// \brief Solve a boolean equation system while generating a counter example.
549 : /// \param G A structure graph.
550 : /// \param ltsspec The original LTS that was used to create the PBES.
551 : inline
552 : bool solve_with_counter_example(structure_graph& G, lts::lts_lts_t& ltsspec)
553 : {
554 : mCRL2log(log::verbose) << "Solving parity game..." << std::endl;
555 : vertex_set Wconj;
556 : vertex_set Wdisj;
557 : std::tie(Wdisj, Wconj) = solve_recursive_extended(G);
558 : structure_graph::index_type init = G.initial_vertex();
559 :
560 : mCRL2log(log::verbose) << "Extracting evidence..." << std::endl;
561 : std::set<structure_graph::index_type> W = extract_minimal_structure_graph(G, init, Wdisj, Wconj);
562 : create_counter_example_lts(G, W, ltsspec);
563 : return Wdisj.contains(init);
564 : }
565 : };
566 :
567 : inline
568 133 : bool solve_structure_graph(structure_graph& G, bool check_strategy = false)
569 : {
570 133 : bool use_toms_optimization = !check_strategy;
571 133 : solve_structure_graph_algorithm algorithm(check_strategy, use_toms_optimization);
572 266 : return algorithm.solve(G);
573 : }
574 :
575 : inline
576 : std::pair<bool, lps::specification> solve_structure_graph_with_counter_example(structure_graph& G, const lps::specification& lpsspec, const pbes& p, const pbes_equation_index& p_index)
577 : {
578 : lps_solve_structure_graph_algorithm algorithm;
579 : return algorithm.solve_with_counter_example(G, lpsspec, p, p_index);
580 : }
581 :
582 : /// \brief Solve this pbes_system using a structure graph generating a counter example.
583 : /// \param G The structure graph.
584 : /// \param ltsspec The original LTS that was used to create the PBES.
585 : inline
586 : bool solve_structure_graph_with_counter_example(structure_graph& G, lts::lts_lts_t& ltsspec)
587 : {
588 : lts_solve_structure_graph_algorithm algorithm;
589 : return algorithm.solve_with_counter_example(G, ltsspec);
590 : }
591 :
592 : } // namespace pbes_system
593 :
594 : } // namespace mcrl2
595 :
596 : #endif // MCRL2_PBES_SOLVE_STRUCTURE_GRAPH_H
|
