mCRL2
Loading...
Searching...
No Matches
pbesinst_structure_graph2.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_PBES_PBESINST_STRUCTURE_GRAPH2_H
13#define MCRL2_PBES_PBESINST_STRUCTURE_GRAPH2_H
14
23
24namespace mcrl2 {
25
26namespace pbes_system {
27
28namespace detail {
29
31{
32 protected:
33 std::size_t m_count = 64;
34
35 public:
36 explicit computation_guard(std::size_t initial_count = 64)
37 : m_count(initial_count)
38 {}
39
40 bool operator()(std::size_t count)
41 {
42 bool result = count >= m_count;
43 while (m_count <= count)
44 {
45 m_count *= 2;
46 }
47 return result;
48 }
49};
50
52{
53 protected:
54 std::size_t count = 0;
55 std::size_t regeneration_period = 100;
56
57 public:
58 bool operator()(std::size_t period)
59 {
61 {
62 count = 0;
63 regeneration_period = period;
64 return true;
65 }
66 return false;
67 }
68};
69
70} // namespace detail
71
74{
75 protected:
76 std::array<vertex_set, 2> S;
77 std::array<strategy_vector, 2> tau;
78 std::array<detail::computation_guard, 2> S_guard;
79
80 atermpp::vector<pbes_expression> b; // to store the result of the Rplus computation
84
85 template<typename T>
86 pbes_expression expr(const T& x) const
87 {
88 return static_cast<const pbes_expression&>(x);
89 }
90
91 struct Rplus_traverser: public pbes_expression_traverser<Rplus_traverser>
92 {
94 using super::enter;
95 using super::leave;
96 using super::apply;
97
99 {
104
108 pbes_expression g0_,
110 )
111 : b(std::move(b_)), f(std::move(f_)), g0(std::move(g0_)), g1(std::move(g1_))
112 {}
113
115 {
116 mark_term(b, todo);
117 mark_term(f, todo);
118 mark_term(g0, todo);
119 mark_term(g1, todo);
120 }
121 };
122
123 std::array<vertex_set, 2>& S;
124
126 // TODO: replace with aterm container
128
129 Rplus_traverser(std::array<vertex_set, 2>& S_, detail::structure_graph_builder& graph_builder_)
130 : S(S_), graph_builder(graph_builder_)
131 {}
132
133 void push(const stack_element& elem)
134 {
135 stack.push_back(elem);
136 }
137
139 {
140 auto result = stack.back();
141 stack.pop_back();
142 return result;
143 }
144
145 // Return the top element of result_stack
147 {
148 return stack.back();
149 }
150
151 // Return the top element of result_stack
152 const stack_element& top() const
153 {
154 return stack.back();
155 }
156
157 // TODO: use a heuristic for the smallest term
158 static bool less(const pbes_expression& /* x1 */, const pbes_expression& /* x2 */)
159 {
160 return true;
161 }
162
164 {
165 if (is_true(x) || is_false(x))
166 {
167 stack.emplace_back(x, x, true_(), false_());
168 }
169 else
170 {
171 throw mcrl2::runtime_error("Fail to evaluate the expression " + pbes_system::pp(x) + " as it should be equal to true or false.");
172 }
173 }
174
176 {
177 auto u = graph_builder.find_vertex(x);
178 if (u == undefined_vertex())
179 {
180 // if x is not yet in the graph, then it certainly isn't in S[0] or S[1]
181 stack.emplace_back(data::undefined_data_expression(), x, true_(), false_());
182 }
183 else if (S[0].contains(u))
184 {
185 stack.emplace_back(true_(), x, x, false_());
186 }
187 else if (S[1].contains(u))
188 {
189 stack.emplace_back(false_(), x, true_(), x);
190 }
191 else
192 {
193 stack.emplace_back(data::undefined_data_expression(), x, true_(), false_());
194 }
195 }
196
197 void leave(const and_& /* x */)
198 {
199 stack_element elem2 = pop();
200 stack_element& elem1 = top();
201 auto& b_1 = elem1.b;
202 auto& f1_prime = elem1.f;
203 auto& g0_1 = elem1.g0;
204 auto& g1_1 = elem1.g1;
205 auto& b_2 = elem2.b;
206 auto& f2_prime = elem2.f;
207 auto& g0_2 = elem2.g0;
208 auto& g1_2 = elem2.g1;
209
210 // put the result in (b1, f1_prime, g0, g1)
211 if (is_true(b_1) && is_true(b_2))
212 {
213 b_1 = true_();
214 f1_prime = and_(f1_prime, f2_prime);
215 g0_1 = and_(g0_1, g0_2);
216 g1_1 = false_();
217 }
218 else if (is_false(b_1) && !is_false(b_2))
219 {
220 b_1 = false_();
221 // f1_prime = f1_prime;
222 g0_1 = true_();
223 // g1_1 = g1_1;
224 }
225 else if (!is_false(b_1) && is_false(b_2))
226 {
227 b_1 = false_();
228 f1_prime = f2_prime;
229 g0_1 = true_();
230 g1_1 = g1_2;
231 }
232 else if (is_false(b_1) && is_false(b_2))
233 {
234 if (less(f1_prime, f2_prime))
235 {
236 b_1 = false_();
237 // f1_prime = f1_prime;
238 g0_1 = true_();
239 // g1_1 = g1_1;
240 }
241 else
242 {
243 b_1 = false_();
244 f1_prime = f2_prime;
245 g0_1 = true_();
246 g1_1 = g1_2;
247 }
248 }
249 else // if (b1 == data::undefined_data_expression() && b2 == data::undefined_data_expression())
250 {
252 f1_prime = and_(f1_prime, f2_prime);
253 g0_1 = true_();
254 g1_1 = false_();
255 }
256 }
257
258 void leave(const or_& /* x */)
259 {
260 stack_element elem2 = pop();
261 stack_element& elem1 = top();
262 auto& b_1 = elem1.b;
263 auto& f1_prime = elem1.f;
264 auto& g0_1 = elem1.g0;
265 auto& g1_1 = elem1.g1;
266 auto& b_2 = elem2.b;
267 auto& f2_prime = elem2.f;
268 auto& g0_2 = elem2.g0;
269 auto& g1_2 = elem2.g1;
270
271 // put the result in (b1, f1_prime, g0, g1)
272 if (is_false(b_1) && is_false(b_2))
273 {
274 b_1 = false_();
275 f1_prime = or_(f1_prime, f2_prime);
276 g0_1 = true_();
277 g1_1 = or_(g1_1, g1_2);
278 }
279 else if (is_true(b_1) && !is_true(b_2))
280 {
281 b_1 = true_();
282 // f1_prime = f1_prime;
283 // g0_1 = g0_1;
284 g1_1 = false_();
285 }
286 else if (!is_true(b_1) && is_true(b_2))
287 {
288 b_1 = true_();
289 f1_prime = f2_prime;
290 g0_1 = g0_2;
291 g1_1 = false_();
292 }
293 else if (is_true(b_1) && is_true(b_2))
294 {
295 if (less(f1_prime, f2_prime))
296 {
297 b_1 = true_();
298 // f1_prime = f1_prime;
299 // g0_1 = g0_1;
300 g1_1 = false_();
301 }
302 else
303 {
304 b_1 = true_();
305 f1_prime = f2_prime;
306 g0_1 = g0_2;
307 g1_1 = false_();
308 }
309 }
310 else // if (b1 == data::undefined_data_expression() && b2 == data::undefined_data_expression())
311 {
313 f1_prime = or_(f1_prime, f2_prime);
314 g0_1 = true_();
315 g1_1 = false_();
316 }
317 }
318
319 void enter(const imp& x)
320 {
321 throw mcrl2::runtime_error("Fail to evaluate the expression " + pbes_system::pp(x) + " as the routine Rplus does not expect an implication, which is an internal error.");
322 }
323
324 void leave(const imp& x)
325 {
326 enter(x); // Print an error message, although this should never be reached..
327 }
328
329 void enter(const exists& x)
330 {
331 throw mcrl2::runtime_error("Fail to evaluate the expression " + pbes_system::pp(x) + " as enumeration of this exists is not possible.");
332 }
333
334 void leave(const exists& x)
335 {
336 enter(x); // Print an error message.
337 }
338
339 void enter(const forall& x)
340 {
341 throw mcrl2::runtime_error("Fail to evaluate the expression " + pbes_system::pp(x) + " as enumeration of this forall is not possible.");
342 }
343
344 void leave(const forall& x)
345 {
346 enter(x); // Print an error.
347 }
348 };
349
351 {
353 f.apply(x);
354 return f.top();
355 }
356
358 {
360 return S[0].contains(u) || S[1].contains(u);
361 }
362
363 // Returns true if all nodes in the todo list are undefined (i.e. have not been processed yet)
365 {
366 /* for (const propositional_variable_instantiation& X: todo.all_elements()) all_elements does not seem to work. Therefore split below.
367 {
368 structure_graph::index_type u = m_graph_builder.find_vertex(X);
369 const structure_graph::vertex& u_ = m_graph_builder.vertex(u);
370 if (u_.is_defined())
371 {
372 return false;
373 }
374 } */
376 {
379 if (u_.is_defined())
380 {
381 return false;
382 }
383 }
385 {
388 if (u_.is_defined())
389 {
390 return false;
391 }
392 }
393 return true;
394 }
395
399 std::size_t regeneration_period
400 )
401 {
403
404 if (!reset_guard(regeneration_period) && !m_options.aggressive && !todo.elements().empty())
405 {
406 return;
407 }
408
413
415 while (!todo1.empty())
416 {
418
419 X = todo1.front();
420 todo1.pop_front();
421 done1.insert(X);
422 auto u = m_graph_builder.find_vertex(X);
423 const auto& u_ = m_graph_builder.vertex(u);
424
425 if (u_.decoration == structure_graph::d_none && u_.successors.empty())
426 {
427 assert(is_propositional_variable_instantiation(u_.formula()));
428 new_todo.insert(atermpp::down_cast<propositional_variable_instantiation>(u_.formula()));
429 }
430 else
431 {
432 if (!S[0].contains(u) && !S[1].contains(u))
433 {
434 // todo' := todo' U (succ(u) \ done')
435 for (auto v: G.successors(u))
436 {
437 const auto& v_ = m_graph_builder.vertex(v);
438 const auto& Y = v_.formula();
439 if (contains(done1, Y))
440 {
441 continue;
442 }
443 todo1.push_back(Y);
444 }
445 }
446 }
447 }
448
449 // new_todo_list := new_todo \cap (todo U irrelevant)
450 // N.B. An attempt is made to preserve the order of the current todo list, to not
451 // disturb breadth first and depth first search.
454 {
455 if (contains(new_todo, X))
456 {
457 new_todo_list.push_back(X);
458 }
459 }
461 {
462 if (contains(new_todo, X))
463 {
464 new_todo_list.push_back(X);
465 }
466 }
467 todo.set_todo(new_todo_list);
469 };
470
472 {
474 for (structure_graph::index_type u: S[0].vertices())
475 {
476 // if (G.decoration(u) == structure_graph::d_disjunction && G.strategy(u) == undefined_vertex())
478 {
479 mCRL2log(log::debug) << "Error: no strategy has been set for disjunctive node " << u << " in S0." << std::endl;
480 mCRL2log(log::debug) << G << std::endl;
481 mCRL2log(log::debug) << "S0 = " << S[0] << std::endl;
482 mCRL2log(log::debug) << "S1 = " << S[1] << std::endl;
483 return false;
484 }
485 }
486 for (structure_graph::index_type u: S[1].vertices())
487 {
488 // if (G.decoration(u) == structure_graph::d_conjunction && G.strategy(u) == undefined_vertex())
490 {
491 mCRL2log(log::debug) << "Error: no strategy has been set for conjunctive node " << u << " in S1." << std::endl;
492 mCRL2log(log::debug) << G << std::endl;
493 mCRL2log(log::debug) << "S0 = " << S[0] << std::endl;
494 mCRL2log(log::debug) << "S1 = " << S[1] << std::endl;
495 return false;
496 }
497 }
498 return true;
499 }
500
501 public:
503
505 const pbessolve_options& options,
506 const pbes& p,
508 )
509 : pbesinst_structure_graph_algorithm(options, p, G),
510 b(options.number_of_threads+1), find_loops_guard(2), fatal_attractors_guard(2)
511 {}
512
513 // Optimization 2 is implemented by overriding the function rewrite_psi.
514 void rewrite_psi(const std::size_t thread_index,
515 pbes_expression& result,
516 const fixpoint_symbol& symbol,
518 const pbes_expression& psi
519 ) override
520 {
521 super::rewrite_psi(thread_index, result, symbol, X, psi);
522 auto rplus_result = Rplus(result);
523 b[thread_index] = rplus_result.b;
524 if (is_true(rplus_result.b))
525 {
526 result = rplus_result.g0;
527 return;
528 }
529 else if (is_false(rplus_result.b))
530 {
531 result = rplus_result.g1;
532 return;
533 }
534 result = rplus_result.f;
535 }
536
537 void on_report_equation(const std::size_t thread_index,
539 const pbes_expression& psi, std::size_t k
540 ) override
541 {
542 super::on_report_equation(thread_index, X, psi, k);
543
544 // The structure graph has just been extended, so S[0] and S[1] need to be resized.
545 S[0].resize(m_graph_builder.extent());
546 S[1].resize(m_graph_builder.extent());
547
548 auto u = m_graph_builder.find_vertex(X);
549 if (is_true(b[thread_index]))
550 {
551 S[0].insert(u);
552 }
553 else if (is_false(b[thread_index]))
554 {
555 S[1].insert(u);
556 }
557 }
558
559
560 void on_discovered_elements(const std::set<propositional_variable_instantiation>& elements) override
561 {
563 stopwatch timer;
564
565 bool report = false;
566 if (m_options.optimization == 3)
567 {
568 if (S_guard[0](S[0].size()))
569 {
571 S[0] = attr_default_with_tau(G, S[0], 0, tau);
572 }
573 if (S_guard[1](S[1].size()))
574 {
576 S[1] = attr_default_with_tau(G, S[1], 1, tau);
577 }
579 }
581 {
582 mCRL2log(log::verbose) << "start partial solving\n"; report = true;
583
585 detail::find_loops2(G, S, tau, m_iteration_count); // modifies S[0] and S[1]
587
588 }
590 {
591 mCRL2log(log::verbose) << "start partial solving\n"; report = true;
592
594 if (m_options.optimization == 5)
595 {
596 detail::fatal_attractors(G, S, tau, m_iteration_count); // modifies S[0] and S[1]
598 }
599 else if (m_options.optimization == 6)
600 {
601 detail::fatal_attractors_original(G, S, tau, m_iteration_count); // modifies S[0] and S[1]
603 }
604 else if (m_options.optimization == 7)
605 {
609 }
610 }
612 {
613 mCRL2log(log::verbose) << "start partial solving\n"; report = true;
614
616 detail::find_loops(G, discovered, todo, S, tau, m_iteration_count, m_graph_builder); // modifies S[0] and S[1]
618 }
619
620 if (report)
621 {
622 mCRL2log(log::verbose) << "found solution for" << std::setw(12) << S[0].size() + S[1].size() << " BES equations" << std::endl;
623 mCRL2log(log::verbose) << "finished partial solving (time = " << std::setprecision(2) << std::fixed << timer.seconds() << "s)\n";
624 }
625
627 {
628 for (const propositional_variable_instantiation& e: elements)
629 {
630 todo.irrelevant_elements().erase(e);
631 }
632 prune_todo_list(init, todo, (discovered.size() - todo.size()) / 2);
633 }
634 }
635
636 void on_end_while_loop() override
637 {
639
641
644
645 std::set<structure_graph::index_type> V = extract_minimal_structure_graph(G, u, S[0], S[1], tau[0], tau[1]);
646
647 std::size_t n = m_graph_builder.extent();
648 vertex_set to_be_removed(n);
649 for (std::size_t v = 0; v < n; v++)
650 {
651 if (!contains(V, v))
652 {
653 to_be_removed.insert(v);
654 }
655 }
656 m_graph_builder.erase_vertices(to_be_removed);
657 mCRL2log(log::debug) << G << std::endl;
658 }
659};
660
661} // namespace pbes_system
662
663} // namespace mcrl2
664
665#endif // MCRL2_PBES_PBESINST_STRUCTURE_GRAPH2_H
A deque class in which aterms can be stored.
Definition deque.h:34
void push_back(const T &value)
Definition deque.h:183
Base class that should not be used.
A set that assigns each element an unique index, and protects its internal terms en masse.
Definition indexed_set.h:30
std::pair< size_type, bool > insert(const Key &key, std::size_t thread_index=0)
Definition indexed_set.h:63
A vector class in which aterms can be stored.
Definition vector.h:34
\brief The and operator for pbes expressions
\brief The existential quantification operator for pbes expressions
\brief The universal quantification operator for pbes expressions
\brief The implication operator for pbes expressions
\brief The or operator for pbes expressions
parameterized boolean equation system
Definition pbes.h:58
const pbessolve_options & m_options
Algorithm options.
virtual void rewrite_psi(const std::size_t, pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)
pbesinst_lazy_todo todo
The propositional variable instantiations that need to be handled.
propositional_variable_instantiation init
The initial value (after rewriting).
const fixpoint_symbol & symbol(std::size_t i) const
atermpp::indexed_set< propositional_variable_instantiation, true > discovered
The propositional variable instantiations that have been discovered (not necessarily handled).
const atermpp::deque< propositional_variable_instantiation > & elements() const
void set_todo(atermpp::deque< propositional_variable_instantiation > &new_todo)
const std::unordered_set< propositional_variable_instantiation > & irrelevant_elements() const
Adds an optimization to pbesinst_structure_graph.
void on_discovered_elements(const std::set< propositional_variable_instantiation > &elements) override
This function is called when new elements are added to discovered.
void rewrite_psi(const std::size_t thread_index, pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi) override
Rplus_traverser::stack_element Rplus(const pbes_expression &x)
pbesinst_structure_graph_algorithm2(const pbessolve_options &options, const pbes &p, structure_graph &G)
void prune_todo_list(const propositional_variable_instantiation &init, pbesinst_lazy_todo &todo, std::size_t regeneration_period)
bool solution_found(const propositional_variable_instantiation &init) const override
void on_report_equation(const std::size_t thread_index, const propositional_variable_instantiation &X, const pbes_expression &psi, std::size_t k) override
Reports BES equations that are produced by the algorithm. This function is called for every BES equat...
void on_end_while_loop() override
This function is called right after the while loop is finished.
Variant of pbesinst that will compute a structure graph for a PBES. The result will be put in the str...
void on_report_equation(const std::size_t, const propositional_variable_instantiation &X, const pbes_expression &psi, std::size_t k) override
Reports BES equations that are produced by the algorithm. This function is called for every BES equat...
\brief A propositional variable instantiation
const std::vector< index_type > & successors(index_type u) const
decoration_type decoration(index_type u) const
Standard exception class for reporting runtime errors.
Definition exception.h:27
Implements a simple stopwatch that starts on construction.
Definition stopwatch.h:17
double seconds()
Definition stopwatch.h:37
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
std::stack< std::reference_wrapper< detail::_aterm > > term_mark_stack
const data::data_expression & undefined_data_expression()
Returns a data expression that corresponds to 'undefined'.
Definition undefined.h:58
@ verbose
Definition logger.h:37
void fatal_attractors_original(const simple_structure_graph &G, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count)
void partial_solve(structure_graph &G, const pbesinst_lazy_todo &todo, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count, const detail::structure_graph_builder &graph_builder)
void find_loops2(const simple_structure_graph &G, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count)
void find_loops(const simple_structure_graph &G, const Container &discovered, const pbesinst_lazy_todo &todo, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t iteration_count, const detail::structure_graph_builder &graph_builder)
void fatal_attractors(const simple_structure_graph &G, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count)
constexpr unsigned int undefined_vertex()
const pbes_expression & true_()
bool is_false(const pbes_expression &t)
Test for the value false.
std::set< structure_graph::index_type > extract_minimal_structure_graph(StructureGraph &G, typename StructureGraph::index_type init, const vertex_set &S0, const vertex_set &S1)
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
std::string pp(const fixpoint_symbol &x)
Definition pbes.cpp:37
bool is_true(const pbes_expression &t)
Test for the value true.
const pbes_expression & false_()
vertex_set attr_default_with_tau(const StructureGraph &G, vertex_set A, std::size_t alpha, std::array< strategy_vector, 2 > &tau)
bool contains(const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &c, const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &v, const std::size_t thread_index=0)
Definition indexed_set.h:86
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
add your file description here.
add your file description here.
add your file description here.
A variant of the lazy algorithm for instantiating a PBES, that produces a structure_graph.
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:323
index_type find_vertex(const pbes_expression &x) const
stack_element(pbes_expression b_, pbes_expression f_, pbes_expression g0_, pbes_expression g1_)
static bool less(const pbes_expression &, const pbes_expression &)
Rplus_traverser(std::array< vertex_set, 2 > &S_, detail::structure_graph_builder &graph_builder_)
const pbes_expression & formula() const
void insert(structure_graph::index_type u)