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/lps2pbes_rhs.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_LPS2PBES_RHS_H
13 : #define MCRL2_PBES_DETAIL_LPS2PBES_RHS_H
14 :
15 : #include "mcrl2/data/consistency.h"
16 : #include "mcrl2/pbes/detail/lps2pbes_par.h"
17 : #include "mcrl2/pbes/detail/lps2pbes_sat.h"
18 : #include "mcrl2/pbes/replace.h"
19 :
20 : namespace mcrl2 {
21 :
22 : namespace pbes_system {
23 :
24 : namespace detail {
25 :
26 : struct lps2pbes_parameters
27 : {
28 : const state_formulas::state_formula& phi0; // the original formula
29 : const lps::stochastic_linear_process& lps;
30 : data::set_identifier_generator& id_generator;
31 : const data::variable& T;
32 :
33 137 : lps2pbes_parameters(const state_formulas::state_formula& phi0_,
34 : const lps::stochastic_linear_process& lps_,
35 : data::set_identifier_generator& id_generator_,
36 : const data::variable& T_
37 : )
38 137 : : phi0(phi0_), lps(lps_), id_generator(id_generator_), T(T_)
39 137 : {}
40 :
41 : bool is_timed() const
42 : {
43 : return T != data::undefined_real_variable();
44 : }
45 :
46 : template <typename TermTraits>
47 791 : pbes_expression rhs_may_must(bool is_must,
48 : const data::variable_list& y,
49 : const pbes_expression& left, // Sat(ai(fi(x,y)) && ci(x,y) && (ti(x,y) > T)
50 : const pbes_expression& right, // RHS(phi)[T, x := ti(x,y), gi(x,y)]
51 : const lps::multi_action& /* ai */,
52 : const data::assignment_list& /* gi */,
53 : TermTraits
54 : )
55 : {
56 : typedef TermTraits tr;
57 791 : if (is_must)
58 : {
59 464 : return tr::forall(y, tr::imp(left, right));
60 : }
61 : else
62 : {
63 327 : return tr::exists(y, tr::and_(left, right));
64 : }
65 : }
66 : };
67 :
68 : struct lps2pbes_counter_example_parameters: public lps2pbes_parameters
69 : {
70 : data::variable_list d1; // d'
71 : data::mutable_map_substitution<> sigma; // the substitution [d := d'], where d is the sequence of process parameters of lps
72 : std::map<lps::multi_action, propositional_variable> Zpos; // represents the additional equations { nu Zpos_ai(d, fi(x,y), d') = true }
73 : std::map<lps::multi_action, propositional_variable> Zneg; // represents the additional equations { nu Zneg_ai(d, fi(x,y), d') = false }
74 :
75 : // creates variables corresponding to the action label sorts in actions
76 2 : data::variable_list action_variables(const process::action_list& actions) const
77 : {
78 2 : std::vector<data::variable> result;
79 4 : for (const process::action& a: actions)
80 : {
81 2 : for (const data::sort_expression& s: a.label().sorts())
82 : {
83 0 : data::variable v(id_generator("v"), s);
84 0 : result.push_back(v);
85 0 : }
86 : }
87 4 : return data::variable_list(result.begin(), result.end());
88 2 : }
89 :
90 : // returns the concatenation of the arguments of the list of actions
91 4 : data::data_expression_list action_expressions(const process::action_list& actions) const
92 : {
93 4 : std::vector<data::data_expression> result;
94 8 : for (const process::action& a: actions)
95 : {
96 4 : auto const& args = a.arguments();
97 4 : result.insert(result.end(), args.begin(), args.end());
98 : }
99 8 : return data::data_expression_list(result.begin(), result.end());
100 4 : }
101 :
102 : // returns the equations needed for counter example generation
103 1 : std::vector<pbes_equation> equations() const
104 : {
105 1 : std::vector<pbes_equation> result;
106 3 : for (auto const& p: Zneg)
107 : {
108 2 : pbes_equation eqn(fixpoint_symbol::nu(), p.second, false_());
109 2 : result.push_back(eqn);
110 2 : }
111 3 : for (auto const& p: Zpos)
112 : {
113 2 : pbes_equation eqn(fixpoint_symbol::nu(), p.second, true_());
114 2 : result.push_back(eqn);
115 2 : }
116 1 : return result;
117 0 : }
118 :
119 4 : std::string multi_action_name(const lps::multi_action& a) const
120 : {
121 4 : std::vector<std::string> v;
122 8 : for (const process::action& ai: a.actions())
123 : {
124 4 : v.emplace_back(ai.label().name());
125 : }
126 8 : return utilities::string_join(v, "_");
127 4 : }
128 :
129 1 : lps2pbes_counter_example_parameters(const state_formulas::state_formula& phi0,
130 : const lps::stochastic_linear_process& lps,
131 : data::set_identifier_generator& id_generator,
132 : const data::variable& T
133 : )
134 1 : : lps2pbes_parameters(phi0, lps, id_generator, T)
135 : {
136 1 : const data::variable_list& d = lps.process_parameters();
137 1 : sigma = detail::make_fresh_variable_substitution(d, id_generator);
138 1 : d1 = data::replace_variables(d, sigma);
139 :
140 1 : std::size_t index = 0;
141 3 : for (const lps::action_summand& summand: lps.action_summands())
142 : {
143 2 : const lps::multi_action& ai = summand.multi_action();
144 2 : data::variable_list actvars = action_variables(ai.actions());
145 4 : core::identifier_string pos = id_generator("Zpos_" + utilities::number2string(index) + "_" + multi_action_name(ai));
146 4 : core::identifier_string neg = id_generator("Zneg_" + utilities::number2string(index) + "_" + multi_action_name(ai));
147 2 : Zpos[ai] = propositional_variable(pos, d + actvars + d1);
148 2 : Zneg[ai] = propositional_variable(neg, d + actvars + d1);
149 2 : index++;
150 2 : }
151 1 : }
152 :
153 : data::data_expression equal_to(const data::variable_list& d, const data::data_expression_list& e) const
154 : {
155 : std::vector<data::data_expression> v;
156 : auto i = d.begin();
157 : auto j = e.begin();
158 : for (; i != d.end(); ++i, ++j)
159 : {
160 : v.push_back(data::equal_to(*i, *j));
161 : }
162 : return data::lazy::join_and(v.begin(), v.end());
163 : }
164 :
165 : template <typename TermTraits>
166 4 : pbes_expression rhs_may_must(bool is_must,
167 : const data::variable_list& y,
168 : const pbes_expression& left, // Sat(ai(fi(x,y)) && ci(x,y) && (ti(x,y) > T)
169 : const pbes_expression& right, // RHS(phi)[T, x := ti(x,y), gi(x,y)]
170 : const lps::multi_action& ai,
171 : const data::assignment_list& gi,
172 : TermTraits
173 : )
174 : {
175 : typedef TermTraits tr;
176 4 : const data::variable_list& d = lps.process_parameters();
177 4 : data::data_expression_list gi1 = data::replace_variables(atermpp::container_cast<data::data_expression_list>(d), data::assignment_sequence_substitution(gi));
178 4 : auto fi = action_expressions(ai.actions());
179 4 : data::data_expression_list da = atermpp::container_cast<data::data_expression_list>(d) + fi + gi1;
180 4 : propositional_variable_instantiation Pos(Zpos.at(ai).name(), da);
181 4 : propositional_variable_instantiation Neg(Zneg.at(ai).name(), da);
182 4 : auto right1 = right;
183 :
184 4 : if (is_must)
185 : {
186 4 : right1 = tr::or_(tr::and_(right, Pos), Neg);
187 4 : return tr::forall(y, tr::imp(left, right1));
188 : }
189 : else
190 : {
191 0 : right1 = tr::and_(tr::or_(right, Neg), Pos);
192 0 : return tr::exists(y, tr::and_(left, right1));
193 : }
194 4 : }
195 : };
196 :
197 : //--- RHS default variant ---//
198 :
199 : template <typename TermTraits, typename Parameters>
200 : pbes_expression RHS(const state_formulas::state_formula& x, Parameters& parameters, TermTraits tr);
201 :
202 : template <typename Derived, typename TermTraits, typename Parameters>
203 : struct rhs_traverser: public state_formulas::state_formula_traverser<Derived>
204 : {
205 : typedef state_formulas::state_formula_traverser<Derived> super;
206 : typedef TermTraits tr;
207 : typedef typename tr::term_type pbes_expression;
208 :
209 : using super::enter;
210 : using super::leave;
211 : using super::apply;
212 :
213 : Parameters& parameters;
214 : std::vector<pbes_expression> result_stack;
215 :
216 375 : rhs_traverser(Parameters& parameters_, TermTraits)
217 375 : : parameters(parameters_)
218 375 : {}
219 :
220 1037 : Derived& derived()
221 : {
222 1037 : return static_cast<Derived&>(*this);
223 : }
224 :
225 553 : void push(const pbes_expression& x)
226 : {
227 553 : result_stack.push_back(x);
228 553 : }
229 :
230 583 : pbes_expression& top()
231 : {
232 583 : return result_stack.back();
233 : }
234 :
235 : const pbes_expression& top() const
236 : {
237 : return result_stack.back();
238 : }
239 :
240 178 : pbes_expression pop()
241 : {
242 178 : pbes_expression result = top();
243 178 : result_stack.pop_back();
244 178 : return result;
245 : }
246 :
247 15 : void push_variables(const data::variable_list& variables)
248 : {
249 45 : for (const data::variable& v: variables)
250 : {
251 15 : parameters.id_generator.add_identifier(v.name());
252 : }
253 15 : }
254 :
255 : void pop_variables(const data::variable_list& variables)
256 : {
257 : for (const data::variable& v: variables)
258 : {
259 : parameters.id_generator.remove_identifier(v.name());
260 : }
261 : }
262 :
263 323 : bool is_timed() const
264 : {
265 323 : return parameters.T != data::undefined_real_variable();
266 : }
267 :
268 16 : void leave(const data::data_expression& x)
269 : {
270 16 : push(x);
271 16 : }
272 :
273 62 : void leave(const state_formulas::true_&)
274 : {
275 62 : push(true_());
276 62 : }
277 :
278 59 : void leave(const state_formulas::false_&)
279 : {
280 59 : push(false_());
281 59 : }
282 :
283 0 : void apply(const state_formulas::not_&)
284 : {
285 0 : throw mcrl2::runtime_error("rhs_traverser: negation is not supported!");
286 : }
287 :
288 49 : void leave(const state_formulas::and_&)
289 : {
290 49 : pbes_expression right = pop();
291 49 : pbes_expression left = pop();
292 49 : push(tr::and_(left, right));
293 49 : }
294 :
295 40 : void leave(const state_formulas::or_&)
296 : {
297 40 : pbes_expression right = pop();
298 40 : pbes_expression left = pop();
299 40 : push(tr::or_(left, right));
300 40 : }
301 :
302 0 : void apply(const state_formulas::imp&)
303 : {
304 0 : throw mcrl2::runtime_error("rhs_traverser: implication is not supported!");
305 : }
306 :
307 11 : void apply(const state_formulas::forall& x)
308 : {
309 11 : derived().enter(x);
310 11 : push_variables(x.variables());
311 11 : derived().apply(x.body());
312 11 : tr::make_forall(top(), x.variables(), top());
313 : //pop_variables(x.variables());
314 11 : derived().leave(x);
315 11 : }
316 :
317 4 : void apply(const state_formulas::exists& x)
318 : {
319 4 : derived().enter(x);
320 4 : push_variables(x.variables());
321 4 : derived().apply(x.body());
322 4 : tr::make_exists(top(), x.variables(), top());
323 : //pop_variables(x.variables());
324 4 : derived().leave(x);
325 4 : }
326 :
327 : // This function is overridden in the structured variant of the algorithm
328 : template <typename MustMayExpression>
329 197 : pbes_expression apply_may_must_rhs(const MustMayExpression& x)
330 : {
331 197 : return RHS(x.operand(), parameters, TermTraits());
332 : }
333 :
334 : // This function is overridden in the structured variant of the algorithm
335 795 : pbes_expression apply_may_must_result(const pbes_expression& p)
336 : {
337 795 : return p;
338 : }
339 :
340 : // share code between must and may
341 : template <typename MustMayExpression>
342 197 : void apply_may_must(const MustMayExpression& x, bool is_must)
343 : {
344 197 : bool timed = is_timed();
345 197 : std::vector<pbes_expression> v;
346 197 : pbes_expression rhs_phi = derived().apply_may_must_rhs(x);
347 197 : assert(action_formulas::is_action_formula(x.formula()));
348 197 : const action_formulas::action_formula& alpha = atermpp::down_cast<const action_formulas::action_formula>(x.formula());
349 :
350 992 : for (const lps::action_summand& summand: parameters.lps.action_summands())
351 : {
352 795 : const data::data_expression& ci = summand.condition();
353 795 : const lps::multi_action& ai = summand.multi_action();
354 795 : const data::assignment_list& gi = summand.assignments();
355 795 : const data::variable_list& yi = summand.summation_variables();
356 :
357 795 : pbes_expression right = rhs_phi;
358 795 : const data::data_expression& ti = ai.time();
359 795 : pbes_expression sat = Sat(ai, alpha, parameters.id_generator, TermTraits());
360 795 : data::mutable_map_substitution<> sigma;
361 3287 : for (const data::assignment& a: gi)
362 : {
363 1697 : sigma[a.lhs()] = a.rhs();
364 : }
365 795 : pbes_expression left = tr::and_(sat, ci);
366 :
367 795 : if (timed)
368 : {
369 2 : sigma[parameters.T] = ti;
370 2 : left = tr::and_(left, data::greater(ti, parameters.T));
371 : }
372 :
373 795 : right = pbes_system::replace_variables_capture_avoiding(right, sigma);
374 :
375 795 : pbes_expression p = parameters.rhs_may_must(is_must, yi, left, right, ai, gi, TermTraits());
376 795 : v.push_back(derived().apply_may_must_result(p));
377 : }
378 :
379 197 : pbes_expression result = is_must ? tr::join_and(v.begin(), v.end()) : tr::join_or(v.begin(), v.end());
380 197 : push(result);
381 197 : }
382 :
383 111 : void apply(const state_formulas::must& x)
384 : {
385 111 : apply_may_must(x, true);
386 111 : }
387 :
388 86 : void apply(const state_formulas::may& x)
389 : {
390 86 : apply_may_must(x, false);
391 86 : }
392 :
393 0 : void leave(const state_formulas::yaled&)
394 : {
395 0 : throw mcrl2::runtime_error("rhs_traverser: yaled is not supported!");
396 : }
397 :
398 2 : void leave(const state_formulas::yaled_timed& x)
399 : {
400 2 : const data::data_expression& t = x.time_stamp();
401 2 : std::vector<pbes_expression> v;
402 4 : for (const lps::action_summand& i: parameters.lps.action_summands())
403 : {
404 2 : const data::data_expression& ci = i.condition();
405 2 : const data::data_expression& ti = i.multi_action().time();
406 2 : const data::variable_list& yi = i.summation_variables();
407 4 : pbes_expression p = tr::forall(yi, tr::or_(data::not_(ci), data::greater(t, ti)));
408 2 : v.push_back(p);
409 : }
410 2 : for (const lps::deadlock_summand& j: parameters.lps.deadlock_summands())
411 : {
412 0 : const data::data_expression& cj = j.condition();
413 0 : const data::data_expression& tj = j.deadlock().time();
414 0 : const data::variable_list& yj = j.summation_variables();
415 0 : pbes_expression p = tr::forall(yj, tr::or_(data::not_(cj), data::greater(t, tj)));
416 0 : v.push_back(p);
417 : }
418 2 : push(tr::and_(tr::join_or(v.begin(), v.end()), data::greater(t, parameters.T)));
419 2 : }
420 :
421 0 : void leave(const state_formulas::delay&)
422 : {
423 0 : throw mcrl2::runtime_error("rhs_traverser: delay is not supported!");
424 : }
425 :
426 2 : void leave(const state_formulas::delay_timed& x)
427 : {
428 2 : const data::data_expression& t = x.time_stamp();
429 2 : std::vector<pbes_expression> v;
430 4 : for (const lps::action_summand& i : parameters.lps.action_summands())
431 : {
432 2 : const data::data_expression& ci = i.condition();
433 2 : data::data_expression ti = i.multi_action().time();
434 2 : const data::variable_list& yi = i.summation_variables();
435 4 : pbes_expression p = tr::exists(yi, tr::and_(ci, data::less_equal(t, ti)));
436 2 : v.push_back(p);
437 : }
438 2 : for (const lps::deadlock_summand& j: parameters.lps.deadlock_summands())
439 : {
440 0 : const data::data_expression& cj = j.condition();
441 0 : data::data_expression tj = j.deadlock().time();
442 0 : const data::variable_list& yj = j.summation_variables();
443 0 : pbes_expression p = tr::exists(yj, tr::and_(cj, data::less_equal(t, tj)));
444 0 : v.push_back(p);
445 : }
446 2 : push(tr::or_(tr::join_or(v.begin(), v.end()), data::less_equal(t, parameters.T)));
447 2 : }
448 :
449 85 : void leave(const state_formulas::variable& x)
450 : {
451 85 : const core::identifier_string& X = x.name();
452 85 : const data::data_expression_list& d = x.arguments();
453 85 : data::variable_list xp = parameters.lps.process_parameters();
454 170 : data::data_expression_list e = d + xp + Par(X, data::variable_list(), parameters.phi0);
455 85 : if (is_timed())
456 : {
457 2 : e.push_front(parameters.T);
458 : }
459 85 : push(propositional_variable_instantiation(X, e));
460 85 : }
461 :
462 16 : void apply(const state_formulas::nu& x)
463 : {
464 16 : const core::identifier_string& X = x.name();
465 16 : data::data_expression_list d = detail::mu_expressions(x);
466 16 : data::variable_list xp = parameters.lps.process_parameters();
467 32 : data::data_expression_list e = d + xp + Par(X, data::variable_list(), parameters.phi0);
468 16 : if (is_timed())
469 : {
470 0 : e.push_front(parameters.T);
471 : }
472 16 : push(propositional_variable_instantiation(X, e));
473 16 : }
474 :
475 25 : void apply(const state_formulas::mu& x)
476 : {
477 25 : const core::identifier_string& X = x.name();
478 25 : data::data_expression_list d = detail::mu_expressions(x);
479 25 : data::variable_list xp = parameters.lps.process_parameters();
480 50 : data::data_expression_list e = d + xp + Par(X, data::variable_list(), parameters.phi0);
481 25 : if (is_timed())
482 : {
483 1 : e.push_front(parameters.T);
484 : }
485 25 : push(propositional_variable_instantiation(X, e));
486 25 : }
487 : };
488 :
489 : template <template <class, class, class> class Traverser, typename TermTraits, typename Parameters>
490 : struct apply_rhs_traverser: public Traverser<apply_rhs_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters>
491 : {
492 : typedef Traverser<apply_rhs_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters> super;
493 : using super::enter;
494 : using super::leave;
495 : using super::apply;
496 :
497 375 : apply_rhs_traverser(Parameters& parameters, TermTraits tr)
498 375 : : super(parameters, tr)
499 375 : {}
500 : };
501 :
502 : template <typename TermTraits, typename Parameters>
503 : inline
504 375 : pbes_expression RHS(const state_formulas::state_formula& x, Parameters& parameters, TermTraits tr)
505 : {
506 375 : apply_rhs_traverser<rhs_traverser, TermTraits, Parameters> f(parameters, tr);
507 375 : f.apply(x);
508 750 : return f.top();
509 375 : }
510 :
511 : //--- RHS_structured variant ---//
512 :
513 : template <typename TermTraits, typename Parameters>
514 : inline
515 : typename TermTraits::term_type RHS_structured(const state_formulas::state_formula& x,
516 : Parameters& parameters,
517 : const data::variable_list& variables,
518 : const fixpoint_symbol& sigma,
519 : std::vector<pbes_equation>& equations,
520 : TermTraits tr
521 : );
522 :
523 : template <typename Derived, typename TermTraits, typename Parameters>
524 : struct rhs_structured_traverser: public rhs_traverser<Derived, TermTraits, Parameters>
525 : {
526 : typedef rhs_traverser<Derived, TermTraits, Parameters> super;
527 : typedef TermTraits tr;
528 :
529 : using super::enter;
530 : using super::leave;
531 : using super::apply;
532 : using super::push;
533 : using super::top;
534 : using super::pop;
535 : using super::is_timed;
536 : using super::parameters;
537 : using super::apply_may_must;
538 : using super::derived;
539 :
540 : std::multiset<data::variable> variables;
541 : const fixpoint_symbol& sigma;
542 : std::vector<pbes_equation>& equations; // new equations that are generated on the fly
543 :
544 0 : rhs_structured_traverser(Parameters& parameters,
545 : const data::variable_list& variables_,
546 : const fixpoint_symbol& sigma_,
547 : std::vector<pbes_equation>& equations_,
548 : TermTraits tr
549 : )
550 : : super(parameters, tr),
551 0 : variables(variables_.begin(), variables_.end()),
552 0 : sigma(sigma_),
553 0 : equations(equations_)
554 0 : {}
555 :
556 0 : data::variable_list rhs_structured_compute_variables(const state_formulas::state_formula& x, const std::multiset<data::variable>& variables) const
557 : {
558 0 : std::set<data::variable> fv = state_formulas::find_free_variables(x);
559 0 : fv.insert(variables.begin(), variables.end());
560 0 : return data::variable_list(fv.begin(), fv.end());
561 0 : }
562 :
563 0 : void enter(const state_formulas::forall& x)
564 : {
565 0 : const data::variable_list& v = x.variables();
566 0 : variables.insert(v.begin(), v.end());
567 0 : }
568 :
569 0 : void leave(const state_formulas::forall& x)
570 : {
571 0 : for (const data::variable& var: x.variables())
572 : {
573 0 : variables.erase(var);
574 : }
575 0 : }
576 :
577 0 : void enter(const state_formulas::exists& x)
578 : {
579 0 : const data::variable_list& v = x.variables();
580 0 : variables.insert(v.begin(), v.end());
581 0 : }
582 :
583 0 : void leave(const state_formulas::exists& x)
584 : {
585 0 : for (const data::variable& var: x.variables())
586 : {
587 0 : variables.erase(var);
588 : }
589 0 : }
590 :
591 : // override
592 : template <typename MustMayExpression>
593 0 : pbes_expression apply_may_must_rhs(const MustMayExpression& x)
594 : {
595 0 : return RHS_structured(x.operand(), parameters, rhs_structured_compute_variables(x.operand(), variables), sigma, equations, TermTraits());
596 : }
597 :
598 : // override
599 0 : pbes_expression apply_may_must_result(const pbes_expression& p)
600 : {
601 : // generate a new equation 'Y(d) = p', and add Y(d) to v
602 0 : core::identifier_string Y = parameters.id_generator("Y");
603 0 : data::variable_list d(variables.begin(), variables.end());
604 0 : propositional_variable Yd(Y, d);
605 0 : pbes_equation eqn(sigma, Yd, p);
606 0 : equations.push_back(eqn);
607 0 : return propositional_variable_instantiation(Y, data::make_data_expression_list(d));
608 0 : }
609 :
610 0 : void apply(const state_formulas::must& x)
611 : {
612 0 : apply_may_must(x, true);
613 0 : }
614 :
615 0 : void apply(const state_formulas::may& x)
616 : {
617 0 : apply_may_must(x, false);
618 0 : }
619 : };
620 :
621 : template <template <class, class, class> class Traverser, typename TermTraits, typename Parameters>
622 : struct apply_rhs_structured_traverser: public Traverser<apply_rhs_structured_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters>
623 : {
624 : typedef Traverser<apply_rhs_structured_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters> super;
625 : using super::enter;
626 : using super::leave;
627 : using super::apply;
628 :
629 0 : apply_rhs_structured_traverser(Parameters& parameters,
630 : const data::variable_list& variables,
631 : const fixpoint_symbol& sigma,
632 : std::vector<pbes_equation>& equations,
633 : TermTraits tr
634 : )
635 0 : : super(parameters, variables, sigma, equations, tr)
636 0 : {}
637 : };
638 :
639 : template <typename TermTraits, typename Parameters>
640 : inline
641 0 : typename TermTraits::term_type RHS_structured(const state_formulas::state_formula& x,
642 : Parameters& parameters,
643 : const data::variable_list& variables,
644 : const fixpoint_symbol& sigma,
645 : std::vector<pbes_equation>& equations,
646 : TermTraits tr
647 : )
648 : {
649 0 : apply_rhs_structured_traverser<rhs_structured_traverser, TermTraits, Parameters> f(parameters, variables, sigma, equations, tr);
650 0 : f.apply(x);
651 0 : return f.top();
652 0 : }
653 :
654 : } // namespace detail
655 :
656 : } // namespace pbes_system
657 :
658 : } // namespace mcrl2
659 :
660 : #endif // MCRL2_PBES_DETAIL_LPS2PBES_RHS_H
|