LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - builder.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 214 220 97.3 %
Date: 2020-09-16 00:45:56 Functions: 140 275 50.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/builder.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_BUILDER_H
      13             : #define MCRL2_PBES_BUILDER_H
      14             : 
      15             : #include "mcrl2/data/builder.h"
      16             : #include "mcrl2/pbes/pbes.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace pbes_system
      22             : {
      23             : 
      24             : /// \brief Builder class
      25             : template <typename Derived>
      26             : struct pbes_expression_builder_base: public core::builder<Derived>
      27             : {
      28             :   typedef core::builder<Derived> super;
      29             :   using super::enter;
      30             :   using super::leave;
      31             :   using super::update;
      32             :   using super::apply;
      33             :         
      34        1191 :   data::data_expression apply(const data::data_expression& x)
      35             :   {
      36        1191 :     return x;
      37             :   }
      38             : };
      39             : 
      40             : // Adds sort expression traversal to a builder
      41             : //--- start generated add_sort_expressions code ---//
      42             : template <template <class> class Builder, class Derived>
      43             : struct add_sort_expressions: public Builder<Derived>
      44             : {
      45             :   typedef Builder<Derived> super;
      46             :   using super::enter;
      47             :   using super::leave;
      48             :   using super::update;
      49             :   using super::apply;
      50             : 
      51        2818 :   pbes_system::propositional_variable apply(const pbes_system::propositional_variable& x)
      52             :   {
      53        2818 :     static_cast<Derived&>(*this).enter(x);
      54        2818 :     pbes_system::propositional_variable result = pbes_system::propositional_variable(x.name(), static_cast<Derived&>(*this).apply(x.parameters()));
      55        2818 :     static_cast<Derived&>(*this).leave(x);
      56        2818 :     return result;
      57             :   }
      58             : 
      59        2817 :   void update(pbes_system::pbes_equation& x)
      60             :   {
      61        2817 :     static_cast<Derived&>(*this).enter(x);
      62        2817 :     x.variable() = static_cast<Derived&>(*this).apply(x.variable());
      63        2817 :     x.formula() = static_cast<Derived&>(*this).apply(x.formula());
      64        2817 :     static_cast<Derived&>(*this).leave(x);
      65        2817 :   }
      66             : 
      67         471 :   void update(pbes_system::pbes& x)
      68             :   {
      69         471 :     static_cast<Derived&>(*this).enter(x);
      70         471 :     static_cast<Derived&>(*this).update(x.equations());
      71         471 :     static_cast<Derived&>(*this).update(x.global_variables());
      72         471 :     x.initial_state() = static_cast<Derived&>(*this).apply(x.initial_state());
      73         471 :     static_cast<Derived&>(*this).leave(x);
      74         471 :   }
      75             : 
      76         473 :   pbes_system::propositional_variable_instantiation apply(const pbes_system::propositional_variable_instantiation& x)
      77             :   {
      78         473 :     static_cast<Derived&>(*this).enter(x);
      79         473 :     pbes_system::propositional_variable_instantiation result = pbes_system::propositional_variable_instantiation(x.name(), static_cast<Derived&>(*this).apply(x.parameters()));
      80         473 :     static_cast<Derived&>(*this).leave(x);
      81         473 :     return result;
      82             :   }
      83             : 
      84         143 :   pbes_system::not_ apply(const pbes_system::not_& x)
      85             :   {
      86         143 :     static_cast<Derived&>(*this).enter(x);
      87         143 :     pbes_system::not_ result = pbes_system::not_(static_cast<Derived&>(*this).apply(x.operand()));
      88         143 :     static_cast<Derived&>(*this).leave(x);
      89         143 :     return result;
      90             :   }
      91             : 
      92         429 :   pbes_system::and_ apply(const pbes_system::and_& x)
      93             :   {
      94         429 :     static_cast<Derived&>(*this).enter(x);
      95         429 :     pbes_system::and_ result = pbes_system::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
      96         429 :     static_cast<Derived&>(*this).leave(x);
      97         429 :     return result;
      98             :   }
      99             : 
     100         389 :   pbes_system::or_ apply(const pbes_system::or_& x)
     101             :   {
     102         389 :     static_cast<Derived&>(*this).enter(x);
     103         389 :     pbes_system::or_ result = pbes_system::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     104         389 :     static_cast<Derived&>(*this).leave(x);
     105         389 :     return result;
     106             :   }
     107             : 
     108         176 :   pbes_system::imp apply(const pbes_system::imp& x)
     109             :   {
     110         176 :     static_cast<Derived&>(*this).enter(x);
     111         176 :     pbes_system::imp result = pbes_system::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     112         176 :     static_cast<Derived&>(*this).leave(x);
     113         176 :     return result;
     114             :   }
     115             : 
     116         218 :   pbes_system::forall apply(const pbes_system::forall& x)
     117             :   {
     118         218 :     static_cast<Derived&>(*this).enter(x);
     119         218 :     pbes_system::forall result = pbes_system::forall(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
     120         218 :     static_cast<Derived&>(*this).leave(x);
     121         218 :     return result;
     122             :   }
     123             : 
     124         117 :   pbes_system::exists apply(const pbes_system::exists& x)
     125             :   {
     126         117 :     static_cast<Derived&>(*this).enter(x);
     127         117 :     pbes_system::exists result = pbes_system::exists(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
     128         117 :     static_cast<Derived&>(*this).leave(x);
     129         117 :     return result;
     130             :   }
     131             : 
     132        5285 :   pbes_system::pbes_expression apply(const pbes_system::pbes_expression& x)
     133             :   {
     134        5285 :     static_cast<Derived&>(*this).enter(x);
     135        5285 :     pbes_system::pbes_expression result;
     136        5285 :     if (data::is_data_expression(x))
     137             :     {
     138        2986 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     139             :     }
     140        2299 :     else if (pbes_system::is_propositional_variable_instantiation(x))
     141             :     {
     142           2 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
     143             :     }
     144        2297 :     else if (pbes_system::is_not(x))
     145             :     {
     146         143 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
     147             :     }
     148        2154 :     else if (pbes_system::is_and(x))
     149             :     {
     150         429 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
     151             :     }
     152        1725 :     else if (pbes_system::is_or(x))
     153             :     {
     154         389 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
     155             :     }
     156        1336 :     else if (pbes_system::is_imp(x))
     157             :     {
     158         176 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
     159             :     }
     160        1160 :     else if (pbes_system::is_forall(x))
     161             :     {
     162         218 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
     163             :     }
     164         942 :     else if (pbes_system::is_exists(x))
     165             :     {
     166         117 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
     167             :     }
     168         825 :     else if (data::is_variable(x))
     169             :     {
     170           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     171             :     }
     172         825 :     else if (data::is_untyped_data_parameter(x))
     173             :     {
     174         825 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     175             :     }
     176        5285 :     static_cast<Derived&>(*this).leave(x);
     177        5285 :     return result;
     178             :   }
     179             : 
     180             : };
     181             : 
     182             : /// \brief Builder class
     183             : template <typename Derived>
     184             : struct sort_expression_builder: public add_sort_expressions<data::sort_expression_builder, Derived>
     185             : {
     186             : };
     187             : //--- end generated add_sort_expressions code ---//
     188             : 
     189             : // Adds data expression traversal to a builder
     190             : //--- start generated add_data_expressions code ---//
     191             : template <template <class> class Builder, class Derived>
     192             : struct add_data_expressions: public Builder<Derived>
     193             : {
     194             :   typedef Builder<Derived> super;
     195             :   using super::enter;
     196             :   using super::leave;
     197             :   using super::update;
     198             :   using super::apply;
     199             : 
     200        2822 :   void update(pbes_system::pbes_equation& x)
     201             :   {
     202        2822 :     static_cast<Derived&>(*this).enter(x);
     203        2822 :     x.formula() = static_cast<Derived&>(*this).apply(x.formula());
     204        2822 :     static_cast<Derived&>(*this).leave(x);
     205        2822 :   }
     206             : 
     207         470 :   void update(pbes_system::pbes& x)
     208             :   {
     209         470 :     static_cast<Derived&>(*this).enter(x);
     210         470 :     static_cast<Derived&>(*this).update(x.equations());
     211         470 :     x.initial_state() = static_cast<Derived&>(*this).apply(x.initial_state());
     212         470 :     static_cast<Derived&>(*this).leave(x);
     213         470 :   }
     214             : 
     215        1838 :   pbes_system::propositional_variable_instantiation apply(const pbes_system::propositional_variable_instantiation& x)
     216             :   {
     217        1838 :     static_cast<Derived&>(*this).enter(x);
     218        1838 :     pbes_system::propositional_variable_instantiation result = pbes_system::propositional_variable_instantiation(x.name(), static_cast<Derived&>(*this).apply(x.parameters()));
     219        1838 :     static_cast<Derived&>(*this).leave(x);
     220        1838 :     return result;
     221             :   }
     222             : 
     223         193 :   pbes_system::not_ apply(const pbes_system::not_& x)
     224             :   {
     225         193 :     static_cast<Derived&>(*this).enter(x);
     226         193 :     pbes_system::not_ result = pbes_system::not_(static_cast<Derived&>(*this).apply(x.operand()));
     227         193 :     static_cast<Derived&>(*this).leave(x);
     228         193 :     return result;
     229             :   }
     230             : 
     231         576 :   pbes_system::and_ apply(const pbes_system::and_& x)
     232             :   {
     233         576 :     static_cast<Derived&>(*this).enter(x);
     234         576 :     pbes_system::and_ result = pbes_system::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     235         576 :     static_cast<Derived&>(*this).leave(x);
     236         576 :     return result;
     237             :   }
     238             : 
     239         487 :   pbes_system::or_ apply(const pbes_system::or_& x)
     240             :   {
     241         487 :     static_cast<Derived&>(*this).enter(x);
     242         487 :     pbes_system::or_ result = pbes_system::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     243         487 :     static_cast<Derived&>(*this).leave(x);
     244         487 :     return result;
     245             :   }
     246             : 
     247         178 :   pbes_system::imp apply(const pbes_system::imp& x)
     248             :   {
     249         178 :     static_cast<Derived&>(*this).enter(x);
     250         178 :     pbes_system::imp result = pbes_system::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     251         178 :     static_cast<Derived&>(*this).leave(x);
     252         178 :     return result;
     253             :   }
     254             : 
     255         238 :   pbes_system::forall apply(const pbes_system::forall& x)
     256             :   {
     257         238 :     static_cast<Derived&>(*this).enter(x);
     258         238 :     pbes_system::forall result = pbes_system::forall(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
     259         238 :     static_cast<Derived&>(*this).leave(x);
     260         238 :     return result;
     261             :   }
     262             : 
     263         134 :   pbes_system::exists apply(const pbes_system::exists& x)
     264             :   {
     265         134 :     static_cast<Derived&>(*this).enter(x);
     266         134 :     pbes_system::exists result = pbes_system::exists(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
     267         134 :     static_cast<Derived&>(*this).leave(x);
     268         134 :     return result;
     269             :   }
     270             : 
     271        6815 :   pbes_system::pbes_expression apply(const pbes_system::pbes_expression& x)
     272             :   {
     273        6815 :     static_cast<Derived&>(*this).enter(x);
     274        6815 :     pbes_system::pbes_expression result;
     275        6815 :     if (data::is_data_expression(x))
     276             :     {
     277        3637 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     278             :     }
     279        3178 :     else if (pbes_system::is_propositional_variable_instantiation(x))
     280             :     {
     281        1364 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
     282             :     }
     283        1814 :     else if (pbes_system::is_not(x))
     284             :     {
     285         193 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
     286             :     }
     287        1621 :     else if (pbes_system::is_and(x))
     288             :     {
     289         576 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
     290             :     }
     291        1045 :     else if (pbes_system::is_or(x))
     292             :     {
     293         487 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
     294             :     }
     295         558 :     else if (pbes_system::is_imp(x))
     296             :     {
     297         178 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
     298             :     }
     299         380 :     else if (pbes_system::is_forall(x))
     300             :     {
     301         242 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
     302             :     }
     303         138 :     else if (pbes_system::is_exists(x))
     304             :     {
     305         138 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
     306             :     }
     307           0 :     else if (data::is_variable(x))
     308             :     {
     309           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     310             :     }
     311           0 :     else if (data::is_untyped_data_parameter(x))
     312             :     {
     313           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     314             :     }
     315        6815 :     static_cast<Derived&>(*this).leave(x);
     316        6815 :     return result;
     317             :   }
     318             : 
     319             : };
     320             : 
     321             : /// \brief Builder class
     322             : template <typename Derived>
     323             : struct data_expression_builder: public add_data_expressions<data::data_expression_builder, Derived>
     324             : {
     325             : };
     326             : //--- end generated add_data_expressions code ---//
     327             : 
     328             : //--- start generated add_variables code ---//
     329             : template <template <class> class Builder, class Derived>
     330             : struct add_variables: public Builder<Derived>
     331             : {
     332             :   typedef Builder<Derived> super;
     333             :   using super::enter;
     334             :   using super::leave;
     335             :   using super::update;
     336             :   using super::apply;
     337             : 
     338             :   pbes_system::propositional_variable apply(const pbes_system::propositional_variable& x)
     339             :   {
     340             :     static_cast<Derived&>(*this).enter(x);
     341             :     pbes_system::propositional_variable result = pbes_system::propositional_variable(x.name(), static_cast<Derived&>(*this).apply(x.parameters()));
     342             :     static_cast<Derived&>(*this).leave(x);
     343             :     return result;
     344             :   }
     345             : 
     346             :   void update(pbes_system::pbes_equation& x)
     347             :   {
     348             :     static_cast<Derived&>(*this).enter(x);
     349             :     x.variable() = static_cast<Derived&>(*this).apply(x.variable());
     350             :     x.formula() = static_cast<Derived&>(*this).apply(x.formula());
     351             :     static_cast<Derived&>(*this).leave(x);
     352             :   }
     353             : 
     354             :   void update(pbes_system::pbes& x)
     355             :   {
     356             :     static_cast<Derived&>(*this).enter(x);
     357             :     static_cast<Derived&>(*this).update(x.equations());
     358             :     static_cast<Derived&>(*this).update(x.global_variables());
     359             :     x.initial_state() = static_cast<Derived&>(*this).apply(x.initial_state());
     360             :     static_cast<Derived&>(*this).leave(x);
     361             :   }
     362             : 
     363             :   pbes_system::propositional_variable_instantiation apply(const pbes_system::propositional_variable_instantiation& x)
     364             :   {
     365             :     static_cast<Derived&>(*this).enter(x);
     366             :     pbes_system::propositional_variable_instantiation result = pbes_system::propositional_variable_instantiation(x.name(), static_cast<Derived&>(*this).apply(x.parameters()));
     367             :     static_cast<Derived&>(*this).leave(x);
     368             :     return result;
     369             :   }
     370             : 
     371             :   pbes_system::not_ apply(const pbes_system::not_& x)
     372             :   {
     373             :     static_cast<Derived&>(*this).enter(x);
     374             :     pbes_system::not_ result = pbes_system::not_(static_cast<Derived&>(*this).apply(x.operand()));
     375             :     static_cast<Derived&>(*this).leave(x);
     376             :     return result;
     377             :   }
     378             : 
     379             :   pbes_system::and_ apply(const pbes_system::and_& x)
     380             :   {
     381             :     static_cast<Derived&>(*this).enter(x);
     382             :     pbes_system::and_ result = pbes_system::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     383             :     static_cast<Derived&>(*this).leave(x);
     384             :     return result;
     385             :   }
     386             : 
     387             :   pbes_system::or_ apply(const pbes_system::or_& x)
     388             :   {
     389             :     static_cast<Derived&>(*this).enter(x);
     390             :     pbes_system::or_ result = pbes_system::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     391             :     static_cast<Derived&>(*this).leave(x);
     392             :     return result;
     393             :   }
     394             : 
     395             :   pbes_system::imp apply(const pbes_system::imp& x)
     396             :   {
     397             :     static_cast<Derived&>(*this).enter(x);
     398             :     pbes_system::imp result = pbes_system::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     399             :     static_cast<Derived&>(*this).leave(x);
     400             :     return result;
     401             :   }
     402             : 
     403             :   pbes_system::forall apply(const pbes_system::forall& x)
     404             :   {
     405             :     static_cast<Derived&>(*this).enter(x);
     406             :     pbes_system::forall result = pbes_system::forall(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
     407             :     static_cast<Derived&>(*this).leave(x);
     408             :     return result;
     409             :   }
     410             : 
     411             :   pbes_system::exists apply(const pbes_system::exists& x)
     412             :   {
     413             :     static_cast<Derived&>(*this).enter(x);
     414             :     pbes_system::exists result = pbes_system::exists(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
     415             :     static_cast<Derived&>(*this).leave(x);
     416             :     return result;
     417             :   }
     418             : 
     419             :   pbes_system::pbes_expression apply(const pbes_system::pbes_expression& x)
     420             :   {
     421             :     static_cast<Derived&>(*this).enter(x);
     422             :     pbes_system::pbes_expression result;
     423             :     if (data::is_data_expression(x))
     424             :     {
     425             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     426             :     }
     427             :     else if (pbes_system::is_propositional_variable_instantiation(x))
     428             :     {
     429             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
     430             :     }
     431             :     else if (pbes_system::is_not(x))
     432             :     {
     433             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
     434             :     }
     435             :     else if (pbes_system::is_and(x))
     436             :     {
     437             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
     438             :     }
     439             :     else if (pbes_system::is_or(x))
     440             :     {
     441             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
     442             :     }
     443             :     else if (pbes_system::is_imp(x))
     444             :     {
     445             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
     446             :     }
     447             :     else if (pbes_system::is_forall(x))
     448             :     {
     449             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
     450             :     }
     451             :     else if (pbes_system::is_exists(x))
     452             :     {
     453             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
     454             :     }
     455             :     else if (data::is_variable(x))
     456             :     {
     457             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     458             :     }
     459             :     else if (data::is_untyped_data_parameter(x))
     460             :     {
     461             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     462             :     }
     463             :     static_cast<Derived&>(*this).leave(x);
     464             :     return result;
     465             :   }
     466             : 
     467             : };
     468             : 
     469             : /// \brief Builder class
     470             : template <typename Derived>
     471             : struct variable_builder: public add_variables<data::data_expression_builder, Derived>
     472             : {
     473             : };
     474             : //--- end generated add_variables code ---//
     475             : 
     476             : // Adds pbes expression traversal to a builder
     477             : //--- start generated add_pbes_expressions code ---//
     478             : template <template <class> class Builder, class Derived>
     479             : struct add_pbes_expressions: public Builder<Derived>
     480             : {
     481             :   typedef Builder<Derived> super;
     482             :   using super::enter;
     483             :   using super::leave;
     484             :   using super::update;
     485             :   using super::apply;
     486             : 
     487        1144 :   void update(pbes_system::pbes_equation& x)
     488             :   {
     489        1144 :     static_cast<Derived&>(*this).enter(x);
     490        1144 :     x.formula() = static_cast<Derived&>(*this).apply(x.formula());
     491        1144 :     static_cast<Derived&>(*this).leave(x);
     492        1144 :   }
     493             : 
     494         594 :   void update(pbes_system::pbes& x)
     495             :   {
     496         594 :     static_cast<Derived&>(*this).enter(x);
     497         594 :     static_cast<Derived&>(*this).update(x.equations());
     498         594 :     static_cast<Derived&>(*this).leave(x);
     499         594 :   }
     500             : 
     501        2264 :   pbes_system::propositional_variable_instantiation apply(const pbes_system::propositional_variable_instantiation& x)
     502             :   {
     503        2264 :     static_cast<Derived&>(*this).enter(x);
     504             :     // skip
     505        2264 :     static_cast<Derived&>(*this).leave(x);
     506        2264 :     return x;
     507             :   }
     508             : 
     509         143 :   pbes_system::not_ apply(const pbes_system::not_& x)
     510             :   {
     511         143 :     static_cast<Derived&>(*this).enter(x);
     512         143 :     pbes_system::not_ result = pbes_system::not_(static_cast<Derived&>(*this).apply(x.operand()));
     513         143 :     static_cast<Derived&>(*this).leave(x);
     514         143 :     return result;
     515             :   }
     516             : 
     517        2906 :   pbes_system::and_ apply(const pbes_system::and_& x)
     518             :   {
     519        2906 :     static_cast<Derived&>(*this).enter(x);
     520        2906 :     pbes_system::and_ result = pbes_system::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     521        2906 :     static_cast<Derived&>(*this).leave(x);
     522        2906 :     return result;
     523             :   }
     524             : 
     525        1801 :   pbes_system::or_ apply(const pbes_system::or_& x)
     526             :   {
     527        1801 :     static_cast<Derived&>(*this).enter(x);
     528        1801 :     pbes_system::or_ result = pbes_system::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     529        1801 :     static_cast<Derived&>(*this).leave(x);
     530        1801 :     return result;
     531             :   }
     532             : 
     533         178 :   pbes_system::imp apply(const pbes_system::imp& x)
     534             :   {
     535         178 :     static_cast<Derived&>(*this).enter(x);
     536         178 :     pbes_system::imp result = pbes_system::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     537         178 :     static_cast<Derived&>(*this).leave(x);
     538         178 :     return result;
     539             :   }
     540             : 
     541          64 :   pbes_system::forall apply(const pbes_system::forall& x)
     542             :   {
     543          64 :     static_cast<Derived&>(*this).enter(x);
     544          64 :     pbes_system::forall result = pbes_system::forall(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
     545          64 :     static_cast<Derived&>(*this).leave(x);
     546          64 :     return result;
     547             :   }
     548             : 
     549          19 :   pbes_system::exists apply(const pbes_system::exists& x)
     550             :   {
     551          19 :     static_cast<Derived&>(*this).enter(x);
     552          19 :     pbes_system::exists result = pbes_system::exists(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
     553          19 :     static_cast<Derived&>(*this).leave(x);
     554          19 :     return result;
     555             :   }
     556             : 
     557      124879 :   pbes_system::pbes_expression apply(const pbes_system::pbes_expression& x)
     558             :   {
     559      124879 :     static_cast<Derived&>(*this).enter(x);
     560      124879 :     pbes_system::pbes_expression result;
     561      124879 :     if (data::is_data_expression(x))
     562             :     {
     563       39212 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     564             :     }
     565       85667 :     else if (pbes_system::is_propositional_variable_instantiation(x))
     566             :     {
     567       16781 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
     568             :     }
     569       68886 :     else if (pbes_system::is_not(x))
     570             :     {
     571         296 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
     572             :     }
     573       68590 :     else if (pbes_system::is_and(x))
     574             :     {
     575       32382 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
     576             :     }
     577       36208 :     else if (pbes_system::is_or(x))
     578             :     {
     579       30075 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
     580             :     }
     581        6133 :     else if (pbes_system::is_imp(x))
     582             :     {
     583         778 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
     584             :     }
     585        5355 :     else if (pbes_system::is_forall(x))
     586             :     {
     587        2998 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
     588             :     }
     589        2357 :     else if (pbes_system::is_exists(x))
     590             :     {
     591        1532 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
     592             :     }
     593         825 :     else if (data::is_variable(x))
     594             :     {
     595           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x));
     596             :     }
     597         825 :     else if (data::is_untyped_data_parameter(x))
     598             :     {
     599         825 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     600             :     }
     601      124879 :     static_cast<Derived&>(*this).leave(x);
     602      124879 :     return result;
     603             :   }
     604             : 
     605             : };
     606             : 
     607             : /// \brief Builder class
     608             : template <typename Derived>
     609             : struct pbes_expression_builder: public add_pbes_expressions<pbes_system::pbes_expression_builder_base, Derived>
     610             : {
     611             : };
     612             : //--- end generated add_pbes_expressions code ---//
     613             : 
     614             : } // namespace pbes_system
     615             : 
     616             : } // namespace mcrl2
     617             : 
     618             : #endif // MCRL2_PBES_BUILDER_H

Generated by: LCOV version 1.13