LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/detail - lps2pbes_e.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 86 134 64.2 %
Date: 2020-09-16 00:45:56 Functions: 42 248 16.9 %
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_e.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_LPS2PBES_E_H
      13             : #define MCRL2_PBES_DETAIL_LPS2PBES_E_H
      14             : 
      15             : #include "mcrl2/pbes/detail/lps2pbes_rhs.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace pbes_system {
      20             : 
      21             : namespace detail {
      22             : 
      23             : template <typename TermTraits, typename Parameters>
      24             : void E(const state_formulas::state_formula& x,
      25             :        Parameters& parameters,
      26             :        std::vector<pbes_equation>& result,
      27             :        TermTraits tr
      28             :       );
      29             : 
      30             : template <typename Derived, typename TermTraits, typename Parameters>
      31         303 : struct e_traverser: public state_formulas::state_formula_traverser<Derived>
      32             : {
      33             :   typedef state_formulas::state_formula_traverser<Derived> super;
      34             :   using super::enter;
      35             :   using super::leave;
      36             :   using super::apply;
      37             : 
      38             :   typedef std::vector<pbes_equation> result_type;
      39             : 
      40             :   Parameters& parameters;
      41             :   std::vector<result_type> result_stack;
      42             : 
      43         303 :   e_traverser(Parameters& parameters_, TermTraits)
      44         303 :     : parameters(parameters_)
      45         303 :   {}
      46             : 
      47             :   Derived& derived()
      48             :   {
      49             :     return static_cast<Derived&>(*this);
      50             :   }
      51             : 
      52         481 :   void push(const result_type& x)
      53             :   {
      54         481 :     result_stack.push_back(x);
      55         481 :   }
      56             : 
      57         784 :   result_type& top()
      58             :   {
      59         784 :     return result_stack.back();
      60             :   }
      61             : 
      62             :   const result_type& top() const
      63             :   {
      64             :     return result_stack.back();
      65             :   }
      66             : 
      67         178 :   result_type pop()
      68             :   {
      69         178 :     result_type result = top();
      70         178 :     result_stack.pop_back();
      71         178 :     return result;
      72             :   }
      73             : 
      74         170 :   bool is_timed() const
      75             :   {
      76         170 :     return parameters.T != data::undefined_real_variable();
      77             :   }
      78             : 
      79             :   // the empty equation list
      80         222 :   result_type epsilon() const
      81             :   {
      82         222 :     return result_type();
      83             :   }
      84             : 
      85          16 :   void leave(const data::data_expression&)
      86             :   {
      87          16 :     push(epsilon());
      88          16 :   }
      89             : 
      90          62 :   void leave(const state_formulas::true_&)
      91             :   {
      92          62 :     push(epsilon());
      93          62 :   }
      94             : 
      95          59 :   void leave(const state_formulas::false_&)
      96             :   {
      97          59 :     push(epsilon());
      98          59 :   }
      99             : 
     100           0 :   void apply(const state_formulas::not_&)
     101             :   {
     102           0 :     throw mcrl2::runtime_error("e_traverser: negation is not supported!");
     103             :   }
     104             : 
     105          49 :   void leave(const state_formulas::and_&)
     106             :   {
     107          98 :     std::vector<pbes_equation> right = pop();
     108          98 :     std::vector<pbes_equation> left = pop();
     109          49 :     push(left + right);
     110          49 :   }
     111             : 
     112          40 :   void leave(const state_formulas::or_&)
     113             :   {
     114          80 :     std::vector<pbes_equation> right = pop();
     115          80 :     std::vector<pbes_equation> left = pop();
     116          40 :     push(left + right);
     117          40 :   }
     118             : 
     119           0 :   void apply(const state_formulas::imp&)
     120             :   {
     121           0 :     throw mcrl2::runtime_error("e_traverser: implication is not supported!");
     122             :   }
     123             : 
     124          11 :   void leave(const state_formulas::forall&)
     125             :   {
     126             :     // skip
     127          11 :   }
     128             : 
     129           4 :   void leave(const state_formulas::exists&)
     130             :   {
     131             :     // skip
     132           4 :   }
     133             : 
     134         111 :   void leave(const state_formulas::must&)
     135             :   {
     136             :     // skip
     137         111 :   }
     138             : 
     139          86 :   void leave(const state_formulas::may&)
     140             :   {
     141             :     // skip
     142          86 :   }
     143             : 
     144           0 :   void leave(const state_formulas::yaled&)
     145             :   {
     146           0 :     push(epsilon());
     147           0 :   }
     148             : 
     149           2 :   void leave(const state_formulas::yaled_timed&)
     150             :   {
     151           2 :     push(epsilon());
     152           2 :   }
     153             : 
     154           0 :   void leave(const state_formulas::delay&)
     155             :   {
     156           0 :     push(epsilon());
     157           0 :   }
     158             : 
     159           2 :   void leave(const state_formulas::delay_timed&)
     160             :   {
     161           2 :     push(epsilon());
     162           2 :   }
     163             : 
     164          81 :   void leave(const state_formulas::variable&)
     165             :   {
     166          81 :     push(epsilon());
     167          81 :   }
     168             : 
     169             :   template <typename Expr>
     170         170 :   void apply_mu_nu(const Expr& x, const fixpoint_symbol& sigma)
     171             :   {
     172         170 :     const core::identifier_string& X = x.name();
     173         340 :     data::variable_list xf = detail::mu_variables(x);
     174         340 :     data::variable_list xp = parameters.lps.process_parameters();
     175         170 :     const state_formulas::state_formula& phi = x.operand();
     176         340 :     data::variable_list e = xf + xp + Par(X, data::variable_list(), parameters.phi0);
     177         170 :     if (is_timed())
     178             :     {
     179           6 :       e.push_front(parameters.T);
     180             :     }
     181         340 :     propositional_variable v(X, e);
     182         340 :     pbes_expression expr = detail::RHS(phi, parameters, TermTraits());
     183         340 :     pbes_equation eqn(sigma, v, expr);
     184         340 :     std::vector<pbes_equation> result = { eqn };
     185         170 :     E(phi, parameters, result, TermTraits());
     186         170 :     push(result);
     187         170 :   }
     188             : 
     189         132 :   void apply(const state_formulas::nu& x)
     190             :   {
     191         132 :     apply_mu_nu(x, fixpoint_symbol::nu());
     192         132 :     mCRL2log(log::debug1, "lps2pbes") << "E(" << x << ") = " << core::detail::print_list(top()) << std::endl;
     193         132 :   }
     194             : 
     195          38 :   void apply(const state_formulas::mu& x)
     196             :   {
     197          38 :     apply_mu_nu(x, fixpoint_symbol::mu());
     198          38 :     mCRL2log(log::debug1, "lps2pbes") << "E(" << x << ") = " << core::detail::print_list(top()) << std::endl;
     199          38 :   }
     200             : };
     201             : 
     202             : template <template <class, class, class> class Traverser, typename TermTraits, typename Parameters>
     203         303 : struct apply_e_traverser: public Traverser<apply_e_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters>
     204             : {
     205             :   typedef Traverser<apply_e_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters> super;
     206             :   using super::enter;
     207             :   using super::leave;
     208             :   using super::apply;
     209             : 
     210         303 :   apply_e_traverser(Parameters& parameters, TermTraits tr)
     211         303 :     : super(parameters, tr)
     212         303 :   {}
     213             : };
     214             : 
     215             : template <typename TermTraits, typename Parameters>
     216         303 : void E(const state_formulas::state_formula& x, Parameters& parameters, std::vector<pbes_equation>& result, TermTraits tr)
     217             : {
     218         606 :   apply_e_traverser<e_traverser, TermTraits, Parameters> f(parameters, tr);
     219         303 :   f.apply(x);
     220         303 :   assert(f.result_stack.size() == 1);
     221         303 :   result.insert(result.end(), f.top().begin(), f.top().end());
     222         303 : }
     223             : 
     224             : template <typename TermTraits, typename Parameters>
     225             : void E_structured(const state_formulas::state_formula& x,
     226             :                   Parameters& parameters,
     227             :                   std::vector<pbes_equation>& result,
     228             :                   TermTraits tr
     229             :                  );
     230             : 
     231             : template <typename Derived, typename TermTraits, typename Parameters>
     232           0 : struct e_structured_traverser: public e_traverser<Derived, TermTraits, Parameters>
     233             : {
     234             :   typedef e_traverser<Derived, TermTraits, Parameters> super;
     235             :   using super::enter;
     236             :   using super::leave;
     237             :   using super::apply;
     238             :   using super::push;
     239             :   using super::top;
     240             :   using super::pop;
     241             :   using super::is_timed;
     242             :   using super::epsilon;
     243             :   using super::parameters;
     244             : 
     245             :   // typedef std::vector<pbes_equation> result_type;
     246             : 
     247           0 :   e_structured_traverser(Parameters& parameters,
     248             :                          TermTraits tr
     249             :                         )
     250           0 :     : super(parameters, tr)
     251           0 :   {}
     252             : 
     253             :   Derived& derived()
     254             :   {
     255             :     return static_cast<Derived&>(*this);
     256             :   }
     257             : 
     258             :   template <typename Expr>
     259           0 :   void apply_mu_nu(const Expr& x, const fixpoint_symbol& sigma)
     260             :   {
     261           0 :     const core::identifier_string& X = x.name();
     262           0 :     data::variable_list xf = detail::mu_variables(x);
     263           0 :     data::variable_list xp = parameters.lps.process_parameters();
     264           0 :     const state_formulas::state_formula& phi = x.operand();
     265           0 :     data::variable_list d = xf + xp + Par(X, data::variable_list(), parameters.phi0);
     266           0 :     if (is_timed())  
     267             :     {
     268           0 :       d.push_front(parameters.T);
     269             :     }
     270           0 :     data::data_expression_list e = data::make_data_expression_list(d);
     271           0 :     propositional_variable v(X, d);
     272           0 :     std::vector<pbes_equation> equations;
     273           0 :     pbes_expression expr = detail::RHS_structured(phi, parameters, d, sigma, equations, TermTraits());
     274           0 :     pbes_equation eqn(sigma, v, expr);
     275           0 :     std::vector<pbes_equation> result = { eqn };
     276           0 :     result.insert(result.end(), equations.begin(), equations.end());
     277           0 :     E_structured(phi, parameters, result, TermTraits());
     278           0 :     push(result);
     279           0 :   }
     280             : 
     281           0 :   void apply(const state_formulas::nu& x)
     282             :   {
     283           0 :     apply_mu_nu(x, fixpoint_symbol::nu());
     284           0 :   }
     285             : 
     286           0 :   void apply(const state_formulas::mu& x)
     287             :   {
     288           0 :     apply_mu_nu(x, fixpoint_symbol::mu());
     289           0 :   }
     290             : };
     291             : 
     292             : template <template <class, class, class> class Traverser, typename TermTraits, typename Parameters>
     293           0 : struct apply_e_structured_traverser: public Traverser<apply_e_structured_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters>
     294             : {
     295             :   typedef Traverser<apply_e_structured_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters> super;
     296             :   using super::enter;
     297             :   using super::leave;
     298             :   using super::apply;
     299             : 
     300           0 :   apply_e_structured_traverser(Parameters& parameters,
     301             :                                TermTraits tr
     302             :                               )
     303           0 :     : super(parameters, tr)
     304           0 :   {}
     305             : };
     306             : 
     307             : template <typename TermTraits, typename Parameters>
     308           0 : void E_structured(const state_formulas::state_formula& x,
     309             :                   Parameters& parameters,
     310             :                   std::vector<pbes_equation>& result,
     311             :                   TermTraits tr
     312             :                  )
     313             : {
     314           0 :   apply_e_structured_traverser<e_structured_traverser, TermTraits, Parameters> f(parameters, tr);
     315           0 :   f.apply(x);
     316           0 :   assert(f.result_stack.size() == 1);
     317           0 :   result.insert(result.end(), f.top().begin(), f.top().end());
     318           0 : }
     319             : 
     320             : } // namespace detail
     321             : 
     322             : } // namespace pbes_system
     323             : 
     324             : } // namespace mcrl2
     325             : 
     326             : #endif // MCRL2_PBES_DETAIL_LPS2PBES_E_H

Generated by: LCOV version 1.13