LCOV - code coverage report
Current view: top level - modal_formula/include/mcrl2/modal_formula - builder.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 564 725 77.8 %
Date: 2020-02-21 00:44:40 Functions: 133 272 48.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/modal_formula/builder.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_BUILDER_H
      13             : #define MCRL2_MODAL_FORMULA_BUILDER_H
      14             : 
      15             : #include "mcrl2/lps/builder.h"
      16             : #include "mcrl2/modal_formula/state_formula_specification.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace action_formulas
      22             : {
      23             : 
      24             : /// \brief Base class for action_formula_builder.
      25             : template <typename Derived>
      26             : struct action_formula_builder_base: public core::builder<Derived>
      27             : {
      28             :   typedef core::builder<Derived> super;
      29             :   using super::apply;
      30             : 
      31             :   action_formula apply(const data::data_expression& x)
      32             :   {
      33             :     static_cast<Derived&>(*this).enter(x);
      34             :     // skip
      35             :     static_cast<Derived&>(*this).leave(x);
      36             :     return x;
      37             :   }
      38             : };
      39             : 
      40             : //--- start generated action_formulas::add_sort_expressions code ---//
      41             : template <template <class> class Builder, class Derived>
      42             : struct add_sort_expressions: public Builder<Derived>
      43             : {
      44             :   typedef Builder<Derived> super;
      45             :   using super::enter;
      46             :   using super::leave;
      47             :   using super::update;
      48             :   using super::apply;
      49             : 
      50          99 :   action_formulas::true_ apply(const action_formulas::true_& x)
      51             :   {
      52          99 :     static_cast<Derived&>(*this).enter(x);
      53             :     // skip
      54          99 :     static_cast<Derived&>(*this).leave(x);
      55          99 :     return x;
      56             :   }
      57             : 
      58           0 :   action_formulas::false_ apply(const action_formulas::false_& x)
      59             :   {
      60           0 :     static_cast<Derived&>(*this).enter(x);
      61             :     // skip
      62           0 :     static_cast<Derived&>(*this).leave(x);
      63           0 :     return x;
      64             :   }
      65             : 
      66          69 :   action_formulas::not_ apply(const action_formulas::not_& x)
      67             :   {
      68          69 :     static_cast<Derived&>(*this).enter(x);
      69          69 :     action_formulas::not_ result = action_formulas::not_(static_cast<Derived&>(*this).apply(x.operand()));
      70          69 :     static_cast<Derived&>(*this).leave(x);
      71          69 :     return result;
      72             :   }
      73             : 
      74          22 :   action_formulas::and_ apply(const action_formulas::and_& x)
      75             :   {
      76          22 :     static_cast<Derived&>(*this).enter(x);
      77          22 :     action_formulas::and_ result = action_formulas::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
      78          22 :     static_cast<Derived&>(*this).leave(x);
      79          22 :     return result;
      80             :   }
      81             : 
      82           9 :   action_formulas::or_ apply(const action_formulas::or_& x)
      83             :   {
      84           9 :     static_cast<Derived&>(*this).enter(x);
      85           9 :     action_formulas::or_ result = action_formulas::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
      86           9 :     static_cast<Derived&>(*this).leave(x);
      87           9 :     return result;
      88             :   }
      89             : 
      90           0 :   action_formulas::imp apply(const action_formulas::imp& x)
      91             :   {
      92           0 :     static_cast<Derived&>(*this).enter(x);
      93           0 :     action_formulas::imp result = action_formulas::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
      94           0 :     static_cast<Derived&>(*this).leave(x);
      95           0 :     return result;
      96             :   }
      97             : 
      98           9 :   action_formulas::forall apply(const action_formulas::forall& x)
      99             :   {
     100           9 :     static_cast<Derived&>(*this).enter(x);
     101           9 :     action_formulas::forall result = action_formulas::forall(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
     102           9 :     static_cast<Derived&>(*this).leave(x);
     103           9 :     return result;
     104             :   }
     105             : 
     106           5 :   action_formulas::exists apply(const action_formulas::exists& x)
     107             :   {
     108           5 :     static_cast<Derived&>(*this).enter(x);
     109           5 :     action_formulas::exists result = action_formulas::exists(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
     110           5 :     static_cast<Derived&>(*this).leave(x);
     111           5 :     return result;
     112             :   }
     113             : 
     114           0 :   action_formulas::at apply(const action_formulas::at& x)
     115             :   {
     116           0 :     static_cast<Derived&>(*this).enter(x);
     117           0 :     action_formulas::at result = action_formulas::at(static_cast<Derived&>(*this).apply(x.operand()), static_cast<Derived&>(*this).apply(x.time_stamp()));
     118           0 :     static_cast<Derived&>(*this).leave(x);
     119           0 :     return result;
     120             :   }
     121             : 
     122         176 :   action_formulas::multi_action apply(const action_formulas::multi_action& x)
     123             :   {
     124         176 :     static_cast<Derived&>(*this).enter(x);
     125         176 :     action_formulas::multi_action result = action_formulas::multi_action(static_cast<Derived&>(*this).apply(x.actions()));
     126         176 :     static_cast<Derived&>(*this).leave(x);
     127         176 :     return result;
     128             :   }
     129             : 
     130         553 :   action_formulas::action_formula apply(const action_formulas::action_formula& x)
     131             :   {
     132         553 :     static_cast<Derived&>(*this).enter(x);
     133         553 :     action_formulas::action_formula result;
     134         553 :     if (data::is_data_expression(x))
     135             :     {
     136           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     137             :     }
     138         553 :     else if (action_formulas::is_true(x))
     139             :     {
     140          99 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
     141             :     }
     142         454 :     else if (action_formulas::is_false(x))
     143             :     {
     144           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
     145             :     }
     146         454 :     else if (action_formulas::is_not(x))
     147             :     {
     148          69 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
     149             :     }
     150         385 :     else if (action_formulas::is_and(x))
     151             :     {
     152          22 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
     153             :     }
     154         363 :     else if (action_formulas::is_or(x))
     155             :     {
     156           9 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
     157             :     }
     158         354 :     else if (action_formulas::is_imp(x))
     159             :     {
     160           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
     161             :     }
     162         354 :     else if (action_formulas::is_forall(x))
     163             :     {
     164           9 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
     165             :     }
     166         345 :     else if (action_formulas::is_exists(x))
     167             :     {
     168           5 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
     169             :     }
     170         340 :     else if (action_formulas::is_at(x))
     171             :     {
     172           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
     173             :     }
     174         340 :     else if (action_formulas::is_multi_action(x))
     175             :     {
     176         176 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
     177             :     }
     178         164 :     else if (process::is_untyped_multi_action(x))
     179             :     {
     180         164 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
     181             :     }
     182           0 :     else if (data::is_untyped_data_parameter(x))
     183             :     {
     184           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     185             :     }
     186         553 :     static_cast<Derived&>(*this).leave(x);
     187         553 :     return result;
     188             :   }
     189             : 
     190             : };
     191             : 
     192             : /// \brief Builder class
     193             : template <typename Derived>
     194             : struct sort_expression_builder: public add_sort_expressions<lps::sort_expression_builder, Derived>
     195             : {
     196             : };
     197             : //--- end generated action_formulas::add_sort_expressions code ---//
     198             : 
     199             : //--- start generated action_formulas::add_data_expressions code ---//
     200             : template <template <class> class Builder, class Derived>
     201             : struct add_data_expressions: public Builder<Derived>
     202             : {
     203             :   typedef Builder<Derived> super;
     204             :   using super::enter;
     205             :   using super::leave;
     206             :   using super::update;
     207             :   using super::apply;
     208             : 
     209          58 :   action_formulas::true_ apply(const action_formulas::true_& x)
     210             :   {
     211          58 :     static_cast<Derived&>(*this).enter(x);
     212             :     // skip
     213          58 :     static_cast<Derived&>(*this).leave(x);
     214          58 :     return x;
     215             :   }
     216             : 
     217           0 :   action_formulas::false_ apply(const action_formulas::false_& x)
     218             :   {
     219           0 :     static_cast<Derived&>(*this).enter(x);
     220             :     // skip
     221           0 :     static_cast<Derived&>(*this).leave(x);
     222           0 :     return x;
     223             :   }
     224             : 
     225          35 :   action_formulas::not_ apply(const action_formulas::not_& x)
     226             :   {
     227          35 :     static_cast<Derived&>(*this).enter(x);
     228          35 :     action_formulas::not_ result = action_formulas::not_(static_cast<Derived&>(*this).apply(x.operand()));
     229          35 :     static_cast<Derived&>(*this).leave(x);
     230          35 :     return result;
     231             :   }
     232             : 
     233           9 :   action_formulas::and_ apply(const action_formulas::and_& x)
     234             :   {
     235           9 :     static_cast<Derived&>(*this).enter(x);
     236           9 :     action_formulas::and_ result = action_formulas::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     237           9 :     static_cast<Derived&>(*this).leave(x);
     238           9 :     return result;
     239             :   }
     240             : 
     241           3 :   action_formulas::or_ apply(const action_formulas::or_& x)
     242             :   {
     243           3 :     static_cast<Derived&>(*this).enter(x);
     244           3 :     action_formulas::or_ result = action_formulas::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     245           3 :     static_cast<Derived&>(*this).leave(x);
     246           3 :     return result;
     247             :   }
     248             : 
     249           0 :   action_formulas::imp apply(const action_formulas::imp& x)
     250             :   {
     251           0 :     static_cast<Derived&>(*this).enter(x);
     252           0 :     action_formulas::imp result = action_formulas::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     253           0 :     static_cast<Derived&>(*this).leave(x);
     254           0 :     return result;
     255             :   }
     256             : 
     257           3 :   action_formulas::forall apply(const action_formulas::forall& x)
     258             :   {
     259           3 :     static_cast<Derived&>(*this).enter(x);
     260           3 :     action_formulas::forall result = action_formulas::forall(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
     261           3 :     static_cast<Derived&>(*this).leave(x);
     262           3 :     return result;
     263             :   }
     264             : 
     265           2 :   action_formulas::exists apply(const action_formulas::exists& x)
     266             :   {
     267           2 :     static_cast<Derived&>(*this).enter(x);
     268           2 :     action_formulas::exists result = action_formulas::exists(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
     269           2 :     static_cast<Derived&>(*this).leave(x);
     270           2 :     return result;
     271             :   }
     272             : 
     273           0 :   action_formulas::at apply(const action_formulas::at& x)
     274             :   {
     275           0 :     static_cast<Derived&>(*this).enter(x);
     276           0 :     action_formulas::at result = action_formulas::at(static_cast<Derived&>(*this).apply(x.operand()), static_cast<Derived&>(*this).apply(x.time_stamp()));
     277           0 :     static_cast<Derived&>(*this).leave(x);
     278           0 :     return result;
     279             :   }
     280             : 
     281         170 :   action_formulas::multi_action apply(const action_formulas::multi_action& x)
     282             :   {
     283         170 :     static_cast<Derived&>(*this).enter(x);
     284         170 :     action_formulas::multi_action result = action_formulas::multi_action(static_cast<Derived&>(*this).apply(x.actions()));
     285         170 :     static_cast<Derived&>(*this).leave(x);
     286         170 :     return result;
     287             :   }
     288             : 
     289         280 :   action_formulas::action_formula apply(const action_formulas::action_formula& x)
     290             :   {
     291         280 :     static_cast<Derived&>(*this).enter(x);
     292         280 :     action_formulas::action_formula result;
     293         280 :     if (data::is_data_expression(x))
     294             :     {
     295           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     296             :     }
     297         280 :     else if (action_formulas::is_true(x))
     298             :     {
     299          58 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
     300             :     }
     301         222 :     else if (action_formulas::is_false(x))
     302             :     {
     303           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
     304             :     }
     305         222 :     else if (action_formulas::is_not(x))
     306             :     {
     307          35 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
     308             :     }
     309         187 :     else if (action_formulas::is_and(x))
     310             :     {
     311           9 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
     312             :     }
     313         178 :     else if (action_formulas::is_or(x))
     314             :     {
     315           3 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
     316             :     }
     317         175 :     else if (action_formulas::is_imp(x))
     318             :     {
     319           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
     320             :     }
     321         175 :     else if (action_formulas::is_forall(x))
     322             :     {
     323           3 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
     324             :     }
     325         172 :     else if (action_formulas::is_exists(x))
     326             :     {
     327           2 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
     328             :     }
     329         170 :     else if (action_formulas::is_at(x))
     330             :     {
     331           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
     332             :     }
     333         170 :     else if (action_formulas::is_multi_action(x))
     334             :     {
     335         170 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
     336             :     }
     337           0 :     else if (process::is_untyped_multi_action(x))
     338             :     {
     339           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
     340             :     }
     341           0 :     else if (data::is_untyped_data_parameter(x))
     342             :     {
     343           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     344             :     }
     345         280 :     static_cast<Derived&>(*this).leave(x);
     346         280 :     return result;
     347             :   }
     348             : 
     349             : };
     350             : 
     351             : /// \brief Builder class
     352             : template <typename Derived>
     353             : struct data_expression_builder: public add_data_expressions<lps::data_expression_builder, Derived>
     354             : {
     355             : };
     356             : //--- end generated action_formulas::add_data_expressions code ---//
     357             : 
     358             : //--- start generated action_formulas::add_variables code ---//
     359             : template <template <class> class Builder, class Derived>
     360             : struct add_variables: public Builder<Derived>
     361             : {
     362             :   typedef Builder<Derived> super;
     363             :   using super::enter;
     364             :   using super::leave;
     365             :   using super::update;
     366             :   using super::apply;
     367             : 
     368             :   action_formulas::true_ apply(const action_formulas::true_& x)
     369             :   {
     370             :     static_cast<Derived&>(*this).enter(x);
     371             :     // skip
     372             :     static_cast<Derived&>(*this).leave(x);
     373             :     return x;
     374             :   }
     375             : 
     376             :   action_formulas::false_ apply(const action_formulas::false_& x)
     377             :   {
     378             :     static_cast<Derived&>(*this).enter(x);
     379             :     // skip
     380             :     static_cast<Derived&>(*this).leave(x);
     381             :     return x;
     382             :   }
     383             : 
     384             :   action_formulas::not_ apply(const action_formulas::not_& x)
     385             :   {
     386             :     static_cast<Derived&>(*this).enter(x);
     387             :     action_formulas::not_ result = action_formulas::not_(static_cast<Derived&>(*this).apply(x.operand()));
     388             :     static_cast<Derived&>(*this).leave(x);
     389             :     return result;
     390             :   }
     391             : 
     392             :   action_formulas::and_ apply(const action_formulas::and_& x)
     393             :   {
     394             :     static_cast<Derived&>(*this).enter(x);
     395             :     action_formulas::and_ result = action_formulas::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     396             :     static_cast<Derived&>(*this).leave(x);
     397             :     return result;
     398             :   }
     399             : 
     400             :   action_formulas::or_ apply(const action_formulas::or_& x)
     401             :   {
     402             :     static_cast<Derived&>(*this).enter(x);
     403             :     action_formulas::or_ result = action_formulas::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     404             :     static_cast<Derived&>(*this).leave(x);
     405             :     return result;
     406             :   }
     407             : 
     408             :   action_formulas::imp apply(const action_formulas::imp& x)
     409             :   {
     410             :     static_cast<Derived&>(*this).enter(x);
     411             :     action_formulas::imp result = action_formulas::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     412             :     static_cast<Derived&>(*this).leave(x);
     413             :     return result;
     414             :   }
     415             : 
     416             :   action_formulas::forall apply(const action_formulas::forall& x)
     417             :   {
     418             :     static_cast<Derived&>(*this).enter(x);
     419             :     action_formulas::forall result = action_formulas::forall(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
     420             :     static_cast<Derived&>(*this).leave(x);
     421             :     return result;
     422             :   }
     423             : 
     424             :   action_formulas::exists apply(const action_formulas::exists& x)
     425             :   {
     426             :     static_cast<Derived&>(*this).enter(x);
     427             :     action_formulas::exists result = action_formulas::exists(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
     428             :     static_cast<Derived&>(*this).leave(x);
     429             :     return result;
     430             :   }
     431             : 
     432             :   action_formulas::at apply(const action_formulas::at& x)
     433             :   {
     434             :     static_cast<Derived&>(*this).enter(x);
     435             :     action_formulas::at result = action_formulas::at(static_cast<Derived&>(*this).apply(x.operand()), static_cast<Derived&>(*this).apply(x.time_stamp()));
     436             :     static_cast<Derived&>(*this).leave(x);
     437             :     return result;
     438             :   }
     439             : 
     440             :   action_formulas::multi_action apply(const action_formulas::multi_action& x)
     441             :   {
     442             :     static_cast<Derived&>(*this).enter(x);
     443             :     action_formulas::multi_action result = action_formulas::multi_action(static_cast<Derived&>(*this).apply(x.actions()));
     444             :     static_cast<Derived&>(*this).leave(x);
     445             :     return result;
     446             :   }
     447             : 
     448             :   action_formulas::action_formula apply(const action_formulas::action_formula& x)
     449             :   {
     450             :     static_cast<Derived&>(*this).enter(x);
     451             :     action_formulas::action_formula result;
     452             :     if (data::is_data_expression(x))
     453             :     {
     454             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     455             :     }
     456             :     else if (action_formulas::is_true(x))
     457             :     {
     458             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
     459             :     }
     460             :     else if (action_formulas::is_false(x))
     461             :     {
     462             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
     463             :     }
     464             :     else if (action_formulas::is_not(x))
     465             :     {
     466             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
     467             :     }
     468             :     else if (action_formulas::is_and(x))
     469             :     {
     470             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
     471             :     }
     472             :     else if (action_formulas::is_or(x))
     473             :     {
     474             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
     475             :     }
     476             :     else if (action_formulas::is_imp(x))
     477             :     {
     478             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
     479             :     }
     480             :     else if (action_formulas::is_forall(x))
     481             :     {
     482             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
     483             :     }
     484             :     else if (action_formulas::is_exists(x))
     485             :     {
     486             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
     487             :     }
     488             :     else if (action_formulas::is_at(x))
     489             :     {
     490             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
     491             :     }
     492             :     else if (action_formulas::is_multi_action(x))
     493             :     {
     494             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
     495             :     }
     496             :     else if (process::is_untyped_multi_action(x))
     497             :     {
     498             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
     499             :     }
     500             :     else if (data::is_untyped_data_parameter(x))
     501             :     {
     502             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     503             :     }
     504             :     static_cast<Derived&>(*this).leave(x);
     505             :     return result;
     506             :   }
     507             : 
     508             : };
     509             : 
     510             : /// \brief Builder class
     511             : template <typename Derived>
     512             : struct variable_builder: public add_variables<lps::data_expression_builder, Derived>
     513             : {
     514             : };
     515             : //--- end generated action_formulas::add_variables code ---//
     516             : 
     517             : //--- start generated action_formulas::add_action_formula_expressions code ---//
     518             : template <template <class> class Builder, class Derived>
     519             : struct add_action_formula_expressions: public Builder<Derived>
     520             : {
     521             :   typedef Builder<Derived> super;
     522             :   using super::enter;
     523             :   using super::leave;
     524             :   using super::update;
     525             :   using super::apply;
     526             : 
     527          58 :   action_formulas::true_ apply(const action_formulas::true_& x)
     528             :   {
     529          58 :     static_cast<Derived&>(*this).enter(x);
     530             :     // skip
     531          58 :     static_cast<Derived&>(*this).leave(x);
     532          58 :     return x;
     533             :   }
     534             : 
     535           0 :   action_formulas::false_ apply(const action_formulas::false_& x)
     536             :   {
     537           0 :     static_cast<Derived&>(*this).enter(x);
     538             :     // skip
     539           0 :     static_cast<Derived&>(*this).leave(x);
     540           0 :     return x;
     541             :   }
     542             : 
     543          35 :   action_formulas::not_ apply(const action_formulas::not_& x)
     544             :   {
     545          35 :     static_cast<Derived&>(*this).enter(x);
     546          35 :     action_formulas::not_ result = action_formulas::not_(static_cast<Derived&>(*this).apply(x.operand()));
     547          35 :     static_cast<Derived&>(*this).leave(x);
     548          35 :     return result;
     549             :   }
     550             : 
     551           9 :   action_formulas::and_ apply(const action_formulas::and_& x)
     552             :   {
     553           9 :     static_cast<Derived&>(*this).enter(x);
     554           9 :     action_formulas::and_ result = action_formulas::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     555           9 :     static_cast<Derived&>(*this).leave(x);
     556           9 :     return result;
     557             :   }
     558             : 
     559           3 :   action_formulas::or_ apply(const action_formulas::or_& x)
     560             :   {
     561           3 :     static_cast<Derived&>(*this).enter(x);
     562           3 :     action_formulas::or_ result = action_formulas::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     563           3 :     static_cast<Derived&>(*this).leave(x);
     564           3 :     return result;
     565             :   }
     566             : 
     567           0 :   action_formulas::imp apply(const action_formulas::imp& x)
     568             :   {
     569           0 :     static_cast<Derived&>(*this).enter(x);
     570           0 :     action_formulas::imp result = action_formulas::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     571           0 :     static_cast<Derived&>(*this).leave(x);
     572           0 :     return result;
     573             :   }
     574             : 
     575             :   action_formulas::forall apply(const action_formulas::forall& x)
     576             :   {
     577             :     static_cast<Derived&>(*this).enter(x);
     578             :     action_formulas::forall result = action_formulas::forall(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
     579             :     static_cast<Derived&>(*this).leave(x);
     580             :     return result;
     581             :   }
     582             : 
     583             :   action_formulas::exists apply(const action_formulas::exists& x)
     584             :   {
     585             :     static_cast<Derived&>(*this).enter(x);
     586             :     action_formulas::exists result = action_formulas::exists(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
     587             :     static_cast<Derived&>(*this).leave(x);
     588             :     return result;
     589             :   }
     590             : 
     591             :   action_formulas::at apply(const action_formulas::at& x)
     592             :   {
     593             :     static_cast<Derived&>(*this).enter(x);
     594             :     action_formulas::at result = action_formulas::at(static_cast<Derived&>(*this).apply(x.operand()), x.time_stamp());
     595             :     static_cast<Derived&>(*this).leave(x);
     596             :     return result;
     597             :   }
     598             : 
     599           0 :   action_formulas::multi_action apply(const action_formulas::multi_action& x)
     600             :   {
     601           0 :     static_cast<Derived&>(*this).enter(x);
     602             :     // skip
     603           0 :     static_cast<Derived&>(*this).leave(x);
     604           0 :     return x;
     605             :   }
     606             : 
     607         271 :   action_formulas::action_formula apply(const action_formulas::action_formula& x)
     608             :   {
     609         271 :     static_cast<Derived&>(*this).enter(x);
     610         271 :     action_formulas::action_formula result;
     611         271 :     if (data::is_data_expression(x))
     612             :     {
     613           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     614             :     }
     615         271 :     else if (action_formulas::is_true(x))
     616             :     {
     617          58 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
     618             :     }
     619         213 :     else if (action_formulas::is_false(x))
     620             :     {
     621           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
     622             :     }
     623         213 :     else if (action_formulas::is_not(x))
     624             :     {
     625          35 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
     626             :     }
     627         178 :     else if (action_formulas::is_and(x))
     628             :     {
     629           9 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
     630             :     }
     631         169 :     else if (action_formulas::is_or(x))
     632             :     {
     633           3 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
     634             :     }
     635         166 :     else if (action_formulas::is_imp(x))
     636             :     {
     637           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
     638             :     }
     639         166 :     else if (action_formulas::is_forall(x))
     640             :     {
     641           3 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
     642             :     }
     643         163 :     else if (action_formulas::is_exists(x))
     644             :     {
     645           2 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
     646             :     }
     647         161 :     else if (action_formulas::is_at(x))
     648             :     {
     649           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
     650             :     }
     651         161 :     else if (action_formulas::is_multi_action(x))
     652             :     {
     653           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
     654             :     }
     655         161 :     else if (process::is_untyped_multi_action(x))
     656             :     {
     657         161 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
     658             :     }
     659           0 :     else if (data::is_untyped_data_parameter(x))
     660             :     {
     661           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     662             :     }
     663         271 :     static_cast<Derived&>(*this).leave(x);
     664         271 :     return result;
     665             :   }
     666             : 
     667             : };
     668             : 
     669             : /// \brief Builder class
     670             : template <typename Derived>
     671             : struct action_formula_builder: public add_action_formula_expressions<action_formulas::action_formula_builder_base, Derived>
     672             : {
     673             : };
     674             : //--- end generated action_formulas::add_action_formula_expressions code ---//
     675             : 
     676             : } // namespace action_formulas
     677             : 
     678             : namespace regular_formulas
     679             : {
     680             : 
     681             : /// \brief Builder class for regular_formula_builder. Used as a base class for pbes_expression_builder.
     682             : template <typename Derived>
     683             : struct regular_formula_builder_base: public core::builder<Derived>
     684             : {
     685             :   typedef core::builder<Derived> super;
     686             :   using super::apply;
     687             : 
     688           0 :   regular_formula apply(const data::data_expression& x)
     689             :   {
     690           0 :     static_cast<Derived&>(*this).enter(x);
     691             :     // skip
     692           0 :     static_cast<Derived&>(*this).leave(x);
     693           0 :     return x;
     694             :   }
     695             : };
     696             : 
     697             : //--- start generated regular_formulas::add_sort_expressions code ---//
     698             : template <template <class> class Builder, class Derived>
     699             : struct add_sort_expressions: public Builder<Derived>
     700             : {
     701             :   typedef Builder<Derived> super;
     702             :   using super::enter;
     703             :   using super::leave;
     704             :   using super::update;
     705             :   using super::apply;
     706             : 
     707           0 :   regular_formulas::seq apply(const regular_formulas::seq& x)
     708             :   {
     709           0 :     static_cast<Derived&>(*this).enter(x);
     710           0 :     regular_formulas::seq result = regular_formulas::seq(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     711           0 :     static_cast<Derived&>(*this).leave(x);
     712           0 :     return result;
     713             :   }
     714             : 
     715           0 :   regular_formulas::alt apply(const regular_formulas::alt& x)
     716             :   {
     717           0 :     static_cast<Derived&>(*this).enter(x);
     718           0 :     regular_formulas::alt result = regular_formulas::alt(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     719           0 :     static_cast<Derived&>(*this).leave(x);
     720           0 :     return result;
     721             :   }
     722             : 
     723           0 :   regular_formulas::trans apply(const regular_formulas::trans& x)
     724             :   {
     725           0 :     static_cast<Derived&>(*this).enter(x);
     726           0 :     regular_formulas::trans result = regular_formulas::trans(static_cast<Derived&>(*this).apply(x.operand()));
     727           0 :     static_cast<Derived&>(*this).leave(x);
     728           0 :     return result;
     729             :   }
     730             : 
     731          24 :   regular_formulas::trans_or_nil apply(const regular_formulas::trans_or_nil& x)
     732             :   {
     733          24 :     static_cast<Derived&>(*this).enter(x);
     734          24 :     regular_formulas::trans_or_nil result = regular_formulas::trans_or_nil(static_cast<Derived&>(*this).apply(x.operand()));
     735          24 :     static_cast<Derived&>(*this).leave(x);
     736          24 :     return result;
     737             :   }
     738             : 
     739           3 :   regular_formulas::untyped_regular_formula apply(const regular_formulas::untyped_regular_formula& x)
     740             :   {
     741           3 :     static_cast<Derived&>(*this).enter(x);
     742           3 :     regular_formulas::untyped_regular_formula result = regular_formulas::untyped_regular_formula(x.name(), static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     743           3 :     static_cast<Derived&>(*this).leave(x);
     744           3 :     return result;
     745             :   }
     746             : 
     747         435 :   regular_formulas::regular_formula apply(const regular_formulas::regular_formula& x)
     748             :   {
     749         435 :     static_cast<Derived&>(*this).enter(x);
     750         435 :     regular_formulas::regular_formula result;
     751         435 :     if (action_formulas::is_action_formula(x))
     752             :     {
     753         408 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
     754             :     }
     755          27 :     else if (data::is_data_expression(x))
     756             :     {
     757           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     758             :     }
     759          27 :     else if (regular_formulas::is_seq(x))
     760             :     {
     761           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
     762             :     }
     763          27 :     else if (regular_formulas::is_alt(x))
     764             :     {
     765           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
     766             :     }
     767          27 :     else if (regular_formulas::is_trans(x))
     768             :     {
     769           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
     770             :     }
     771          27 :     else if (regular_formulas::is_trans_or_nil(x))
     772             :     {
     773          24 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
     774             :     }
     775           3 :     else if (regular_formulas::is_untyped_regular_formula(x))
     776             :     {
     777           3 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
     778             :     }
     779         435 :     static_cast<Derived&>(*this).leave(x);
     780         435 :     return result;
     781             :   }
     782             : 
     783             : };
     784             : 
     785             : /// \brief Builder class
     786             : template <typename Derived>
     787             : struct sort_expression_builder: public add_sort_expressions<action_formulas::sort_expression_builder, Derived>
     788             : {
     789             : };
     790             : //--- end generated regular_formulas::add_sort_expressions code ---//
     791             : 
     792             : //--- start generated regular_formulas::add_data_expressions code ---//
     793             : template <template <class> class Builder, class Derived>
     794             : struct add_data_expressions: public Builder<Derived>
     795             : {
     796             :   typedef Builder<Derived> super;
     797             :   using super::enter;
     798             :   using super::leave;
     799             :   using super::update;
     800             :   using super::apply;
     801             : 
     802           0 :   regular_formulas::seq apply(const regular_formulas::seq& x)
     803             :   {
     804           0 :     static_cast<Derived&>(*this).enter(x);
     805           0 :     regular_formulas::seq result = regular_formulas::seq(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     806           0 :     static_cast<Derived&>(*this).leave(x);
     807           0 :     return result;
     808             :   }
     809             : 
     810           0 :   regular_formulas::alt apply(const regular_formulas::alt& x)
     811             :   {
     812           0 :     static_cast<Derived&>(*this).enter(x);
     813           0 :     regular_formulas::alt result = regular_formulas::alt(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     814           0 :     static_cast<Derived&>(*this).leave(x);
     815           0 :     return result;
     816             :   }
     817             : 
     818           0 :   regular_formulas::trans apply(const regular_formulas::trans& x)
     819             :   {
     820           0 :     static_cast<Derived&>(*this).enter(x);
     821           0 :     regular_formulas::trans result = regular_formulas::trans(static_cast<Derived&>(*this).apply(x.operand()));
     822           0 :     static_cast<Derived&>(*this).leave(x);
     823           0 :     return result;
     824             :   }
     825             : 
     826           2 :   regular_formulas::trans_or_nil apply(const regular_formulas::trans_or_nil& x)
     827             :   {
     828           2 :     static_cast<Derived&>(*this).enter(x);
     829           2 :     regular_formulas::trans_or_nil result = regular_formulas::trans_or_nil(static_cast<Derived&>(*this).apply(x.operand()));
     830           2 :     static_cast<Derived&>(*this).leave(x);
     831           2 :     return result;
     832             :   }
     833             : 
     834           0 :   regular_formulas::untyped_regular_formula apply(const regular_formulas::untyped_regular_formula& x)
     835             :   {
     836           0 :     static_cast<Derived&>(*this).enter(x);
     837           0 :     regular_formulas::untyped_regular_formula result = regular_formulas::untyped_regular_formula(x.name(), static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     838           0 :     static_cast<Derived&>(*this).leave(x);
     839           0 :     return result;
     840             :   }
     841             : 
     842         209 :   regular_formulas::regular_formula apply(const regular_formulas::regular_formula& x)
     843             :   {
     844         209 :     static_cast<Derived&>(*this).enter(x);
     845         209 :     regular_formulas::regular_formula result;
     846         209 :     if (action_formulas::is_action_formula(x))
     847             :     {
     848         207 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
     849             :     }
     850           2 :     else if (data::is_data_expression(x))
     851             :     {
     852           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     853             :     }
     854           2 :     else if (regular_formulas::is_seq(x))
     855             :     {
     856           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
     857             :     }
     858           2 :     else if (regular_formulas::is_alt(x))
     859             :     {
     860           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
     861             :     }
     862           2 :     else if (regular_formulas::is_trans(x))
     863             :     {
     864           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
     865             :     }
     866           2 :     else if (regular_formulas::is_trans_or_nil(x))
     867             :     {
     868           2 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
     869             :     }
     870           0 :     else if (regular_formulas::is_untyped_regular_formula(x))
     871             :     {
     872           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
     873             :     }
     874         209 :     static_cast<Derived&>(*this).leave(x);
     875         209 :     return result;
     876             :   }
     877             : 
     878             : };
     879             : 
     880             : /// \brief Builder class
     881             : template <typename Derived>
     882             : struct data_expression_builder: public add_data_expressions<action_formulas::data_expression_builder, Derived>
     883             : {
     884             : };
     885             : //--- end generated regular_formulas::add_data_expressions code ---//
     886             : 
     887             : //--- start generated regular_formulas::add_variables code ---//
     888             : template <template <class> class Builder, class Derived>
     889             : struct add_variables: public Builder<Derived>
     890             : {
     891             :   typedef Builder<Derived> super;
     892             :   using super::enter;
     893             :   using super::leave;
     894             :   using super::update;
     895             :   using super::apply;
     896             : 
     897             :   regular_formulas::seq apply(const regular_formulas::seq& x)
     898             :   {
     899             :     static_cast<Derived&>(*this).enter(x);
     900             :     regular_formulas::seq result = regular_formulas::seq(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     901             :     static_cast<Derived&>(*this).leave(x);
     902             :     return result;
     903             :   }
     904             : 
     905             :   regular_formulas::alt apply(const regular_formulas::alt& x)
     906             :   {
     907             :     static_cast<Derived&>(*this).enter(x);
     908             :     regular_formulas::alt result = regular_formulas::alt(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     909             :     static_cast<Derived&>(*this).leave(x);
     910             :     return result;
     911             :   }
     912             : 
     913             :   regular_formulas::trans apply(const regular_formulas::trans& x)
     914             :   {
     915             :     static_cast<Derived&>(*this).enter(x);
     916             :     regular_formulas::trans result = regular_formulas::trans(static_cast<Derived&>(*this).apply(x.operand()));
     917             :     static_cast<Derived&>(*this).leave(x);
     918             :     return result;
     919             :   }
     920             : 
     921             :   regular_formulas::trans_or_nil apply(const regular_formulas::trans_or_nil& x)
     922             :   {
     923             :     static_cast<Derived&>(*this).enter(x);
     924             :     regular_formulas::trans_or_nil result = regular_formulas::trans_or_nil(static_cast<Derived&>(*this).apply(x.operand()));
     925             :     static_cast<Derived&>(*this).leave(x);
     926             :     return result;
     927             :   }
     928             : 
     929             :   regular_formulas::untyped_regular_formula apply(const regular_formulas::untyped_regular_formula& x)
     930             :   {
     931             :     static_cast<Derived&>(*this).enter(x);
     932             :     regular_formulas::untyped_regular_formula result = regular_formulas::untyped_regular_formula(x.name(), static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     933             :     static_cast<Derived&>(*this).leave(x);
     934             :     return result;
     935             :   }
     936             : 
     937             :   regular_formulas::regular_formula apply(const regular_formulas::regular_formula& x)
     938             :   {
     939             :     static_cast<Derived&>(*this).enter(x);
     940             :     regular_formulas::regular_formula result;
     941             :     if (action_formulas::is_action_formula(x))
     942             :     {
     943             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
     944             :     }
     945             :     else if (data::is_data_expression(x))
     946             :     {
     947             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     948             :     }
     949             :     else if (regular_formulas::is_seq(x))
     950             :     {
     951             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
     952             :     }
     953             :     else if (regular_formulas::is_alt(x))
     954             :     {
     955             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
     956             :     }
     957             :     else if (regular_formulas::is_trans(x))
     958             :     {
     959             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
     960             :     }
     961             :     else if (regular_formulas::is_trans_or_nil(x))
     962             :     {
     963             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
     964             :     }
     965             :     else if (regular_formulas::is_untyped_regular_formula(x))
     966             :     {
     967             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
     968             :     }
     969             :     static_cast<Derived&>(*this).leave(x);
     970             :     return result;
     971             :   }
     972             : 
     973             : };
     974             : 
     975             : /// \brief Builder class
     976             : template <typename Derived>
     977             : struct variable_builder: public add_variables<action_formulas::data_expression_builder, Derived>
     978             : {
     979             : };
     980             : //--- end generated regular_formulas::add_variables code ---//
     981             : 
     982             : //--- start generated regular_formulas::add_regular_formula_expressions code ---//
     983             : template <template <class> class Builder, class Derived>
     984             : struct add_regular_formula_expressions: public Builder<Derived>
     985             : {
     986             :   typedef Builder<Derived> super;
     987             :   using super::enter;
     988             :   using super::leave;
     989             :   using super::update;
     990             :   using super::apply;
     991             : 
     992           0 :   regular_formulas::seq apply(const regular_formulas::seq& x)
     993             :   {
     994           0 :     static_cast<Derived&>(*this).enter(x);
     995           0 :     regular_formulas::seq result = regular_formulas::seq(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
     996           0 :     static_cast<Derived&>(*this).leave(x);
     997           0 :     return result;
     998             :   }
     999             : 
    1000           0 :   regular_formulas::alt apply(const regular_formulas::alt& x)
    1001             :   {
    1002           0 :     static_cast<Derived&>(*this).enter(x);
    1003           0 :     regular_formulas::alt result = regular_formulas::alt(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1004           0 :     static_cast<Derived&>(*this).leave(x);
    1005           0 :     return result;
    1006             :   }
    1007             : 
    1008           0 :   regular_formulas::trans apply(const regular_formulas::trans& x)
    1009             :   {
    1010           0 :     static_cast<Derived&>(*this).enter(x);
    1011           0 :     regular_formulas::trans result = regular_formulas::trans(static_cast<Derived&>(*this).apply(x.operand()));
    1012           0 :     static_cast<Derived&>(*this).leave(x);
    1013           0 :     return result;
    1014             :   }
    1015             : 
    1016          23 :   regular_formulas::trans_or_nil apply(const regular_formulas::trans_or_nil& x)
    1017             :   {
    1018          23 :     static_cast<Derived&>(*this).enter(x);
    1019          23 :     regular_formulas::trans_or_nil result = regular_formulas::trans_or_nil(static_cast<Derived&>(*this).apply(x.operand()));
    1020          23 :     static_cast<Derived&>(*this).leave(x);
    1021          23 :     return result;
    1022             :   }
    1023             : 
    1024             :   regular_formulas::untyped_regular_formula apply(const regular_formulas::untyped_regular_formula& x)
    1025             :   {
    1026             :     static_cast<Derived&>(*this).enter(x);
    1027             :     regular_formulas::untyped_regular_formula result = regular_formulas::untyped_regular_formula(x.name(), static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1028             :     static_cast<Derived&>(*this).leave(x);
    1029             :     return result;
    1030             :   }
    1031             : 
    1032         233 :   regular_formulas::regular_formula apply(const regular_formulas::regular_formula& x)
    1033             :   {
    1034         233 :     static_cast<Derived&>(*this).enter(x);
    1035         233 :     regular_formulas::regular_formula result;
    1036         233 :     if (action_formulas::is_action_formula(x))
    1037             :     {
    1038         207 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
    1039             :     }
    1040          26 :     else if (data::is_data_expression(x))
    1041             :     {
    1042           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1043             :     }
    1044          26 :     else if (regular_formulas::is_seq(x))
    1045             :     {
    1046           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
    1047             :     }
    1048          26 :     else if (regular_formulas::is_alt(x))
    1049             :     {
    1050           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
    1051             :     }
    1052          26 :     else if (regular_formulas::is_trans(x))
    1053             :     {
    1054           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
    1055             :     }
    1056          26 :     else if (regular_formulas::is_trans_or_nil(x))
    1057             :     {
    1058          23 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
    1059             :     }
    1060           3 :     else if (regular_formulas::is_untyped_regular_formula(x))
    1061             :     {
    1062           3 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
    1063             :     }
    1064         233 :     static_cast<Derived&>(*this).leave(x);
    1065         233 :     return result;
    1066             :   }
    1067             : 
    1068             : };
    1069             : 
    1070             : /// \brief Builder class
    1071             : template <typename Derived>
    1072             : struct regular_formula_builder: public add_regular_formula_expressions<regular_formulas::regular_formula_builder_base, Derived>
    1073             : {
    1074             : };
    1075             : //--- end generated regular_formulas::add_regular_formula_expressions code ---//
    1076             : 
    1077             : } // namespace regular_formulas
    1078             : 
    1079             : namespace state_formulas
    1080             : {
    1081             : 
    1082             : /// \brief Builder class for pbes_expressions. Used as a base class for pbes_expression_builder.
    1083             : template <typename Derived>
    1084             : struct state_formula_builder_base: public core::builder<Derived>
    1085             : {
    1086             :   typedef core::builder<Derived> super;
    1087             :   using super::apply;
    1088             : 
    1089          18 :   state_formula apply(const data::data_expression& x)
    1090             :   {
    1091          18 :     static_cast<Derived&>(*this).enter(x);
    1092             :     // skip
    1093          18 :     static_cast<Derived&>(*this).leave(x);
    1094          18 :     return x;
    1095             :   }
    1096             : };
    1097             : 
    1098             : //--- start generated state_formulas::add_sort_expressions code ---//
    1099             : template <template <class> class Builder, class Derived>
    1100             : struct add_sort_expressions: public Builder<Derived>
    1101             : {
    1102             :   typedef Builder<Derived> super;
    1103             :   using super::enter;
    1104             :   using super::leave;
    1105             :   using super::update;
    1106             :   using super::apply;
    1107             : 
    1108         163 :   state_formulas::true_ apply(const state_formulas::true_& x)
    1109             :   {
    1110         163 :     static_cast<Derived&>(*this).enter(x);
    1111             :     // skip
    1112         163 :     static_cast<Derived&>(*this).leave(x);
    1113         163 :     return x;
    1114             :   }
    1115             : 
    1116          82 :   state_formulas::false_ apply(const state_formulas::false_& x)
    1117             :   {
    1118          82 :     static_cast<Derived&>(*this).enter(x);
    1119             :     // skip
    1120          82 :     static_cast<Derived&>(*this).leave(x);
    1121          82 :     return x;
    1122             :   }
    1123             : 
    1124          92 :   state_formulas::not_ apply(const state_formulas::not_& x)
    1125             :   {
    1126          92 :     static_cast<Derived&>(*this).enter(x);
    1127          92 :     state_formulas::not_ result = state_formulas::not_(static_cast<Derived&>(*this).apply(x.operand()));
    1128          92 :     static_cast<Derived&>(*this).leave(x);
    1129          92 :     return result;
    1130             :   }
    1131             : 
    1132         134 :   state_formulas::and_ apply(const state_formulas::and_& x)
    1133             :   {
    1134         134 :     static_cast<Derived&>(*this).enter(x);
    1135         134 :     state_formulas::and_ result = state_formulas::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1136         134 :     static_cast<Derived&>(*this).leave(x);
    1137         134 :     return result;
    1138             :   }
    1139             : 
    1140          40 :   state_formulas::or_ apply(const state_formulas::or_& x)
    1141             :   {
    1142          40 :     static_cast<Derived&>(*this).enter(x);
    1143          40 :     state_formulas::or_ result = state_formulas::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1144          40 :     static_cast<Derived&>(*this).leave(x);
    1145          40 :     return result;
    1146             :   }
    1147             : 
    1148          38 :   state_formulas::imp apply(const state_formulas::imp& x)
    1149             :   {
    1150          38 :     static_cast<Derived&>(*this).enter(x);
    1151          38 :     state_formulas::imp result = state_formulas::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1152          38 :     static_cast<Derived&>(*this).leave(x);
    1153          38 :     return result;
    1154             :   }
    1155             : 
    1156          28 :   state_formulas::forall apply(const state_formulas::forall& x)
    1157             :   {
    1158          28 :     static_cast<Derived&>(*this).enter(x);
    1159          28 :     state_formulas::forall result = state_formulas::forall(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
    1160          28 :     static_cast<Derived&>(*this).leave(x);
    1161          28 :     return result;
    1162             :   }
    1163             : 
    1164          14 :   state_formulas::exists apply(const state_formulas::exists& x)
    1165             :   {
    1166          14 :     static_cast<Derived&>(*this).enter(x);
    1167          14 :     state_formulas::exists result = state_formulas::exists(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
    1168          14 :     static_cast<Derived&>(*this).leave(x);
    1169          14 :     return result;
    1170             :   }
    1171             : 
    1172         245 :   state_formulas::must apply(const state_formulas::must& x)
    1173             :   {
    1174         245 :     static_cast<Derived&>(*this).enter(x);
    1175         245 :     state_formulas::must result = state_formulas::must(static_cast<Derived&>(*this).apply(x.formula()), static_cast<Derived&>(*this).apply(x.operand()));
    1176         245 :     static_cast<Derived&>(*this).leave(x);
    1177         245 :     return result;
    1178             :   }
    1179             : 
    1180         160 :   state_formulas::may apply(const state_formulas::may& x)
    1181             :   {
    1182         160 :     static_cast<Derived&>(*this).enter(x);
    1183         160 :     state_formulas::may result = state_formulas::may(static_cast<Derived&>(*this).apply(x.formula()), static_cast<Derived&>(*this).apply(x.operand()));
    1184         160 :     static_cast<Derived&>(*this).leave(x);
    1185         160 :     return result;
    1186             :   }
    1187             : 
    1188           0 :   state_formulas::yaled apply(const state_formulas::yaled& x)
    1189             :   {
    1190           0 :     static_cast<Derived&>(*this).enter(x);
    1191             :     // skip
    1192           0 :     static_cast<Derived&>(*this).leave(x);
    1193           0 :     return x;
    1194             :   }
    1195             : 
    1196           3 :   state_formulas::yaled_timed apply(const state_formulas::yaled_timed& x)
    1197             :   {
    1198           3 :     static_cast<Derived&>(*this).enter(x);
    1199           3 :     state_formulas::yaled_timed result = state_formulas::yaled_timed(static_cast<Derived&>(*this).apply(x.time_stamp()));
    1200           3 :     static_cast<Derived&>(*this).leave(x);
    1201           3 :     return result;
    1202             :   }
    1203             : 
    1204           0 :   state_formulas::delay apply(const state_formulas::delay& x)
    1205             :   {
    1206           0 :     static_cast<Derived&>(*this).enter(x);
    1207             :     // skip
    1208           0 :     static_cast<Derived&>(*this).leave(x);
    1209           0 :     return x;
    1210             :   }
    1211             : 
    1212           5 :   state_formulas::delay_timed apply(const state_formulas::delay_timed& x)
    1213             :   {
    1214           5 :     static_cast<Derived&>(*this).enter(x);
    1215           5 :     state_formulas::delay_timed result = state_formulas::delay_timed(static_cast<Derived&>(*this).apply(x.time_stamp()));
    1216           5 :     static_cast<Derived&>(*this).leave(x);
    1217           5 :     return result;
    1218             :   }
    1219             : 
    1220          81 :   state_formulas::variable apply(const state_formulas::variable& x)
    1221             :   {
    1222          81 :     static_cast<Derived&>(*this).enter(x);
    1223          81 :     state_formulas::variable result = state_formulas::variable(x.name(), static_cast<Derived&>(*this).apply(x.arguments()));
    1224          81 :     static_cast<Derived&>(*this).leave(x);
    1225          81 :     return result;
    1226             :   }
    1227             : 
    1228         112 :   state_formulas::nu apply(const state_formulas::nu& x)
    1229             :   {
    1230         112 :     static_cast<Derived&>(*this).enter(x);
    1231         112 :     state_formulas::nu result = state_formulas::nu(x.name(), static_cast<Derived&>(*this).apply(x.assignments()), static_cast<Derived&>(*this).apply(x.operand()));
    1232         112 :     static_cast<Derived&>(*this).leave(x);
    1233         112 :     return result;
    1234             :   }
    1235             : 
    1236         136 :   state_formulas::mu apply(const state_formulas::mu& x)
    1237             :   {
    1238         136 :     static_cast<Derived&>(*this).enter(x);
    1239         136 :     state_formulas::mu result = state_formulas::mu(x.name(), static_cast<Derived&>(*this).apply(x.assignments()), static_cast<Derived&>(*this).apply(x.operand()));
    1240         136 :     static_cast<Derived&>(*this).leave(x);
    1241         136 :     return result;
    1242             :   }
    1243             : 
    1244             :   void update(state_formulas::state_formula_specification& x)
    1245             :   {
    1246             :     static_cast<Derived&>(*this).enter(x);
    1247             :     x.action_labels() = static_cast<Derived&>(*this).apply(x.action_labels());
    1248             :     x.formula() = static_cast<Derived&>(*this).apply(x.formula());
    1249             :     static_cast<Derived&>(*this).leave(x);
    1250             :   }
    1251             : 
    1252        1513 :   state_formulas::state_formula apply(const state_formulas::state_formula& x)
    1253             :   {
    1254        1513 :     static_cast<Derived&>(*this).enter(x);
    1255        1513 :     state_formulas::state_formula result;
    1256        1513 :     if (data::is_data_expression(x))
    1257             :     {
    1258          40 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1259             :     }
    1260        1473 :     else if (data::is_untyped_data_parameter(x))
    1261             :     {
    1262         140 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    1263             :     }
    1264        1333 :     else if (state_formulas::is_true(x))
    1265             :     {
    1266         163 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    1267             :     }
    1268        1170 :     else if (state_formulas::is_false(x))
    1269             :     {
    1270          82 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    1271             :     }
    1272        1088 :     else if (state_formulas::is_not(x))
    1273             :     {
    1274          92 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    1275             :     }
    1276         996 :     else if (state_formulas::is_and(x))
    1277             :     {
    1278         134 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    1279             :     }
    1280         862 :     else if (state_formulas::is_or(x))
    1281             :     {
    1282          40 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    1283             :     }
    1284         822 :     else if (state_formulas::is_imp(x))
    1285             :     {
    1286          38 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    1287             :     }
    1288         784 :     else if (state_formulas::is_forall(x))
    1289             :     {
    1290          28 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    1291             :     }
    1292         756 :     else if (state_formulas::is_exists(x))
    1293             :     {
    1294          14 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    1295             :     }
    1296         742 :     else if (state_formulas::is_must(x))
    1297             :     {
    1298         245 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    1299             :     }
    1300         497 :     else if (state_formulas::is_may(x))
    1301             :     {
    1302         160 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    1303             :     }
    1304         337 :     else if (state_formulas::is_yaled(x))
    1305             :     {
    1306           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    1307             :     }
    1308         337 :     else if (state_formulas::is_yaled_timed(x))
    1309             :     {
    1310           3 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    1311             :     }
    1312         334 :     else if (state_formulas::is_delay(x))
    1313             :     {
    1314           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    1315             :     }
    1316         334 :     else if (state_formulas::is_delay_timed(x))
    1317             :     {
    1318           5 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    1319             :     }
    1320         329 :     else if (state_formulas::is_variable(x))
    1321             :     {
    1322          81 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    1323             :     }
    1324         248 :     else if (state_formulas::is_nu(x))
    1325             :     {
    1326         112 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    1327             :     }
    1328         136 :     else if (state_formulas::is_mu(x))
    1329             :     {
    1330         136 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    1331             :     }
    1332        1513 :     static_cast<Derived&>(*this).leave(x);
    1333        1513 :     return result;
    1334             :   }
    1335             : 
    1336             : };
    1337             : 
    1338             : /// \brief Builder class
    1339             : template <typename Derived>
    1340             : struct sort_expression_builder: public add_sort_expressions<regular_formulas::sort_expression_builder, Derived>
    1341             : {
    1342             : };
    1343             : //--- end generated state_formulas::add_sort_expressions code ---//
    1344             : 
    1345             : //--- start generated state_formulas::add_data_expressions code ---//
    1346             : template <template <class> class Builder, class Derived>
    1347             : struct add_data_expressions: public Builder<Derived>
    1348             : {
    1349             :   typedef Builder<Derived> super;
    1350             :   using super::enter;
    1351             :   using super::leave;
    1352             :   using super::update;
    1353             :   using super::apply;
    1354             : 
    1355          88 :   state_formulas::true_ apply(const state_formulas::true_& x)
    1356             :   {
    1357          88 :     static_cast<Derived&>(*this).enter(x);
    1358             :     // skip
    1359          88 :     static_cast<Derived&>(*this).leave(x);
    1360          88 :     return x;
    1361             :   }
    1362             : 
    1363          36 :   state_formulas::false_ apply(const state_formulas::false_& x)
    1364             :   {
    1365          36 :     static_cast<Derived&>(*this).enter(x);
    1366             :     // skip
    1367          36 :     static_cast<Derived&>(*this).leave(x);
    1368          36 :     return x;
    1369             :   }
    1370             : 
    1371          33 :   state_formulas::not_ apply(const state_formulas::not_& x)
    1372             :   {
    1373          33 :     static_cast<Derived&>(*this).enter(x);
    1374          33 :     state_formulas::not_ result = state_formulas::not_(static_cast<Derived&>(*this).apply(x.operand()));
    1375          33 :     static_cast<Derived&>(*this).leave(x);
    1376          33 :     return result;
    1377             :   }
    1378             : 
    1379          87 :   state_formulas::and_ apply(const state_formulas::and_& x)
    1380             :   {
    1381          87 :     static_cast<Derived&>(*this).enter(x);
    1382          87 :     state_formulas::and_ result = state_formulas::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1383          87 :     static_cast<Derived&>(*this).leave(x);
    1384          87 :     return result;
    1385             :   }
    1386             : 
    1387          32 :   state_formulas::or_ apply(const state_formulas::or_& x)
    1388             :   {
    1389          32 :     static_cast<Derived&>(*this).enter(x);
    1390          32 :     state_formulas::or_ result = state_formulas::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1391          32 :     static_cast<Derived&>(*this).leave(x);
    1392          32 :     return result;
    1393             :   }
    1394             : 
    1395          24 :   state_formulas::imp apply(const state_formulas::imp& x)
    1396             :   {
    1397          24 :     static_cast<Derived&>(*this).enter(x);
    1398          24 :     state_formulas::imp result = state_formulas::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1399          24 :     static_cast<Derived&>(*this).leave(x);
    1400          24 :     return result;
    1401             :   }
    1402             : 
    1403          19 :   state_formulas::forall apply(const state_formulas::forall& x)
    1404             :   {
    1405          19 :     static_cast<Derived&>(*this).enter(x);
    1406          19 :     state_formulas::forall result = state_formulas::forall(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
    1407          19 :     static_cast<Derived&>(*this).leave(x);
    1408          19 :     return result;
    1409             :   }
    1410             : 
    1411           8 :   state_formulas::exists apply(const state_formulas::exists& x)
    1412             :   {
    1413           8 :     static_cast<Derived&>(*this).enter(x);
    1414           8 :     state_formulas::exists result = state_formulas::exists(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
    1415           8 :     static_cast<Derived&>(*this).leave(x);
    1416           8 :     return result;
    1417             :   }
    1418             : 
    1419         132 :   state_formulas::must apply(const state_formulas::must& x)
    1420             :   {
    1421         132 :     static_cast<Derived&>(*this).enter(x);
    1422         132 :     state_formulas::must result = state_formulas::must(static_cast<Derived&>(*this).apply(x.formula()), static_cast<Derived&>(*this).apply(x.operand()));
    1423         132 :     static_cast<Derived&>(*this).leave(x);
    1424         132 :     return result;
    1425             :   }
    1426             : 
    1427          75 :   state_formulas::may apply(const state_formulas::may& x)
    1428             :   {
    1429          75 :     static_cast<Derived&>(*this).enter(x);
    1430          75 :     state_formulas::may result = state_formulas::may(static_cast<Derived&>(*this).apply(x.formula()), static_cast<Derived&>(*this).apply(x.operand()));
    1431          75 :     static_cast<Derived&>(*this).leave(x);
    1432          75 :     return result;
    1433             :   }
    1434             : 
    1435           0 :   state_formulas::yaled apply(const state_formulas::yaled& x)
    1436             :   {
    1437           0 :     static_cast<Derived&>(*this).enter(x);
    1438             :     // skip
    1439           0 :     static_cast<Derived&>(*this).leave(x);
    1440           0 :     return x;
    1441             :   }
    1442             : 
    1443           1 :   state_formulas::yaled_timed apply(const state_formulas::yaled_timed& x)
    1444             :   {
    1445           1 :     static_cast<Derived&>(*this).enter(x);
    1446           1 :     state_formulas::yaled_timed result = state_formulas::yaled_timed(static_cast<Derived&>(*this).apply(x.time_stamp()));
    1447           1 :     static_cast<Derived&>(*this).leave(x);
    1448           1 :     return result;
    1449             :   }
    1450             : 
    1451           0 :   state_formulas::delay apply(const state_formulas::delay& x)
    1452             :   {
    1453           0 :     static_cast<Derived&>(*this).enter(x);
    1454             :     // skip
    1455           0 :     static_cast<Derived&>(*this).leave(x);
    1456           0 :     return x;
    1457             :   }
    1458             : 
    1459           3 :   state_formulas::delay_timed apply(const state_formulas::delay_timed& x)
    1460             :   {
    1461           3 :     static_cast<Derived&>(*this).enter(x);
    1462           3 :     state_formulas::delay_timed result = state_formulas::delay_timed(static_cast<Derived&>(*this).apply(x.time_stamp()));
    1463           3 :     static_cast<Derived&>(*this).leave(x);
    1464           3 :     return result;
    1465             :   }
    1466             : 
    1467         159 :   state_formulas::variable apply(const state_formulas::variable& x)
    1468             :   {
    1469         159 :     static_cast<Derived&>(*this).enter(x);
    1470         159 :     state_formulas::variable result = state_formulas::variable(x.name(), static_cast<Derived&>(*this).apply(x.arguments()));
    1471         159 :     static_cast<Derived&>(*this).leave(x);
    1472         159 :     return result;
    1473             :   }
    1474             : 
    1475          79 :   state_formulas::nu apply(const state_formulas::nu& x)
    1476             :   {
    1477          79 :     static_cast<Derived&>(*this).enter(x);
    1478          79 :     state_formulas::nu result = state_formulas::nu(x.name(), static_cast<Derived&>(*this).apply(x.assignments()), static_cast<Derived&>(*this).apply(x.operand()));
    1479          79 :     static_cast<Derived&>(*this).leave(x);
    1480          79 :     return result;
    1481             :   }
    1482             : 
    1483         103 :   state_formulas::mu apply(const state_formulas::mu& x)
    1484             :   {
    1485         103 :     static_cast<Derived&>(*this).enter(x);
    1486         103 :     state_formulas::mu result = state_formulas::mu(x.name(), static_cast<Derived&>(*this).apply(x.assignments()), static_cast<Derived&>(*this).apply(x.operand()));
    1487         103 :     static_cast<Derived&>(*this).leave(x);
    1488         103 :     return result;
    1489             :   }
    1490             : 
    1491             :   void update(state_formulas::state_formula_specification& x)
    1492             :   {
    1493             :     static_cast<Derived&>(*this).enter(x);
    1494             :     x.formula() = static_cast<Derived&>(*this).apply(x.formula());
    1495             :     static_cast<Derived&>(*this).leave(x);
    1496             :   }
    1497             : 
    1498         903 :   state_formulas::state_formula apply(const state_formulas::state_formula& x)
    1499             :   {
    1500         903 :     static_cast<Derived&>(*this).enter(x);
    1501         903 :     state_formulas::state_formula result;
    1502         903 :     if (data::is_data_expression(x))
    1503             :     {
    1504          24 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1505             :     }
    1506         879 :     else if (data::is_untyped_data_parameter(x))
    1507             :     {
    1508           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    1509             :     }
    1510         879 :     else if (state_formulas::is_true(x))
    1511             :     {
    1512          88 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    1513             :     }
    1514         791 :     else if (state_formulas::is_false(x))
    1515             :     {
    1516          36 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    1517             :     }
    1518         755 :     else if (state_formulas::is_not(x))
    1519             :     {
    1520          33 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    1521             :     }
    1522         722 :     else if (state_formulas::is_and(x))
    1523             :     {
    1524          87 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    1525             :     }
    1526         635 :     else if (state_formulas::is_or(x))
    1527             :     {
    1528          32 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    1529             :     }
    1530         603 :     else if (state_formulas::is_imp(x))
    1531             :     {
    1532          24 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    1533             :     }
    1534         579 :     else if (state_formulas::is_forall(x))
    1535             :     {
    1536          19 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    1537             :     }
    1538         560 :     else if (state_formulas::is_exists(x))
    1539             :     {
    1540           8 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    1541             :     }
    1542         552 :     else if (state_formulas::is_must(x))
    1543             :     {
    1544         132 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    1545             :     }
    1546         420 :     else if (state_formulas::is_may(x))
    1547             :     {
    1548          75 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    1549             :     }
    1550         345 :     else if (state_formulas::is_yaled(x))
    1551             :     {
    1552           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    1553             :     }
    1554         345 :     else if (state_formulas::is_yaled_timed(x))
    1555             :     {
    1556           1 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    1557             :     }
    1558         344 :     else if (state_formulas::is_delay(x))
    1559             :     {
    1560           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    1561             :     }
    1562         344 :     else if (state_formulas::is_delay_timed(x))
    1563             :     {
    1564           3 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    1565             :     }
    1566         341 :     else if (state_formulas::is_variable(x))
    1567             :     {
    1568         159 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    1569             :     }
    1570         182 :     else if (state_formulas::is_nu(x))
    1571             :     {
    1572          79 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    1573             :     }
    1574         103 :     else if (state_formulas::is_mu(x))
    1575             :     {
    1576         103 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    1577             :     }
    1578         903 :     static_cast<Derived&>(*this).leave(x);
    1579         903 :     return result;
    1580             :   }
    1581             : 
    1582             : };
    1583             : 
    1584             : /// \brief Builder class
    1585             : template <typename Derived>
    1586             : struct data_expression_builder: public add_data_expressions<regular_formulas::data_expression_builder, Derived>
    1587             : {
    1588             : };
    1589             : //--- end generated state_formulas::add_data_expressions code ---//
    1590             : 
    1591             : //--- start generated state_formulas::add_variables code ---//
    1592             : template <template <class> class Builder, class Derived>
    1593             : struct add_variables: public Builder<Derived>
    1594             : {
    1595             :   typedef Builder<Derived> super;
    1596             :   using super::enter;
    1597             :   using super::leave;
    1598             :   using super::update;
    1599             :   using super::apply;
    1600             : 
    1601             :   state_formulas::true_ apply(const state_formulas::true_& x)
    1602             :   {
    1603             :     static_cast<Derived&>(*this).enter(x);
    1604             :     // skip
    1605             :     static_cast<Derived&>(*this).leave(x);
    1606             :     return x;
    1607             :   }
    1608             : 
    1609             :   state_formulas::false_ apply(const state_formulas::false_& x)
    1610             :   {
    1611             :     static_cast<Derived&>(*this).enter(x);
    1612             :     // skip
    1613             :     static_cast<Derived&>(*this).leave(x);
    1614             :     return x;
    1615             :   }
    1616             : 
    1617             :   state_formulas::not_ apply(const state_formulas::not_& x)
    1618             :   {
    1619             :     static_cast<Derived&>(*this).enter(x);
    1620             :     state_formulas::not_ result = state_formulas::not_(static_cast<Derived&>(*this).apply(x.operand()));
    1621             :     static_cast<Derived&>(*this).leave(x);
    1622             :     return result;
    1623             :   }
    1624             : 
    1625             :   state_formulas::and_ apply(const state_formulas::and_& x)
    1626             :   {
    1627             :     static_cast<Derived&>(*this).enter(x);
    1628             :     state_formulas::and_ result = state_formulas::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1629             :     static_cast<Derived&>(*this).leave(x);
    1630             :     return result;
    1631             :   }
    1632             : 
    1633             :   state_formulas::or_ apply(const state_formulas::or_& x)
    1634             :   {
    1635             :     static_cast<Derived&>(*this).enter(x);
    1636             :     state_formulas::or_ result = state_formulas::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1637             :     static_cast<Derived&>(*this).leave(x);
    1638             :     return result;
    1639             :   }
    1640             : 
    1641             :   state_formulas::imp apply(const state_formulas::imp& x)
    1642             :   {
    1643             :     static_cast<Derived&>(*this).enter(x);
    1644             :     state_formulas::imp result = state_formulas::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1645             :     static_cast<Derived&>(*this).leave(x);
    1646             :     return result;
    1647             :   }
    1648             : 
    1649             :   state_formulas::forall apply(const state_formulas::forall& x)
    1650             :   {
    1651             :     static_cast<Derived&>(*this).enter(x);
    1652             :     state_formulas::forall result = state_formulas::forall(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
    1653             :     static_cast<Derived&>(*this).leave(x);
    1654             :     return result;
    1655             :   }
    1656             : 
    1657             :   state_formulas::exists apply(const state_formulas::exists& x)
    1658             :   {
    1659             :     static_cast<Derived&>(*this).enter(x);
    1660             :     state_formulas::exists result = state_formulas::exists(static_cast<Derived&>(*this).apply(x.variables()), static_cast<Derived&>(*this).apply(x.body()));
    1661             :     static_cast<Derived&>(*this).leave(x);
    1662             :     return result;
    1663             :   }
    1664             : 
    1665             :   state_formulas::must apply(const state_formulas::must& x)
    1666             :   {
    1667             :     static_cast<Derived&>(*this).enter(x);
    1668             :     state_formulas::must result = state_formulas::must(static_cast<Derived&>(*this).apply(x.formula()), static_cast<Derived&>(*this).apply(x.operand()));
    1669             :     static_cast<Derived&>(*this).leave(x);
    1670             :     return result;
    1671             :   }
    1672             : 
    1673             :   state_formulas::may apply(const state_formulas::may& x)
    1674             :   {
    1675             :     static_cast<Derived&>(*this).enter(x);
    1676             :     state_formulas::may result = state_formulas::may(static_cast<Derived&>(*this).apply(x.formula()), static_cast<Derived&>(*this).apply(x.operand()));
    1677             :     static_cast<Derived&>(*this).leave(x);
    1678             :     return result;
    1679             :   }
    1680             : 
    1681             :   state_formulas::yaled apply(const state_formulas::yaled& x)
    1682             :   {
    1683             :     static_cast<Derived&>(*this).enter(x);
    1684             :     // skip
    1685             :     static_cast<Derived&>(*this).leave(x);
    1686             :     return x;
    1687             :   }
    1688             : 
    1689             :   state_formulas::yaled_timed apply(const state_formulas::yaled_timed& x)
    1690             :   {
    1691             :     static_cast<Derived&>(*this).enter(x);
    1692             :     state_formulas::yaled_timed result = state_formulas::yaled_timed(static_cast<Derived&>(*this).apply(x.time_stamp()));
    1693             :     static_cast<Derived&>(*this).leave(x);
    1694             :     return result;
    1695             :   }
    1696             : 
    1697             :   state_formulas::delay apply(const state_formulas::delay& x)
    1698             :   {
    1699             :     static_cast<Derived&>(*this).enter(x);
    1700             :     // skip
    1701             :     static_cast<Derived&>(*this).leave(x);
    1702             :     return x;
    1703             :   }
    1704             : 
    1705             :   state_formulas::delay_timed apply(const state_formulas::delay_timed& x)
    1706             :   {
    1707             :     static_cast<Derived&>(*this).enter(x);
    1708             :     state_formulas::delay_timed result = state_formulas::delay_timed(static_cast<Derived&>(*this).apply(x.time_stamp()));
    1709             :     static_cast<Derived&>(*this).leave(x);
    1710             :     return result;
    1711             :   }
    1712             : 
    1713             :   state_formulas::variable apply(const state_formulas::variable& x)
    1714             :   {
    1715             :     static_cast<Derived&>(*this).enter(x);
    1716             :     state_formulas::variable result = state_formulas::variable(x.name(), static_cast<Derived&>(*this).apply(x.arguments()));
    1717             :     static_cast<Derived&>(*this).leave(x);
    1718             :     return result;
    1719             :   }
    1720             : 
    1721             :   state_formulas::nu apply(const state_formulas::nu& x)
    1722             :   {
    1723             :     static_cast<Derived&>(*this).enter(x);
    1724             :     state_formulas::nu result = state_formulas::nu(x.name(), static_cast<Derived&>(*this).apply(x.assignments()), static_cast<Derived&>(*this).apply(x.operand()));
    1725             :     static_cast<Derived&>(*this).leave(x);
    1726             :     return result;
    1727             :   }
    1728             : 
    1729             :   state_formulas::mu apply(const state_formulas::mu& x)
    1730             :   {
    1731             :     static_cast<Derived&>(*this).enter(x);
    1732             :     state_formulas::mu result = state_formulas::mu(x.name(), static_cast<Derived&>(*this).apply(x.assignments()), static_cast<Derived&>(*this).apply(x.operand()));
    1733             :     static_cast<Derived&>(*this).leave(x);
    1734             :     return result;
    1735             :   }
    1736             : 
    1737             :   void update(state_formulas::state_formula_specification& x)
    1738             :   {
    1739             :     static_cast<Derived&>(*this).enter(x);
    1740             :     x.formula() = static_cast<Derived&>(*this).apply(x.formula());
    1741             :     static_cast<Derived&>(*this).leave(x);
    1742             :   }
    1743             : 
    1744             :   state_formulas::state_formula apply(const state_formulas::state_formula& x)
    1745             :   {
    1746             :     static_cast<Derived&>(*this).enter(x);
    1747             :     state_formulas::state_formula result;
    1748             :     if (data::is_data_expression(x))
    1749             :     {
    1750             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1751             :     }
    1752             :     else if (data::is_untyped_data_parameter(x))
    1753             :     {
    1754             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    1755             :     }
    1756             :     else if (state_formulas::is_true(x))
    1757             :     {
    1758             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    1759             :     }
    1760             :     else if (state_formulas::is_false(x))
    1761             :     {
    1762             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    1763             :     }
    1764             :     else if (state_formulas::is_not(x))
    1765             :     {
    1766             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    1767             :     }
    1768             :     else if (state_formulas::is_and(x))
    1769             :     {
    1770             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    1771             :     }
    1772             :     else if (state_formulas::is_or(x))
    1773             :     {
    1774             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    1775             :     }
    1776             :     else if (state_formulas::is_imp(x))
    1777             :     {
    1778             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    1779             :     }
    1780             :     else if (state_formulas::is_forall(x))
    1781             :     {
    1782             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    1783             :     }
    1784             :     else if (state_formulas::is_exists(x))
    1785             :     {
    1786             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    1787             :     }
    1788             :     else if (state_formulas::is_must(x))
    1789             :     {
    1790             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    1791             :     }
    1792             :     else if (state_formulas::is_may(x))
    1793             :     {
    1794             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    1795             :     }
    1796             :     else if (state_formulas::is_yaled(x))
    1797             :     {
    1798             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    1799             :     }
    1800             :     else if (state_formulas::is_yaled_timed(x))
    1801             :     {
    1802             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    1803             :     }
    1804             :     else if (state_formulas::is_delay(x))
    1805             :     {
    1806             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    1807             :     }
    1808             :     else if (state_formulas::is_delay_timed(x))
    1809             :     {
    1810             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    1811             :     }
    1812             :     else if (state_formulas::is_variable(x))
    1813             :     {
    1814             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    1815             :     }
    1816             :     else if (state_formulas::is_nu(x))
    1817             :     {
    1818             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    1819             :     }
    1820             :     else if (state_formulas::is_mu(x))
    1821             :     {
    1822             :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    1823             :     }
    1824             :     static_cast<Derived&>(*this).leave(x);
    1825             :     return result;
    1826             :   }
    1827             : 
    1828             : };
    1829             : 
    1830             : /// \brief Builder class
    1831             : template <typename Derived>
    1832             : struct variable_builder: public add_variables<regular_formulas::data_expression_builder, Derived>
    1833             : {
    1834             : };
    1835             : //--- end generated state_formulas::add_variables code ---//
    1836             : 
    1837             : //--- start generated state_formulas::add_state_formula_expressions code ---//
    1838             : template <template <class> class Builder, class Derived>
    1839             : struct add_state_formula_expressions: public Builder<Derived>
    1840             : {
    1841             :   typedef Builder<Derived> super;
    1842             :   using super::enter;
    1843             :   using super::leave;
    1844             :   using super::update;
    1845             :   using super::apply;
    1846             : 
    1847         172 :   state_formulas::true_ apply(const state_formulas::true_& x)
    1848             :   {
    1849         172 :     static_cast<Derived&>(*this).enter(x);
    1850             :     // skip
    1851         172 :     static_cast<Derived&>(*this).leave(x);
    1852         172 :     return x;
    1853             :   }
    1854             : 
    1855          82 :   state_formulas::false_ apply(const state_formulas::false_& x)
    1856             :   {
    1857          82 :     static_cast<Derived&>(*this).enter(x);
    1858             :     // skip
    1859          82 :     static_cast<Derived&>(*this).leave(x);
    1860          82 :     return x;
    1861             :   }
    1862             : 
    1863         102 :   state_formulas::not_ apply(const state_formulas::not_& x)
    1864             :   {
    1865         102 :     static_cast<Derived&>(*this).enter(x);
    1866         102 :     state_formulas::not_ result = state_formulas::not_(static_cast<Derived&>(*this).apply(x.operand()));
    1867         102 :     static_cast<Derived&>(*this).leave(x);
    1868         102 :     return result;
    1869             :   }
    1870             : 
    1871         151 :   state_formulas::and_ apply(const state_formulas::and_& x)
    1872             :   {
    1873         151 :     static_cast<Derived&>(*this).enter(x);
    1874         151 :     state_formulas::and_ result = state_formulas::and_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1875         150 :     static_cast<Derived&>(*this).leave(x);
    1876         150 :     return result;
    1877             :   }
    1878             : 
    1879          44 :   state_formulas::or_ apply(const state_formulas::or_& x)
    1880             :   {
    1881          44 :     static_cast<Derived&>(*this).enter(x);
    1882          44 :     state_formulas::or_ result = state_formulas::or_(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1883          44 :     static_cast<Derived&>(*this).leave(x);
    1884          44 :     return result;
    1885             :   }
    1886             : 
    1887          39 :   state_formulas::imp apply(const state_formulas::imp& x)
    1888             :   {
    1889          39 :     static_cast<Derived&>(*this).enter(x);
    1890          39 :     state_formulas::imp result = state_formulas::imp(static_cast<Derived&>(*this).apply(x.left()), static_cast<Derived&>(*this).apply(x.right()));
    1891          39 :     static_cast<Derived&>(*this).leave(x);
    1892          39 :     return result;
    1893             :   }
    1894             : 
    1895           9 :   state_formulas::forall apply(const state_formulas::forall& x)
    1896             :   {
    1897           9 :     static_cast<Derived&>(*this).enter(x);
    1898           9 :     state_formulas::forall result = state_formulas::forall(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
    1899           9 :     static_cast<Derived&>(*this).leave(x);
    1900           9 :     return result;
    1901             :   }
    1902             : 
    1903           6 :   state_formulas::exists apply(const state_formulas::exists& x)
    1904             :   {
    1905           6 :     static_cast<Derived&>(*this).enter(x);
    1906           6 :     state_formulas::exists result = state_formulas::exists(x.variables(), static_cast<Derived&>(*this).apply(x.body()));
    1907           6 :     static_cast<Derived&>(*this).leave(x);
    1908           6 :     return result;
    1909             :   }
    1910             : 
    1911         135 :   state_formulas::must apply(const state_formulas::must& x)
    1912             :   {
    1913         135 :     static_cast<Derived&>(*this).enter(x);
    1914         135 :     state_formulas::must result = state_formulas::must(x.formula(), static_cast<Derived&>(*this).apply(x.operand()));
    1915         135 :     static_cast<Derived&>(*this).leave(x);
    1916         135 :     return result;
    1917             :   }
    1918             : 
    1919          90 :   state_formulas::may apply(const state_formulas::may& x)
    1920             :   {
    1921          90 :     static_cast<Derived&>(*this).enter(x);
    1922          90 :     state_formulas::may result = state_formulas::may(x.formula(), static_cast<Derived&>(*this).apply(x.operand()));
    1923          90 :     static_cast<Derived&>(*this).leave(x);
    1924          90 :     return result;
    1925             :   }
    1926             : 
    1927           0 :   state_formulas::yaled apply(const state_formulas::yaled& x)
    1928             :   {
    1929           0 :     static_cast<Derived&>(*this).enter(x);
    1930             :     // skip
    1931           0 :     static_cast<Derived&>(*this).leave(x);
    1932           0 :     return x;
    1933             :   }
    1934             : 
    1935           2 :   state_formulas::yaled_timed apply(const state_formulas::yaled_timed& x)
    1936             :   {
    1937           2 :     static_cast<Derived&>(*this).enter(x);
    1938             :     // skip
    1939           2 :     static_cast<Derived&>(*this).leave(x);
    1940           2 :     return x;
    1941             :   }
    1942             : 
    1943           0 :   state_formulas::delay apply(const state_formulas::delay& x)
    1944             :   {
    1945           0 :     static_cast<Derived&>(*this).enter(x);
    1946             :     // skip
    1947           0 :     static_cast<Derived&>(*this).leave(x);
    1948           0 :     return x;
    1949             :   }
    1950             : 
    1951           2 :   state_formulas::delay_timed apply(const state_formulas::delay_timed& x)
    1952             :   {
    1953           2 :     static_cast<Derived&>(*this).enter(x);
    1954             :     // skip
    1955           2 :     static_cast<Derived&>(*this).leave(x);
    1956           2 :     return x;
    1957             :   }
    1958             : 
    1959          13 :   state_formulas::variable apply(const state_formulas::variable& x)
    1960             :   {
    1961          13 :     static_cast<Derived&>(*this).enter(x);
    1962             :     // skip
    1963          13 :     static_cast<Derived&>(*this).leave(x);
    1964          13 :     return x;
    1965             :   }
    1966             : 
    1967           1 :   state_formulas::nu apply(const state_formulas::nu& x)
    1968             :   {
    1969           1 :     static_cast<Derived&>(*this).enter(x);
    1970           1 :     state_formulas::nu result = state_formulas::nu(x.name(), x.assignments(), static_cast<Derived&>(*this).apply(x.operand()));
    1971           1 :     static_cast<Derived&>(*this).leave(x);
    1972           1 :     return result;
    1973             :   }
    1974             : 
    1975           8 :   state_formulas::mu apply(const state_formulas::mu& x)
    1976             :   {
    1977           8 :     static_cast<Derived&>(*this).enter(x);
    1978           8 :     state_formulas::mu result = state_formulas::mu(x.name(), x.assignments(), static_cast<Derived&>(*this).apply(x.operand()));
    1979           8 :     static_cast<Derived&>(*this).leave(x);
    1980           8 :     return result;
    1981             :   }
    1982             : 
    1983             :   void update(state_formulas::state_formula_specification& x)
    1984             :   {
    1985             :     static_cast<Derived&>(*this).enter(x);
    1986             :     x.formula() = static_cast<Derived&>(*this).apply(x.formula());
    1987             :     static_cast<Derived&>(*this).leave(x);
    1988             :   }
    1989             : 
    1990        2065 :   state_formulas::state_formula apply(const state_formulas::state_formula& x)
    1991             :   {
    1992        2065 :     static_cast<Derived&>(*this).enter(x);
    1993        2065 :     state_formulas::state_formula result;
    1994        2065 :     if (data::is_data_expression(x))
    1995             :     {
    1996          56 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1997             :     }
    1998        2009 :     else if (data::is_untyped_data_parameter(x))
    1999             :     {
    2000         139 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    2001             :     }
    2002        1870 :     else if (state_formulas::is_true(x))
    2003             :     {
    2004         209 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    2005             :     }
    2006        1661 :     else if (state_formulas::is_false(x))
    2007             :     {
    2008         101 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    2009             :     }
    2010        1560 :     else if (state_formulas::is_not(x))
    2011             :     {
    2012         201 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    2013             :     }
    2014        1359 :     else if (state_formulas::is_and(x))
    2015             :     {
    2016         181 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    2017             :     }
    2018        1178 :     else if (state_formulas::is_or(x))
    2019             :     {
    2020          64 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    2021             :     }
    2022        1114 :     else if (state_formulas::is_imp(x))
    2023             :     {
    2024          54 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    2025             :     }
    2026        1060 :     else if (state_formulas::is_forall(x))
    2027             :     {
    2028          31 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    2029             :     }
    2030        1029 :     else if (state_formulas::is_exists(x))
    2031             :     {
    2032          17 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    2033             :     }
    2034        1012 :     else if (state_formulas::is_must(x))
    2035             :     {
    2036         316 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    2037             :     }
    2038         696 :     else if (state_formulas::is_may(x))
    2039             :     {
    2040         209 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    2041             :     }
    2042         487 :     else if (state_formulas::is_yaled(x))
    2043             :     {
    2044           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    2045             :     }
    2046         487 :     else if (state_formulas::is_yaled_timed(x))
    2047             :     {
    2048           4 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    2049             :     }
    2050         483 :     else if (state_formulas::is_delay(x))
    2051             :     {
    2052           0 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    2053             :     }
    2054         483 :     else if (state_formulas::is_delay_timed(x))
    2055             :     {
    2056           6 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    2057             :     }
    2058         477 :     else if (state_formulas::is_variable(x))
    2059             :     {
    2060         167 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    2061             :     }
    2062         310 :     else if (state_formulas::is_nu(x))
    2063             :     {
    2064         132 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    2065             :     }
    2066         178 :     else if (state_formulas::is_mu(x))
    2067             :     {
    2068         178 :       result = static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    2069             :     }
    2070        2058 :     static_cast<Derived&>(*this).leave(x);
    2071        2058 :     return result;
    2072             :   }
    2073             : 
    2074             : };
    2075             : 
    2076             : /// \brief Builder class
    2077             : template <typename Derived>
    2078             : struct state_formula_builder: public add_state_formula_expressions<state_formulas::state_formula_builder_base, Derived>
    2079             : {
    2080             : };
    2081             : //--- end generated state_formulas::add_state_formula_expressions code ---//
    2082             : 
    2083             : } // namespace state_formulas
    2084             : 
    2085             : } // namespace mcrl2
    2086             : 
    2087             : #endif // MCRL2_MODAL_FORMULA_BUILDER_H

Generated by: LCOV version 1.13