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/modal_formula/find.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_FIND_H
13 : #define MCRL2_MODAL_FORMULA_FIND_H
14 :
15 : #include "mcrl2/process/find.h"
16 : #include "mcrl2/modal_formula/add_binding.h"
17 : #include "mcrl2/modal_formula/traverser.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace action_formulas
23 : {
24 :
25 : //--- start generated action_formulas find code ---//
26 : /// \\brief Returns all variables that occur in an object
27 : /// \\param[in] x an object containing variables
28 : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
29 : /// \\return All variables that occur in the term x
30 : template <typename T, typename OutputIterator>
31 0 : void find_all_variables(const T& x, OutputIterator o)
32 : {
33 0 : data::detail::make_find_all_variables_traverser<action_formulas::variable_traverser>(o).apply(x);
34 0 : }
35 :
36 : /// \\brief Returns all variables that occur in an object
37 : /// \\param[in] x an object containing variables
38 : /// \\return All variables that occur in the object x
39 : template <typename T>
40 0 : std::set<data::variable> find_all_variables(const T& x)
41 : {
42 0 : std::set<data::variable> result;
43 0 : action_formulas::find_all_variables(x, std::inserter(result, result.end()));
44 0 : return result;
45 0 : }
46 :
47 : /// \\brief Returns all variables that occur in an object
48 : /// \\param[in] x an object containing variables
49 : /// \\param[in,out] o an output iterator to which all variables occurring in x are added.
50 : /// \\return All free variables that occur in the object x
51 : template <typename T, typename OutputIterator>
52 : void find_free_variables(const T& x, OutputIterator o)
53 : {
54 : data::detail::make_find_free_variables_traverser<action_formulas::data_expression_traverser, action_formulas::add_data_variable_traverser_binding>(o).apply(x);
55 : }
56 :
57 : /// \\brief Returns all variables that occur in an object
58 : /// \\param[in] x an object containing variables
59 : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
60 : /// \\param[in] bound a container of variables
61 : /// \\return All free variables that occur in the object x
62 : template <typename T, typename OutputIterator, typename VariableContainer>
63 : void find_free_variables_with_bound(const T& x, OutputIterator o, const VariableContainer& bound)
64 : {
65 : data::detail::make_find_free_variables_traverser<action_formulas::data_expression_traverser, action_formulas::add_data_variable_traverser_binding>(o, bound).apply(x);
66 : }
67 :
68 : /// \\brief Returns all variables that occur in an object
69 : /// \\param[in] x an object containing variables
70 : /// \\return All free variables that occur in the object x
71 : template <typename T>
72 : std::set<data::variable> find_free_variables(const T& x)
73 : {
74 : std::set<data::variable> result;
75 : action_formulas::find_free_variables(x, std::inserter(result, result.end()));
76 : return result;
77 : }
78 :
79 : /// \\brief Returns all variables that occur in an object
80 : /// \\param[in] x an object containing variables
81 : /// \\param[in] bound a bound a container of variables
82 : /// \\return All free variables that occur in the object x
83 : template <typename T, typename VariableContainer>
84 : std::set<data::variable> find_free_variables_with_bound(const T& x, VariableContainer const& bound)
85 : {
86 : std::set<data::variable> result;
87 : action_formulas::find_free_variables_with_bound(x, std::inserter(result, result.end()), bound);
88 : return result;
89 : }
90 :
91 : /// \\brief Returns all identifiers that occur in an object
92 : /// \\param[in] x an object containing identifiers
93 : /// \\param[in,out] o an output iterator to which all identifiers occurring in x are written.
94 : /// \\return All identifiers that occur in the term x
95 : template <typename T, typename OutputIterator>
96 9 : void find_identifiers(const T& x, OutputIterator o)
97 : {
98 9 : data::detail::make_find_identifiers_traverser<action_formulas::identifier_string_traverser>(o).apply(x);
99 9 : }
100 :
101 : /// \\brief Returns all identifiers that occur in an object
102 : /// \\param[in] x an object containing identifiers
103 : /// \\return All identifiers that occur in the object x
104 : template <typename T>
105 9 : std::set<core::identifier_string> find_identifiers(const T& x)
106 : {
107 9 : std::set<core::identifier_string> result;
108 9 : action_formulas::find_identifiers(x, std::inserter(result, result.end()));
109 9 : return result;
110 0 : }
111 :
112 : /// \\brief Returns all sort expressions that occur in an object
113 : /// \\param[in] x an object containing sort expressions
114 : /// \\param[in,out] o an output iterator to which all sort expressions occurring in x are written.
115 : /// \\return All sort expressions that occur in the term x
116 : template <typename T, typename OutputIterator>
117 : void find_sort_expressions(const T& x, OutputIterator o)
118 : {
119 : data::detail::make_find_sort_expressions_traverser<action_formulas::sort_expression_traverser>(o).apply(x);
120 : }
121 :
122 : /// \\brief Returns all sort expressions that occur in an object
123 : /// \\param[in] x an object containing sort expressions
124 : /// \\return All sort expressions that occur in the object x
125 : template <typename T>
126 : std::set<data::sort_expression> find_sort_expressions(const T& x)
127 : {
128 : std::set<data::sort_expression> result;
129 : action_formulas::find_sort_expressions(x, std::inserter(result, result.end()));
130 : return result;
131 : }
132 :
133 : /// \\brief Returns all function symbols that occur in an object
134 : /// \\param[in] x an object containing function symbols
135 : /// \\param[in,out] o an output iterator to which all function symbols occurring in x are written.
136 : /// \\return All function symbols that occur in the term x
137 : template <typename T, typename OutputIterator>
138 : void find_function_symbols(const T& x, OutputIterator o)
139 : {
140 : data::detail::make_find_function_symbols_traverser<action_formulas::data_expression_traverser>(o).apply(x);
141 : }
142 :
143 : /// \\brief Returns all function symbols that occur in an object
144 : /// \\param[in] x an object containing function symbols
145 : /// \\return All function symbols that occur in the object x
146 : template <typename T>
147 : std::set<data::function_symbol> find_function_symbols(const T& x)
148 : {
149 : std::set<data::function_symbol> result;
150 : action_formulas::find_function_symbols(x, std::inserter(result, result.end()));
151 : return result;
152 : }
153 : //--- end generated action_formulas find code ---//
154 :
155 : } // namespace action_formulas
156 :
157 : namespace regular_formulas
158 : {
159 :
160 : //--- start generated regular_formulas find code ---//
161 : /// \\brief Returns all variables that occur in an object
162 : /// \\param[in] x an object containing variables
163 : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
164 : /// \\return All variables that occur in the term x
165 : template <typename T, typename OutputIterator>
166 : void find_all_variables(const T& x, OutputIterator o)
167 : {
168 : data::detail::make_find_all_variables_traverser<regular_formulas::variable_traverser>(o).apply(x);
169 : }
170 :
171 : /// \\brief Returns all variables that occur in an object
172 : /// \\param[in] x an object containing variables
173 : /// \\return All variables that occur in the object x
174 : template <typename T>
175 : std::set<data::variable> find_all_variables(const T& x)
176 : {
177 : std::set<data::variable> result;
178 : regular_formulas::find_all_variables(x, std::inserter(result, result.end()));
179 : return result;
180 : }
181 :
182 : /// \\brief Returns all variables that occur in an object
183 : /// \\param[in] x an object containing variables
184 : /// \\param[in,out] o an output iterator to which all variables occurring in x are added.
185 : /// \\return All free variables that occur in the object x
186 : template <typename T, typename OutputIterator>
187 : void find_free_variables(const T& x, OutputIterator o)
188 : {
189 : data::detail::make_find_free_variables_traverser<regular_formulas::data_expression_traverser, regular_formulas::add_data_variable_traverser_binding>(o).apply(x);
190 : }
191 :
192 : /// \\brief Returns all variables that occur in an object
193 : /// \\param[in] x an object containing variables
194 : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
195 : /// \\param[in] bound a container of variables
196 : /// \\return All free variables that occur in the object x
197 : template <typename T, typename OutputIterator, typename VariableContainer>
198 : void find_free_variables_with_bound(const T& x, OutputIterator o, const VariableContainer& bound)
199 : {
200 : data::detail::make_find_free_variables_traverser<regular_formulas::data_expression_traverser, regular_formulas::add_data_variable_traverser_binding>(o, bound).apply(x);
201 : }
202 :
203 : /// \\brief Returns all variables that occur in an object
204 : /// \\param[in] x an object containing variables
205 : /// \\return All free variables that occur in the object x
206 : template <typename T>
207 : std::set<data::variable> find_free_variables(const T& x)
208 : {
209 : std::set<data::variable> result;
210 : regular_formulas::find_free_variables(x, std::inserter(result, result.end()));
211 : return result;
212 : }
213 :
214 : /// \\brief Returns all variables that occur in an object
215 : /// \\param[in] x an object containing variables
216 : /// \\param[in] bound a bound a container of variables
217 : /// \\return All free variables that occur in the object x
218 : template <typename T, typename VariableContainer>
219 : std::set<data::variable> find_free_variables_with_bound(const T& x, VariableContainer const& bound)
220 : {
221 : std::set<data::variable> result;
222 : regular_formulas::find_free_variables_with_bound(x, std::inserter(result, result.end()), bound);
223 : return result;
224 : }
225 :
226 : /// \\brief Returns all identifiers that occur in an object
227 : /// \\param[in] x an object containing identifiers
228 : /// \\param[in,out] o an output iterator to which all identifiers occurring in x are written.
229 : /// \\return All identifiers that occur in the term x
230 : template <typename T, typename OutputIterator>
231 : void find_identifiers(const T& x, OutputIterator o)
232 : {
233 : data::detail::make_find_identifiers_traverser<regular_formulas::identifier_string_traverser>(o).apply(x);
234 : }
235 :
236 : /// \\brief Returns all identifiers that occur in an object
237 : /// \\param[in] x an object containing identifiers
238 : /// \\return All identifiers that occur in the object x
239 : template <typename T>
240 : std::set<core::identifier_string> find_identifiers(const T& x)
241 : {
242 : std::set<core::identifier_string> result;
243 : regular_formulas::find_identifiers(x, std::inserter(result, result.end()));
244 : return result;
245 : }
246 :
247 : /// \\brief Returns all sort expressions that occur in an object
248 : /// \\param[in] x an object containing sort expressions
249 : /// \\param[in,out] o an output iterator to which all sort expressions occurring in x are written.
250 : /// \\return All sort expressions that occur in the term x
251 : template <typename T, typename OutputIterator>
252 : void find_sort_expressions(const T& x, OutputIterator o)
253 : {
254 : data::detail::make_find_sort_expressions_traverser<regular_formulas::sort_expression_traverser>(o).apply(x);
255 : }
256 :
257 : /// \\brief Returns all sort expressions that occur in an object
258 : /// \\param[in] x an object containing sort expressions
259 : /// \\return All sort expressions that occur in the object x
260 : template <typename T>
261 : std::set<data::sort_expression> find_sort_expressions(const T& x)
262 : {
263 : std::set<data::sort_expression> result;
264 : regular_formulas::find_sort_expressions(x, std::inserter(result, result.end()));
265 : return result;
266 : }
267 :
268 : /// \\brief Returns all function symbols that occur in an object
269 : /// \\param[in] x an object containing function symbols
270 : /// \\param[in,out] o an output iterator to which all function symbols occurring in x are written.
271 : /// \\return All function symbols that occur in the term x
272 : template <typename T, typename OutputIterator>
273 : void find_function_symbols(const T& x, OutputIterator o)
274 : {
275 : data::detail::make_find_function_symbols_traverser<regular_formulas::data_expression_traverser>(o).apply(x);
276 : }
277 :
278 : /// \\brief Returns all function symbols that occur in an object
279 : /// \\param[in] x an object containing function symbols
280 : /// \\return All function symbols that occur in the object x
281 : template <typename T>
282 : std::set<data::function_symbol> find_function_symbols(const T& x)
283 : {
284 : std::set<data::function_symbol> result;
285 : regular_formulas::find_function_symbols(x, std::inserter(result, result.end()));
286 : return result;
287 : }
288 : //--- end generated regular_formulas find code ---//
289 :
290 : } // namespace regular_formulas
291 :
292 : namespace state_formulas
293 : {
294 :
295 : //--- start generated state_formulas find code ---//
296 : /// \\brief Returns all variables that occur in an object
297 : /// \\param[in] x an object containing variables
298 : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
299 : /// \\return All variables that occur in the term x
300 : template <typename T, typename OutputIterator>
301 1 : void find_all_variables(const T& x, OutputIterator o)
302 : {
303 1 : data::detail::make_find_all_variables_traverser<state_formulas::variable_traverser>(o).apply(x);
304 1 : }
305 :
306 : /// \\brief Returns all variables that occur in an object
307 : /// \\param[in] x an object containing variables
308 : /// \\return All variables that occur in the object x
309 : template <typename T>
310 1 : std::set<data::variable> find_all_variables(const T& x)
311 : {
312 1 : std::set<data::variable> result;
313 1 : state_formulas::find_all_variables(x, std::inserter(result, result.end()));
314 1 : return result;
315 0 : }
316 :
317 : /// \\brief Returns all variables that occur in an object
318 : /// \\param[in] x an object containing variables
319 : /// \\param[in,out] o an output iterator to which all variables occurring in x are added.
320 : /// \\return All free variables that occur in the object x
321 : template <typename T, typename OutputIterator>
322 1 : void find_free_variables(const T& x, OutputIterator o)
323 : {
324 1 : data::detail::make_find_free_variables_traverser<state_formulas::data_expression_traverser, state_formulas::add_data_variable_traverser_binding>(o).apply(x);
325 1 : }
326 :
327 : /// \\brief Returns all variables that occur in an object
328 : /// \\param[in] x an object containing variables
329 : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
330 : /// \\param[in] bound a container of variables
331 : /// \\return All free variables that occur in the object x
332 : template <typename T, typename OutputIterator, typename VariableContainer>
333 : void find_free_variables_with_bound(const T& x, OutputIterator o, const VariableContainer& bound)
334 : {
335 : data::detail::make_find_free_variables_traverser<state_formulas::data_expression_traverser, state_formulas::add_data_variable_traverser_binding>(o, bound).apply(x);
336 : }
337 :
338 : /// \\brief Returns all variables that occur in an object
339 : /// \\param[in] x an object containing variables
340 : /// \\return All free variables that occur in the object x
341 : template <typename T>
342 1 : std::set<data::variable> find_free_variables(const T& x)
343 : {
344 1 : std::set<data::variable> result;
345 1 : state_formulas::find_free_variables(x, std::inserter(result, result.end()));
346 1 : return result;
347 0 : }
348 :
349 : /// \\brief Returns all variables that occur in an object
350 : /// \\param[in] x an object containing variables
351 : /// \\param[in] bound a bound a container of variables
352 : /// \\return All free variables that occur in the object x
353 : template <typename T, typename VariableContainer>
354 : std::set<data::variable> find_free_variables_with_bound(const T& x, VariableContainer const& bound)
355 : {
356 : std::set<data::variable> result;
357 : state_formulas::find_free_variables_with_bound(x, std::inserter(result, result.end()), bound);
358 : return result;
359 : }
360 :
361 : /// \\brief Returns all identifiers that occur in an object
362 : /// \\param[in] x an object containing identifiers
363 : /// \\param[in,out] o an output iterator to which all identifiers occurring in x are written.
364 : /// \\return All identifiers that occur in the term x
365 : template <typename T, typename OutputIterator>
366 673 : void find_identifiers(const T& x, OutputIterator o)
367 : {
368 673 : data::detail::make_find_identifiers_traverser<state_formulas::identifier_string_traverser>(o).apply(x);
369 673 : }
370 :
371 : /// \\brief Returns all identifiers that occur in an object
372 : /// \\param[in] x an object containing identifiers
373 : /// \\return All identifiers that occur in the object x
374 : template <typename T>
375 673 : std::set<core::identifier_string> find_identifiers(const T& x)
376 : {
377 673 : std::set<core::identifier_string> result;
378 673 : state_formulas::find_identifiers(x, std::inserter(result, result.end()));
379 673 : return result;
380 0 : }
381 :
382 : /// \\brief Returns all sort expressions that occur in an object
383 : /// \\param[in] x an object containing sort expressions
384 : /// \\param[in,out] o an output iterator to which all sort expressions occurring in x are written.
385 : /// \\return All sort expressions that occur in the term x
386 : template <typename T, typename OutputIterator>
387 174 : void find_sort_expressions(const T& x, OutputIterator o)
388 : {
389 174 : data::detail::make_find_sort_expressions_traverser<state_formulas::sort_expression_traverser>(o).apply(x);
390 174 : }
391 :
392 : /// \\brief Returns all sort expressions that occur in an object
393 : /// \\param[in] x an object containing sort expressions
394 : /// \\return All sort expressions that occur in the object x
395 : template <typename T>
396 174 : std::set<data::sort_expression> find_sort_expressions(const T& x)
397 : {
398 174 : std::set<data::sort_expression> result;
399 174 : state_formulas::find_sort_expressions(x, std::inserter(result, result.end()));
400 174 : return result;
401 0 : }
402 :
403 : /// \\brief Returns all function symbols that occur in an object
404 : /// \\param[in] x an object containing function symbols
405 : /// \\param[in,out] o an output iterator to which all function symbols occurring in x are written.
406 : /// \\return All function symbols that occur in the term x
407 : template <typename T, typename OutputIterator>
408 : void find_function_symbols(const T& x, OutputIterator o)
409 : {
410 : data::detail::make_find_function_symbols_traverser<state_formulas::data_expression_traverser>(o).apply(x);
411 : }
412 :
413 : /// \\brief Returns all function symbols that occur in an object
414 : /// \\param[in] x an object containing function symbols
415 : /// \\return All function symbols that occur in the object x
416 : template <typename T>
417 : std::set<data::function_symbol> find_function_symbols(const T& x)
418 : {
419 : std::set<data::function_symbol> result;
420 : state_formulas::find_function_symbols(x, std::inserter(result, result.end()));
421 : return result;
422 : }
423 : //--- end generated state_formulas find code ---//
424 :
425 : namespace detail {
426 :
427 : // collects state variable names in a set
428 : struct state_variable_name_traverser: public state_formulas::state_formula_traverser<state_variable_name_traverser>
429 : {
430 : typedef state_formulas::state_formula_traverser<state_variable_name_traverser> super;
431 : using super::enter;
432 : using super::leave;
433 : using super::apply;
434 :
435 : std::set<core::identifier_string> names;
436 :
437 0 : void apply(const state_formulas::variable& x)
438 : {
439 0 : names.insert(x.name());
440 0 : }
441 : };
442 :
443 : template <template <class> class Traverser, class OutputIterator>
444 : struct find_state_variables_traverser: public Traverser<find_state_variables_traverser<Traverser, OutputIterator> >
445 : {
446 : typedef Traverser<find_state_variables_traverser<Traverser, OutputIterator> > super;
447 : using super::enter;
448 : using super::leave;
449 : using super::apply;
450 :
451 : OutputIterator out;
452 :
453 4 : find_state_variables_traverser(OutputIterator out_)
454 4 : : out(out_)
455 4 : {}
456 :
457 9 : void apply(const variable& v)
458 : {
459 9 : *out = v;
460 9 : }
461 : };
462 :
463 : template <template <class> class Traverser, class OutputIterator>
464 : find_state_variables_traverser<Traverser, OutputIterator>
465 4 : make_find_state_variables_traverser(OutputIterator out)
466 : {
467 4 : return find_state_variables_traverser<Traverser, OutputIterator>(out);
468 : }
469 :
470 : template <template <class> class Traverser, template <template <class> class, class> class Binder, class OutputIterator>
471 : struct find_free_state_variables_traverser: public Binder<Traverser, find_free_state_variables_traverser<Traverser, Binder, OutputIterator> >
472 : {
473 : typedef Binder<Traverser, find_free_state_variables_traverser<Traverser, Binder, OutputIterator> > super;
474 : using super::enter;
475 : using super::leave;
476 : using super::apply;
477 : using super::is_bound;
478 : using super::bound_variables;
479 : using super::increase_bind_count;
480 :
481 : OutputIterator out;
482 :
483 2 : find_free_state_variables_traverser(OutputIterator out_)
484 2 : : out(out_)
485 2 : {}
486 :
487 : /*
488 : template <typename VariableContainer>
489 : find_free_state_variables_traverser(OutputIterator out_, const VariableContainer& v)
490 : : out(out_)
491 : {
492 : increase_bind_count(v);
493 : }
494 : */
495 :
496 4 : void apply(const variable& v)
497 : {
498 4 : if (!is_bound(v.name()))
499 : {
500 3 : *out = v;
501 : }
502 4 : }
503 : };
504 :
505 : template <template <class> class Traverser, template <template <class> class, class> class Binder, class OutputIterator>
506 : find_free_state_variables_traverser<Traverser, Binder, OutputIterator>
507 2 : make_find_free_state_variables_traverser(OutputIterator out)
508 : {
509 2 : return find_free_state_variables_traverser<Traverser, Binder, OutputIterator>(out);
510 : }
511 :
512 : template <template <class> class Traverser, template <template <class> class, class> class Binder, class OutputIterator, class VariableContainer>
513 : find_free_state_variables_traverser<Traverser, Binder, OutputIterator>
514 : make_find_free_state_variables_traverser(OutputIterator out, const VariableContainer& v)
515 : {
516 : return find_free_state_variables_traverser<Traverser, Binder, OutputIterator>(out, v);
517 : }
518 :
519 : } // namespace detail
520 :
521 : /// \brief Returns the names of the state variables that occur in x.
522 : /// \param[in] x A state formula
523 : inline
524 0 : std::set<core::identifier_string> find_state_variable_names(const state_formula& x)
525 : {
526 0 : detail::state_variable_name_traverser f;
527 0 : f.apply(x);
528 0 : return f.names;
529 0 : }
530 :
531 : /// \brief Returns all state variables that occur in an object
532 : /// \param[in] x an object containing state variables
533 : /// \param[in,out] o an output iterator to which all state variables occurring in x are written.
534 : /// \return All variables that occur in the term x
535 : template <typename T, typename OutputIterator>
536 4 : void find_state_variables(const T& x, OutputIterator o)
537 : {
538 4 : state_formulas::detail::make_find_state_variables_traverser<state_formulas::state_variable_traverser>(o).apply(x);
539 4 : }
540 :
541 : /// \brief Returns all state variables that occur in an object
542 : /// \param[in] x an object containing variables
543 : /// \return All state variables that occur in the object x
544 : template <typename T>
545 4 : std::set<state_formulas::variable> find_state_variables(const T& x)
546 : {
547 4 : std::set<state_formulas::variable> result;
548 4 : state_formulas::find_state_variables(x, std::inserter(result, result.end()));
549 4 : return result;
550 0 : }
551 :
552 : /// \brief Returns all free state variables that occur in an object
553 : /// \param[in] x an object containing state variables
554 : /// \param[in,out] o an output iterator to which all state variables occurring in x are added.
555 : /// \return All free state variables that occur in the object x
556 : template <typename T, typename OutputIterator>
557 2 : void find_free_state_variables(const T& x, OutputIterator o)
558 : {
559 2 : state_formulas::detail::make_find_free_state_variables_traverser<state_formulas::state_variable_traverser, state_formulas::add_state_variable_binding>(o).apply(x);
560 2 : }
561 :
562 : /// \brief Returns all free state variables that occur in an object
563 : /// \param[in] x an object containing variables
564 : /// \return All state variables that occur in the object x
565 : template <typename T>
566 2 : std::set<state_formulas::variable> find_free_state_variables(const T& x)
567 : {
568 2 : std::set<state_formulas::variable> result;
569 2 : state_formulas::find_free_state_variables(x, std::inserter(result, result.end()));
570 2 : return result;
571 0 : }
572 :
573 : /// \brief Returns all action labels that occur in an object
574 : /// \param[in] x an object containing action labels
575 : /// \param[in,out] o an output iterator to which all action labels occurring in x are written.
576 : /// \return All action labels that occur in the term x
577 : template <typename T, typename OutputIterator>
578 0 : void find_action_labels(const T& x, OutputIterator o)
579 : {
580 0 : process::detail::make_find_action_labels_traverser<state_formulas::action_label_traverser>(o).apply(x);
581 0 : }
582 :
583 : /// \brief Returns all action labels that occur in an object
584 : /// \param[in] x an object containing action labels
585 : /// \return All action labels that occur in the object x
586 : template <typename T>
587 0 : std::set<process::action_label> find_action_labels(const T& x)
588 : {
589 0 : std::set<process::action_label> result;
590 0 : state_formulas::find_action_labels(x, std::inserter(result, result.end()));
591 0 : return result;
592 0 : }
593 :
594 : } // namespace state_formulas
595 :
596 : } // namespace mcrl2
597 :
598 : #endif // MCRL2_MODAL_FORMULA_FIND_H
|
