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/detail/stategraph_graph.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_STATEGRAPH_GRAPH_H
13 : #define MCRL2_PBES_DETAIL_STATEGRAPH_GRAPH_H
14 :
15 : #include "mcrl2/data/detail/print_utility.h"
16 : #include "mcrl2/pbes/detail/stategraph_pbes.h"
17 :
18 : namespace mcrl2 {
19 :
20 : namespace pbes_system {
21 :
22 : namespace detail {
23 :
24 : // Vertex in the graph of LCFP parameters
25 : class LCFP_vertex
26 : {
27 : protected:
28 : core::identifier_string m_name;
29 : std::size_t m_index;
30 : data::variable m_variable;
31 :
32 : public:
33 78 : LCFP_vertex(const core::identifier_string& name, std::size_t index = data::undefined_index(), const data::variable& variable = data::undefined_variable())
34 78 : : m_name(name), m_index(index), m_variable(variable)
35 78 : {}
36 :
37 1401 : const core::identifier_string& name() const
38 : {
39 1401 : return m_name;
40 : }
41 :
42 719 : std::size_t index() const
43 : {
44 719 : return m_index;
45 : }
46 :
47 118 : const data::variable& variable() const
48 : {
49 118 : return m_variable;
50 : }
51 :
52 106 : bool has_variable() const
53 : {
54 106 : return m_index != data::undefined_index();
55 : }
56 : };
57 :
58 : inline
59 52 : std::ostream& operator<<(std::ostream& out, const LCFP_vertex& u)
60 : {
61 52 : out << '(' << u.name() << ", ";
62 52 : if (u.index() == data::undefined_index())
63 : {
64 0 : out << "?";
65 : }
66 : else
67 : {
68 52 : out << u.index();
69 : }
70 52 : out << ", ";
71 52 : if (u.variable() == data::undefined_variable())
72 : {
73 0 : out << "?";
74 : }
75 : else
76 : {
77 52 : out << u.variable();
78 : }
79 52 : return out << ')';
80 : }
81 :
82 : // Vertex in the graph of GCFP parameters
83 : class GCFP_vertex: public LCFP_vertex
84 : {
85 : protected:
86 : std::set<GCFP_vertex*> m_neighbors;
87 :
88 : public:
89 65 : GCFP_vertex(const core::identifier_string& name, std::size_t index, const data::variable& variable)
90 65 : : LCFP_vertex(name, index, variable)
91 65 : {}
92 :
93 65 : const std::set<GCFP_vertex*>& neighbors() const
94 : {
95 65 : return m_neighbors;
96 : }
97 :
98 96 : std::set<GCFP_vertex*>& neighbors()
99 : {
100 96 : return m_neighbors;
101 : }
102 : };
103 :
104 : class GCFP_graph;
105 : std::ostream& operator<<(std::ostream& out, const GCFP_graph& G);
106 :
107 : class GCFP_graph
108 : {
109 : protected:
110 : std::vector<GCFP_vertex> m_vertices;
111 :
112 : public:
113 58 : const std::vector<GCFP_vertex>& vertices() const
114 : {
115 58 : return m_vertices;
116 : }
117 :
118 651 : const GCFP_vertex& vertex(std::size_t i) const
119 : {
120 651 : return m_vertices[i];
121 : }
122 :
123 65 : void add_vertex(const GCFP_vertex& u)
124 : {
125 65 : m_vertices.push_back(u);
126 65 : }
127 :
128 96 : GCFP_vertex& find_vertex(const core::identifier_string& X, std::size_t n)
129 : {
130 245 : for (GCFP_vertex& u: m_vertices)
131 : {
132 245 : if (u.name() == X && u.index() == n)
133 : {
134 96 : return u;
135 : }
136 : }
137 0 : std::ostringstream out;
138 0 : out << "vertex (" << X << ", " << n << ") not found in GCFP graph";
139 0 : throw mcrl2::runtime_error(out.str());
140 0 : }
141 :
142 75 : std::size_t index(const GCFP_vertex& u) const
143 : {
144 75 : return &u - &(m_vertices.front());
145 : }
146 : };
147 :
148 : inline
149 0 : std::ostream& operator<<(std::ostream& out, const GCFP_graph& G)
150 : {
151 0 : for (const auto& v: G.vertices())
152 : {
153 0 : out << v << std::endl;
154 : }
155 0 : return out;
156 : }
157 :
158 : // This class is used to add labeled edges to a vertex
159 : template <typename Vertex>
160 : class add_edges
161 : {
162 : protected:
163 : mutable std::map<const Vertex*, std::set<std::size_t> > m_outgoing_edges;
164 : mutable std::map<const Vertex*, std::set<std::size_t> > m_incoming_edges;
165 : // the mapped values are the edge labels; note that there can be multiple edges with different labels
166 :
167 : public:
168 43 : const std::map<const Vertex*, std::set<std::size_t> >& outgoing_edges() const
169 : {
170 43 : return m_outgoing_edges;
171 : }
172 :
173 16 : const std::map<const Vertex*, std::set<std::size_t> >& incoming_edges() const
174 : {
175 16 : return m_incoming_edges;
176 : }
177 :
178 16 : void insert_outgoing_edge(const Vertex* u, std::size_t label) const
179 : {
180 16 : m_outgoing_edges[u].insert(label);
181 16 : }
182 :
183 16 : void insert_incoming_edge(const Vertex* u, std::size_t label) const
184 : {
185 16 : m_incoming_edges[u].insert(label);
186 16 : }
187 :
188 0 : std::string print_outgoing_edges() const
189 : {
190 0 : std::ostringstream out;
191 0 : for (auto i = m_outgoing_edges.begin(); i != m_outgoing_edges.end(); ++i)
192 : {
193 0 : if (i != m_outgoing_edges.begin())
194 : {
195 0 : out << "; ";
196 : }
197 0 : out << *i->first << " (labels = " << core::detail::print_set(i->second) << ")";
198 : }
199 0 : return out.str();
200 0 : }
201 :
202 12 : void remove_edges()
203 : {
204 12 : m_outgoing_edges.clear();
205 12 : m_incoming_edges.clear();
206 12 : }
207 : };
208 :
209 : // Vertex in a local control flow graph.
210 : class local_control_flow_graph_vertex: public LCFP_vertex, public add_edges<local_control_flow_graph_vertex>
211 : {
212 : protected:
213 : typedef add_edges<local_control_flow_graph_vertex> super;
214 :
215 : data::data_expression m_value;
216 : mutable std::set<data::variable> m_marking; // used in the reset variables procedure
217 :
218 : // (i, l) is mapped to FV(rewr(e[l], [d_X[n] := z])) intersect {d | (X, d) in B},
219 : // where Y(e) = PVI(phi_X, i), d_X[n] = variable(), z = value(), and B is the belongs relation
220 : // corresponding to the graph of this vertex
221 : mutable std::map<std::pair<std::size_t, data::variable>, std::set<data::variable> > m_marking_update;
222 :
223 : public:
224 : using super::incoming_edges;
225 : using super::outgoing_edges;
226 : using super::print_outgoing_edges;
227 : using super::insert_outgoing_edge;
228 : using super::insert_incoming_edge;
229 : using super::remove_edges;
230 :
231 10 : local_control_flow_graph_vertex(const core::identifier_string& name, std::size_t index, const data::variable& variable, const data::data_expression& value)
232 10 : : LCFP_vertex(name, index, variable), m_value(value)
233 10 : {}
234 :
235 3 : local_control_flow_graph_vertex(const core::identifier_string& name, const data::data_expression& value)
236 3 : : LCFP_vertex(name), m_value(value)
237 3 : {}
238 :
239 116 : const data::data_expression& value() const
240 : {
241 116 : return m_value;
242 : }
243 :
244 57 : const std::set<data::variable>& marking() const
245 : {
246 57 : return m_marking;
247 : }
248 :
249 6 : void set_marking(const std::set<data::variable>& marking) const
250 : {
251 6 : m_marking = marking;
252 6 : }
253 :
254 6 : void extend_marking(const std::set<data::variable>& marking) const
255 : {
256 6 : m_marking.insert(marking.begin(), marking.end());
257 6 : }
258 :
259 9 : bool operator==(const local_control_flow_graph_vertex& other) const
260 : {
261 9 : return m_name == other.m_name && m_index == other.m_index && m_value == other.m_value;
262 : }
263 :
264 0 : std::string print_marking() const
265 : {
266 0 : std::ostringstream out;
267 0 : out << "vertex " << *this << " marking = " << core::detail::print_set(m_marking);
268 0 : return out.str();
269 0 : }
270 :
271 0 : void set_marking_update(std::size_t i, const data::variable& d, const std::set<data::variable>& V) const
272 : {
273 0 : std::pair<std::size_t, data::variable> p(i, d);
274 0 : m_marking_update[p] = V;
275 0 : }
276 :
277 0 : const std::map<std::pair<std::size_t, data::variable>, std::set<data::variable> >& marking_update() const
278 : {
279 0 : return m_marking_update;
280 : }
281 : };
282 :
283 : inline
284 0 : std::ostream& operator<<(std::ostream& out, const local_control_flow_graph_vertex& u)
285 : {
286 0 : if (u.index() == data::undefined_index())
287 : {
288 0 : return out << '(' << u.name() << ", ?, ?=?)";
289 : assert(u.value() == data::undefined_data_expression());
290 : }
291 0 : return out << '(' << u.name() << ", " << u.index() << ", " << data::pp(u.variable()) << "=" << data::pp(u.value()) << ')';
292 : }
293 :
294 : inline
295 97 : bool operator<(const local_control_flow_graph_vertex& u, const local_control_flow_graph_vertex& v)
296 : {
297 97 : if (u.name() != v.name())
298 : {
299 45 : return u.name() < v.name();
300 : }
301 52 : if (u.index() != v.index())
302 : {
303 0 : return u.index() < v.index();
304 : }
305 52 : return u.value() < v.value();
306 : }
307 :
308 : template <typename Vertex>
309 : struct control_flow_graph
310 : {
311 : std::set<Vertex> vertices;
312 :
313 : // an index for the vertices in the control flow graph with a given name
314 : std::map<core::identifier_string, std::set<const Vertex*> > m_graph_index;
315 :
316 26 : const Vertex& find_vertex(const Vertex& u) const
317 : {
318 26 : auto i = vertices.find(u);
319 26 : if (i == vertices.end())
320 : {
321 0 : std::cout << "could not find vertex " << u << " in the graph\n" << *this << std::endl;
322 0 : throw mcrl2::runtime_error("control_flow_graph::find_vertex: vertex not found!");
323 : }
324 52 : return *i;
325 : }
326 :
327 9 : void compute_index()
328 : {
329 9 : m_graph_index.clear();
330 :
331 : // create an index for the vertices in the control flow graph with a given name
332 27 : for (auto i = vertices.begin(); i != vertices.end(); ++i)
333 : {
334 18 : const Vertex& u = *i;
335 18 : m_graph_index[u.name()].insert(&u);
336 : }
337 9 : }
338 :
339 0 : std::set<const Vertex*> index(const core::identifier_string& X) const
340 : {
341 0 : auto i = m_graph_index.find(X);
342 0 : if (i == m_graph_index.end())
343 : {
344 0 : return std::set<const Vertex*>();
345 : }
346 : else
347 : {
348 0 : return i->second;
349 : }
350 : }
351 :
352 : bool has_vertex(const core::identifier_string& X, std::size_t p) const
353 : {
354 : for (auto i = vertices.begin(); i != vertices.end(); ++i)
355 : {
356 : if (i->name() == X && i->index() == p)
357 : {
358 : return true;
359 : }
360 : }
361 : return false;
362 : }
363 :
364 : /// \brief Default constructor
365 3 : control_flow_graph() = default;
366 :
367 : /// \brief Copy constructor N.B. The implementation is rather inefficient!
368 6 : control_flow_graph(const control_flow_graph<Vertex>& other)
369 6 : {
370 : // copy the vertices, but not the neighbors
371 18 : for (auto i = other.vertices.begin(); i != other.vertices.end(); ++i)
372 : {
373 12 : auto u = *i;
374 12 : u.remove_edges();
375 12 : vertices.insert(u);
376 : }
377 :
378 : // reconstruct the incoming and outgoing edges
379 18 : for (auto i = other.vertices.begin(); i != other.vertices.end(); ++i)
380 : {
381 12 : const Vertex& u = find_vertex(*i);
382 12 : auto const& outgoing_edges = i->outgoing_edges();
383 23 : for (auto j = outgoing_edges.begin(); j != outgoing_edges.end(); ++j)
384 : {
385 11 : const Vertex& v = find_vertex(*(j->first));
386 11 : std::set<std::size_t> labels = j->second;
387 22 : for (std::size_t label: labels)
388 : {
389 11 : u.insert_outgoing_edge(&v, label);
390 11 : v.insert_incoming_edge(&u, label);
391 : }
392 : }
393 : }
394 6 : compute_index();
395 6 : }
396 :
397 : // throws a runtime_error if an error is found in the internal representation
398 : void self_check() const
399 : {
400 : // check if all targets of outgoing edges are part of the graph
401 : for (auto i = vertices.begin(); i != vertices.end(); ++i)
402 : {
403 : auto const& outgoing_edges = i->outgoing_edges();
404 : for (auto j = outgoing_edges.begin(); j != outgoing_edges.end(); ++j)
405 : {
406 : const Vertex& v = *(j->first);
407 : find_vertex(v);
408 : }
409 :
410 : auto const& incoming_edges = i->incoming_edges();
411 : for (auto j = incoming_edges.begin(); j != incoming_edges.end(); ++j)
412 : {
413 : const Vertex& v = *(j->first);
414 : find_vertex(v);
415 : }
416 : }
417 :
418 : // check if no two vertices (X, i, v) and (X, i', v') are in the graph with i != i'
419 : std::map<core::identifier_string, std::set<std::size_t> > m;
420 : for (auto i = vertices.begin(); i != vertices.end(); ++i)
421 : {
422 : auto& m_i = m[i->name()];
423 : m_i.insert(i->index());
424 : if (m_i.size() > 1)
425 : {
426 : auto const& X = i->name();
427 : std::ostringstream out;
428 : out << "Illegal state in control flow graph::vertices";
429 : for (auto k = m_i.begin(); k != m_i.end(); ++k)
430 : {
431 : out << " (" << X << ", " << *k << ")";
432 : }
433 : out << " encountered";
434 : throw mcrl2::runtime_error(out.str());
435 : }
436 : }
437 : }
438 :
439 3 : std::pair<typename std::set<Vertex>::iterator, bool> insert(const Vertex& u)
440 : {
441 3 : auto result = vertices.insert(u);
442 : // self_check();
443 3 : return result;
444 : }
445 :
446 7 : const Vertex& insert_vertex(const Vertex& v_)
447 : {
448 7 : auto j = std::find(vertices.begin(), vertices.end(), v_);
449 7 : if (j == vertices.end())
450 : {
451 3 : mCRL2log(log::trace) << " add vertex v = " << v_ << std::endl;
452 3 : auto k = vertices.insert(v_);
453 3 : j = k.first;
454 : }
455 14 : return *j;
456 : }
457 :
458 5 : void insert_edge(const Vertex& u,
459 : std::size_t i,
460 : const Vertex& v
461 : )
462 : {
463 : // add edge (u, v)
464 5 : auto q = u.outgoing_edges().find(&v);
465 5 : if (u.outgoing_edges().find(&v) == u.outgoing_edges().end() || q->second.find(i) == q->second.end())
466 : {
467 5 : mCRL2log(log::trace) << " add edge " << u << " -> " << v << std::endl;
468 5 : u.insert_outgoing_edge(&v, i);
469 5 : v.insert_incoming_edge(&u, i);
470 : }
471 : else
472 : {
473 0 : mCRL2log(log::trace) << " edge already exists!" << std::endl;
474 : }
475 5 : }
476 :
477 : // Returns true if there is an edge X(e) -- label --> Y(f) in the graph, for some e, f, Y.
478 15 : bool has_label(const core::identifier_string& X, std::size_t label) const
479 : {
480 29 : for (auto i = vertices.begin(); i != vertices.end(); ++i)
481 : {
482 23 : if (i->name() != X)
483 : {
484 8 : continue;
485 : }
486 15 : auto const& outgoing_edges = i->outgoing_edges();
487 20 : for (auto j = outgoing_edges.begin(); j != outgoing_edges.end(); ++j)
488 : {
489 14 : if (j->second.find(label) != j->second.end())
490 : {
491 9 : return true;
492 : }
493 : }
494 : }
495 6 : return false;
496 : }
497 :
498 0 : typename std::set<Vertex>::const_iterator begin() const
499 : {
500 0 : return vertices.begin();
501 : }
502 :
503 0 : typename std::set<Vertex>::const_iterator end() const
504 : {
505 0 : return vertices.end();
506 : }
507 : };
508 :
509 : template <typename Vertex>
510 0 : std::ostream& operator<<(std::ostream& out, const control_flow_graph<Vertex>& G)
511 : {
512 0 : for (auto i = G.vertices.begin(); i != G.vertices.end(); ++i)
513 : {
514 0 : out << *i << " outgoing_edges: " << i->print_outgoing_edges() << std::endl;
515 : }
516 0 : return out;
517 : }
518 :
519 : struct local_control_flow_graph: public control_flow_graph<local_control_flow_graph_vertex>
520 : {
521 : typedef control_flow_graph<local_control_flow_graph_vertex> super;
522 :
523 : using super::find_vertex;
524 : using super::has_label;
525 : using super::insert_edge;
526 : using super::insert_vertex;
527 :
528 : /// \brief Default constructor
529 3 : local_control_flow_graph() = default;
530 :
531 : /// \brief Copy constructor N.B. The implementation is rather inefficient!
532 6 : local_control_flow_graph(const local_control_flow_graph& other) = default;
533 :
534 : // Inserts an edge between the vertex u and the vertex v = (Y, k1, e1).
535 4 : void insert_edge(std::set<const local_control_flow_graph_vertex*>& todo,
536 : const stategraph_pbes& p,
537 : const local_control_flow_graph_vertex& u,
538 : const core::identifier_string& Y,
539 : std::size_t k1,
540 : const data::data_expression& e1,
541 : std::size_t edge_label
542 : )
543 : {
544 4 : mCRL2log(log::trace) << " insert_edge" << std::endl;
545 4 : const stategraph_equation& eq_Y = *find_equation(p, Y);
546 4 : const data::variable& d1 = (k1 == data::undefined_index() ? data::undefined_variable() : eq_Y.parameters()[k1]);
547 :
548 4 : std::size_t size = vertices.size();
549 4 : const local_control_flow_graph_vertex& v = insert_vertex(local_control_flow_graph_vertex(Y, k1, d1, e1));
550 4 : if (vertices.size() != size)
551 : {
552 1 : todo.insert(&v);
553 : }
554 :
555 4 : mCRL2log(log::trace) << " u.outgoing_edges() = " << u.print_outgoing_edges() << std::endl;
556 4 : insert_edge(u, edge_label, v);
557 : // self_check();
558 4 : }
559 :
560 0 : std::string print_marking() const
561 : {
562 0 : std::ostringstream out;
563 0 : for (const auto& v: vertices)
564 : {
565 0 : out << v.print_marking() << std::endl;
566 : }
567 0 : return out.str();
568 0 : }
569 :
570 : // finds the vertex with given name and index
571 : const local_control_flow_graph_vertex& find_vertex(const core::identifier_string& X, std::size_t p) const
572 : {
573 : for (const auto& v: vertices)
574 : {
575 : if (v.name() == X && v.index() == p)
576 : {
577 : return v;
578 : }
579 : }
580 : throw mcrl2::runtime_error("stategraph_global_graph::find_vertex: vertex not found!");
581 : }
582 :
583 : // finds the vertex with given name
584 5 : const local_control_flow_graph_vertex& find_vertex(const core::identifier_string& X) const
585 : {
586 9 : for (const auto& v: vertices)
587 : {
588 9 : if (v.name() == X)
589 : {
590 5 : return v;
591 : }
592 : }
593 0 : throw mcrl2::runtime_error("stategraph_global_graph::find_vertex: vertex not found!");
594 : }
595 : };
596 :
597 : class global_control_flow_graph_vertex;
598 : std::ostream& operator<<(std::ostream& out, const global_control_flow_graph_vertex&);
599 :
600 : // Vertex in the global control flow graph.
601 : class global_control_flow_graph_vertex: public add_edges<global_control_flow_graph_vertex>
602 : {
603 : protected:
604 : typedef add_edges<global_control_flow_graph_vertex> super;
605 : core::identifier_string m_name;
606 : data::data_expression_list m_values;
607 : mutable std::set<data::variable> m_sig;
608 : mutable std::set<data::variable> m_marking; // used in the reset variables procedure
609 : mutable std::vector<bool> m_marked_parameters; // will be set after computing the marking
610 :
611 : public:
612 : using super::incoming_edges;
613 : using super::outgoing_edges;
614 : using super::print_outgoing_edges;
615 : using super::insert_outgoing_edge;
616 : using super::insert_incoming_edge;
617 : using super::remove_edges;
618 :
619 0 : global_control_flow_graph_vertex(const core::identifier_string& name, const data::data_expression_list& values)
620 0 : : m_name(name), m_values(values)
621 0 : {}
622 :
623 0 : const core::identifier_string& name() const
624 : {
625 0 : return m_name;
626 : }
627 :
628 0 : const data::data_expression_list& values() const
629 : {
630 0 : return m_values;
631 : }
632 :
633 0 : void set_marking(const std::set<data::variable>& marking) const
634 : {
635 0 : m_marking = marking;
636 0 : }
637 :
638 : void extend_marking(const std::set<data::variable>& marking) const
639 : {
640 : m_marking.insert(marking.begin(), marking.end());
641 : }
642 :
643 0 : void set_significant_variables(const std::set<data::variable>& sig) const
644 : {
645 0 : m_sig = sig;
646 0 : }
647 :
648 0 : bool operator==(const global_control_flow_graph_vertex& other) const
649 : {
650 0 : return m_name == other.m_name && m_values == other.m_values;
651 : }
652 :
653 : std::string print() const
654 : {
655 : return print_outgoing_edges();
656 : // std::ostringstream out;
657 : // out << pbes_system::pp(X);
658 : // out << " edges:";
659 : // for (auto i = outgoing_edges.begin(); i != outgoing_edges.end(); ++i)
660 : // {
661 : // out << " " << pbes_system::pp(i->target->X);
662 : // }
663 : // out << " sig: " << core::detail::print_set(sig);
664 : // return out.str();
665 : }
666 :
667 : // also print the parameters
668 : std::string print(const data::variable_list&) const
669 : {
670 : return print_outgoing_edges();
671 : // std::ostringstream out;
672 : // out << core::pp(X.name());
673 : // out << "(";
674 : // out << data::pp(data::make_assignment_list(d_X, X.parameters()));
675 : // out << ")";
676 : // out << " edges:";
677 : // for (auto i = outgoing_edges.begin(); i != outgoing_edges.end(); ++i)
678 : // {
679 : // out << " " << i->print();
680 : // }
681 : // out << " sig: " << core::detail::print_set(sig);
682 : // return out.str();
683 : }
684 :
685 0 : std::set<std::size_t> marking_variable_indices(const stategraph_pbes& p) const
686 : {
687 0 : std::set<std::size_t> result;
688 0 : for (const data::variable& v: marking())
689 : {
690 : // TODO: make this code more efficient
691 0 : const stategraph_equation& eqn = *find_equation(p, m_name);
692 0 : const std::vector<data::variable>& d = eqn.parameters();
693 0 : for (auto j = d.begin(); j != d.end(); ++j)
694 : {
695 0 : if (v == *j)
696 : {
697 0 : result.insert(j - d.begin());
698 0 : break;
699 : }
700 : }
701 : }
702 0 : return result;
703 0 : }
704 :
705 : // returns true if the i-th parameter of X is marked
706 0 : bool is_marked_parameter(std::size_t i) const
707 : {
708 0 : return m_marked_parameters[i];
709 : }
710 :
711 0 : void add_marked_parameter(bool b) const
712 : {
713 0 : m_marked_parameters.push_back(b);
714 0 : }
715 :
716 0 : std::string print_marking() const
717 : {
718 0 : std::ostringstream out;
719 0 : out << "vertex " << *this << " = " << core::detail::print_set(m_marking);
720 0 : return out.str();
721 0 : }
722 :
723 0 : const std::set<data::variable>& sig() const
724 : {
725 0 : return m_sig;
726 : }
727 :
728 0 : const std::set<data::variable>& marking() const
729 : {
730 0 : return m_marking;
731 : }
732 :
733 0 : const std::vector<bool>& marked_parameters() const
734 : {
735 0 : return m_marked_parameters;
736 : }
737 : };
738 :
739 : inline
740 0 : bool operator<(const global_control_flow_graph_vertex& x, const global_control_flow_graph_vertex& y)
741 : {
742 0 : return x.name() < y.name() || (x.name() == y.name() && x.values() < y.values());
743 : }
744 :
745 0 : std::ostream& operator<<(std::ostream& out, const global_control_flow_graph_vertex& u)
746 : {
747 0 : return out << u.name() << core::detail::print_container(u.values(), "(", ")", "", false, false);
748 : }
749 :
750 : struct global_control_flow_graph: public control_flow_graph<global_control_flow_graph_vertex>
751 : {
752 : typedef control_flow_graph<global_control_flow_graph_vertex> super;
753 : typedef global_control_flow_graph_vertex vertex_type;
754 :
755 : /// \brief Default constructor
756 0 : global_control_flow_graph() = default;
757 :
758 : /// \brief Copy constructor N.B. The implementation is rather inefficient!
759 : global_control_flow_graph(const global_control_flow_graph& other) = default;
760 :
761 0 : std::string print_marking() const
762 : {
763 0 : std::ostringstream out;
764 0 : for (const auto& v: vertices)
765 : {
766 0 : out << v.print_marking() << std::endl;
767 : }
768 0 : return out.str();
769 0 : }
770 : };
771 :
772 : } // namespace detail
773 :
774 : } // namespace pbes_system
775 :
776 : } // namespace mcrl2
777 :
778 : #endif // MCRL2_PBES_DETAIL_STATEGRAPH_GRAPH_H
|
