LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - traverser.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 336 392 85.7 %
Date: 2024-03-08 02:52:28 Functions: 158 240 65.8 %
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/traverser.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_TRAVERSER_H
      13             : #define MCRL2_PBES_TRAVERSER_H
      14             : 
      15             : #include "mcrl2/pbes/pbes.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace pbes_system
      21             : {
      22             : 
      23             : /// \brief Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser.
      24             : template <typename Derived>
      25             : struct pbes_expression_traverser_base: public core::traverser<Derived>
      26             : {
      27             :   typedef core::traverser<Derived> super;
      28             :   using super::apply;
      29             :   using super::enter;
      30             :   using super::leave;
      31             : 
      32             :   void apply(pbes_expression& result, const data::data_expression& x)
      33             :   {
      34             :     static_cast<Derived&>(*this).enter(x);
      35             :     // skip
      36             :     static_cast<Derived&>(*this).leave(x);
      37             :     result=x;
      38             :   }
      39             : };
      40             : 
      41             : //--- start generated add_traverser_sort_expressions code ---//
      42             : template <template <class> class Traverser, class Derived>
      43             : struct add_traverser_sort_expressions: public Traverser<Derived>
      44             : {
      45             :   typedef Traverser<Derived> super;
      46             :   using super::enter;
      47             :   using super::leave;
      48             :   using super::apply;
      49             : 
      50        3075 :   void apply(const pbes_system::propositional_variable& x)
      51             :   {
      52        3075 :     static_cast<Derived&>(*this).enter(x);
      53        3075 :     static_cast<Derived&>(*this).apply(x.parameters());
      54        3075 :     static_cast<Derived&>(*this).leave(x);
      55        3075 :   }
      56             : 
      57        3075 :   void apply(const pbes_system::pbes_equation& x)
      58             :   {
      59        3075 :     static_cast<Derived&>(*this).enter(x);
      60        3075 :     static_cast<Derived&>(*this).apply(x.variable());
      61        3075 :     static_cast<Derived&>(*this).apply(x.formula());
      62        3075 :     static_cast<Derived&>(*this).leave(x);
      63        3075 :   }
      64             : 
      65         621 :   void apply(const pbes_system::pbes& x)
      66             :   {
      67         621 :     static_cast<Derived&>(*this).enter(x);
      68         621 :     static_cast<Derived&>(*this).apply(x.global_variables());
      69         621 :     static_cast<Derived&>(*this).apply(x.equations());
      70         621 :     static_cast<Derived&>(*this).apply(x.initial_state());
      71         621 :     static_cast<Derived&>(*this).leave(x);
      72         621 :   }
      73             : 
      74        1801 :   void apply(const pbes_system::propositional_variable_instantiation& x)
      75             :   {
      76        1801 :     static_cast<Derived&>(*this).enter(x);
      77        1801 :     static_cast<Derived&>(*this).apply(x.parameters());
      78        1801 :     static_cast<Derived&>(*this).leave(x);
      79        1801 :   }
      80             : 
      81         143 :   void apply(const pbes_system::not_& x)
      82             :   {
      83         143 :     static_cast<Derived&>(*this).enter(x);
      84         143 :     static_cast<Derived&>(*this).apply(x.operand());
      85         143 :     static_cast<Derived&>(*this).leave(x);
      86         143 :   }
      87             : 
      88         772 :   void apply(const pbes_system::and_& x)
      89             :   {
      90         772 :     static_cast<Derived&>(*this).enter(x);
      91         772 :     static_cast<Derived&>(*this).apply(x.left());
      92         772 :     static_cast<Derived&>(*this).apply(x.right());
      93         772 :     static_cast<Derived&>(*this).leave(x);
      94         772 :   }
      95             : 
      96         792 :   void apply(const pbes_system::or_& x)
      97             :   {
      98         792 :     static_cast<Derived&>(*this).enter(x);
      99         792 :     static_cast<Derived&>(*this).apply(x.left());
     100         792 :     static_cast<Derived&>(*this).apply(x.right());
     101         792 :     static_cast<Derived&>(*this).leave(x);
     102         792 :   }
     103             : 
     104         176 :   void apply(const pbes_system::imp& x)
     105             :   {
     106         176 :     static_cast<Derived&>(*this).enter(x);
     107         176 :     static_cast<Derived&>(*this).apply(x.left());
     108         176 :     static_cast<Derived&>(*this).apply(x.right());
     109         176 :     static_cast<Derived&>(*this).leave(x);
     110         176 :   }
     111             : 
     112         353 :   void apply(const pbes_system::forall& x)
     113             :   {
     114         353 :     static_cast<Derived&>(*this).enter(x);
     115         353 :     static_cast<Derived&>(*this).apply(x.variables());
     116         353 :     static_cast<Derived&>(*this).apply(x.body());
     117         353 :     static_cast<Derived&>(*this).leave(x);
     118         353 :   }
     119             : 
     120         190 :   void apply(const pbes_system::exists& x)
     121             :   {
     122         190 :     static_cast<Derived&>(*this).enter(x);
     123         190 :     static_cast<Derived&>(*this).apply(x.variables());
     124         190 :     static_cast<Derived&>(*this).apply(x.body());
     125         190 :     static_cast<Derived&>(*this).leave(x);
     126         190 :   }
     127             : 
     128       30058 :   void apply(const pbes_system::pbes_expression& x)
     129             :   {
     130       30058 :     static_cast<Derived&>(*this).enter(x);
     131       30058 :     if (data::is_data_expression(x))
     132             :     {
     133        8733 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     134             :     }
     135       21325 :     else if (data::is_variable(x))
     136             :     {
     137           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     138             :     }
     139       21325 :     else if (data::is_untyped_data_parameter(x))
     140             :     {
     141           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     142             :     }
     143       21325 :     else if (pbes_system::is_propositional_variable_instantiation(x))
     144             :     {
     145       10796 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
     146             :     }
     147       10529 :     else if (pbes_system::is_not(x))
     148             :     {
     149         165 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
     150             :     }
     151       10364 :     else if (pbes_system::is_and(x))
     152             :     {
     153        3996 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
     154             :     }
     155        6368 :     else if (pbes_system::is_or(x))
     156             :     {
     157        5320 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
     158             :     }
     159        1048 :     else if (pbes_system::is_imp(x))
     160             :     {
     161         194 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
     162             :     }
     163         854 :     else if (pbes_system::is_forall(x))
     164             :     {
     165         567 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
     166             :     }
     167         287 :     else if (pbes_system::is_exists(x))
     168             :     {
     169         287 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
     170             :     }
     171       30058 :     static_cast<Derived&>(*this).leave(x);
     172       30058 :   }
     173             : 
     174             : };
     175             : 
     176             : /// \\brief Traverser class
     177             : template <typename Derived>
     178             : struct sort_expression_traverser: public add_traverser_sort_expressions<data::sort_expression_traverser, Derived>
     179             : {
     180             : };
     181             : //--- end generated add_traverser_sort_expressions code ---//
     182             : 
     183             : //--- start generated add_traverser_data_expressions code ---//
     184             : template <template <class> class Traverser, class Derived>
     185             : struct add_traverser_data_expressions: public Traverser<Derived>
     186             : {
     187             :   typedef Traverser<Derived> super;
     188             :   using super::enter;
     189             :   using super::leave;
     190             :   using super::apply;
     191             : 
     192        1479 :   void apply(const pbes_system::pbes_equation& x)
     193             :   {
     194        1479 :     static_cast<Derived&>(*this).enter(x);
     195        1479 :     static_cast<Derived&>(*this).apply(x.formula());
     196        1479 :     static_cast<Derived&>(*this).leave(x);
     197        1479 :   }
     198             : 
     199         364 :   void apply(const pbes_system::pbes& x)
     200             :   {
     201         364 :     static_cast<Derived&>(*this).enter(x);
     202         364 :     static_cast<Derived&>(*this).apply(x.equations());
     203         364 :     static_cast<Derived&>(*this).apply(x.initial_state());
     204         364 :     static_cast<Derived&>(*this).leave(x);
     205         364 :   }
     206             : 
     207        6120 :   void apply(const pbes_system::propositional_variable_instantiation& x)
     208             :   {
     209        6120 :     static_cast<Derived&>(*this).enter(x);
     210        6120 :     static_cast<Derived&>(*this).apply(x.parameters());
     211        6120 :     static_cast<Derived&>(*this).leave(x);
     212        6120 :   }
     213             : 
     214          67 :   void apply(const pbes_system::not_& x)
     215             :   {
     216          67 :     static_cast<Derived&>(*this).enter(x);
     217          67 :     static_cast<Derived&>(*this).apply(x.operand());
     218          67 :     static_cast<Derived&>(*this).leave(x);
     219          67 :   }
     220             : 
     221        4544 :   void apply(const pbes_system::and_& x)
     222             :   {
     223        4544 :     static_cast<Derived&>(*this).enter(x);
     224        4544 :     static_cast<Derived&>(*this).apply(x.left());
     225        4544 :     static_cast<Derived&>(*this).apply(x.right());
     226        4544 :     static_cast<Derived&>(*this).leave(x);
     227        4544 :   }
     228             : 
     229        2487 :   void apply(const pbes_system::or_& x)
     230             :   {
     231        2487 :     static_cast<Derived&>(*this).enter(x);
     232        2487 :     static_cast<Derived&>(*this).apply(x.left());
     233        2487 :     static_cast<Derived&>(*this).apply(x.right());
     234        2487 :     static_cast<Derived&>(*this).leave(x);
     235        2487 :   }
     236             : 
     237        1097 :   void apply(const pbes_system::imp& x)
     238             :   {
     239        1097 :     static_cast<Derived&>(*this).enter(x);
     240        1097 :     static_cast<Derived&>(*this).apply(x.left());
     241        1097 :     static_cast<Derived&>(*this).apply(x.right());
     242        1097 :     static_cast<Derived&>(*this).leave(x);
     243        1097 :   }
     244             : 
     245         429 :   void apply(const pbes_system::forall& x)
     246             :   {
     247         429 :     static_cast<Derived&>(*this).enter(x);
     248         429 :     static_cast<Derived&>(*this).apply(x.body());
     249         429 :     static_cast<Derived&>(*this).leave(x);
     250         429 :   }
     251             : 
     252         888 :   void apply(const pbes_system::exists& x)
     253             :   {
     254         888 :     static_cast<Derived&>(*this).enter(x);
     255         888 :     static_cast<Derived&>(*this).apply(x.body());
     256         888 :     static_cast<Derived&>(*this).leave(x);
     257         888 :   }
     258             : 
     259       23196 :   void apply(const pbes_system::pbes_expression& x)
     260             :   {
     261       23196 :     static_cast<Derived&>(*this).enter(x);
     262       23196 :     if (data::is_data_expression(x))
     263             :     {
     264        7784 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     265             :     }
     266       15412 :     else if (data::is_variable(x))
     267             :     {
     268           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     269             :     }
     270       15412 :     else if (data::is_untyped_data_parameter(x))
     271             :     {
     272           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     273             :     }
     274       15412 :     else if (pbes_system::is_propositional_variable_instantiation(x))
     275             :     {
     276        5900 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
     277             :     }
     278        9512 :     else if (pbes_system::is_not(x))
     279             :     {
     280          67 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
     281             :     }
     282        9445 :     else if (pbes_system::is_and(x))
     283             :     {
     284        4544 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
     285             :     }
     286        4901 :     else if (pbes_system::is_or(x))
     287             :     {
     288        2487 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
     289             :     }
     290        2414 :     else if (pbes_system::is_imp(x))
     291             :     {
     292        1097 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
     293             :     }
     294        1317 :     else if (pbes_system::is_forall(x))
     295             :     {
     296         429 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
     297             :     }
     298         888 :     else if (pbes_system::is_exists(x))
     299             :     {
     300         888 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
     301             :     }
     302       23196 :     static_cast<Derived&>(*this).leave(x);
     303       23196 :   }
     304             : 
     305             : };
     306             : 
     307             : /// \\brief Traverser class
     308             : template <typename Derived>
     309             : struct data_expression_traverser: public add_traverser_data_expressions<data::data_expression_traverser, Derived>
     310             : {
     311             : };
     312             : //--- end generated add_traverser_data_expressions code ---//
     313             : 
     314             : //--- start generated add_traverser_pbes_expressions code ---//
     315             : template <template <class> class Traverser, class Derived>
     316             : struct add_traverser_pbes_expressions: public Traverser<Derived>
     317             : {
     318             :   typedef Traverser<Derived> super;
     319             :   using super::enter;
     320             :   using super::leave;
     321             :   using super::apply;
     322             : 
     323         336 :   void apply(const pbes_system::pbes_equation& x)
     324             :   {
     325         336 :     static_cast<Derived&>(*this).enter(x);
     326         336 :     static_cast<Derived&>(*this).apply(x.formula());
     327         336 :     static_cast<Derived&>(*this).leave(x);
     328         336 :   }
     329             : 
     330         172 :   void apply(const pbes_system::pbes& x)
     331             :   {
     332         172 :     static_cast<Derived&>(*this).enter(x);
     333         172 :     static_cast<Derived&>(*this).apply(x.equations());
     334         172 :     static_cast<Derived&>(*this).leave(x);
     335         172 :   }
     336             : 
     337        4642 :   void apply(const pbes_system::propositional_variable_instantiation& x)
     338             :   {
     339        4642 :     static_cast<Derived&>(*this).enter(x);
     340             :     // skip
     341        4642 :     static_cast<Derived&>(*this).leave(x);
     342        4642 :   }
     343             : 
     344         385 :   void apply(const pbes_system::not_& x)
     345             :   {
     346         385 :     static_cast<Derived&>(*this).enter(x);
     347         385 :     static_cast<Derived&>(*this).apply(x.operand());
     348         385 :     static_cast<Derived&>(*this).leave(x);
     349         385 :   }
     350             : 
     351       10328 :   void apply(const pbes_system::and_& x)
     352             :   {
     353       10328 :     static_cast<Derived&>(*this).enter(x);
     354       10328 :     static_cast<Derived&>(*this).apply(x.left());
     355       10328 :     static_cast<Derived&>(*this).apply(x.right());
     356       10328 :     static_cast<Derived&>(*this).leave(x);
     357       10328 :   }
     358             : 
     359        5781 :   void apply(const pbes_system::or_& x)
     360             :   {
     361        5781 :     static_cast<Derived&>(*this).enter(x);
     362        5781 :     static_cast<Derived&>(*this).apply(x.left());
     363        5781 :     static_cast<Derived&>(*this).apply(x.right());
     364        5781 :     static_cast<Derived&>(*this).leave(x);
     365        5781 :   }
     366             : 
     367        2104 :   void apply(const pbes_system::imp& x)
     368             :   {
     369        2104 :     static_cast<Derived&>(*this).enter(x);
     370        2104 :     static_cast<Derived&>(*this).apply(x.left());
     371        2104 :     static_cast<Derived&>(*this).apply(x.right());
     372        2104 :     static_cast<Derived&>(*this).leave(x);
     373        2104 :   }
     374             : 
     375        1097 :   void apply(const pbes_system::forall& x)
     376             :   {
     377        1097 :     static_cast<Derived&>(*this).enter(x);
     378        1097 :     static_cast<Derived&>(*this).apply(x.body());
     379        1097 :     static_cast<Derived&>(*this).leave(x);
     380        1097 :   }
     381             : 
     382        1535 :   void apply(const pbes_system::exists& x)
     383             :   {
     384        1535 :     static_cast<Derived&>(*this).enter(x);
     385        1535 :     static_cast<Derived&>(*this).apply(x.body());
     386        1535 :     static_cast<Derived&>(*this).leave(x);
     387        1535 :   }
     388             : 
     389       47134 :   void apply(const pbes_system::pbes_expression& x)
     390             :   {
     391       47134 :     static_cast<Derived&>(*this).enter(x);
     392       47134 :     if (data::is_data_expression(x))
     393             :     {
     394       11340 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     395             :     }
     396       35794 :     else if (data::is_variable(x))
     397             :     {
     398           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     399             :     }
     400       35794 :     else if (data::is_untyped_data_parameter(x))
     401             :     {
     402           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     403             :     }
     404       35794 :     else if (pbes_system::is_propositional_variable_instantiation(x))
     405             :     {
     406       14728 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
     407             :     }
     408       21066 :     else if (pbes_system::is_not(x))
     409             :     {
     410         385 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
     411             :     }
     412       20681 :     else if (pbes_system::is_and(x))
     413             :     {
     414       10260 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
     415             :     }
     416       10421 :     else if (pbes_system::is_or(x))
     417             :     {
     418        5681 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
     419             :     }
     420        4740 :     else if (pbes_system::is_imp(x))
     421             :     {
     422        2104 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
     423             :     }
     424        2636 :     else if (pbes_system::is_forall(x))
     425             :     {
     426        1097 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
     427             :     }
     428        1539 :     else if (pbes_system::is_exists(x))
     429             :     {
     430        1539 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
     431             :     }
     432       47134 :     static_cast<Derived&>(*this).leave(x);
     433       47134 :   }
     434             : 
     435             : };
     436             : 
     437             : /// \\brief Traverser class
     438             : template <typename Derived>
     439             : struct pbes_expression_traverser: public add_traverser_pbes_expressions<pbes_system::pbes_expression_traverser_base, Derived>
     440             : {
     441             : };
     442             : //--- end generated add_traverser_pbes_expressions code ---//
     443             : 
     444             : //--- start generated add_traverser_variables code ---//
     445             : template <template <class> class Traverser, class Derived>
     446             : struct add_traverser_variables: public Traverser<Derived>
     447             : {
     448             :   typedef Traverser<Derived> super;
     449             :   using super::enter;
     450             :   using super::leave;
     451             :   using super::apply;
     452             : 
     453           1 :   void apply(const pbes_system::propositional_variable& x)
     454             :   {
     455           1 :     static_cast<Derived&>(*this).enter(x);
     456           1 :     static_cast<Derived&>(*this).apply(x.parameters());
     457           1 :     static_cast<Derived&>(*this).leave(x);
     458           1 :   }
     459             : 
     460           1 :   void apply(const pbes_system::pbes_equation& x)
     461             :   {
     462           1 :     static_cast<Derived&>(*this).enter(x);
     463           1 :     static_cast<Derived&>(*this).apply(x.variable());
     464           1 :     static_cast<Derived&>(*this).apply(x.formula());
     465           1 :     static_cast<Derived&>(*this).leave(x);
     466           1 :   }
     467             : 
     468           1 :   void apply(const pbes_system::pbes& x)
     469             :   {
     470           1 :     static_cast<Derived&>(*this).enter(x);
     471           1 :     static_cast<Derived&>(*this).apply(x.global_variables());
     472           1 :     static_cast<Derived&>(*this).apply(x.equations());
     473           1 :     static_cast<Derived&>(*this).apply(x.initial_state());
     474           1 :     static_cast<Derived&>(*this).leave(x);
     475           1 :   }
     476             : 
     477           4 :   void apply(const pbes_system::propositional_variable_instantiation& x)
     478             :   {
     479           4 :     static_cast<Derived&>(*this).enter(x);
     480           4 :     static_cast<Derived&>(*this).apply(x.parameters());
     481           4 :     static_cast<Derived&>(*this).leave(x);
     482           4 :   }
     483             : 
     484           0 :   void apply(const pbes_system::not_& x)
     485             :   {
     486           0 :     static_cast<Derived&>(*this).enter(x);
     487           0 :     static_cast<Derived&>(*this).apply(x.operand());
     488           0 :     static_cast<Derived&>(*this).leave(x);
     489           0 :   }
     490             : 
     491           2 :   void apply(const pbes_system::and_& x)
     492             :   {
     493           2 :     static_cast<Derived&>(*this).enter(x);
     494           2 :     static_cast<Derived&>(*this).apply(x.left());
     495           2 :     static_cast<Derived&>(*this).apply(x.right());
     496           2 :     static_cast<Derived&>(*this).leave(x);
     497           2 :   }
     498             : 
     499           0 :   void apply(const pbes_system::or_& x)
     500             :   {
     501           0 :     static_cast<Derived&>(*this).enter(x);
     502           0 :     static_cast<Derived&>(*this).apply(x.left());
     503           0 :     static_cast<Derived&>(*this).apply(x.right());
     504           0 :     static_cast<Derived&>(*this).leave(x);
     505           0 :   }
     506             : 
     507           0 :   void apply(const pbes_system::imp& x)
     508             :   {
     509           0 :     static_cast<Derived&>(*this).enter(x);
     510           0 :     static_cast<Derived&>(*this).apply(x.left());
     511           0 :     static_cast<Derived&>(*this).apply(x.right());
     512           0 :     static_cast<Derived&>(*this).leave(x);
     513           0 :   }
     514             : 
     515           0 :   void apply(const pbes_system::forall& x)
     516             :   {
     517           0 :     static_cast<Derived&>(*this).enter(x);
     518           0 :     static_cast<Derived&>(*this).apply(x.variables());
     519           0 :     static_cast<Derived&>(*this).apply(x.body());
     520           0 :     static_cast<Derived&>(*this).leave(x);
     521           0 :   }
     522             : 
     523           1 :   void apply(const pbes_system::exists& x)
     524             :   {
     525           1 :     static_cast<Derived&>(*this).enter(x);
     526           1 :     static_cast<Derived&>(*this).apply(x.variables());
     527           1 :     static_cast<Derived&>(*this).apply(x.body());
     528           1 :     static_cast<Derived&>(*this).leave(x);
     529           1 :   }
     530             : 
     531           7 :   void apply(const pbes_system::pbes_expression& x)
     532             :   {
     533           7 :     static_cast<Derived&>(*this).enter(x);
     534           7 :     if (data::is_data_expression(x))
     535             :     {
     536           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     537             :     }
     538           6 :     else if (data::is_variable(x))
     539             :     {
     540           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     541             :     }
     542           6 :     else if (data::is_untyped_data_parameter(x))
     543             :     {
     544           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     545             :     }
     546           6 :     else if (pbes_system::is_propositional_variable_instantiation(x))
     547             :     {
     548           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
     549             :     }
     550           3 :     else if (pbes_system::is_not(x))
     551             :     {
     552           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
     553             :     }
     554           3 :     else if (pbes_system::is_and(x))
     555             :     {
     556           2 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
     557             :     }
     558           1 :     else if (pbes_system::is_or(x))
     559             :     {
     560           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
     561             :     }
     562           1 :     else if (pbes_system::is_imp(x))
     563             :     {
     564           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
     565             :     }
     566           1 :     else if (pbes_system::is_forall(x))
     567             :     {
     568           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
     569             :     }
     570           1 :     else if (pbes_system::is_exists(x))
     571             :     {
     572           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
     573             :     }
     574           7 :     static_cast<Derived&>(*this).leave(x);
     575           7 :   }
     576             : 
     577             : };
     578             : 
     579             : /// \\brief Traverser class
     580             : template <typename Derived>
     581             : struct variable_traverser: public add_traverser_variables<data::variable_traverser, Derived>
     582             : {
     583             : };
     584             : //--- end generated add_traverser_variables code ---//
     585             : 
     586             : //--- start generated add_traverser_identifier_strings code ---//
     587             : template <template <class> class Traverser, class Derived>
     588             : struct add_traverser_identifier_strings: public Traverser<Derived>
     589             : {
     590             :   typedef Traverser<Derived> super;
     591             :   using super::enter;
     592             :   using super::leave;
     593             :   using super::apply;
     594             : 
     595           0 :   void apply(const pbes_system::propositional_variable& x)
     596             :   {
     597           0 :     static_cast<Derived&>(*this).enter(x);
     598           0 :     static_cast<Derived&>(*this).apply(x.name());
     599           0 :     static_cast<Derived&>(*this).apply(x.parameters());
     600           0 :     static_cast<Derived&>(*this).leave(x);
     601           0 :   }
     602             : 
     603           0 :   void apply(const pbes_system::pbes_equation& x)
     604             :   {
     605           0 :     static_cast<Derived&>(*this).enter(x);
     606           0 :     static_cast<Derived&>(*this).apply(x.variable());
     607           0 :     static_cast<Derived&>(*this).apply(x.formula());
     608           0 :     static_cast<Derived&>(*this).leave(x);
     609           0 :   }
     610             : 
     611           0 :   void apply(const pbes_system::pbes& x)
     612             :   {
     613           0 :     static_cast<Derived&>(*this).enter(x);
     614           0 :     static_cast<Derived&>(*this).apply(x.global_variables());
     615           0 :     static_cast<Derived&>(*this).apply(x.equations());
     616           0 :     static_cast<Derived&>(*this).apply(x.initial_state());
     617           0 :     static_cast<Derived&>(*this).leave(x);
     618           0 :   }
     619             : 
     620         487 :   void apply(const pbes_system::propositional_variable_instantiation& x)
     621             :   {
     622         487 :     static_cast<Derived&>(*this).enter(x);
     623         487 :     static_cast<Derived&>(*this).apply(x.name());
     624         487 :     static_cast<Derived&>(*this).apply(x.parameters());
     625         487 :     static_cast<Derived&>(*this).leave(x);
     626         487 :   }
     627             : 
     628          50 :   void apply(const pbes_system::not_& x)
     629             :   {
     630          50 :     static_cast<Derived&>(*this).enter(x);
     631          50 :     static_cast<Derived&>(*this).apply(x.operand());
     632          50 :     static_cast<Derived&>(*this).leave(x);
     633          50 :   }
     634             : 
     635         139 :   void apply(const pbes_system::and_& x)
     636             :   {
     637         139 :     static_cast<Derived&>(*this).enter(x);
     638         139 :     static_cast<Derived&>(*this).apply(x.left());
     639         139 :     static_cast<Derived&>(*this).apply(x.right());
     640         139 :     static_cast<Derived&>(*this).leave(x);
     641         139 :   }
     642             : 
     643          61 :   void apply(const pbes_system::or_& x)
     644             :   {
     645          61 :     static_cast<Derived&>(*this).enter(x);
     646          61 :     static_cast<Derived&>(*this).apply(x.left());
     647          61 :     static_cast<Derived&>(*this).apply(x.right());
     648          61 :     static_cast<Derived&>(*this).leave(x);
     649          61 :   }
     650             : 
     651           3 :   void apply(const pbes_system::imp& x)
     652             :   {
     653           3 :     static_cast<Derived&>(*this).enter(x);
     654           3 :     static_cast<Derived&>(*this).apply(x.left());
     655           3 :     static_cast<Derived&>(*this).apply(x.right());
     656           3 :     static_cast<Derived&>(*this).leave(x);
     657           3 :   }
     658             : 
     659          30 :   void apply(const pbes_system::forall& x)
     660             :   {
     661          30 :     static_cast<Derived&>(*this).enter(x);
     662          30 :     static_cast<Derived&>(*this).apply(x.variables());
     663          30 :     static_cast<Derived&>(*this).apply(x.body());
     664          30 :     static_cast<Derived&>(*this).leave(x);
     665          30 :   }
     666             : 
     667          28 :   void apply(const pbes_system::exists& x)
     668             :   {
     669          28 :     static_cast<Derived&>(*this).enter(x);
     670          28 :     static_cast<Derived&>(*this).apply(x.variables());
     671          28 :     static_cast<Derived&>(*this).apply(x.body());
     672          28 :     static_cast<Derived&>(*this).leave(x);
     673          28 :   }
     674             : 
     675        1439 :   void apply(const pbes_system::pbes_expression& x)
     676             :   {
     677        1439 :     static_cast<Derived&>(*this).enter(x);
     678        1439 :     if (data::is_data_expression(x))
     679             :     {
     680         641 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     681             :     }
     682         798 :     else if (data::is_variable(x))
     683             :     {
     684           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     685             :     }
     686         798 :     else if (data::is_untyped_data_parameter(x))
     687             :     {
     688           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     689             :     }
     690         798 :     else if (pbes_system::is_propositional_variable_instantiation(x))
     691             :     {
     692         487 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
     693             :     }
     694         311 :     else if (pbes_system::is_not(x))
     695             :     {
     696          50 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
     697             :     }
     698         261 :     else if (pbes_system::is_and(x))
     699             :     {
     700         139 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
     701             :     }
     702         122 :     else if (pbes_system::is_or(x))
     703             :     {
     704          61 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
     705             :     }
     706          61 :     else if (pbes_system::is_imp(x))
     707             :     {
     708           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
     709             :     }
     710          58 :     else if (pbes_system::is_forall(x))
     711             :     {
     712          30 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
     713             :     }
     714          28 :     else if (pbes_system::is_exists(x))
     715             :     {
     716          28 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
     717             :     }
     718        1439 :     static_cast<Derived&>(*this).leave(x);
     719        1439 :   }
     720             : 
     721             : };
     722             : 
     723             : /// \\brief Traverser class
     724             : template <typename Derived>
     725             : struct identifier_string_traverser: public add_traverser_identifier_strings<data::identifier_string_traverser, Derived>
     726             : {
     727             : };
     728             : //--- end generated add_traverser_identifier_strings code ---//
     729             : 
     730             : } // namespace pbes_system
     731             : 
     732             : } // namespace mcrl2
     733             : 
     734             : #endif // MCRL2_PBES_TRAVERSER_H

Generated by: LCOV version 1.14