mCRL2
Loading...
Searching...
No Matches
lps2pbes_rhs.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_DETAIL_LPS2PBES_RHS_H
13#define MCRL2_PBES_DETAIL_LPS2PBES_RHS_H
14
18#include "mcrl2/pbes/replace.h"
19
20namespace mcrl2 {
21
22namespace pbes_system {
23
24namespace detail {
25
27{
28 const state_formulas::state_formula& phi0; // the original formula
32
35 data::set_identifier_generator& id_generator_,
36 const data::variable& T_
37 )
38 : phi0(phi0_), lps(lps_), id_generator(id_generator_), T(T_)
39 {}
40
41 bool is_timed() const
42 {
44 }
45
46 template <typename TermTraits>
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 if (is_must)
58 {
59 return tr::forall(y, tr::imp(left, right));
60 }
61 else
62 {
63 return tr::exists(y, tr::and_(left, right));
64 }
65 }
66};
67
69{
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
77 {
78 std::vector<data::variable> result;
79 for (const process::action& a: actions)
80 {
81 for (const data::sort_expression& s: a.label().sorts())
82 {
84 result.push_back(v);
85 }
86 }
87 return data::variable_list(result.begin(), result.end());
88 }
89
90 // returns the concatenation of the arguments of the list of actions
92 {
93 std::vector<data::data_expression> result;
94 for (const process::action& a: actions)
95 {
96 auto const& args = a.arguments();
97 result.insert(result.end(), args.begin(), args.end());
98 }
99 return data::data_expression_list(result.begin(), result.end());
100 }
101
102 // returns the equations needed for counter example generation
103 std::vector<pbes_equation> equations() const
104 {
105 std::vector<pbes_equation> result;
106 for (auto const& p: Zneg)
107 {
108 pbes_equation eqn(fixpoint_symbol::nu(), p.second, false_());
109 result.push_back(eqn);
110 }
111 for (auto const& p: Zpos)
112 {
113 pbes_equation eqn(fixpoint_symbol::nu(), p.second, true_());
114 result.push_back(eqn);
115 }
116 return result;
117 }
118
119 std::string multi_action_name(const lps::multi_action& a) const
120 {
121 std::vector<std::string> v;
122 for (const process::action& ai: a.actions())
123 {
124 v.emplace_back(ai.label().name());
125 }
126 return utilities::string_join(v, "_");
127 }
128
132 const data::variable& T
133 )
135 {
139
140 std::size_t index = 0;
141 for (const lps::action_summand& summand: lps.action_summands())
142 {
143 const lps::multi_action& ai = summand.multi_action();
147 Zpos[ai] = propositional_variable(pos, d + actvars + d1);
148 Zneg[ai] = propositional_variable(neg, d + actvars + d1);
149 index++;
150 }
151 }
152
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>
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;
177 data::data_expression_list gi1 = data::replace_variables(atermpp::container_cast<data::data_expression_list>(d), data::assignment_sequence_substitution(gi));
178 auto fi = action_expressions(ai.actions());
179 data::data_expression_list da = atermpp::container_cast<data::data_expression_list>(d) + fi + gi1;
180 propositional_variable_instantiation Pos(Zpos.at(ai).name(), da);
181 propositional_variable_instantiation Neg(Zneg.at(ai).name(), da);
182 auto right1 = right;
183
184 if (is_must)
185 {
186 right1 = tr::or_(tr::and_(right, Pos), Neg);
187 return tr::forall(y, tr::imp(left, right1));
188 }
189 else
190 {
191 right1 = tr::and_(tr::or_(right, Neg), Pos);
192 return tr::exists(y, tr::and_(left, right1));
193 }
194 }
195};
196
197//--- RHS default variant ---//
198
199template <typename TermTraits, typename Parameters>
200pbes_expression RHS(const state_formulas::state_formula& x, Parameters& parameters, TermTraits tr);
201
202template <typename Derived, typename TermTraits, typename Parameters>
204{
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 rhs_traverser(Parameters& parameters_, TermTraits)
217 : parameters(parameters_)
218 {}
219
220 Derived& derived()
221 {
222 return static_cast<Derived&>(*this);
223 }
224
225 void push(const pbes_expression& x)
226 {
227 result_stack.push_back(x);
228 }
229
231 {
232 return result_stack.back();
233 }
234
235 const pbes_expression& top() const
236 {
237 return result_stack.back();
238 }
239
241 {
242 pbes_expression result = top();
243 result_stack.pop_back();
244 return result;
245 }
246
247 void push_variables(const data::variable_list& variables)
248 {
249 for (const data::variable& v: variables)
250 {
251 parameters.id_generator.add_identifier(v.name());
252 }
253 }
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 bool is_timed() const
264 {
266 }
267
269 {
270 push(x);
271 }
272
274 {
275 push(true_());
276 }
277
279 {
280 push(false_());
281 }
282
284 {
285 throw mcrl2::runtime_error("rhs_traverser: negation is not supported!");
286 }
287
289 {
290 pbes_expression right = pop();
291 pbes_expression left = pop();
292 push(tr::and_(left, right));
293 }
294
296 {
297 pbes_expression right = pop();
298 pbes_expression left = pop();
299 push(tr::or_(left, right));
300 }
301
303 {
304 throw mcrl2::runtime_error("rhs_traverser: implication is not supported!");
305 }
306
308 {
309 derived().enter(x);
311 derived().apply(x.body());
312 tr::make_forall(top(), x.variables(), top());
313 //pop_variables(x.variables());
314 derived().leave(x);
315 }
316
318 {
319 derived().enter(x);
321 derived().apply(x.body());
322 tr::make_exists(top(), x.variables(), top());
323 //pop_variables(x.variables());
324 derived().leave(x);
325 }
326
327 // This function is overridden in the structured variant of the algorithm
328 template <typename MustMayExpression>
329 pbes_expression apply_may_must_rhs(const MustMayExpression& x)
330 {
331 return RHS(x.operand(), parameters, TermTraits());
332 }
333
334 // This function is overridden in the structured variant of the algorithm
336 {
337 return p;
338 }
339
340 // share code between must and may
341 template <typename MustMayExpression>
342 void apply_may_must(const MustMayExpression& x, bool is_must)
343 {
344 bool timed = is_timed();
345 std::vector<pbes_expression> v;
346 pbes_expression rhs_phi = derived().apply_may_must_rhs(x);
347 assert(action_formulas::is_action_formula(x.formula()));
348 const action_formulas::action_formula& alpha = atermpp::down_cast<const action_formulas::action_formula>(x.formula());
349
350 for (const lps::action_summand& summand: parameters.lps.action_summands())
351 {
352 const data::data_expression& ci = summand.condition();
353 const lps::multi_action& ai = summand.multi_action();
354 const data::assignment_list& gi = summand.assignments();
355 const data::variable_list& yi = summand.summation_variables();
356
357 pbes_expression right = rhs_phi;
358 const data::data_expression& ti = ai.time();
359 pbes_expression sat = Sat(ai, alpha, parameters.id_generator, TermTraits());
361 for (const data::assignment& a: gi)
362 {
363 sigma[a.lhs()] = a.rhs();
364 }
365 pbes_expression left = tr::and_(sat, ci);
366
367 if (timed)
368 {
369 sigma[parameters.T] = ti;
370 left = tr::and_(left, data::greater(ti, parameters.T));
371 }
372
374
375 pbes_expression p = parameters.rhs_may_must(is_must, yi, left, right, ai, gi, TermTraits());
376 v.push_back(derived().apply_may_must_result(p));
377 }
378
379 pbes_expression result = is_must ? tr::join_and(v.begin(), v.end()) : tr::join_or(v.begin(), v.end());
380 push(result);
381 }
382
384 {
385 apply_may_must(x, true);
386 }
387
389 {
390 apply_may_must(x, false);
391 }
392
394 {
395 throw mcrl2::runtime_error("rhs_traverser: yaled is not supported!");
396 }
397
399 {
400 const data::data_expression& t = x.time_stamp();
401 std::vector<pbes_expression> v;
402 for (const lps::action_summand& i: parameters.lps.action_summands())
403 {
404 const data::data_expression& ci = i.condition();
405 const data::data_expression& ti = i.multi_action().time();
406 const data::variable_list& yi = i.summation_variables();
407 pbes_expression p = tr::forall(yi, tr::or_(data::not_(ci), data::greater(t, ti)));
408 v.push_back(p);
409 }
410 for (const lps::deadlock_summand& j: parameters.lps.deadlock_summands())
411 {
412 const data::data_expression& cj = j.condition();
413 const data::data_expression& tj = j.deadlock().time();
414 const data::variable_list& yj = j.summation_variables();
415 pbes_expression p = tr::forall(yj, tr::or_(data::not_(cj), data::greater(t, tj)));
416 v.push_back(p);
417 }
418 push(tr::and_(tr::join_or(v.begin(), v.end()), data::greater(t, parameters.T)));
419 }
420
422 {
423 throw mcrl2::runtime_error("rhs_traverser: delay is not supported!");
424 }
425
427 {
428 const data::data_expression& t = x.time_stamp();
429 std::vector<pbes_expression> v;
430 for (const lps::action_summand& i : parameters.lps.action_summands())
431 {
432 const data::data_expression& ci = i.condition();
433 data::data_expression ti = i.multi_action().time();
434 const data::variable_list& yi = i.summation_variables();
435 pbes_expression p = tr::exists(yi, tr::and_(ci, data::less_equal(t, ti)));
436 v.push_back(p);
437 }
438 for (const lps::deadlock_summand& j: parameters.lps.deadlock_summands())
439 {
440 const data::data_expression& cj = j.condition();
441 data::data_expression tj = j.deadlock().time();
442 const data::variable_list& yj = j.summation_variables();
443 pbes_expression p = tr::exists(yj, tr::and_(cj, data::less_equal(t, tj)));
444 v.push_back(p);
445 }
446 push(tr::or_(tr::join_or(v.begin(), v.end()), data::less_equal(t, parameters.T)));
447 }
448
450 {
451 const core::identifier_string& X = x.name();
453 data::variable_list xp = parameters.lps.process_parameters();
455 if (is_timed())
456 {
458 }
460 }
461
463 {
464 const core::identifier_string& X = x.name();
466 data::variable_list xp = parameters.lps.process_parameters();
468 if (is_timed())
469 {
471 }
473 }
474
476 {
477 const core::identifier_string& X = x.name();
479 data::variable_list xp = parameters.lps.process_parameters();
481 if (is_timed())
482 {
484 }
486 }
487};
488
489template <template <class, class, class> class Traverser, typename TermTraits, typename Parameters>
490struct 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 apply_rhs_traverser(Parameters& parameters, TermTraits tr)
498 : super(parameters, tr)
499 {}
500};
501
502template <typename TermTraits, typename Parameters>
503inline
504pbes_expression RHS(const state_formulas::state_formula& x, Parameters& parameters, TermTraits tr)
505{
507 f.apply(x);
508 return f.top();
509}
510
511//--- RHS_structured variant ---//
512
513template <typename TermTraits, typename Parameters>
514inline
515typename 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
523template <typename Derived, typename TermTraits, typename Parameters>
524struct rhs_structured_traverser: public rhs_traverser<Derived, TermTraits, Parameters>
525{
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;
538 using super::derived;
539
540 std::multiset<data::variable> variables;
542 std::vector<pbes_equation>& equations; // new equations that are generated on the fly
543
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 variables(variables_.begin(), variables_.end()),
552 sigma(sigma_),
553 equations(equations_)
554 {}
555
557 {
558 std::set<data::variable> fv = state_formulas::find_free_variables(x);
559 fv.insert(variables.begin(), variables.end());
560 return data::variable_list(fv.begin(), fv.end());
561 }
562
564 {
565 const data::variable_list& v = x.variables();
566 variables.insert(v.begin(), v.end());
567 }
568
570 {
571 for (const data::variable& var: x.variables())
572 {
573 variables.erase(var);
574 }
575 }
576
578 {
579 const data::variable_list& v = x.variables();
580 variables.insert(v.begin(), v.end());
581 }
582
584 {
585 for (const data::variable& var: x.variables())
586 {
587 variables.erase(var);
588 }
589 }
590
591 // override
592 template <typename MustMayExpression>
593 pbes_expression apply_may_must_rhs(const MustMayExpression& x)
594 {
595 return RHS_structured(x.operand(), parameters, rhs_structured_compute_variables(x.operand(), variables), sigma, equations, TermTraits());
596 }
597
598 // override
600 {
601 // generate a new equation 'Y(d) = p', and add Y(d) to v
602 core::identifier_string Y = parameters.id_generator("Y");
603 data::variable_list d(variables.begin(), variables.end());
604 propositional_variable Yd(Y, d);
605 pbes_equation eqn(sigma, Yd, p);
606 equations.push_back(eqn);
608 }
609
611 {
612 apply_may_must(x, true);
613 }
614
616 {
617 apply_may_must(x, false);
618 }
619};
620
621template <template <class, class, class> class Traverser, typename TermTraits, typename Parameters>
622struct 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 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 : super(parameters, variables, sigma, equations, tr)
636 {}
637};
638
639template <typename TermTraits, typename Parameters>
640inline
641typename 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{
650 f.apply(x);
651 return f.top();
652}
653
654} // namespace detail
655
656} // namespace pbes_system
657
658} // namespace mcrl2
659
660#endif // MCRL2_PBES_DETAIL_LPS2PBES_RHS_H
Term containing a string.
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:281
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:274
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
\brief Assignment of a data expression to a variable
Definition assignment.h:91
Generic substitution function. The substitution is stored as a mapping of variables to expressions....
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
\brief A sort expression
\brief A data variable
Definition variable.h:28
LPS summand containing a multi-action.
LPS summand containing a deadlock.
const std::vector< ActionSummand > & action_summands() const
Returns the sequence of action summands.
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
\brief A timed multi-action
multi_action(const multi_action &) noexcept=default
Move semantics.
const process::action_list & actions() const
const data::data_expression & time() const
static fixpoint_symbol nu()
Returns the nu symbol.
\brief A propositional variable instantiation
\brief A propositional variable declaration
Standard exception class for reporting runtime errors.
Definition exception.h:27
\brief The and operator for state formulas
\brief The timed delay operator for state formulas
const data::data_expression & time_stamp() const
\brief The delay operator for state formulas
\brief The existential quantification operator for state formulas
const state_formula & body() const
const data::variable_list & variables() const
\brief The value false for state formulas
\brief The universal quantification operator for state formulas
const state_formula & body() const
const data::variable_list & variables() const
\brief The implication operator for state formulas
\brief The may operator for state formulas
\brief The mu operator for state formulas
const core::identifier_string & name() const
\brief The must operator for state formulas
\brief The not operator for state formulas
\brief The nu operator for state formulas
const core::identifier_string & name() const
\brief The or operator for state formulas
\brief The value true for state formulas
\brief The state formula variable
const core::identifier_string & name() const
const data::data_expression_list & arguments() const
\brief The timed yaled operator for state formulas
const data::data_expression & time_stamp() const
\brief The yaled operator for state formulas
This file contains some functions that are present in all libraries except the data library....
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
add your file description here.
add your file description here.
bool is_action_formula(const atermpp::aterm_appl &x)
data_expression join_and(ForwardTraversalIterator first, ForwardTraversalIterator last)
Returns and applied to the sequence of data expressions [first, last)
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
Definition standard.h:277
data_expression not_(const data_expression &x)
data_expression_list make_data_expression_list(Container const &r, typename atermpp::enable_if_container< Container, data_expression >::type *=nullptr)
Converts an container with data expressions to data_expression_list.
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
atermpp::term_list< variable > variable_list
\brief list of variables
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
const data::variable & undefined_real_variable()
Returns a data variable that corresponds to 'undefined'.
Definition undefined.h:38
void replace_variables(T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
Definition replace.h:213
function_symbol greater(const sort_expression &s)
Constructor for function symbol >
Definition standard.h:314
data::mutable_map_substitution make_fresh_variable_substitution(const data::variable_list &variables, data::set_identifier_generator &id_generator, bool add_to_context=true)
Generates a substitution that assigns fresh variables to the given sequence of variables....
data::data_expression_list mu_expressions(const state_formulas::state_formula &f)
Returns the data expressions corresponding to ass(f)
data::variable pos(const std::string &name)
Returns a data variable of type Pos with a given name.
pbes_expression RHS(const state_formulas::state_formula &x, Parameters &parameters, TermTraits tr)
TermTraits::term_type Sat(const lps::multi_action &a, const action_formulas::action_formula &x, data::set_identifier_generator &id_generator, TermTraits tr)
data::variable_list Par(const core::identifier_string &X, const data::variable_list &l, const state_formulas::state_formula &x)
TermTraits::term_type RHS_structured(const state_formulas::state_formula &x, Parameters &parameters, const data::variable_list &variables, const fixpoint_symbol &sigma, std::vector< pbes_equation > &equations, TermTraits tr)
const pbes_expression & true_()
void replace_variables_capture_avoiding(T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
const pbes_expression & false_()
void find_free_variables(const T &x, OutputIterator o)
Definition find.h:322
std::string string_join(const Container &c, const std::string &separator)
Joins a sequence of strings. This is a replacement for boost::algorithm::join, since it gives stack o...
void number2string(std::size_t number, std::string &buffer, std::size_t start_position)
Convert a number to a string in the buffer starting at position start_position.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
add your file description here.
Substitution that maps data variables to data expressions. The substitution is stored as an assignmen...
apply_rhs_structured_traverser(Parameters &parameters, const data::variable_list &variables, const fixpoint_symbol &sigma, std::vector< pbes_equation > &equations, TermTraits tr)
Traverser< apply_rhs_structured_traverser< Traverser, TermTraits, Parameters >, TermTraits, Parameters > super
Traverser< apply_rhs_traverser< Traverser, TermTraits, Parameters >, TermTraits, Parameters > super
apply_rhs_traverser(Parameters &parameters, TermTraits tr)
std::string multi_action_name(const lps::multi_action &a) const
data::data_expression equal_to(const data::variable_list &d, const data::data_expression_list &e) const
std::map< lps::multi_action, propositional_variable > Zneg
lps2pbes_counter_example_parameters(const state_formulas::state_formula &phi0, const lps::stochastic_linear_process &lps, data::set_identifier_generator &id_generator, const data::variable &T)
std::map< lps::multi_action, propositional_variable > Zpos
data::variable_list action_variables(const process::action_list &actions) const
pbes_expression rhs_may_must(bool is_must, const data::variable_list &y, const pbes_expression &left, const pbes_expression &right, const lps::multi_action &ai, const data::assignment_list &gi, TermTraits)
data::data_expression_list action_expressions(const process::action_list &actions) const
pbes_expression rhs_may_must(bool is_must, const data::variable_list &y, const pbes_expression &left, const pbes_expression &right, const lps::multi_action &, const data::assignment_list &, TermTraits)
const state_formulas::state_formula & phi0
const lps::stochastic_linear_process & lps
lps2pbes_parameters(const state_formulas::state_formula &phi0_, const lps::stochastic_linear_process &lps_, data::set_identifier_generator &id_generator_, const data::variable &T_)
data::set_identifier_generator & id_generator
pbes_expression apply_may_must_rhs(const MustMayExpression &x)
void leave(const state_formulas::forall &x)
data::variable_list rhs_structured_compute_variables(const state_formulas::state_formula &x, const std::multiset< data::variable > &variables) const
void apply_may_must(const MustMayExpression &x, bool is_must)
void leave(const state_formulas::exists &x)
rhs_traverser< Derived, TermTraits, Parameters > super
rhs_structured_traverser(Parameters &parameters, const data::variable_list &variables_, const fixpoint_symbol &sigma_, std::vector< pbes_equation > &equations_, TermTraits tr)
void enter(const state_formulas::forall &x)
void enter(const state_formulas::exists &x)
pbes_expression apply_may_must_result(const pbes_expression &p)
void apply(const state_formulas::must &x)
void apply(const state_formulas::not_ &)
pbes_expression apply_may_must_rhs(const MustMayExpression &x)
void leave(const state_formulas::delay_timed &x)
void apply(const state_formulas::must &x)
void apply(const state_formulas::may &x)
state_formulas::state_formula_traverser< Derived > super
void push(const pbes_expression &x)
rhs_traverser(Parameters &parameters_, TermTraits)
void apply_may_must(const MustMayExpression &x, bool is_must)
void leave(const state_formulas::or_ &)
void leave(const state_formulas::yaled_timed &x)
void pop_variables(const data::variable_list &variables)
void apply(const state_formulas::forall &x)
void leave(const state_formulas::true_ &)
void apply(const state_formulas::mu &x)
void apply(const state_formulas::exists &x)
std::vector< pbes_expression > result_stack
void apply(const state_formulas::imp &)
void push_variables(const data::variable_list &variables)
void leave(const state_formulas::and_ &)
void apply(const state_formulas::nu &x)
pbes_expression apply_may_must_result(const pbes_expression &p)
void leave(const state_formulas::yaled &)
void leave(const state_formulas::false_ &)
void leave(const state_formulas::delay &)
const pbes_expression & top() const
void leave(const state_formulas::variable &x)
void leave(const data::data_expression &x)