LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/detail - lps2pbes_rhs.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 213 288 74.0 %
Date: 2024-03-08 02:52:28 Functions: 51 290 17.6 %
Legend: Lines: hit not hit

          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

Generated by: LCOV version 1.14