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/traverser.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_TRAVERSER_H
      13             : #define MCRL2_MODAL_FORMULA_TRAVERSER_H
      14             : 
      15             : #include "mcrl2/lps/traverser.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_traverser.
      25             : template <typename Derived>
      26             : struct action_formula_traverser_base: public core::traverser<Derived>
      27             : {
      28             :   typedef core::traverser<Derived> super;
      29             :   using super::apply;
      30             :   using super::enter;
      31             :   using super::leave;
      32             : 
      33           0 :   void apply(const data::data_expression& x)
      34             :   {
      35           0 :     static_cast<Derived&>(*this).enter(x);
      36             :     // skip
      37           0 :     static_cast<Derived&>(*this).leave(x);
      38           0 :   }
      39             : };
      40             : 
      41             : //--- start generated action_formulas::add_traverser_sort_expressions code ---//
      42             : template <template <class> class Traverser, class Derived>
      43             : struct add_traverser_sort_expressions: public Traverser<Derived>
      44             : {
      45             :   typedef Traverser<Derived> super;
      46             :   using super::enter;
      47             :   using super::leave;
      48             :   using super::apply;
      49             : 
      50          60 :   void apply(const action_formulas::true_& x)
      51             :   {
      52          60 :     static_cast<Derived&>(*this).enter(x);
      53             :     // skip
      54          60 :     static_cast<Derived&>(*this).leave(x);
      55          60 :   }
      56             : 
      57           2 :   void apply(const action_formulas::false_& x)
      58             :   {
      59           2 :     static_cast<Derived&>(*this).enter(x);
      60             :     // skip
      61           2 :     static_cast<Derived&>(*this).leave(x);
      62           2 :   }
      63             : 
      64          35 :   void apply(const action_formulas::not_& x)
      65             :   {
      66          35 :     static_cast<Derived&>(*this).enter(x);
      67          35 :     static_cast<Derived&>(*this).apply(x.operand());
      68          35 :     static_cast<Derived&>(*this).leave(x);
      69          35 :   }
      70             : 
      71           9 :   void apply(const action_formulas::and_& x)
      72             :   {
      73           9 :     static_cast<Derived&>(*this).enter(x);
      74           9 :     static_cast<Derived&>(*this).apply(x.left());
      75           9 :     static_cast<Derived&>(*this).apply(x.right());
      76           9 :     static_cast<Derived&>(*this).leave(x);
      77           9 :   }
      78             : 
      79           3 :   void apply(const action_formulas::or_& x)
      80             :   {
      81           3 :     static_cast<Derived&>(*this).enter(x);
      82           3 :     static_cast<Derived&>(*this).apply(x.left());
      83           3 :     static_cast<Derived&>(*this).apply(x.right());
      84           3 :     static_cast<Derived&>(*this).leave(x);
      85           3 :   }
      86             : 
      87           0 :   void apply(const action_formulas::imp& x)
      88             :   {
      89           0 :     static_cast<Derived&>(*this).enter(x);
      90           0 :     static_cast<Derived&>(*this).apply(x.left());
      91           0 :     static_cast<Derived&>(*this).apply(x.right());
      92           0 :     static_cast<Derived&>(*this).leave(x);
      93           0 :   }
      94             : 
      95           3 :   void apply(const action_formulas::forall& x)
      96             :   {
      97           3 :     static_cast<Derived&>(*this).enter(x);
      98           3 :     static_cast<Derived&>(*this).apply(x.variables());
      99           3 :     static_cast<Derived&>(*this).apply(x.body());
     100           3 :     static_cast<Derived&>(*this).leave(x);
     101           3 :   }
     102             : 
     103           2 :   void apply(const action_formulas::exists& x)
     104             :   {
     105           2 :     static_cast<Derived&>(*this).enter(x);
     106           2 :     static_cast<Derived&>(*this).apply(x.variables());
     107           2 :     static_cast<Derived&>(*this).apply(x.body());
     108           2 :     static_cast<Derived&>(*this).leave(x);
     109           2 :   }
     110             : 
     111           0 :   void apply(const action_formulas::at& x)
     112             :   {
     113           0 :     static_cast<Derived&>(*this).enter(x);
     114           0 :     static_cast<Derived&>(*this).apply(x.operand());
     115           0 :     static_cast<Derived&>(*this).apply(x.time_stamp());
     116           0 :     static_cast<Derived&>(*this).leave(x);
     117           0 :   }
     118             : 
     119         172 :   void apply(const action_formulas::multi_action& x)
     120             :   {
     121         172 :     static_cast<Derived&>(*this).enter(x);
     122         172 :     static_cast<Derived&>(*this).apply(x.actions());
     123         172 :     static_cast<Derived&>(*this).leave(x);
     124         172 :   }
     125             : 
     126         381 :   void apply(const action_formulas::action_formula& x)
     127             :   {
     128         381 :     static_cast<Derived&>(*this).enter(x);
     129         381 :     if (data::is_data_expression(x))
     130             :     {
     131           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     132             :     }
     133         381 :     else if (data::is_untyped_data_parameter(x))
     134             :     {
     135           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     136             :     }
     137         381 :     else if (action_formulas::is_true(x))
     138             :     {
     139          74 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
     140             :     }
     141         307 :     else if (action_formulas::is_false(x))
     142             :     {
     143           4 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
     144             :     }
     145         303 :     else if (action_formulas::is_not(x))
     146             :     {
     147          40 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
     148             :     }
     149         263 :     else if (action_formulas::is_and(x))
     150             :     {
     151          10 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
     152             :     }
     153         253 :     else if (action_formulas::is_or(x))
     154             :     {
     155           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
     156             :     }
     157         250 :     else if (action_formulas::is_imp(x))
     158             :     {
     159           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
     160             :     }
     161         250 :     else if (action_formulas::is_forall(x))
     162             :     {
     163           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
     164             :     }
     165         247 :     else if (action_formulas::is_exists(x))
     166             :     {
     167           2 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
     168             :     }
     169         245 :     else if (action_formulas::is_at(x))
     170             :     {
     171           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
     172             :     }
     173         245 :     else if (action_formulas::is_multi_action(x))
     174             :     {
     175         242 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
     176             :     }
     177           3 :     else if (process::is_untyped_multi_action(x))
     178             :     {
     179           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
     180             :     }
     181         381 :     static_cast<Derived&>(*this).leave(x);
     182         381 :   }
     183             : 
     184             : };
     185             : 
     186             : /// \\brief Traverser class
     187             : template <typename Derived>
     188             : struct sort_expression_traverser: public add_traverser_sort_expressions<lps::sort_expression_traverser, Derived>
     189             : {
     190             : };
     191             : //--- end generated action_formulas::add_traverser_sort_expressions code ---//
     192             : 
     193             : //--- start generated action_formulas::add_traverser_data_expressions code ---//
     194             : template <template <class> class Traverser, class Derived>
     195             : struct add_traverser_data_expressions: public Traverser<Derived>
     196             : {
     197             :   typedef Traverser<Derived> super;
     198             :   using super::enter;
     199             :   using super::leave;
     200             :   using super::apply;
     201             : 
     202           0 :   void apply(const action_formulas::true_& x)
     203             :   {
     204           0 :     static_cast<Derived&>(*this).enter(x);
     205             :     // skip
     206           0 :     static_cast<Derived&>(*this).leave(x);
     207           0 :   }
     208             : 
     209           0 :   void apply(const action_formulas::false_& x)
     210             :   {
     211           0 :     static_cast<Derived&>(*this).enter(x);
     212             :     // skip
     213           0 :     static_cast<Derived&>(*this).leave(x);
     214           0 :   }
     215             : 
     216           0 :   void apply(const action_formulas::not_& x)
     217             :   {
     218           0 :     static_cast<Derived&>(*this).enter(x);
     219           0 :     static_cast<Derived&>(*this).apply(x.operand());
     220           0 :     static_cast<Derived&>(*this).leave(x);
     221           0 :   }
     222             : 
     223           0 :   void apply(const action_formulas::and_& x)
     224             :   {
     225           0 :     static_cast<Derived&>(*this).enter(x);
     226           0 :     static_cast<Derived&>(*this).apply(x.left());
     227           0 :     static_cast<Derived&>(*this).apply(x.right());
     228           0 :     static_cast<Derived&>(*this).leave(x);
     229           0 :   }
     230             : 
     231           0 :   void apply(const action_formulas::or_& x)
     232             :   {
     233           0 :     static_cast<Derived&>(*this).enter(x);
     234           0 :     static_cast<Derived&>(*this).apply(x.left());
     235           0 :     static_cast<Derived&>(*this).apply(x.right());
     236           0 :     static_cast<Derived&>(*this).leave(x);
     237           0 :   }
     238             : 
     239           0 :   void apply(const action_formulas::imp& x)
     240             :   {
     241           0 :     static_cast<Derived&>(*this).enter(x);
     242           0 :     static_cast<Derived&>(*this).apply(x.left());
     243           0 :     static_cast<Derived&>(*this).apply(x.right());
     244           0 :     static_cast<Derived&>(*this).leave(x);
     245           0 :   }
     246             : 
     247           0 :   void apply(const action_formulas::forall& x)
     248             :   {
     249           0 :     static_cast<Derived&>(*this).enter(x);
     250           0 :     static_cast<Derived&>(*this).apply(x.body());
     251           0 :     static_cast<Derived&>(*this).leave(x);
     252           0 :   }
     253             : 
     254           0 :   void apply(const action_formulas::exists& x)
     255             :   {
     256           0 :     static_cast<Derived&>(*this).enter(x);
     257           0 :     static_cast<Derived&>(*this).apply(x.body());
     258           0 :     static_cast<Derived&>(*this).leave(x);
     259           0 :   }
     260             : 
     261           0 :   void apply(const action_formulas::at& x)
     262             :   {
     263           0 :     static_cast<Derived&>(*this).enter(x);
     264           0 :     static_cast<Derived&>(*this).apply(x.operand());
     265           0 :     static_cast<Derived&>(*this).apply(x.time_stamp());
     266           0 :     static_cast<Derived&>(*this).leave(x);
     267           0 :   }
     268             : 
     269           0 :   void apply(const action_formulas::multi_action& x)
     270             :   {
     271           0 :     static_cast<Derived&>(*this).enter(x);
     272           0 :     static_cast<Derived&>(*this).apply(x.actions());
     273           0 :     static_cast<Derived&>(*this).leave(x);
     274           0 :   }
     275             : 
     276           0 :   void apply(const action_formulas::action_formula& x)
     277             :   {
     278           0 :     static_cast<Derived&>(*this).enter(x);
     279           0 :     if (data::is_data_expression(x))
     280             :     {
     281           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     282             :     }
     283           0 :     else if (data::is_untyped_data_parameter(x))
     284             :     {
     285           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     286             :     }
     287           0 :     else if (action_formulas::is_true(x))
     288             :     {
     289           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
     290             :     }
     291           0 :     else if (action_formulas::is_false(x))
     292             :     {
     293           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
     294             :     }
     295           0 :     else if (action_formulas::is_not(x))
     296             :     {
     297           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
     298             :     }
     299           0 :     else if (action_formulas::is_and(x))
     300             :     {
     301           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
     302             :     }
     303           0 :     else if (action_formulas::is_or(x))
     304             :     {
     305           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
     306             :     }
     307           0 :     else if (action_formulas::is_imp(x))
     308             :     {
     309           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
     310             :     }
     311           0 :     else if (action_formulas::is_forall(x))
     312             :     {
     313           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
     314             :     }
     315           0 :     else if (action_formulas::is_exists(x))
     316             :     {
     317           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
     318             :     }
     319           0 :     else if (action_formulas::is_at(x))
     320             :     {
     321           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
     322             :     }
     323           0 :     else if (action_formulas::is_multi_action(x))
     324             :     {
     325           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
     326             :     }
     327           0 :     else if (process::is_untyped_multi_action(x))
     328             :     {
     329           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
     330             :     }
     331           0 :     static_cast<Derived&>(*this).leave(x);
     332           0 :   }
     333             : 
     334             : };
     335             : 
     336             : /// \\brief Traverser class
     337             : template <typename Derived>
     338             : struct data_expression_traverser: public add_traverser_data_expressions<lps::data_expression_traverser, Derived>
     339             : {
     340             : };
     341             : //--- end generated action_formulas::add_traverser_data_expressions code ---//
     342             : 
     343             : //--- start generated action_formulas::add_traverser_action_formula_expressions code ---//
     344             : template <template <class> class Traverser, class Derived>
     345             : struct add_traverser_action_formula_expressions: public Traverser<Derived>
     346             : {
     347             :   typedef Traverser<Derived> super;
     348             :   using super::enter;
     349             :   using super::leave;
     350             :   using super::apply;
     351             : 
     352         311 :   void apply(const action_formulas::true_& x)
     353             :   {
     354         311 :     static_cast<Derived&>(*this).enter(x);
     355             :     // skip
     356         311 :     static_cast<Derived&>(*this).leave(x);
     357         311 :   }
     358             : 
     359          25 :   void apply(const action_formulas::false_& x)
     360             :   {
     361          25 :     static_cast<Derived&>(*this).enter(x);
     362             :     // skip
     363          25 :     static_cast<Derived&>(*this).leave(x);
     364          25 :   }
     365             : 
     366             :   void apply(const action_formulas::not_& x)
     367             :   {
     368             :     static_cast<Derived&>(*this).enter(x);
     369             :     static_cast<Derived&>(*this).apply(x.operand());
     370             :     static_cast<Derived&>(*this).leave(x);
     371             :   }
     372             : 
     373          39 :   void apply(const action_formulas::and_& x)
     374             :   {
     375          39 :     static_cast<Derived&>(*this).enter(x);
     376          39 :     static_cast<Derived&>(*this).apply(x.left());
     377          39 :     static_cast<Derived&>(*this).apply(x.right());
     378          39 :     static_cast<Derived&>(*this).leave(x);
     379          39 :   }
     380             : 
     381          12 :   void apply(const action_formulas::or_& x)
     382             :   {
     383          12 :     static_cast<Derived&>(*this).enter(x);
     384          12 :     static_cast<Derived&>(*this).apply(x.left());
     385          12 :     static_cast<Derived&>(*this).apply(x.right());
     386          12 :     static_cast<Derived&>(*this).leave(x);
     387          12 :   }
     388             : 
     389           0 :   void apply(const action_formulas::imp& x)
     390             :   {
     391           0 :     static_cast<Derived&>(*this).enter(x);
     392           0 :     static_cast<Derived&>(*this).apply(x.left());
     393           0 :     static_cast<Derived&>(*this).apply(x.right());
     394           0 :     static_cast<Derived&>(*this).leave(x);
     395           0 :   }
     396             : 
     397             :   void apply(const action_formulas::forall& x)
     398             :   {
     399             :     static_cast<Derived&>(*this).enter(x);
     400             :     static_cast<Derived&>(*this).apply(x.body());
     401             :     static_cast<Derived&>(*this).leave(x);
     402             :   }
     403             : 
     404             :   void apply(const action_formulas::exists& x)
     405             :   {
     406             :     static_cast<Derived&>(*this).enter(x);
     407             :     static_cast<Derived&>(*this).apply(x.body());
     408             :     static_cast<Derived&>(*this).leave(x);
     409             :   }
     410             : 
     411             :   void apply(const action_formulas::at& x)
     412             :   {
     413             :     static_cast<Derived&>(*this).enter(x);
     414             :     static_cast<Derived&>(*this).apply(x.operand());
     415             :     static_cast<Derived&>(*this).leave(x);
     416             :   }
     417             : 
     418         813 :   void apply(const action_formulas::multi_action& x)
     419             :   {
     420         813 :     static_cast<Derived&>(*this).enter(x);
     421             :     // skip
     422         813 :     static_cast<Derived&>(*this).leave(x);
     423         813 :   }
     424             : 
     425        1335 :   void apply(const action_formulas::action_formula& x)
     426             :   {
     427        1335 :     static_cast<Derived&>(*this).enter(x);
     428        1335 :     if (data::is_data_expression(x))
     429             :     {
     430           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     431             :     }
     432        1335 :     else if (data::is_untyped_data_parameter(x))
     433             :     {
     434           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     435             :     }
     436        1335 :     else if (action_formulas::is_true(x))
     437             :     {
     438         311 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
     439             :     }
     440        1024 :     else if (action_formulas::is_false(x))
     441             :     {
     442          25 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
     443             :     }
     444         999 :     else if (action_formulas::is_not(x))
     445             :     {
     446         126 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
     447             :     }
     448         873 :     else if (action_formulas::is_and(x))
     449             :     {
     450          39 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
     451             :     }
     452         834 :     else if (action_formulas::is_or(x))
     453             :     {
     454          12 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
     455             :     }
     456         822 :     else if (action_formulas::is_imp(x))
     457             :     {
     458           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
     459             :     }
     460         822 :     else if (action_formulas::is_forall(x))
     461             :     {
     462           6 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
     463             :     }
     464         816 :     else if (action_formulas::is_exists(x))
     465             :     {
     466           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
     467             :     }
     468         813 :     else if (action_formulas::is_at(x))
     469             :     {
     470           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
     471             :     }
     472         813 :     else if (action_formulas::is_multi_action(x))
     473             :     {
     474         813 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
     475             :     }
     476           0 :     else if (process::is_untyped_multi_action(x))
     477             :     {
     478           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
     479             :     }
     480        1335 :     static_cast<Derived&>(*this).leave(x);
     481        1335 :   }
     482             : 
     483             : };
     484             : 
     485             : /// \\brief Traverser class
     486             : template <typename Derived>
     487             : struct action_formula_traverser: public add_traverser_action_formula_expressions<action_formulas::action_formula_traverser_base, Derived>
     488             : {
     489             : };
     490             : //--- end generated action_formulas::add_traverser_action_formula_expressions code ---//
     491             : 
     492             : //--- start generated action_formulas::add_traverser_variables code ---//
     493             : template <template <class> class Traverser, class Derived>
     494             : struct add_traverser_variables: public Traverser<Derived>
     495             : {
     496             :   typedef Traverser<Derived> super;
     497             :   using super::enter;
     498             :   using super::leave;
     499             :   using super::apply;
     500             : 
     501           0 :   void apply(const action_formulas::true_& x)
     502             :   {
     503           0 :     static_cast<Derived&>(*this).enter(x);
     504             :     // skip
     505           0 :     static_cast<Derived&>(*this).leave(x);
     506           0 :   }
     507             : 
     508           0 :   void apply(const action_formulas::false_& x)
     509             :   {
     510           0 :     static_cast<Derived&>(*this).enter(x);
     511             :     // skip
     512           0 :     static_cast<Derived&>(*this).leave(x);
     513           0 :   }
     514             : 
     515           0 :   void apply(const action_formulas::not_& x)
     516             :   {
     517           0 :     static_cast<Derived&>(*this).enter(x);
     518           0 :     static_cast<Derived&>(*this).apply(x.operand());
     519           0 :     static_cast<Derived&>(*this).leave(x);
     520           0 :   }
     521             : 
     522           0 :   void apply(const action_formulas::and_& x)
     523             :   {
     524           0 :     static_cast<Derived&>(*this).enter(x);
     525           0 :     static_cast<Derived&>(*this).apply(x.left());
     526           0 :     static_cast<Derived&>(*this).apply(x.right());
     527           0 :     static_cast<Derived&>(*this).leave(x);
     528           0 :   }
     529             : 
     530           0 :   void apply(const action_formulas::or_& x)
     531             :   {
     532           0 :     static_cast<Derived&>(*this).enter(x);
     533           0 :     static_cast<Derived&>(*this).apply(x.left());
     534           0 :     static_cast<Derived&>(*this).apply(x.right());
     535           0 :     static_cast<Derived&>(*this).leave(x);
     536           0 :   }
     537             : 
     538           0 :   void apply(const action_formulas::imp& x)
     539             :   {
     540           0 :     static_cast<Derived&>(*this).enter(x);
     541           0 :     static_cast<Derived&>(*this).apply(x.left());
     542           0 :     static_cast<Derived&>(*this).apply(x.right());
     543           0 :     static_cast<Derived&>(*this).leave(x);
     544           0 :   }
     545             : 
     546           0 :   void apply(const action_formulas::forall& x)
     547             :   {
     548           0 :     static_cast<Derived&>(*this).enter(x);
     549           0 :     static_cast<Derived&>(*this).apply(x.variables());
     550           0 :     static_cast<Derived&>(*this).apply(x.body());
     551           0 :     static_cast<Derived&>(*this).leave(x);
     552           0 :   }
     553             : 
     554           0 :   void apply(const action_formulas::exists& x)
     555             :   {
     556           0 :     static_cast<Derived&>(*this).enter(x);
     557           0 :     static_cast<Derived&>(*this).apply(x.variables());
     558           0 :     static_cast<Derived&>(*this).apply(x.body());
     559           0 :     static_cast<Derived&>(*this).leave(x);
     560           0 :   }
     561             : 
     562           0 :   void apply(const action_formulas::at& x)
     563             :   {
     564           0 :     static_cast<Derived&>(*this).enter(x);
     565           0 :     static_cast<Derived&>(*this).apply(x.operand());
     566           0 :     static_cast<Derived&>(*this).apply(x.time_stamp());
     567           0 :     static_cast<Derived&>(*this).leave(x);
     568           0 :   }
     569             : 
     570           0 :   void apply(const action_formulas::multi_action& x)
     571             :   {
     572           0 :     static_cast<Derived&>(*this).enter(x);
     573           0 :     static_cast<Derived&>(*this).apply(x.actions());
     574           0 :     static_cast<Derived&>(*this).leave(x);
     575           0 :   }
     576             : 
     577           0 :   void apply(const action_formulas::action_formula& x)
     578             :   {
     579           0 :     static_cast<Derived&>(*this).enter(x);
     580           0 :     if (data::is_data_expression(x))
     581             :     {
     582           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     583             :     }
     584           0 :     else if (data::is_untyped_data_parameter(x))
     585             :     {
     586           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     587             :     }
     588           0 :     else if (action_formulas::is_true(x))
     589             :     {
     590           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
     591             :     }
     592           0 :     else if (action_formulas::is_false(x))
     593             :     {
     594           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
     595             :     }
     596           0 :     else if (action_formulas::is_not(x))
     597             :     {
     598           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
     599             :     }
     600           0 :     else if (action_formulas::is_and(x))
     601             :     {
     602           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
     603             :     }
     604           0 :     else if (action_formulas::is_or(x))
     605             :     {
     606           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
     607             :     }
     608           0 :     else if (action_formulas::is_imp(x))
     609             :     {
     610           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
     611             :     }
     612           0 :     else if (action_formulas::is_forall(x))
     613             :     {
     614           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
     615             :     }
     616           0 :     else if (action_formulas::is_exists(x))
     617             :     {
     618           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
     619             :     }
     620           0 :     else if (action_formulas::is_at(x))
     621             :     {
     622           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
     623             :     }
     624           0 :     else if (action_formulas::is_multi_action(x))
     625             :     {
     626           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
     627             :     }
     628           0 :     else if (process::is_untyped_multi_action(x))
     629             :     {
     630           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
     631             :     }
     632           0 :     static_cast<Derived&>(*this).leave(x);
     633           0 :   }
     634             : 
     635             : };
     636             : 
     637             : /// \\brief Traverser class
     638             : template <typename Derived>
     639             : struct variable_traverser: public add_traverser_variables<lps::variable_traverser, Derived>
     640             : {
     641             : };
     642             : //--- end generated action_formulas::add_traverser_variables code ---//
     643             : 
     644             : //--- start generated action_formulas::add_traverser_identifier_strings code ---//
     645             : template <template <class> class Traverser, class Derived>
     646             : struct add_traverser_identifier_strings: public Traverser<Derived>
     647             : {
     648             :   typedef Traverser<Derived> super;
     649             :   using super::enter;
     650             :   using super::leave;
     651             :   using super::apply;
     652             : 
     653         182 :   void apply(const action_formulas::true_& x)
     654             :   {
     655         182 :     static_cast<Derived&>(*this).enter(x);
     656             :     // skip
     657         182 :     static_cast<Derived&>(*this).leave(x);
     658         182 :   }
     659             : 
     660          10 :   void apply(const action_formulas::false_& x)
     661             :   {
     662          10 :     static_cast<Derived&>(*this).enter(x);
     663             :     // skip
     664          10 :     static_cast<Derived&>(*this).leave(x);
     665          10 :   }
     666             : 
     667         147 :   void apply(const action_formulas::not_& x)
     668             :   {
     669         147 :     static_cast<Derived&>(*this).enter(x);
     670         147 :     static_cast<Derived&>(*this).apply(x.operand());
     671         147 :     static_cast<Derived&>(*this).leave(x);
     672         147 :   }
     673             : 
     674          59 :   void apply(const action_formulas::and_& x)
     675             :   {
     676          59 :     static_cast<Derived&>(*this).enter(x);
     677          59 :     static_cast<Derived&>(*this).apply(x.left());
     678          59 :     static_cast<Derived&>(*this).apply(x.right());
     679          59 :     static_cast<Derived&>(*this).leave(x);
     680          59 :   }
     681             : 
     682          27 :   void apply(const action_formulas::or_& x)
     683             :   {
     684          27 :     static_cast<Derived&>(*this).enter(x);
     685          27 :     static_cast<Derived&>(*this).apply(x.left());
     686          27 :     static_cast<Derived&>(*this).apply(x.right());
     687          27 :     static_cast<Derived&>(*this).leave(x);
     688          27 :   }
     689             : 
     690           0 :   void apply(const action_formulas::imp& x)
     691             :   {
     692           0 :     static_cast<Derived&>(*this).enter(x);
     693           0 :     static_cast<Derived&>(*this).apply(x.left());
     694           0 :     static_cast<Derived&>(*this).apply(x.right());
     695           0 :     static_cast<Derived&>(*this).leave(x);
     696           0 :   }
     697             : 
     698          23 :   void apply(const action_formulas::forall& x)
     699             :   {
     700          23 :     static_cast<Derived&>(*this).enter(x);
     701          23 :     static_cast<Derived&>(*this).apply(x.variables());
     702          23 :     static_cast<Derived&>(*this).apply(x.body());
     703          23 :     static_cast<Derived&>(*this).leave(x);
     704          23 :   }
     705             : 
     706          14 :   void apply(const action_formulas::exists& x)
     707             :   {
     708          14 :     static_cast<Derived&>(*this).enter(x);
     709          14 :     static_cast<Derived&>(*this).apply(x.variables());
     710          14 :     static_cast<Derived&>(*this).apply(x.body());
     711          14 :     static_cast<Derived&>(*this).leave(x);
     712          14 :   }
     713             : 
     714           0 :   void apply(const action_formulas::at& x)
     715             :   {
     716           0 :     static_cast<Derived&>(*this).enter(x);
     717           0 :     static_cast<Derived&>(*this).apply(x.operand());
     718           0 :     static_cast<Derived&>(*this).apply(x.time_stamp());
     719           0 :     static_cast<Derived&>(*this).leave(x);
     720           0 :   }
     721             : 
     722         918 :   void apply(const action_formulas::multi_action& x)
     723             :   {
     724         918 :     static_cast<Derived&>(*this).enter(x);
     725         918 :     static_cast<Derived&>(*this).apply(x.actions());
     726         918 :     static_cast<Derived&>(*this).leave(x);
     727         918 :   }
     728             : 
     729        1380 :   void apply(const action_formulas::action_formula& x)
     730             :   {
     731        1380 :     static_cast<Derived&>(*this).enter(x);
     732        1380 :     if (data::is_data_expression(x))
     733             :     {
     734           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     735             :     }
     736        1380 :     else if (data::is_untyped_data_parameter(x))
     737             :     {
     738           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     739             :     }
     740        1380 :     else if (action_formulas::is_true(x))
     741             :     {
     742         182 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
     743             :     }
     744        1198 :     else if (action_formulas::is_false(x))
     745             :     {
     746          10 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
     747             :     }
     748        1188 :     else if (action_formulas::is_not(x))
     749             :     {
     750         147 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
     751             :     }
     752        1041 :     else if (action_formulas::is_and(x))
     753             :     {
     754          59 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
     755             :     }
     756         982 :     else if (action_formulas::is_or(x))
     757             :     {
     758          27 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
     759             :     }
     760         955 :     else if (action_formulas::is_imp(x))
     761             :     {
     762           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
     763             :     }
     764         955 :     else if (action_formulas::is_forall(x))
     765             :     {
     766          23 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
     767             :     }
     768         932 :     else if (action_formulas::is_exists(x))
     769             :     {
     770          14 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
     771             :     }
     772         918 :     else if (action_formulas::is_at(x))
     773             :     {
     774           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
     775             :     }
     776         918 :     else if (action_formulas::is_multi_action(x))
     777             :     {
     778         918 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
     779             :     }
     780           0 :     else if (process::is_untyped_multi_action(x))
     781             :     {
     782           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
     783             :     }
     784        1380 :     static_cast<Derived&>(*this).leave(x);
     785        1380 :   }
     786             : 
     787             : };
     788             : 
     789             : /// \\brief Traverser class
     790             : template <typename Derived>
     791             : struct identifier_string_traverser: public add_traverser_identifier_strings<lps::identifier_string_traverser, Derived>
     792             : {
     793             : };
     794             : //--- end generated action_formulas::add_traverser_identifier_strings code ---//
     795             : 
     796             : //--- start generated action_formulas::add_traverser_action_labels code ---//
     797             : template <template <class> class Traverser, class Derived>
     798             : struct add_traverser_action_labels: public Traverser<Derived>
     799             : {
     800             :   typedef Traverser<Derived> super;
     801             :   using super::enter;
     802             :   using super::leave;
     803             :   using super::apply;
     804             : 
     805           0 :   void apply(const action_formulas::true_& x)
     806             :   {
     807           0 :     static_cast<Derived&>(*this).enter(x);
     808             :     // skip
     809           0 :     static_cast<Derived&>(*this).leave(x);
     810           0 :   }
     811             : 
     812           0 :   void apply(const action_formulas::false_& x)
     813             :   {
     814           0 :     static_cast<Derived&>(*this).enter(x);
     815             :     // skip
     816           0 :     static_cast<Derived&>(*this).leave(x);
     817           0 :   }
     818             : 
     819           0 :   void apply(const action_formulas::not_& x)
     820             :   {
     821           0 :     static_cast<Derived&>(*this).enter(x);
     822           0 :     static_cast<Derived&>(*this).apply(x.operand());
     823           0 :     static_cast<Derived&>(*this).leave(x);
     824           0 :   }
     825             : 
     826           0 :   void apply(const action_formulas::and_& x)
     827             :   {
     828           0 :     static_cast<Derived&>(*this).enter(x);
     829           0 :     static_cast<Derived&>(*this).apply(x.left());
     830           0 :     static_cast<Derived&>(*this).apply(x.right());
     831           0 :     static_cast<Derived&>(*this).leave(x);
     832           0 :   }
     833             : 
     834           0 :   void apply(const action_formulas::or_& x)
     835             :   {
     836           0 :     static_cast<Derived&>(*this).enter(x);
     837           0 :     static_cast<Derived&>(*this).apply(x.left());
     838           0 :     static_cast<Derived&>(*this).apply(x.right());
     839           0 :     static_cast<Derived&>(*this).leave(x);
     840           0 :   }
     841             : 
     842           0 :   void apply(const action_formulas::imp& x)
     843             :   {
     844           0 :     static_cast<Derived&>(*this).enter(x);
     845           0 :     static_cast<Derived&>(*this).apply(x.left());
     846           0 :     static_cast<Derived&>(*this).apply(x.right());
     847           0 :     static_cast<Derived&>(*this).leave(x);
     848           0 :   }
     849             : 
     850           0 :   void apply(const action_formulas::forall& x)
     851             :   {
     852           0 :     static_cast<Derived&>(*this).enter(x);
     853           0 :     static_cast<Derived&>(*this).apply(x.body());
     854           0 :     static_cast<Derived&>(*this).leave(x);
     855           0 :   }
     856             : 
     857           0 :   void apply(const action_formulas::exists& x)
     858             :   {
     859           0 :     static_cast<Derived&>(*this).enter(x);
     860           0 :     static_cast<Derived&>(*this).apply(x.body());
     861           0 :     static_cast<Derived&>(*this).leave(x);
     862           0 :   }
     863             : 
     864           0 :   void apply(const action_formulas::at& x)
     865             :   {
     866           0 :     static_cast<Derived&>(*this).enter(x);
     867           0 :     static_cast<Derived&>(*this).apply(x.operand());
     868           0 :     static_cast<Derived&>(*this).leave(x);
     869           0 :   }
     870             : 
     871           0 :   void apply(const action_formulas::multi_action& x)
     872             :   {
     873           0 :     static_cast<Derived&>(*this).enter(x);
     874           0 :     static_cast<Derived&>(*this).apply(x.actions());
     875           0 :     static_cast<Derived&>(*this).leave(x);
     876           0 :   }
     877             : 
     878           0 :   void apply(const action_formulas::action_formula& x)
     879             :   {
     880           0 :     static_cast<Derived&>(*this).enter(x);
     881           0 :     if (data::is_data_expression(x))
     882             :     {
     883           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
     884             :     }
     885           0 :     else if (data::is_untyped_data_parameter(x))
     886             :     {
     887           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
     888             :     }
     889           0 :     else if (action_formulas::is_true(x))
     890             :     {
     891           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
     892             :     }
     893           0 :     else if (action_formulas::is_false(x))
     894             :     {
     895           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
     896             :     }
     897           0 :     else if (action_formulas::is_not(x))
     898             :     {
     899           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
     900             :     }
     901           0 :     else if (action_formulas::is_and(x))
     902             :     {
     903           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
     904             :     }
     905           0 :     else if (action_formulas::is_or(x))
     906             :     {
     907           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
     908             :     }
     909           0 :     else if (action_formulas::is_imp(x))
     910             :     {
     911           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
     912             :     }
     913           0 :     else if (action_formulas::is_forall(x))
     914             :     {
     915           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
     916             :     }
     917           0 :     else if (action_formulas::is_exists(x))
     918             :     {
     919           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
     920             :     }
     921           0 :     else if (action_formulas::is_at(x))
     922             :     {
     923           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
     924             :     }
     925           0 :     else if (action_formulas::is_multi_action(x))
     926             :     {
     927           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
     928             :     }
     929           0 :     else if (process::is_untyped_multi_action(x))
     930             :     {
     931           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
     932             :     }
     933           0 :     static_cast<Derived&>(*this).leave(x);
     934           0 :   }
     935             : 
     936             : };
     937             : 
     938             : /// \\brief Traverser class
     939             : template <typename Derived>
     940             : struct action_label_traverser: public add_traverser_action_labels<lps::action_label_traverser, Derived>
     941             : {
     942             : };
     943             : //--- end generated action_formulas::add_traverser_action_labels code ---//
     944             : 
     945             : } // namespace action_formulas
     946             : 
     947             : namespace regular_formulas
     948             : {
     949             : 
     950             : /// \brief Traversal class for regular_formula_traverser. Used as a base class for pbes_expression_traverser.
     951             : template <typename Derived>
     952             : struct regular_formula_traverser_base: public core::traverser<Derived>
     953             : {
     954             :   typedef core::traverser<Derived> super;
     955             :   using super::apply;
     956             :   using super::enter;
     957             :   using super::leave;
     958             : 
     959             :   void apply(const data::data_expression& x)
     960             :   {
     961             :     static_cast<Derived&>(*this).enter(x);
     962             :     // skip
     963             :     static_cast<Derived&>(*this).leave(x);
     964             :   }
     965             : 
     966             :   void apply(const action_formulas::action_formula& x)
     967             :   {
     968             :     static_cast<Derived&>(*this).enter(x);
     969             :     // skip
     970             :     static_cast<Derived&>(*this).leave(x);
     971             :   }
     972             : };
     973             : 
     974             : //--- start generated regular_formulas::add_traverser_sort_expressions code ---//
     975             : template <template <class> class Traverser, class Derived>
     976             : struct add_traverser_sort_expressions: public Traverser<Derived>
     977             : {
     978             :   typedef Traverser<Derived> super;
     979             :   using super::enter;
     980             :   using super::leave;
     981             :   using super::apply;
     982             : 
     983           3 :   void apply(const regular_formulas::seq& x)
     984             :   {
     985           3 :     static_cast<Derived&>(*this).enter(x);
     986           3 :     static_cast<Derived&>(*this).apply(x.left());
     987           3 :     static_cast<Derived&>(*this).apply(x.right());
     988           3 :     static_cast<Derived&>(*this).leave(x);
     989           3 :   }
     990             : 
     991           2 :   void apply(const regular_formulas::alt& x)
     992             :   {
     993           2 :     static_cast<Derived&>(*this).enter(x);
     994           2 :     static_cast<Derived&>(*this).apply(x.left());
     995           2 :     static_cast<Derived&>(*this).apply(x.right());
     996           2 :     static_cast<Derived&>(*this).leave(x);
     997           2 :   }
     998             : 
     999           0 :   void apply(const regular_formulas::trans& x)
    1000             :   {
    1001           0 :     static_cast<Derived&>(*this).enter(x);
    1002           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1003           0 :     static_cast<Derived&>(*this).leave(x);
    1004           0 :   }
    1005             : 
    1006          32 :   void apply(const regular_formulas::trans_or_nil& x)
    1007             :   {
    1008          32 :     static_cast<Derived&>(*this).enter(x);
    1009          32 :     static_cast<Derived&>(*this).apply(x.operand());
    1010          32 :     static_cast<Derived&>(*this).leave(x);
    1011          32 :   }
    1012             : 
    1013           0 :   void apply(const regular_formulas::untyped_regular_formula& x)
    1014             :   {
    1015           0 :     static_cast<Derived&>(*this).enter(x);
    1016           0 :     static_cast<Derived&>(*this).apply(x.left());
    1017           0 :     static_cast<Derived&>(*this).apply(x.right());
    1018           0 :     static_cast<Derived&>(*this).leave(x);
    1019           0 :   }
    1020             : 
    1021         360 :   void apply(const regular_formulas::regular_formula& x)
    1022             :   {
    1023         360 :     static_cast<Derived&>(*this).enter(x);
    1024         360 :     if (data::is_data_expression(x))
    1025             :     {
    1026           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1027             :     }
    1028         360 :     else if (action_formulas::is_action_formula(x))
    1029             :     {
    1030         310 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
    1031             :     }
    1032          50 :     else if (regular_formulas::is_seq(x))
    1033             :     {
    1034           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
    1035             :     }
    1036          47 :     else if (regular_formulas::is_alt(x))
    1037             :     {
    1038           4 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
    1039             :     }
    1040          43 :     else if (regular_formulas::is_trans(x))
    1041             :     {
    1042           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
    1043             :     }
    1044          43 :     else if (regular_formulas::is_trans_or_nil(x))
    1045             :     {
    1046          43 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
    1047             :     }
    1048           0 :     else if (regular_formulas::is_untyped_regular_formula(x))
    1049             :     {
    1050           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
    1051             :     }
    1052         360 :     static_cast<Derived&>(*this).leave(x);
    1053         360 :   }
    1054             : 
    1055             : };
    1056             : 
    1057             : /// \\brief Traverser class
    1058             : template <typename Derived>
    1059             : struct sort_expression_traverser: public add_traverser_sort_expressions<action_formulas::sort_expression_traverser, Derived>
    1060             : {
    1061             : };
    1062             : //--- end generated regular_formulas::add_traverser_sort_expressions code ---//
    1063             : 
    1064             : //--- start generated regular_formulas::add_traverser_data_expressions code ---//
    1065             : template <template <class> class Traverser, class Derived>
    1066             : struct add_traverser_data_expressions: public Traverser<Derived>
    1067             : {
    1068             :   typedef Traverser<Derived> super;
    1069             :   using super::enter;
    1070             :   using super::leave;
    1071             :   using super::apply;
    1072             : 
    1073           0 :   void apply(const regular_formulas::seq& x)
    1074             :   {
    1075           0 :     static_cast<Derived&>(*this).enter(x);
    1076           0 :     static_cast<Derived&>(*this).apply(x.left());
    1077           0 :     static_cast<Derived&>(*this).apply(x.right());
    1078           0 :     static_cast<Derived&>(*this).leave(x);
    1079           0 :   }
    1080             : 
    1081           0 :   void apply(const regular_formulas::alt& x)
    1082             :   {
    1083           0 :     static_cast<Derived&>(*this).enter(x);
    1084           0 :     static_cast<Derived&>(*this).apply(x.left());
    1085           0 :     static_cast<Derived&>(*this).apply(x.right());
    1086           0 :     static_cast<Derived&>(*this).leave(x);
    1087           0 :   }
    1088             : 
    1089           0 :   void apply(const regular_formulas::trans& x)
    1090             :   {
    1091           0 :     static_cast<Derived&>(*this).enter(x);
    1092           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1093           0 :     static_cast<Derived&>(*this).leave(x);
    1094           0 :   }
    1095             : 
    1096           0 :   void apply(const regular_formulas::trans_or_nil& x)
    1097             :   {
    1098           0 :     static_cast<Derived&>(*this).enter(x);
    1099           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1100           0 :     static_cast<Derived&>(*this).leave(x);
    1101           0 :   }
    1102             : 
    1103           0 :   void apply(const regular_formulas::untyped_regular_formula& x)
    1104             :   {
    1105           0 :     static_cast<Derived&>(*this).enter(x);
    1106           0 :     static_cast<Derived&>(*this).apply(x.left());
    1107           0 :     static_cast<Derived&>(*this).apply(x.right());
    1108           0 :     static_cast<Derived&>(*this).leave(x);
    1109           0 :   }
    1110             : 
    1111           0 :   void apply(const regular_formulas::regular_formula& x)
    1112             :   {
    1113           0 :     static_cast<Derived&>(*this).enter(x);
    1114           0 :     if (data::is_data_expression(x))
    1115             :     {
    1116           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1117             :     }
    1118           0 :     else if (action_formulas::is_action_formula(x))
    1119             :     {
    1120           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
    1121             :     }
    1122           0 :     else if (regular_formulas::is_seq(x))
    1123             :     {
    1124           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
    1125             :     }
    1126           0 :     else if (regular_formulas::is_alt(x))
    1127             :     {
    1128           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
    1129             :     }
    1130           0 :     else if (regular_formulas::is_trans(x))
    1131             :     {
    1132           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
    1133             :     }
    1134           0 :     else if (regular_formulas::is_trans_or_nil(x))
    1135             :     {
    1136           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
    1137             :     }
    1138           0 :     else if (regular_formulas::is_untyped_regular_formula(x))
    1139             :     {
    1140           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
    1141             :     }
    1142           0 :     static_cast<Derived&>(*this).leave(x);
    1143           0 :   }
    1144             : 
    1145             : };
    1146             : 
    1147             : /// \\brief Traverser class
    1148             : template <typename Derived>
    1149             : struct data_expression_traverser: public add_traverser_data_expressions<action_formulas::data_expression_traverser, Derived>
    1150             : {
    1151             : };
    1152             : //--- end generated regular_formulas::add_traverser_data_expressions code ---//
    1153             : 
    1154             : //--- start generated regular_formulas::add_traverser_regular_formula_expressions code ---//
    1155             : template <template <class> class Traverser, class Derived>
    1156             : struct add_traverser_regular_formula_expressions: public Traverser<Derived>
    1157             : {
    1158             :   typedef Traverser<Derived> super;
    1159             :   using super::enter;
    1160             :   using super::leave;
    1161             :   using super::apply;
    1162             : 
    1163             :   void apply(const regular_formulas::seq& x)
    1164             :   {
    1165             :     static_cast<Derived&>(*this).enter(x);
    1166             :     static_cast<Derived&>(*this).apply(x.left());
    1167             :     static_cast<Derived&>(*this).apply(x.right());
    1168             :     static_cast<Derived&>(*this).leave(x);
    1169             :   }
    1170             : 
    1171             :   void apply(const regular_formulas::alt& x)
    1172             :   {
    1173             :     static_cast<Derived&>(*this).enter(x);
    1174             :     static_cast<Derived&>(*this).apply(x.left());
    1175             :     static_cast<Derived&>(*this).apply(x.right());
    1176             :     static_cast<Derived&>(*this).leave(x);
    1177             :   }
    1178             : 
    1179             :   void apply(const regular_formulas::trans& x)
    1180             :   {
    1181             :     static_cast<Derived&>(*this).enter(x);
    1182             :     static_cast<Derived&>(*this).apply(x.operand());
    1183             :     static_cast<Derived&>(*this).leave(x);
    1184             :   }
    1185             : 
    1186             :   void apply(const regular_formulas::trans_or_nil& x)
    1187             :   {
    1188             :     static_cast<Derived&>(*this).enter(x);
    1189             :     static_cast<Derived&>(*this).apply(x.operand());
    1190             :     static_cast<Derived&>(*this).leave(x);
    1191             :   }
    1192             : 
    1193             :   void apply(const regular_formulas::untyped_regular_formula& x)
    1194             :   {
    1195             :     static_cast<Derived&>(*this).enter(x);
    1196             :     static_cast<Derived&>(*this).apply(x.left());
    1197             :     static_cast<Derived&>(*this).apply(x.right());
    1198             :     static_cast<Derived&>(*this).leave(x);
    1199             :   }
    1200             : 
    1201             :   void apply(const regular_formulas::regular_formula& x)
    1202             :   {
    1203             :     static_cast<Derived&>(*this).enter(x);
    1204             :     if (data::is_data_expression(x))
    1205             :     {
    1206             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1207             :     }
    1208             :     else if (action_formulas::is_action_formula(x))
    1209             :     {
    1210             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
    1211             :     }
    1212             :     else if (regular_formulas::is_seq(x))
    1213             :     {
    1214             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
    1215             :     }
    1216             :     else if (regular_formulas::is_alt(x))
    1217             :     {
    1218             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
    1219             :     }
    1220             :     else if (regular_formulas::is_trans(x))
    1221             :     {
    1222             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
    1223             :     }
    1224             :     else if (regular_formulas::is_trans_or_nil(x))
    1225             :     {
    1226             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
    1227             :     }
    1228             :     else if (regular_formulas::is_untyped_regular_formula(x))
    1229             :     {
    1230             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
    1231             :     }
    1232             :     static_cast<Derived&>(*this).leave(x);
    1233             :   }
    1234             : 
    1235             : };
    1236             : 
    1237             : /// \\brief Traverser class
    1238             : template <typename Derived>
    1239             : struct regular_formula_traverser: public add_traverser_regular_formula_expressions<regular_formulas::regular_formula_traverser_base, Derived>
    1240             : {
    1241             : };
    1242             : //--- end generated regular_formulas::add_traverser_regular_formula_expressions code ---//
    1243             : 
    1244             : //--- start generated regular_formulas::add_traverser_variables code ---//
    1245             : template <template <class> class Traverser, class Derived>
    1246             : struct add_traverser_variables: public Traverser<Derived>
    1247             : {
    1248             :   typedef Traverser<Derived> super;
    1249             :   using super::enter;
    1250             :   using super::leave;
    1251             :   using super::apply;
    1252             : 
    1253           0 :   void apply(const regular_formulas::seq& x)
    1254             :   {
    1255           0 :     static_cast<Derived&>(*this).enter(x);
    1256           0 :     static_cast<Derived&>(*this).apply(x.left());
    1257           0 :     static_cast<Derived&>(*this).apply(x.right());
    1258           0 :     static_cast<Derived&>(*this).leave(x);
    1259           0 :   }
    1260             : 
    1261           0 :   void apply(const regular_formulas::alt& x)
    1262             :   {
    1263           0 :     static_cast<Derived&>(*this).enter(x);
    1264           0 :     static_cast<Derived&>(*this).apply(x.left());
    1265           0 :     static_cast<Derived&>(*this).apply(x.right());
    1266           0 :     static_cast<Derived&>(*this).leave(x);
    1267           0 :   }
    1268             : 
    1269           0 :   void apply(const regular_formulas::trans& x)
    1270             :   {
    1271           0 :     static_cast<Derived&>(*this).enter(x);
    1272           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1273           0 :     static_cast<Derived&>(*this).leave(x);
    1274           0 :   }
    1275             : 
    1276           0 :   void apply(const regular_formulas::trans_or_nil& x)
    1277             :   {
    1278           0 :     static_cast<Derived&>(*this).enter(x);
    1279           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1280           0 :     static_cast<Derived&>(*this).leave(x);
    1281           0 :   }
    1282             : 
    1283           0 :   void apply(const regular_formulas::untyped_regular_formula& x)
    1284             :   {
    1285           0 :     static_cast<Derived&>(*this).enter(x);
    1286           0 :     static_cast<Derived&>(*this).apply(x.left());
    1287           0 :     static_cast<Derived&>(*this).apply(x.right());
    1288           0 :     static_cast<Derived&>(*this).leave(x);
    1289           0 :   }
    1290             : 
    1291           0 :   void apply(const regular_formulas::regular_formula& x)
    1292             :   {
    1293           0 :     static_cast<Derived&>(*this).enter(x);
    1294           0 :     if (data::is_data_expression(x))
    1295             :     {
    1296           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1297             :     }
    1298           0 :     else if (action_formulas::is_action_formula(x))
    1299             :     {
    1300           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
    1301             :     }
    1302           0 :     else if (regular_formulas::is_seq(x))
    1303             :     {
    1304           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
    1305             :     }
    1306           0 :     else if (regular_formulas::is_alt(x))
    1307             :     {
    1308           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
    1309             :     }
    1310           0 :     else if (regular_formulas::is_trans(x))
    1311             :     {
    1312           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
    1313             :     }
    1314           0 :     else if (regular_formulas::is_trans_or_nil(x))
    1315             :     {
    1316           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
    1317             :     }
    1318           0 :     else if (regular_formulas::is_untyped_regular_formula(x))
    1319             :     {
    1320           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
    1321             :     }
    1322           0 :     static_cast<Derived&>(*this).leave(x);
    1323           0 :   }
    1324             : 
    1325             : };
    1326             : 
    1327             : /// \\brief Traverser class
    1328             : template <typename Derived>
    1329             : struct variable_traverser: public add_traverser_variables<action_formulas::variable_traverser, Derived>
    1330             : {
    1331             : };
    1332             : //--- end generated regular_formulas::add_traverser_variables code ---//
    1333             : 
    1334             : //--- start generated regular_formulas::add_traverser_identifier_strings code ---//
    1335             : template <template <class> class Traverser, class Derived>
    1336             : struct add_traverser_identifier_strings: public Traverser<Derived>
    1337             : {
    1338             :   typedef Traverser<Derived> super;
    1339             :   using super::enter;
    1340             :   using super::leave;
    1341             :   using super::apply;
    1342             : 
    1343           3 :   void apply(const regular_formulas::seq& x)
    1344             :   {
    1345           3 :     static_cast<Derived&>(*this).enter(x);
    1346           3 :     static_cast<Derived&>(*this).apply(x.left());
    1347           3 :     static_cast<Derived&>(*this).apply(x.right());
    1348           3 :     static_cast<Derived&>(*this).leave(x);
    1349           3 :   }
    1350             : 
    1351           2 :   void apply(const regular_formulas::alt& x)
    1352             :   {
    1353           2 :     static_cast<Derived&>(*this).enter(x);
    1354           2 :     static_cast<Derived&>(*this).apply(x.left());
    1355           2 :     static_cast<Derived&>(*this).apply(x.right());
    1356           2 :     static_cast<Derived&>(*this).leave(x);
    1357           2 :   }
    1358             : 
    1359           0 :   void apply(const regular_formulas::trans& x)
    1360             :   {
    1361           0 :     static_cast<Derived&>(*this).enter(x);
    1362           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1363           0 :     static_cast<Derived&>(*this).leave(x);
    1364           0 :   }
    1365             : 
    1366          30 :   void apply(const regular_formulas::trans_or_nil& x)
    1367             :   {
    1368          30 :     static_cast<Derived&>(*this).enter(x);
    1369          30 :     static_cast<Derived&>(*this).apply(x.operand());
    1370          30 :     static_cast<Derived&>(*this).leave(x);
    1371          30 :   }
    1372             : 
    1373           0 :   void apply(const regular_formulas::untyped_regular_formula& x)
    1374             :   {
    1375           0 :     static_cast<Derived&>(*this).enter(x);
    1376           0 :     static_cast<Derived&>(*this).apply(x.name());
    1377           0 :     static_cast<Derived&>(*this).apply(x.left());
    1378           0 :     static_cast<Derived&>(*this).apply(x.right());
    1379           0 :     static_cast<Derived&>(*this).leave(x);
    1380           0 :   }
    1381             : 
    1382        1050 :   void apply(const regular_formulas::regular_formula& x)
    1383             :   {
    1384        1050 :     static_cast<Derived&>(*this).enter(x);
    1385        1050 :     if (data::is_data_expression(x))
    1386             :     {
    1387           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1388             :     }
    1389        1050 :     else if (action_formulas::is_action_formula(x))
    1390             :     {
    1391        1015 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
    1392             :     }
    1393          35 :     else if (regular_formulas::is_seq(x))
    1394             :     {
    1395           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
    1396             :     }
    1397          32 :     else if (regular_formulas::is_alt(x))
    1398             :     {
    1399           2 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
    1400             :     }
    1401          30 :     else if (regular_formulas::is_trans(x))
    1402             :     {
    1403           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
    1404             :     }
    1405          30 :     else if (regular_formulas::is_trans_or_nil(x))
    1406             :     {
    1407          30 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
    1408             :     }
    1409           0 :     else if (regular_formulas::is_untyped_regular_formula(x))
    1410             :     {
    1411           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
    1412             :     }
    1413        1050 :     static_cast<Derived&>(*this).leave(x);
    1414        1050 :   }
    1415             : 
    1416             : };
    1417             : 
    1418             : /// \\brief Traverser class
    1419             : template <typename Derived>
    1420             : struct identifier_string_traverser: public add_traverser_identifier_strings<action_formulas::identifier_string_traverser, Derived>
    1421             : {
    1422             : };
    1423             : //--- end generated regular_formulas::add_traverser_identifier_strings code ---//
    1424             : 
    1425             : //--- start generated regular_formulas::add_traverser_action_labels code ---//
    1426             : template <template <class> class Traverser, class Derived>
    1427             : struct add_traverser_action_labels: public Traverser<Derived>
    1428             : {
    1429             :   typedef Traverser<Derived> super;
    1430             :   using super::enter;
    1431             :   using super::leave;
    1432             :   using super::apply;
    1433             : 
    1434           0 :   void apply(const regular_formulas::seq& x)
    1435             :   {
    1436           0 :     static_cast<Derived&>(*this).enter(x);
    1437           0 :     static_cast<Derived&>(*this).apply(x.left());
    1438           0 :     static_cast<Derived&>(*this).apply(x.right());
    1439           0 :     static_cast<Derived&>(*this).leave(x);
    1440           0 :   }
    1441             : 
    1442           0 :   void apply(const regular_formulas::alt& x)
    1443             :   {
    1444           0 :     static_cast<Derived&>(*this).enter(x);
    1445           0 :     static_cast<Derived&>(*this).apply(x.left());
    1446           0 :     static_cast<Derived&>(*this).apply(x.right());
    1447           0 :     static_cast<Derived&>(*this).leave(x);
    1448           0 :   }
    1449             : 
    1450           0 :   void apply(const regular_formulas::trans& x)
    1451             :   {
    1452           0 :     static_cast<Derived&>(*this).enter(x);
    1453           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1454           0 :     static_cast<Derived&>(*this).leave(x);
    1455           0 :   }
    1456             : 
    1457           0 :   void apply(const regular_formulas::trans_or_nil& x)
    1458             :   {
    1459           0 :     static_cast<Derived&>(*this).enter(x);
    1460           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1461           0 :     static_cast<Derived&>(*this).leave(x);
    1462           0 :   }
    1463             : 
    1464           0 :   void apply(const regular_formulas::untyped_regular_formula& x)
    1465             :   {
    1466           0 :     static_cast<Derived&>(*this).enter(x);
    1467           0 :     static_cast<Derived&>(*this).apply(x.left());
    1468           0 :     static_cast<Derived&>(*this).apply(x.right());
    1469           0 :     static_cast<Derived&>(*this).leave(x);
    1470           0 :   }
    1471             : 
    1472           0 :   void apply(const regular_formulas::regular_formula& x)
    1473             :   {
    1474           0 :     static_cast<Derived&>(*this).enter(x);
    1475           0 :     if (data::is_data_expression(x))
    1476             :     {
    1477           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1478             :     }
    1479           0 :     else if (action_formulas::is_action_formula(x))
    1480             :     {
    1481           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
    1482             :     }
    1483           0 :     else if (regular_formulas::is_seq(x))
    1484             :     {
    1485           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
    1486             :     }
    1487           0 :     else if (regular_formulas::is_alt(x))
    1488             :     {
    1489           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
    1490             :     }
    1491           0 :     else if (regular_formulas::is_trans(x))
    1492             :     {
    1493           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
    1494             :     }
    1495           0 :     else if (regular_formulas::is_trans_or_nil(x))
    1496             :     {
    1497           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
    1498             :     }
    1499           0 :     else if (regular_formulas::is_untyped_regular_formula(x))
    1500             :     {
    1501           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
    1502             :     }
    1503           0 :     static_cast<Derived&>(*this).leave(x);
    1504           0 :   }
    1505             : 
    1506             : };
    1507             : 
    1508             : /// \\brief Traverser class
    1509             : template <typename Derived>
    1510             : struct action_label_traverser: public add_traverser_action_labels<action_formulas::action_label_traverser, Derived>
    1511             : {
    1512             : };
    1513             : //--- end generated regular_formulas::add_traverser_action_labels code ---//
    1514             : 
    1515             : } // namespace regular_formulas
    1516             : 
    1517             : namespace state_formulas
    1518             : {
    1519             : 
    1520             : /// \brief Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser.
    1521             : template <typename Derived>
    1522             : struct state_formula_traverser_base: public core::traverser<Derived>
    1523             : {
    1524             :   typedef core::traverser<Derived> super;
    1525             :   using super::apply;
    1526             :   using super::enter;
    1527             :   using super::leave;
    1528             : 
    1529         167 :   void apply(const data::data_expression& x)
    1530             :   {
    1531         167 :     static_cast<Derived&>(*this).enter(x);
    1532             :     // skip
    1533         167 :     static_cast<Derived&>(*this).leave(x);
    1534         167 :   }
    1535             : };
    1536             : 
    1537             : //--- start generated state_formulas::add_traverser_sort_expressions code ---//
    1538             : template <template <class> class Traverser, class Derived>
    1539             : struct add_traverser_sort_expressions: public Traverser<Derived>
    1540             : {
    1541             :   typedef Traverser<Derived> super;
    1542             :   using super::enter;
    1543             :   using super::leave;
    1544             :   using super::apply;
    1545             : 
    1546          93 :   void apply(const state_formulas::true_& x)
    1547             :   {
    1548          93 :     static_cast<Derived&>(*this).enter(x);
    1549             :     // skip
    1550          93 :     static_cast<Derived&>(*this).leave(x);
    1551          93 :   }
    1552             : 
    1553          36 :   void apply(const state_formulas::false_& x)
    1554             :   {
    1555          36 :     static_cast<Derived&>(*this).enter(x);
    1556             :     // skip
    1557          36 :     static_cast<Derived&>(*this).leave(x);
    1558          36 :   }
    1559             : 
    1560          36 :   void apply(const state_formulas::not_& x)
    1561             :   {
    1562          36 :     static_cast<Derived&>(*this).enter(x);
    1563          36 :     static_cast<Derived&>(*this).apply(x.operand());
    1564          36 :     static_cast<Derived&>(*this).leave(x);
    1565          36 :   }
    1566             : 
    1567           0 :   void apply(const state_formulas::minus& x)
    1568             :   {
    1569           0 :     static_cast<Derived&>(*this).enter(x);
    1570           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1571           0 :     static_cast<Derived&>(*this).leave(x);
    1572           0 :   }
    1573             : 
    1574          76 :   void apply(const state_formulas::and_& x)
    1575             :   {
    1576          76 :     static_cast<Derived&>(*this).enter(x);
    1577          76 :     static_cast<Derived&>(*this).apply(x.left());
    1578          76 :     static_cast<Derived&>(*this).apply(x.right());
    1579          76 :     static_cast<Derived&>(*this).leave(x);
    1580          76 :   }
    1581             : 
    1582          26 :   void apply(const state_formulas::or_& x)
    1583             :   {
    1584          26 :     static_cast<Derived&>(*this).enter(x);
    1585          26 :     static_cast<Derived&>(*this).apply(x.left());
    1586          26 :     static_cast<Derived&>(*this).apply(x.right());
    1587          26 :     static_cast<Derived&>(*this).leave(x);
    1588          26 :   }
    1589             : 
    1590          24 :   void apply(const state_formulas::imp& x)
    1591             :   {
    1592          24 :     static_cast<Derived&>(*this).enter(x);
    1593          24 :     static_cast<Derived&>(*this).apply(x.left());
    1594          24 :     static_cast<Derived&>(*this).apply(x.right());
    1595          24 :     static_cast<Derived&>(*this).leave(x);
    1596          24 :   }
    1597             : 
    1598           0 :   void apply(const state_formulas::plus& x)
    1599             :   {
    1600           0 :     static_cast<Derived&>(*this).enter(x);
    1601           0 :     static_cast<Derived&>(*this).apply(x.left());
    1602           0 :     static_cast<Derived&>(*this).apply(x.right());
    1603           0 :     static_cast<Derived&>(*this).leave(x);
    1604           0 :   }
    1605             : 
    1606           0 :   void apply(const state_formulas::const_multiply& x)
    1607             :   {
    1608           0 :     static_cast<Derived&>(*this).enter(x);
    1609           0 :     static_cast<Derived&>(*this).apply(x.left());
    1610           0 :     static_cast<Derived&>(*this).apply(x.right());
    1611           0 :     static_cast<Derived&>(*this).leave(x);
    1612           0 :   }
    1613             : 
    1614           0 :   void apply(const state_formulas::const_multiply_alt& x)
    1615             :   {
    1616           0 :     static_cast<Derived&>(*this).enter(x);
    1617           0 :     static_cast<Derived&>(*this).apply(x.left());
    1618           0 :     static_cast<Derived&>(*this).apply(x.right());
    1619           0 :     static_cast<Derived&>(*this).leave(x);
    1620           0 :   }
    1621             : 
    1622          19 :   void apply(const state_formulas::forall& x)
    1623             :   {
    1624          19 :     static_cast<Derived&>(*this).enter(x);
    1625          19 :     static_cast<Derived&>(*this).apply(x.variables());
    1626          19 :     static_cast<Derived&>(*this).apply(x.body());
    1627          19 :     static_cast<Derived&>(*this).leave(x);
    1628          19 :   }
    1629             : 
    1630           8 :   void apply(const state_formulas::exists& x)
    1631             :   {
    1632           8 :     static_cast<Derived&>(*this).enter(x);
    1633           8 :     static_cast<Derived&>(*this).apply(x.variables());
    1634           8 :     static_cast<Derived&>(*this).apply(x.body());
    1635           8 :     static_cast<Derived&>(*this).leave(x);
    1636           8 :   }
    1637             : 
    1638           0 :   void apply(const state_formulas::infimum& x)
    1639             :   {
    1640           0 :     static_cast<Derived&>(*this).enter(x);
    1641           0 :     static_cast<Derived&>(*this).apply(x.variables());
    1642           0 :     static_cast<Derived&>(*this).apply(x.body());
    1643           0 :     static_cast<Derived&>(*this).leave(x);
    1644           0 :   }
    1645             : 
    1646           0 :   void apply(const state_formulas::supremum& x)
    1647             :   {
    1648           0 :     static_cast<Derived&>(*this).enter(x);
    1649           0 :     static_cast<Derived&>(*this).apply(x.variables());
    1650           0 :     static_cast<Derived&>(*this).apply(x.body());
    1651           0 :     static_cast<Derived&>(*this).leave(x);
    1652           0 :   }
    1653             : 
    1654           0 :   void apply(const state_formulas::sum& x)
    1655             :   {
    1656           0 :     static_cast<Derived&>(*this).enter(x);
    1657           0 :     static_cast<Derived&>(*this).apply(x.variables());
    1658           0 :     static_cast<Derived&>(*this).apply(x.body());
    1659           0 :     static_cast<Derived&>(*this).leave(x);
    1660           0 :   }
    1661             : 
    1662         129 :   void apply(const state_formulas::must& x)
    1663             :   {
    1664         129 :     static_cast<Derived&>(*this).enter(x);
    1665         129 :     static_cast<Derived&>(*this).apply(x.formula());
    1666         129 :     static_cast<Derived&>(*this).apply(x.operand());
    1667         129 :     static_cast<Derived&>(*this).leave(x);
    1668         129 :   }
    1669             : 
    1670          88 :   void apply(const state_formulas::may& x)
    1671             :   {
    1672          88 :     static_cast<Derived&>(*this).enter(x);
    1673          88 :     static_cast<Derived&>(*this).apply(x.formula());
    1674          88 :     static_cast<Derived&>(*this).apply(x.operand());
    1675          88 :     static_cast<Derived&>(*this).leave(x);
    1676          88 :   }
    1677             : 
    1678           0 :   void apply(const state_formulas::yaled& x)
    1679             :   {
    1680           0 :     static_cast<Derived&>(*this).enter(x);
    1681             :     // skip
    1682           0 :     static_cast<Derived&>(*this).leave(x);
    1683           0 :   }
    1684             : 
    1685           1 :   void apply(const state_formulas::yaled_timed& x)
    1686             :   {
    1687           1 :     static_cast<Derived&>(*this).enter(x);
    1688           1 :     static_cast<Derived&>(*this).apply(x.time_stamp());
    1689           1 :     static_cast<Derived&>(*this).leave(x);
    1690           1 :   }
    1691             : 
    1692           0 :   void apply(const state_formulas::delay& x)
    1693             :   {
    1694           0 :     static_cast<Derived&>(*this).enter(x);
    1695             :     // skip
    1696           0 :     static_cast<Derived&>(*this).leave(x);
    1697           0 :   }
    1698             : 
    1699           3 :   void apply(const state_formulas::delay_timed& x)
    1700             :   {
    1701           3 :     static_cast<Derived&>(*this).enter(x);
    1702           3 :     static_cast<Derived&>(*this).apply(x.time_stamp());
    1703           3 :     static_cast<Derived&>(*this).leave(x);
    1704           3 :   }
    1705             : 
    1706         142 :   void apply(const state_formulas::variable& x)
    1707             :   {
    1708         142 :     static_cast<Derived&>(*this).enter(x);
    1709         142 :     static_cast<Derived&>(*this).apply(x.arguments());
    1710         142 :     static_cast<Derived&>(*this).leave(x);
    1711         142 :   }
    1712             : 
    1713          67 :   void apply(const state_formulas::nu& x)
    1714             :   {
    1715          67 :     static_cast<Derived&>(*this).enter(x);
    1716          67 :     static_cast<Derived&>(*this).apply(x.assignments());
    1717          67 :     static_cast<Derived&>(*this).apply(x.operand());
    1718          67 :     static_cast<Derived&>(*this).leave(x);
    1719          67 :   }
    1720             : 
    1721         100 :   void apply(const state_formulas::mu& x)
    1722             :   {
    1723         100 :     static_cast<Derived&>(*this).enter(x);
    1724         100 :     static_cast<Derived&>(*this).apply(x.assignments());
    1725         100 :     static_cast<Derived&>(*this).apply(x.operand());
    1726         100 :     static_cast<Derived&>(*this).leave(x);
    1727         100 :   }
    1728             : 
    1729             :   void apply(const state_formulas::state_formula_specification& x)
    1730             :   {
    1731             :     static_cast<Derived&>(*this).enter(x);
    1732             :     static_cast<Derived&>(*this).apply(x.action_labels());
    1733             :     static_cast<Derived&>(*this).apply(x.formula());
    1734             :     static_cast<Derived&>(*this).leave(x);
    1735             :   }
    1736             : 
    1737        1404 :   void apply(const state_formulas::state_formula& x)
    1738             :   {
    1739        1404 :     static_cast<Derived&>(*this).enter(x);
    1740        1404 :     if (data::is_data_expression(x))
    1741             :     {
    1742          49 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    1743             :     }
    1744        1355 :     else if (data::is_untyped_data_parameter(x))
    1745             :     {
    1746           2 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    1747             :     }
    1748        1353 :     else if (state_formulas::is_true(x))
    1749             :     {
    1750         175 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    1751             :     }
    1752        1178 :     else if (state_formulas::is_false(x))
    1753             :     {
    1754          65 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    1755             :     }
    1756        1113 :     else if (state_formulas::is_not(x))
    1757             :     {
    1758          55 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    1759             :     }
    1760        1058 :     else if (state_formulas::is_minus(x))
    1761             :     {
    1762           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
    1763             :     }
    1764        1058 :     else if (state_formulas::is_and(x))
    1765             :     {
    1766         117 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    1767             :     }
    1768         941 :     else if (state_formulas::is_or(x))
    1769             :     {
    1770          49 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    1771             :     }
    1772         892 :     else if (state_formulas::is_imp(x))
    1773             :     {
    1774          34 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    1775             :     }
    1776         858 :     else if (state_formulas::is_plus(x))
    1777             :     {
    1778           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
    1779             :     }
    1780         858 :     else if (state_formulas::is_const_multiply(x))
    1781             :     {
    1782           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
    1783             :     }
    1784         855 :     else if (state_formulas::is_const_multiply_alt(x))
    1785             :     {
    1786           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
    1787             :     }
    1788         852 :     else if (state_formulas::is_forall(x))
    1789             :     {
    1790          30 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    1791             :     }
    1792         822 :     else if (state_formulas::is_exists(x))
    1793             :     {
    1794          13 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    1795             :     }
    1796         809 :     else if (state_formulas::is_infimum(x))
    1797             :     {
    1798           6 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
    1799             :     }
    1800         803 :     else if (state_formulas::is_supremum(x))
    1801             :     {
    1802           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
    1803             :     }
    1804         800 :     else if (state_formulas::is_sum(x))
    1805             :     {
    1806           3 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
    1807             :     }
    1808         797 :     else if (state_formulas::is_must(x))
    1809             :     {
    1810         179 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    1811             :     }
    1812         618 :     else if (state_formulas::is_may(x))
    1813             :     {
    1814         124 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    1815             :     }
    1816         494 :     else if (state_formulas::is_yaled(x))
    1817             :     {
    1818           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    1819             :     }
    1820         494 :     else if (state_formulas::is_yaled_timed(x))
    1821             :     {
    1822           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    1823             :     }
    1824         493 :     else if (state_formulas::is_delay(x))
    1825             :     {
    1826           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    1827             :     }
    1828         493 :     else if (state_formulas::is_delay_timed(x))
    1829             :     {
    1830           5 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    1831             :     }
    1832         488 :     else if (state_formulas::is_variable(x))
    1833             :     {
    1834         225 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    1835             :     }
    1836         263 :     else if (state_formulas::is_nu(x))
    1837             :     {
    1838          87 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    1839             :     }
    1840         176 :     else if (state_formulas::is_mu(x))
    1841             :     {
    1842         176 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    1843             :     }
    1844        1404 :     static_cast<Derived&>(*this).leave(x);
    1845        1404 :   }
    1846             : 
    1847             : };
    1848             : 
    1849             : /// \\brief Traverser class
    1850             : template <typename Derived>
    1851             : struct sort_expression_traverser: public add_traverser_sort_expressions<regular_formulas::sort_expression_traverser, Derived>
    1852             : {
    1853             : };
    1854             : //--- end generated state_formulas::add_traverser_sort_expressions code ---//
    1855             : 
    1856             : //--- start generated state_formulas::add_traverser_data_expressions code ---//
    1857             : template <template <class> class Traverser, class Derived>
    1858             : struct add_traverser_data_expressions: public Traverser<Derived>
    1859             : {
    1860             :   typedef Traverser<Derived> super;
    1861             :   using super::enter;
    1862             :   using super::leave;
    1863             :   using super::apply;
    1864             : 
    1865           0 :   void apply(const state_formulas::true_& x)
    1866             :   {
    1867           0 :     static_cast<Derived&>(*this).enter(x);
    1868             :     // skip
    1869           0 :     static_cast<Derived&>(*this).leave(x);
    1870           0 :   }
    1871             : 
    1872           0 :   void apply(const state_formulas::false_& x)
    1873             :   {
    1874           0 :     static_cast<Derived&>(*this).enter(x);
    1875             :     // skip
    1876           0 :     static_cast<Derived&>(*this).leave(x);
    1877           0 :   }
    1878             : 
    1879           0 :   void apply(const state_formulas::not_& x)
    1880             :   {
    1881           0 :     static_cast<Derived&>(*this).enter(x);
    1882           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1883           0 :     static_cast<Derived&>(*this).leave(x);
    1884           0 :   }
    1885             : 
    1886           0 :   void apply(const state_formulas::minus& x)
    1887             :   {
    1888           0 :     static_cast<Derived&>(*this).enter(x);
    1889           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1890           0 :     static_cast<Derived&>(*this).leave(x);
    1891           0 :   }
    1892             : 
    1893           0 :   void apply(const state_formulas::and_& x)
    1894             :   {
    1895           0 :     static_cast<Derived&>(*this).enter(x);
    1896           0 :     static_cast<Derived&>(*this).apply(x.left());
    1897           0 :     static_cast<Derived&>(*this).apply(x.right());
    1898           0 :     static_cast<Derived&>(*this).leave(x);
    1899           0 :   }
    1900             : 
    1901           0 :   void apply(const state_formulas::or_& x)
    1902             :   {
    1903           0 :     static_cast<Derived&>(*this).enter(x);
    1904           0 :     static_cast<Derived&>(*this).apply(x.left());
    1905           0 :     static_cast<Derived&>(*this).apply(x.right());
    1906           0 :     static_cast<Derived&>(*this).leave(x);
    1907           0 :   }
    1908             : 
    1909           0 :   void apply(const state_formulas::imp& x)
    1910             :   {
    1911           0 :     static_cast<Derived&>(*this).enter(x);
    1912           0 :     static_cast<Derived&>(*this).apply(x.left());
    1913           0 :     static_cast<Derived&>(*this).apply(x.right());
    1914           0 :     static_cast<Derived&>(*this).leave(x);
    1915           0 :   }
    1916             : 
    1917           0 :   void apply(const state_formulas::plus& x)
    1918             :   {
    1919           0 :     static_cast<Derived&>(*this).enter(x);
    1920           0 :     static_cast<Derived&>(*this).apply(x.left());
    1921           0 :     static_cast<Derived&>(*this).apply(x.right());
    1922           0 :     static_cast<Derived&>(*this).leave(x);
    1923           0 :   }
    1924             : 
    1925           0 :   void apply(const state_formulas::const_multiply& x)
    1926             :   {
    1927           0 :     static_cast<Derived&>(*this).enter(x);
    1928           0 :     static_cast<Derived&>(*this).apply(x.left());
    1929           0 :     static_cast<Derived&>(*this).apply(x.right());
    1930           0 :     static_cast<Derived&>(*this).leave(x);
    1931           0 :   }
    1932             : 
    1933           0 :   void apply(const state_formulas::const_multiply_alt& x)
    1934             :   {
    1935           0 :     static_cast<Derived&>(*this).enter(x);
    1936           0 :     static_cast<Derived&>(*this).apply(x.left());
    1937           0 :     static_cast<Derived&>(*this).apply(x.right());
    1938           0 :     static_cast<Derived&>(*this).leave(x);
    1939           0 :   }
    1940             : 
    1941           1 :   void apply(const state_formulas::forall& x)
    1942             :   {
    1943           1 :     static_cast<Derived&>(*this).enter(x);
    1944           1 :     static_cast<Derived&>(*this).apply(x.body());
    1945           1 :     static_cast<Derived&>(*this).leave(x);
    1946           1 :   }
    1947             : 
    1948           0 :   void apply(const state_formulas::exists& x)
    1949             :   {
    1950           0 :     static_cast<Derived&>(*this).enter(x);
    1951           0 :     static_cast<Derived&>(*this).apply(x.body());
    1952           0 :     static_cast<Derived&>(*this).leave(x);
    1953           0 :   }
    1954             : 
    1955           0 :   void apply(const state_formulas::infimum& x)
    1956             :   {
    1957           0 :     static_cast<Derived&>(*this).enter(x);
    1958           0 :     static_cast<Derived&>(*this).apply(x.body());
    1959           0 :     static_cast<Derived&>(*this).leave(x);
    1960           0 :   }
    1961             : 
    1962           0 :   void apply(const state_formulas::supremum& x)
    1963             :   {
    1964           0 :     static_cast<Derived&>(*this).enter(x);
    1965           0 :     static_cast<Derived&>(*this).apply(x.body());
    1966           0 :     static_cast<Derived&>(*this).leave(x);
    1967           0 :   }
    1968             : 
    1969           0 :   void apply(const state_formulas::sum& x)
    1970             :   {
    1971           0 :     static_cast<Derived&>(*this).enter(x);
    1972           0 :     static_cast<Derived&>(*this).apply(x.body());
    1973           0 :     static_cast<Derived&>(*this).leave(x);
    1974           0 :   }
    1975             : 
    1976           0 :   void apply(const state_formulas::must& x)
    1977             :   {
    1978           0 :     static_cast<Derived&>(*this).enter(x);
    1979           0 :     static_cast<Derived&>(*this).apply(x.formula());
    1980           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1981           0 :     static_cast<Derived&>(*this).leave(x);
    1982           0 :   }
    1983             : 
    1984           0 :   void apply(const state_formulas::may& x)
    1985             :   {
    1986           0 :     static_cast<Derived&>(*this).enter(x);
    1987           0 :     static_cast<Derived&>(*this).apply(x.formula());
    1988           0 :     static_cast<Derived&>(*this).apply(x.operand());
    1989           0 :     static_cast<Derived&>(*this).leave(x);
    1990           0 :   }
    1991             : 
    1992           0 :   void apply(const state_formulas::yaled& x)
    1993             :   {
    1994           0 :     static_cast<Derived&>(*this).enter(x);
    1995             :     // skip
    1996           0 :     static_cast<Derived&>(*this).leave(x);
    1997           0 :   }
    1998             : 
    1999           0 :   void apply(const state_formulas::yaled_timed& x)
    2000             :   {
    2001           0 :     static_cast<Derived&>(*this).enter(x);
    2002           0 :     static_cast<Derived&>(*this).apply(x.time_stamp());
    2003           0 :     static_cast<Derived&>(*this).leave(x);
    2004           0 :   }
    2005             : 
    2006           0 :   void apply(const state_formulas::delay& x)
    2007             :   {
    2008           0 :     static_cast<Derived&>(*this).enter(x);
    2009             :     // skip
    2010           0 :     static_cast<Derived&>(*this).leave(x);
    2011           0 :   }
    2012             : 
    2013           0 :   void apply(const state_formulas::delay_timed& x)
    2014             :   {
    2015           0 :     static_cast<Derived&>(*this).enter(x);
    2016           0 :     static_cast<Derived&>(*this).apply(x.time_stamp());
    2017           0 :     static_cast<Derived&>(*this).leave(x);
    2018           0 :   }
    2019             : 
    2020           0 :   void apply(const state_formulas::variable& x)
    2021             :   {
    2022           0 :     static_cast<Derived&>(*this).enter(x);
    2023           0 :     static_cast<Derived&>(*this).apply(x.arguments());
    2024           0 :     static_cast<Derived&>(*this).leave(x);
    2025           0 :   }
    2026             : 
    2027           0 :   void apply(const state_formulas::nu& x)
    2028             :   {
    2029           0 :     static_cast<Derived&>(*this).enter(x);
    2030           0 :     static_cast<Derived&>(*this).apply(x.assignments());
    2031           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2032           0 :     static_cast<Derived&>(*this).leave(x);
    2033           0 :   }
    2034             : 
    2035           0 :   void apply(const state_formulas::mu& x)
    2036             :   {
    2037           0 :     static_cast<Derived&>(*this).enter(x);
    2038           0 :     static_cast<Derived&>(*this).apply(x.assignments());
    2039           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2040           0 :     static_cast<Derived&>(*this).leave(x);
    2041           0 :   }
    2042             : 
    2043             :   void apply(const state_formulas::state_formula_specification& x)
    2044             :   {
    2045             :     static_cast<Derived&>(*this).enter(x);
    2046             :     static_cast<Derived&>(*this).apply(x.formula());
    2047             :     static_cast<Derived&>(*this).leave(x);
    2048             :   }
    2049             : 
    2050           2 :   void apply(const state_formulas::state_formula& x)
    2051             :   {
    2052           2 :     static_cast<Derived&>(*this).enter(x);
    2053           2 :     if (data::is_data_expression(x))
    2054             :     {
    2055           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    2056             :     }
    2057           1 :     else if (data::is_untyped_data_parameter(x))
    2058             :     {
    2059           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    2060             :     }
    2061           1 :     else if (state_formulas::is_true(x))
    2062             :     {
    2063           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    2064             :     }
    2065           1 :     else if (state_formulas::is_false(x))
    2066             :     {
    2067           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    2068             :     }
    2069           1 :     else if (state_formulas::is_not(x))
    2070             :     {
    2071           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    2072             :     }
    2073           1 :     else if (state_formulas::is_minus(x))
    2074             :     {
    2075           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
    2076             :     }
    2077           1 :     else if (state_formulas::is_and(x))
    2078             :     {
    2079           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    2080             :     }
    2081           1 :     else if (state_formulas::is_or(x))
    2082             :     {
    2083           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    2084             :     }
    2085           1 :     else if (state_formulas::is_imp(x))
    2086             :     {
    2087           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    2088             :     }
    2089           1 :     else if (state_formulas::is_plus(x))
    2090             :     {
    2091           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
    2092             :     }
    2093           1 :     else if (state_formulas::is_const_multiply(x))
    2094             :     {
    2095           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
    2096             :     }
    2097           1 :     else if (state_formulas::is_const_multiply_alt(x))
    2098             :     {
    2099           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
    2100             :     }
    2101           1 :     else if (state_formulas::is_forall(x))
    2102             :     {
    2103           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    2104             :     }
    2105           0 :     else if (state_formulas::is_exists(x))
    2106             :     {
    2107           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    2108             :     }
    2109           0 :     else if (state_formulas::is_infimum(x))
    2110             :     {
    2111           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
    2112             :     }
    2113           0 :     else if (state_formulas::is_supremum(x))
    2114             :     {
    2115           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
    2116             :     }
    2117           0 :     else if (state_formulas::is_sum(x))
    2118             :     {
    2119           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
    2120             :     }
    2121           0 :     else if (state_formulas::is_must(x))
    2122             :     {
    2123           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    2124             :     }
    2125           0 :     else if (state_formulas::is_may(x))
    2126             :     {
    2127           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    2128             :     }
    2129           0 :     else if (state_formulas::is_yaled(x))
    2130             :     {
    2131           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    2132             :     }
    2133           0 :     else if (state_formulas::is_yaled_timed(x))
    2134             :     {
    2135           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    2136             :     }
    2137           0 :     else if (state_formulas::is_delay(x))
    2138             :     {
    2139           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    2140             :     }
    2141           0 :     else if (state_formulas::is_delay_timed(x))
    2142             :     {
    2143           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    2144             :     }
    2145           0 :     else if (state_formulas::is_variable(x))
    2146             :     {
    2147           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    2148             :     }
    2149           0 :     else if (state_formulas::is_nu(x))
    2150             :     {
    2151           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    2152             :     }
    2153           0 :     else if (state_formulas::is_mu(x))
    2154             :     {
    2155           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    2156             :     }
    2157           2 :     static_cast<Derived&>(*this).leave(x);
    2158           2 :   }
    2159             : 
    2160             : };
    2161             : 
    2162             : /// \\brief Traverser class
    2163             : template <typename Derived>
    2164             : struct data_expression_traverser: public add_traverser_data_expressions<regular_formulas::data_expression_traverser, Derived>
    2165             : {
    2166             : };
    2167             : //--- end generated state_formulas::add_traverser_data_expressions code ---//
    2168             : 
    2169             : //--- start generated state_formulas::add_traverser_state_formula_expressions code ---//
    2170             : template <template <class> class Traverser, class Derived>
    2171             : struct add_traverser_state_formula_expressions: public Traverser<Derived>
    2172             : {
    2173             :   typedef Traverser<Derived> super;
    2174             :   using super::enter;
    2175             :   using super::leave;
    2176             :   using super::apply;
    2177             : 
    2178         863 :   void apply(const state_formulas::true_& x)
    2179             :   {
    2180         863 :     static_cast<Derived&>(*this).enter(x);
    2181             :     // skip
    2182         863 :     static_cast<Derived&>(*this).leave(x);
    2183         863 :   }
    2184             : 
    2185        1436 :   void apply(const state_formulas::false_& x)
    2186             :   {
    2187        1436 :     static_cast<Derived&>(*this).enter(x);
    2188             :     // skip
    2189        1436 :     static_cast<Derived&>(*this).leave(x);
    2190        1436 :   }
    2191             : 
    2192         244 :   void apply(const state_formulas::not_& x)
    2193             :   {
    2194         244 :     static_cast<Derived&>(*this).enter(x);
    2195         244 :     static_cast<Derived&>(*this).apply(x.operand());
    2196         240 :     static_cast<Derived&>(*this).leave(x);
    2197         240 :   }
    2198             : 
    2199           0 :   void apply(const state_formulas::minus& x)
    2200             :   {
    2201           0 :     static_cast<Derived&>(*this).enter(x);
    2202           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2203           0 :     static_cast<Derived&>(*this).leave(x);
    2204           0 :   }
    2205             : 
    2206        2462 :   void apply(const state_formulas::and_& x)
    2207             :   {
    2208        2462 :     static_cast<Derived&>(*this).enter(x);
    2209        2462 :     static_cast<Derived&>(*this).apply(x.left());
    2210        2462 :     static_cast<Derived&>(*this).apply(x.right());
    2211        2461 :     static_cast<Derived&>(*this).leave(x);
    2212        2461 :   }
    2213             : 
    2214        1701 :   void apply(const state_formulas::or_& x)
    2215             :   {
    2216        1701 :     static_cast<Derived&>(*this).enter(x);
    2217        1701 :     static_cast<Derived&>(*this).apply(x.left());
    2218        1701 :     static_cast<Derived&>(*this).apply(x.right());
    2219        1697 :     static_cast<Derived&>(*this).leave(x);
    2220        1697 :   }
    2221             : 
    2222          67 :   void apply(const state_formulas::imp& x)
    2223             :   {
    2224          67 :     static_cast<Derived&>(*this).enter(x);
    2225          67 :     static_cast<Derived&>(*this).apply(x.left());
    2226          67 :     static_cast<Derived&>(*this).apply(x.right());
    2227          67 :     static_cast<Derived&>(*this).leave(x);
    2228          67 :   }
    2229             : 
    2230           0 :   void apply(const state_formulas::plus& x)
    2231             :   {
    2232           0 :     static_cast<Derived&>(*this).enter(x);
    2233           0 :     static_cast<Derived&>(*this).apply(x.left());
    2234           0 :     static_cast<Derived&>(*this).apply(x.right());
    2235           0 :     static_cast<Derived&>(*this).leave(x);
    2236           0 :   }
    2237             : 
    2238           1 :   void apply(const state_formulas::const_multiply& x)
    2239             :   {
    2240           1 :     static_cast<Derived&>(*this).enter(x);
    2241           1 :     static_cast<Derived&>(*this).apply(x.right());
    2242           1 :     static_cast<Derived&>(*this).leave(x);
    2243           1 :   }
    2244             : 
    2245           1 :   void apply(const state_formulas::const_multiply_alt& x)
    2246             :   {
    2247           1 :     static_cast<Derived&>(*this).enter(x);
    2248           1 :     static_cast<Derived&>(*this).apply(x.left());
    2249           1 :     static_cast<Derived&>(*this).leave(x);
    2250           1 :   }
    2251             : 
    2252          72 :   void apply(const state_formulas::forall& x)
    2253             :   {
    2254          72 :     static_cast<Derived&>(*this).enter(x);
    2255          72 :     static_cast<Derived&>(*this).apply(x.body());
    2256          72 :     static_cast<Derived&>(*this).leave(x);
    2257          72 :   }
    2258             : 
    2259          35 :   void apply(const state_formulas::exists& x)
    2260             :   {
    2261          35 :     static_cast<Derived&>(*this).enter(x);
    2262          35 :     static_cast<Derived&>(*this).apply(x.body());
    2263          35 :     static_cast<Derived&>(*this).leave(x);
    2264          35 :   }
    2265             : 
    2266           2 :   void apply(const state_formulas::infimum& x)
    2267             :   {
    2268           2 :     static_cast<Derived&>(*this).enter(x);
    2269           2 :     static_cast<Derived&>(*this).apply(x.body());
    2270           2 :     static_cast<Derived&>(*this).leave(x);
    2271           2 :   }
    2272             : 
    2273           1 :   void apply(const state_formulas::supremum& x)
    2274             :   {
    2275           1 :     static_cast<Derived&>(*this).enter(x);
    2276           1 :     static_cast<Derived&>(*this).apply(x.body());
    2277           1 :     static_cast<Derived&>(*this).leave(x);
    2278           1 :   }
    2279             : 
    2280           1 :   void apply(const state_formulas::sum& x)
    2281             :   {
    2282           1 :     static_cast<Derived&>(*this).enter(x);
    2283           1 :     static_cast<Derived&>(*this).apply(x.body());
    2284           1 :     static_cast<Derived&>(*this).leave(x);
    2285           1 :   }
    2286             : 
    2287        2773 :   void apply(const state_formulas::must& x)
    2288             :   {
    2289        2773 :     static_cast<Derived&>(*this).enter(x);
    2290        2773 :     static_cast<Derived&>(*this).apply(x.operand());
    2291        2773 :     static_cast<Derived&>(*this).leave(x);
    2292        2773 :   }
    2293             : 
    2294        2186 :   void apply(const state_formulas::may& x)
    2295             :   {
    2296        2186 :     static_cast<Derived&>(*this).enter(x);
    2297        2186 :     static_cast<Derived&>(*this).apply(x.operand());
    2298        2186 :     static_cast<Derived&>(*this).leave(x);
    2299        2186 :   }
    2300             : 
    2301           0 :   void apply(const state_formulas::yaled& x)
    2302             :   {
    2303           0 :     static_cast<Derived&>(*this).enter(x);
    2304             :     // skip
    2305           0 :     static_cast<Derived&>(*this).leave(x);
    2306           0 :   }
    2307             : 
    2308          16 :   void apply(const state_formulas::yaled_timed& x)
    2309             :   {
    2310          16 :     static_cast<Derived&>(*this).enter(x);
    2311             :     // skip
    2312          16 :     static_cast<Derived&>(*this).leave(x);
    2313          16 :   }
    2314             : 
    2315           0 :   void apply(const state_formulas::delay& x)
    2316             :   {
    2317           0 :     static_cast<Derived&>(*this).enter(x);
    2318             :     // skip
    2319           0 :     static_cast<Derived&>(*this).leave(x);
    2320           0 :   }
    2321             : 
    2322          16 :   void apply(const state_formulas::delay_timed& x)
    2323             :   {
    2324          16 :     static_cast<Derived&>(*this).enter(x);
    2325             :     // skip
    2326          16 :     static_cast<Derived&>(*this).leave(x);
    2327          16 :   }
    2328             : 
    2329        2890 :   void apply(const state_formulas::variable& x)
    2330             :   {
    2331        2890 :     static_cast<Derived&>(*this).enter(x);
    2332             :     // skip
    2333        2890 :     static_cast<Derived&>(*this).leave(x);
    2334        2890 :   }
    2335             : 
    2336         427 :   void apply(const state_formulas::nu& x)
    2337             :   {
    2338         427 :     static_cast<Derived&>(*this).enter(x);
    2339         426 :     static_cast<Derived&>(*this).apply(x.operand());
    2340         424 :     static_cast<Derived&>(*this).leave(x);
    2341         424 :   }
    2342             : 
    2343         379 :   void apply(const state_formulas::mu& x)
    2344             :   {
    2345         379 :     static_cast<Derived&>(*this).enter(x);
    2346         371 :     static_cast<Derived&>(*this).apply(x.operand());
    2347         364 :     static_cast<Derived&>(*this).leave(x);
    2348         364 :   }
    2349             : 
    2350             :   void apply(const state_formulas::state_formula_specification& x)
    2351             :   {
    2352             :     static_cast<Derived&>(*this).enter(x);
    2353             :     static_cast<Derived&>(*this).apply(x.formula());
    2354             :     static_cast<Derived&>(*this).leave(x);
    2355             :   }
    2356             : 
    2357       19352 :   void apply(const state_formulas::state_formula& x)
    2358             :   {
    2359       19352 :     static_cast<Derived&>(*this).enter(x);
    2360       19352 :     if (data::is_data_expression(x))
    2361             :     {
    2362         167 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    2363             :     }
    2364       19185 :     else if (data::is_untyped_data_parameter(x))
    2365             :     {
    2366           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    2367             :     }
    2368       19185 :     else if (state_formulas::is_true(x))
    2369             :     {
    2370         863 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    2371             :     }
    2372       18322 :     else if (state_formulas::is_false(x))
    2373             :     {
    2374        1436 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    2375             :     }
    2376       16886 :     else if (state_formulas::is_not(x))
    2377             :     {
    2378         244 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    2379             :     }
    2380       16642 :     else if (state_formulas::is_minus(x))
    2381             :     {
    2382           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
    2383             :     }
    2384       16642 :     else if (state_formulas::is_and(x))
    2385             :     {
    2386        2462 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    2387             :     }
    2388       14180 :     else if (state_formulas::is_or(x))
    2389             :     {
    2390        1701 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    2391             :     }
    2392       12479 :     else if (state_formulas::is_imp(x))
    2393             :     {
    2394          67 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    2395             :     }
    2396       12412 :     else if (state_formulas::is_plus(x))
    2397             :     {
    2398           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
    2399             :     }
    2400       12412 :     else if (state_formulas::is_const_multiply(x))
    2401             :     {
    2402           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
    2403             :     }
    2404       12411 :     else if (state_formulas::is_const_multiply_alt(x))
    2405             :     {
    2406           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
    2407             :     }
    2408       12410 :     else if (state_formulas::is_forall(x))
    2409             :     {
    2410         104 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    2411             :     }
    2412       12306 :     else if (state_formulas::is_exists(x))
    2413             :     {
    2414          42 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    2415             :     }
    2416       12264 :     else if (state_formulas::is_infimum(x))
    2417             :     {
    2418           2 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
    2419             :     }
    2420       12262 :     else if (state_formulas::is_supremum(x))
    2421             :     {
    2422           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
    2423             :     }
    2424       12261 :     else if (state_formulas::is_sum(x))
    2425             :     {
    2426           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
    2427             :     }
    2428       12260 :     else if (state_formulas::is_must(x))
    2429             :     {
    2430        3017 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    2431             :     }
    2432        9243 :     else if (state_formulas::is_may(x))
    2433             :     {
    2434        2358 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    2435             :     }
    2436        6885 :     else if (state_formulas::is_yaled(x))
    2437             :     {
    2438           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    2439             :     }
    2440        6885 :     else if (state_formulas::is_yaled_timed(x))
    2441             :     {
    2442          16 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    2443             :     }
    2444        6869 :     else if (state_formulas::is_delay(x))
    2445             :     {
    2446           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    2447             :     }
    2448        6869 :     else if (state_formulas::is_delay_timed(x))
    2449             :     {
    2450          16 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    2451             :     }
    2452        6853 :     else if (state_formulas::is_variable(x))
    2453             :     {
    2454        2890 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    2455             :     }
    2456        3963 :     else if (state_formulas::is_nu(x))
    2457             :     {
    2458        2276 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    2459             :     }
    2460        1687 :     else if (state_formulas::is_mu(x))
    2461             :     {
    2462        1687 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    2463             :     }
    2464       19325 :     static_cast<Derived&>(*this).leave(x);
    2465       19325 :   }
    2466             : 
    2467             : };
    2468             : 
    2469             : /// \\brief Traverser class
    2470             : template <typename Derived>
    2471             : struct state_formula_traverser: public add_traverser_state_formula_expressions<state_formulas::state_formula_traverser_base, Derived>
    2472             : {
    2473             : };
    2474             : //--- end generated state_formulas::add_traverser_state_formula_expressions code ---//
    2475             : 
    2476             : //--- start generated state_formulas::add_traverser_variables code ---//
    2477             : template <template <class> class Traverser, class Derived>
    2478             : struct add_traverser_variables: public Traverser<Derived>
    2479             : {
    2480             :   typedef Traverser<Derived> super;
    2481             :   using super::enter;
    2482             :   using super::leave;
    2483             :   using super::apply;
    2484             : 
    2485           1 :   void apply(const state_formulas::true_& x)
    2486             :   {
    2487           1 :     static_cast<Derived&>(*this).enter(x);
    2488             :     // skip
    2489           1 :     static_cast<Derived&>(*this).leave(x);
    2490           1 :   }
    2491             : 
    2492           0 :   void apply(const state_formulas::false_& x)
    2493             :   {
    2494           0 :     static_cast<Derived&>(*this).enter(x);
    2495             :     // skip
    2496           0 :     static_cast<Derived&>(*this).leave(x);
    2497           0 :   }
    2498             : 
    2499           0 :   void apply(const state_formulas::not_& x)
    2500             :   {
    2501           0 :     static_cast<Derived&>(*this).enter(x);
    2502           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2503           0 :     static_cast<Derived&>(*this).leave(x);
    2504           0 :   }
    2505             : 
    2506           0 :   void apply(const state_formulas::minus& x)
    2507             :   {
    2508           0 :     static_cast<Derived&>(*this).enter(x);
    2509           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2510           0 :     static_cast<Derived&>(*this).leave(x);
    2511           0 :   }
    2512             : 
    2513           1 :   void apply(const state_formulas::and_& x)
    2514             :   {
    2515           1 :     static_cast<Derived&>(*this).enter(x);
    2516           1 :     static_cast<Derived&>(*this).apply(x.left());
    2517           1 :     static_cast<Derived&>(*this).apply(x.right());
    2518           1 :     static_cast<Derived&>(*this).leave(x);
    2519           1 :   }
    2520             : 
    2521           0 :   void apply(const state_formulas::or_& x)
    2522             :   {
    2523           0 :     static_cast<Derived&>(*this).enter(x);
    2524           0 :     static_cast<Derived&>(*this).apply(x.left());
    2525           0 :     static_cast<Derived&>(*this).apply(x.right());
    2526           0 :     static_cast<Derived&>(*this).leave(x);
    2527           0 :   }
    2528             : 
    2529           0 :   void apply(const state_formulas::imp& x)
    2530             :   {
    2531           0 :     static_cast<Derived&>(*this).enter(x);
    2532           0 :     static_cast<Derived&>(*this).apply(x.left());
    2533           0 :     static_cast<Derived&>(*this).apply(x.right());
    2534           0 :     static_cast<Derived&>(*this).leave(x);
    2535           0 :   }
    2536             : 
    2537           0 :   void apply(const state_formulas::plus& x)
    2538             :   {
    2539           0 :     static_cast<Derived&>(*this).enter(x);
    2540           0 :     static_cast<Derived&>(*this).apply(x.left());
    2541           0 :     static_cast<Derived&>(*this).apply(x.right());
    2542           0 :     static_cast<Derived&>(*this).leave(x);
    2543           0 :   }
    2544             : 
    2545           0 :   void apply(const state_formulas::const_multiply& x)
    2546             :   {
    2547           0 :     static_cast<Derived&>(*this).enter(x);
    2548           0 :     static_cast<Derived&>(*this).apply(x.left());
    2549           0 :     static_cast<Derived&>(*this).apply(x.right());
    2550           0 :     static_cast<Derived&>(*this).leave(x);
    2551           0 :   }
    2552             : 
    2553           0 :   void apply(const state_formulas::const_multiply_alt& x)
    2554             :   {
    2555           0 :     static_cast<Derived&>(*this).enter(x);
    2556           0 :     static_cast<Derived&>(*this).apply(x.left());
    2557           0 :     static_cast<Derived&>(*this).apply(x.right());
    2558           0 :     static_cast<Derived&>(*this).leave(x);
    2559           0 :   }
    2560             : 
    2561           1 :   void apply(const state_formulas::forall& x)
    2562             :   {
    2563           1 :     static_cast<Derived&>(*this).enter(x);
    2564           1 :     static_cast<Derived&>(*this).apply(x.variables());
    2565           1 :     static_cast<Derived&>(*this).apply(x.body());
    2566           1 :     static_cast<Derived&>(*this).leave(x);
    2567           1 :   }
    2568             : 
    2569           0 :   void apply(const state_formulas::exists& x)
    2570             :   {
    2571           0 :     static_cast<Derived&>(*this).enter(x);
    2572           0 :     static_cast<Derived&>(*this).apply(x.variables());
    2573           0 :     static_cast<Derived&>(*this).apply(x.body());
    2574           0 :     static_cast<Derived&>(*this).leave(x);
    2575           0 :   }
    2576             : 
    2577           0 :   void apply(const state_formulas::infimum& x)
    2578             :   {
    2579           0 :     static_cast<Derived&>(*this).enter(x);
    2580           0 :     static_cast<Derived&>(*this).apply(x.variables());
    2581           0 :     static_cast<Derived&>(*this).apply(x.body());
    2582           0 :     static_cast<Derived&>(*this).leave(x);
    2583           0 :   }
    2584             : 
    2585           0 :   void apply(const state_formulas::supremum& x)
    2586             :   {
    2587           0 :     static_cast<Derived&>(*this).enter(x);
    2588           0 :     static_cast<Derived&>(*this).apply(x.variables());
    2589           0 :     static_cast<Derived&>(*this).apply(x.body());
    2590           0 :     static_cast<Derived&>(*this).leave(x);
    2591           0 :   }
    2592             : 
    2593           0 :   void apply(const state_formulas::sum& x)
    2594             :   {
    2595           0 :     static_cast<Derived&>(*this).enter(x);
    2596           0 :     static_cast<Derived&>(*this).apply(x.variables());
    2597           0 :     static_cast<Derived&>(*this).apply(x.body());
    2598           0 :     static_cast<Derived&>(*this).leave(x);
    2599           0 :   }
    2600             : 
    2601           0 :   void apply(const state_formulas::must& x)
    2602             :   {
    2603           0 :     static_cast<Derived&>(*this).enter(x);
    2604           0 :     static_cast<Derived&>(*this).apply(x.formula());
    2605           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2606           0 :     static_cast<Derived&>(*this).leave(x);
    2607           0 :   }
    2608             : 
    2609           0 :   void apply(const state_formulas::may& x)
    2610             :   {
    2611           0 :     static_cast<Derived&>(*this).enter(x);
    2612           0 :     static_cast<Derived&>(*this).apply(x.formula());
    2613           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2614           0 :     static_cast<Derived&>(*this).leave(x);
    2615           0 :   }
    2616             : 
    2617           0 :   void apply(const state_formulas::yaled& x)
    2618             :   {
    2619           0 :     static_cast<Derived&>(*this).enter(x);
    2620             :     // skip
    2621           0 :     static_cast<Derived&>(*this).leave(x);
    2622           0 :   }
    2623             : 
    2624           0 :   void apply(const state_formulas::yaled_timed& x)
    2625             :   {
    2626           0 :     static_cast<Derived&>(*this).enter(x);
    2627           0 :     static_cast<Derived&>(*this).apply(x.time_stamp());
    2628           0 :     static_cast<Derived&>(*this).leave(x);
    2629           0 :   }
    2630             : 
    2631           0 :   void apply(const state_formulas::delay& x)
    2632             :   {
    2633           0 :     static_cast<Derived&>(*this).enter(x);
    2634             :     // skip
    2635           0 :     static_cast<Derived&>(*this).leave(x);
    2636           0 :   }
    2637             : 
    2638           0 :   void apply(const state_formulas::delay_timed& x)
    2639             :   {
    2640           0 :     static_cast<Derived&>(*this).enter(x);
    2641           0 :     static_cast<Derived&>(*this).apply(x.time_stamp());
    2642           0 :     static_cast<Derived&>(*this).leave(x);
    2643           0 :   }
    2644             : 
    2645           1 :   void apply(const state_formulas::variable& x)
    2646             :   {
    2647           1 :     static_cast<Derived&>(*this).enter(x);
    2648           1 :     static_cast<Derived&>(*this).apply(x.arguments());
    2649           1 :     static_cast<Derived&>(*this).leave(x);
    2650           1 :   }
    2651             : 
    2652           0 :   void apply(const state_formulas::nu& x)
    2653             :   {
    2654           0 :     static_cast<Derived&>(*this).enter(x);
    2655           0 :     static_cast<Derived&>(*this).apply(x.assignments());
    2656           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2657           0 :     static_cast<Derived&>(*this).leave(x);
    2658           0 :   }
    2659             : 
    2660           1 :   void apply(const state_formulas::mu& x)
    2661             :   {
    2662           1 :     static_cast<Derived&>(*this).enter(x);
    2663           1 :     static_cast<Derived&>(*this).apply(x.assignments());
    2664           1 :     static_cast<Derived&>(*this).apply(x.operand());
    2665           1 :     static_cast<Derived&>(*this).leave(x);
    2666           1 :   }
    2667             : 
    2668             :   void apply(const state_formulas::state_formula_specification& x)
    2669             :   {
    2670             :     static_cast<Derived&>(*this).enter(x);
    2671             :     static_cast<Derived&>(*this).apply(x.formula());
    2672             :     static_cast<Derived&>(*this).leave(x);
    2673             :   }
    2674             : 
    2675           5 :   void apply(const state_formulas::state_formula& x)
    2676             :   {
    2677           5 :     static_cast<Derived&>(*this).enter(x);
    2678           5 :     if (data::is_data_expression(x))
    2679             :     {
    2680           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    2681             :     }
    2682           5 :     else if (data::is_untyped_data_parameter(x))
    2683             :     {
    2684           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    2685             :     }
    2686           5 :     else if (state_formulas::is_true(x))
    2687             :     {
    2688           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    2689             :     }
    2690           4 :     else if (state_formulas::is_false(x))
    2691             :     {
    2692           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    2693             :     }
    2694           4 :     else if (state_formulas::is_not(x))
    2695             :     {
    2696           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    2697             :     }
    2698           4 :     else if (state_formulas::is_minus(x))
    2699             :     {
    2700           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
    2701             :     }
    2702           4 :     else if (state_formulas::is_and(x))
    2703             :     {
    2704           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    2705             :     }
    2706           3 :     else if (state_formulas::is_or(x))
    2707             :     {
    2708           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    2709             :     }
    2710           3 :     else if (state_formulas::is_imp(x))
    2711             :     {
    2712           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    2713             :     }
    2714           3 :     else if (state_formulas::is_plus(x))
    2715             :     {
    2716           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
    2717             :     }
    2718           3 :     else if (state_formulas::is_const_multiply(x))
    2719             :     {
    2720           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
    2721             :     }
    2722           3 :     else if (state_formulas::is_const_multiply_alt(x))
    2723             :     {
    2724           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
    2725             :     }
    2726           3 :     else if (state_formulas::is_forall(x))
    2727             :     {
    2728           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    2729             :     }
    2730           2 :     else if (state_formulas::is_exists(x))
    2731             :     {
    2732           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    2733             :     }
    2734           2 :     else if (state_formulas::is_infimum(x))
    2735             :     {
    2736           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
    2737             :     }
    2738           2 :     else if (state_formulas::is_supremum(x))
    2739             :     {
    2740           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
    2741             :     }
    2742           2 :     else if (state_formulas::is_sum(x))
    2743             :     {
    2744           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
    2745             :     }
    2746           2 :     else if (state_formulas::is_must(x))
    2747             :     {
    2748           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    2749             :     }
    2750           2 :     else if (state_formulas::is_may(x))
    2751             :     {
    2752           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    2753             :     }
    2754           2 :     else if (state_formulas::is_yaled(x))
    2755             :     {
    2756           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    2757             :     }
    2758           2 :     else if (state_formulas::is_yaled_timed(x))
    2759             :     {
    2760           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    2761             :     }
    2762           2 :     else if (state_formulas::is_delay(x))
    2763             :     {
    2764           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    2765             :     }
    2766           2 :     else if (state_formulas::is_delay_timed(x))
    2767             :     {
    2768           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    2769             :     }
    2770           2 :     else if (state_formulas::is_variable(x))
    2771             :     {
    2772           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    2773             :     }
    2774           1 :     else if (state_formulas::is_nu(x))
    2775             :     {
    2776           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    2777             :     }
    2778           1 :     else if (state_formulas::is_mu(x))
    2779             :     {
    2780           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    2781             :     }
    2782           5 :     static_cast<Derived&>(*this).leave(x);
    2783           5 :   }
    2784             : 
    2785             : };
    2786             : 
    2787             : /// \\brief Traverser class
    2788             : template <typename Derived>
    2789             : struct variable_traverser: public add_traverser_variables<regular_formulas::variable_traverser, Derived>
    2790             : {
    2791             : };
    2792             : //--- end generated state_formulas::add_traverser_variables code ---//
    2793             : 
    2794             : //--- start generated state_formulas::add_traverser_state_variables code ---//
    2795             : template <template <class> class Traverser, class Derived>
    2796             : struct add_traverser_state_variables: public Traverser<Derived>
    2797             : {
    2798             :   typedef Traverser<Derived> super;
    2799             :   using super::enter;
    2800             :   using super::leave;
    2801             :   using super::apply;
    2802             : 
    2803           2 :   void apply(const state_formulas::true_& x)
    2804             :   {
    2805           2 :     static_cast<Derived&>(*this).enter(x);
    2806             :     // skip
    2807           2 :     static_cast<Derived&>(*this).leave(x);
    2808           2 :   }
    2809             : 
    2810           0 :   void apply(const state_formulas::false_& x)
    2811             :   {
    2812           0 :     static_cast<Derived&>(*this).enter(x);
    2813             :     // skip
    2814           0 :     static_cast<Derived&>(*this).leave(x);
    2815           0 :   }
    2816             : 
    2817           0 :   void apply(const state_formulas::not_& x)
    2818             :   {
    2819           0 :     static_cast<Derived&>(*this).enter(x);
    2820           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2821           0 :     static_cast<Derived&>(*this).leave(x);
    2822           0 :   }
    2823             : 
    2824           0 :   void apply(const state_formulas::minus& x)
    2825             :   {
    2826           0 :     static_cast<Derived&>(*this).enter(x);
    2827           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2828           0 :     static_cast<Derived&>(*this).leave(x);
    2829           0 :   }
    2830             : 
    2831           8 :   void apply(const state_formulas::and_& x)
    2832             :   {
    2833           8 :     static_cast<Derived&>(*this).enter(x);
    2834           8 :     static_cast<Derived&>(*this).apply(x.left());
    2835           8 :     static_cast<Derived&>(*this).apply(x.right());
    2836           8 :     static_cast<Derived&>(*this).leave(x);
    2837           8 :   }
    2838             : 
    2839           1 :   void apply(const state_formulas::or_& x)
    2840             :   {
    2841           1 :     static_cast<Derived&>(*this).enter(x);
    2842           1 :     static_cast<Derived&>(*this).apply(x.left());
    2843           1 :     static_cast<Derived&>(*this).apply(x.right());
    2844           1 :     static_cast<Derived&>(*this).leave(x);
    2845           1 :   }
    2846             : 
    2847           0 :   void apply(const state_formulas::imp& x)
    2848             :   {
    2849           0 :     static_cast<Derived&>(*this).enter(x);
    2850           0 :     static_cast<Derived&>(*this).apply(x.left());
    2851           0 :     static_cast<Derived&>(*this).apply(x.right());
    2852           0 :     static_cast<Derived&>(*this).leave(x);
    2853           0 :   }
    2854             : 
    2855           0 :   void apply(const state_formulas::plus& x)
    2856             :   {
    2857           0 :     static_cast<Derived&>(*this).enter(x);
    2858           0 :     static_cast<Derived&>(*this).apply(x.left());
    2859           0 :     static_cast<Derived&>(*this).apply(x.right());
    2860           0 :     static_cast<Derived&>(*this).leave(x);
    2861           0 :   }
    2862             : 
    2863           0 :   void apply(const state_formulas::const_multiply& x)
    2864             :   {
    2865           0 :     static_cast<Derived&>(*this).enter(x);
    2866           0 :     static_cast<Derived&>(*this).apply(x.right());
    2867           0 :     static_cast<Derived&>(*this).leave(x);
    2868           0 :   }
    2869             : 
    2870           0 :   void apply(const state_formulas::const_multiply_alt& x)
    2871             :   {
    2872           0 :     static_cast<Derived&>(*this).enter(x);
    2873           0 :     static_cast<Derived&>(*this).apply(x.left());
    2874           0 :     static_cast<Derived&>(*this).leave(x);
    2875           0 :   }
    2876             : 
    2877           0 :   void apply(const state_formulas::forall& x)
    2878             :   {
    2879           0 :     static_cast<Derived&>(*this).enter(x);
    2880           0 :     static_cast<Derived&>(*this).apply(x.body());
    2881           0 :     static_cast<Derived&>(*this).leave(x);
    2882           0 :   }
    2883             : 
    2884           0 :   void apply(const state_formulas::exists& x)
    2885             :   {
    2886           0 :     static_cast<Derived&>(*this).enter(x);
    2887           0 :     static_cast<Derived&>(*this).apply(x.body());
    2888           0 :     static_cast<Derived&>(*this).leave(x);
    2889           0 :   }
    2890             : 
    2891           0 :   void apply(const state_formulas::infimum& x)
    2892             :   {
    2893           0 :     static_cast<Derived&>(*this).enter(x);
    2894           0 :     static_cast<Derived&>(*this).apply(x.body());
    2895           0 :     static_cast<Derived&>(*this).leave(x);
    2896           0 :   }
    2897             : 
    2898           0 :   void apply(const state_formulas::supremum& x)
    2899             :   {
    2900           0 :     static_cast<Derived&>(*this).enter(x);
    2901           0 :     static_cast<Derived&>(*this).apply(x.body());
    2902           0 :     static_cast<Derived&>(*this).leave(x);
    2903           0 :   }
    2904             : 
    2905           0 :   void apply(const state_formulas::sum& x)
    2906             :   {
    2907           0 :     static_cast<Derived&>(*this).enter(x);
    2908           0 :     static_cast<Derived&>(*this).apply(x.body());
    2909           0 :     static_cast<Derived&>(*this).leave(x);
    2910           0 :   }
    2911             : 
    2912           0 :   void apply(const state_formulas::must& x)
    2913             :   {
    2914           0 :     static_cast<Derived&>(*this).enter(x);
    2915           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2916           0 :     static_cast<Derived&>(*this).leave(x);
    2917           0 :   }
    2918             : 
    2919           0 :   void apply(const state_formulas::may& x)
    2920             :   {
    2921           0 :     static_cast<Derived&>(*this).enter(x);
    2922           0 :     static_cast<Derived&>(*this).apply(x.operand());
    2923           0 :     static_cast<Derived&>(*this).leave(x);
    2924           0 :   }
    2925             : 
    2926           0 :   void apply(const state_formulas::yaled& x)
    2927             :   {
    2928           0 :     static_cast<Derived&>(*this).enter(x);
    2929             :     // skip
    2930           0 :     static_cast<Derived&>(*this).leave(x);
    2931           0 :   }
    2932             : 
    2933           0 :   void apply(const state_formulas::yaled_timed& x)
    2934             :   {
    2935           0 :     static_cast<Derived&>(*this).enter(x);
    2936             :     // skip
    2937           0 :     static_cast<Derived&>(*this).leave(x);
    2938           0 :   }
    2939             : 
    2940           0 :   void apply(const state_formulas::delay& x)
    2941             :   {
    2942           0 :     static_cast<Derived&>(*this).enter(x);
    2943             :     // skip
    2944           0 :     static_cast<Derived&>(*this).leave(x);
    2945           0 :   }
    2946             : 
    2947           0 :   void apply(const state_formulas::delay_timed& x)
    2948             :   {
    2949           0 :     static_cast<Derived&>(*this).enter(x);
    2950             :     // skip
    2951           0 :     static_cast<Derived&>(*this).leave(x);
    2952           0 :   }
    2953             : 
    2954             :   void apply(const state_formulas::variable& x)
    2955             :   {
    2956             :     static_cast<Derived&>(*this).enter(x);
    2957             :     // skip
    2958             :     static_cast<Derived&>(*this).leave(x);
    2959             :   }
    2960             : 
    2961           2 :   void apply(const state_formulas::nu& x)
    2962             :   {
    2963           2 :     static_cast<Derived&>(*this).enter(x);
    2964           2 :     static_cast<Derived&>(*this).apply(x.operand());
    2965           2 :     static_cast<Derived&>(*this).leave(x);
    2966           2 :   }
    2967             : 
    2968           6 :   void apply(const state_formulas::mu& x)
    2969             :   {
    2970           6 :     static_cast<Derived&>(*this).enter(x);
    2971           6 :     static_cast<Derived&>(*this).apply(x.operand());
    2972           6 :     static_cast<Derived&>(*this).leave(x);
    2973           6 :   }
    2974             : 
    2975             :   void apply(const state_formulas::state_formula_specification& x)
    2976             :   {
    2977             :     static_cast<Derived&>(*this).enter(x);
    2978             :     static_cast<Derived&>(*this).apply(x.formula());
    2979             :     static_cast<Derived&>(*this).leave(x);
    2980             :   }
    2981             : 
    2982          32 :   void apply(const state_formulas::state_formula& x)
    2983             :   {
    2984          32 :     static_cast<Derived&>(*this).enter(x);
    2985          32 :     if (data::is_data_expression(x))
    2986             :     {
    2987           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    2988             :     }
    2989          32 :     else if (data::is_untyped_data_parameter(x))
    2990             :     {
    2991           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    2992             :     }
    2993          32 :     else if (state_formulas::is_true(x))
    2994             :     {
    2995           2 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    2996             :     }
    2997          30 :     else if (state_formulas::is_false(x))
    2998             :     {
    2999           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    3000             :     }
    3001          30 :     else if (state_formulas::is_not(x))
    3002             :     {
    3003           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    3004             :     }
    3005          30 :     else if (state_formulas::is_minus(x))
    3006             :     {
    3007           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
    3008             :     }
    3009          30 :     else if (state_formulas::is_and(x))
    3010             :     {
    3011           8 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    3012             :     }
    3013          22 :     else if (state_formulas::is_or(x))
    3014             :     {
    3015           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    3016             :     }
    3017          21 :     else if (state_formulas::is_imp(x))
    3018             :     {
    3019           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    3020             :     }
    3021          21 :     else if (state_formulas::is_plus(x))
    3022             :     {
    3023           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
    3024             :     }
    3025          21 :     else if (state_formulas::is_const_multiply(x))
    3026             :     {
    3027           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
    3028             :     }
    3029          21 :     else if (state_formulas::is_const_multiply_alt(x))
    3030             :     {
    3031           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
    3032             :     }
    3033          21 :     else if (state_formulas::is_forall(x))
    3034             :     {
    3035           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    3036             :     }
    3037          21 :     else if (state_formulas::is_exists(x))
    3038             :     {
    3039           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    3040             :     }
    3041          21 :     else if (state_formulas::is_infimum(x))
    3042             :     {
    3043           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
    3044             :     }
    3045          21 :     else if (state_formulas::is_supremum(x))
    3046             :     {
    3047           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
    3048             :     }
    3049          21 :     else if (state_formulas::is_sum(x))
    3050             :     {
    3051           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
    3052             :     }
    3053          21 :     else if (state_formulas::is_must(x))
    3054             :     {
    3055           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    3056             :     }
    3057          21 :     else if (state_formulas::is_may(x))
    3058             :     {
    3059           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    3060             :     }
    3061          21 :     else if (state_formulas::is_yaled(x))
    3062             :     {
    3063           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    3064             :     }
    3065          21 :     else if (state_formulas::is_yaled_timed(x))
    3066             :     {
    3067           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    3068             :     }
    3069          21 :     else if (state_formulas::is_delay(x))
    3070             :     {
    3071           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    3072             :     }
    3073          21 :     else if (state_formulas::is_delay_timed(x))
    3074             :     {
    3075           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    3076             :     }
    3077          21 :     else if (state_formulas::is_variable(x))
    3078             :     {
    3079          13 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    3080             :     }
    3081           8 :     else if (state_formulas::is_nu(x))
    3082             :     {
    3083           2 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    3084             :     }
    3085           6 :     else if (state_formulas::is_mu(x))
    3086             :     {
    3087           6 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    3088             :     }
    3089          32 :     static_cast<Derived&>(*this).leave(x);
    3090          32 :   }
    3091             : 
    3092             : };
    3093             : 
    3094             : /// \\brief Traverser class
    3095             : template <typename Derived>
    3096             : struct state_variable_traverser: public add_traverser_state_variables<state_formulas::state_formula_traverser_base, Derived>
    3097             : {
    3098             : };
    3099             : //--- end generated state_formulas::add_traverser_state_variables code ---//
    3100             : 
    3101             : //--- start generated state_formulas::add_traverser_identifier_strings code ---//
    3102             : template <template <class> class Traverser, class Derived>
    3103             : struct add_traverser_identifier_strings: public Traverser<Derived>
    3104             : {
    3105             :   typedef Traverser<Derived> super;
    3106             :   using super::enter;
    3107             :   using super::leave;
    3108             :   using super::apply;
    3109             : 
    3110         388 :   void apply(const state_formulas::true_& x)
    3111             :   {
    3112         388 :     static_cast<Derived&>(*this).enter(x);
    3113             :     // skip
    3114         388 :     static_cast<Derived&>(*this).leave(x);
    3115         388 :   }
    3116             : 
    3117         238 :   void apply(const state_formulas::false_& x)
    3118             :   {
    3119         238 :     static_cast<Derived&>(*this).enter(x);
    3120             :     // skip
    3121         238 :     static_cast<Derived&>(*this).leave(x);
    3122         238 :   }
    3123             : 
    3124         180 :   void apply(const state_formulas::not_& x)
    3125             :   {
    3126         180 :     static_cast<Derived&>(*this).enter(x);
    3127         180 :     static_cast<Derived&>(*this).apply(x.operand());
    3128         180 :     static_cast<Derived&>(*this).leave(x);
    3129         180 :   }
    3130             : 
    3131           0 :   void apply(const state_formulas::minus& x)
    3132             :   {
    3133           0 :     static_cast<Derived&>(*this).enter(x);
    3134           0 :     static_cast<Derived&>(*this).apply(x.operand());
    3135           0 :     static_cast<Derived&>(*this).leave(x);
    3136           0 :   }
    3137             : 
    3138         274 :   void apply(const state_formulas::and_& x)
    3139             :   {
    3140         274 :     static_cast<Derived&>(*this).enter(x);
    3141         274 :     static_cast<Derived&>(*this).apply(x.left());
    3142         274 :     static_cast<Derived&>(*this).apply(x.right());
    3143         274 :     static_cast<Derived&>(*this).leave(x);
    3144         274 :   }
    3145             : 
    3146         163 :   void apply(const state_formulas::or_& x)
    3147             :   {
    3148         163 :     static_cast<Derived&>(*this).enter(x);
    3149         163 :     static_cast<Derived&>(*this).apply(x.left());
    3150         163 :     static_cast<Derived&>(*this).apply(x.right());
    3151         163 :     static_cast<Derived&>(*this).leave(x);
    3152         163 :   }
    3153             : 
    3154          52 :   void apply(const state_formulas::imp& x)
    3155             :   {
    3156          52 :     static_cast<Derived&>(*this).enter(x);
    3157          52 :     static_cast<Derived&>(*this).apply(x.left());
    3158          52 :     static_cast<Derived&>(*this).apply(x.right());
    3159          52 :     static_cast<Derived&>(*this).leave(x);
    3160          52 :   }
    3161             : 
    3162           0 :   void apply(const state_formulas::plus& x)
    3163             :   {
    3164           0 :     static_cast<Derived&>(*this).enter(x);
    3165           0 :     static_cast<Derived&>(*this).apply(x.left());
    3166           0 :     static_cast<Derived&>(*this).apply(x.right());
    3167           0 :     static_cast<Derived&>(*this).leave(x);
    3168           0 :   }
    3169             : 
    3170           1 :   void apply(const state_formulas::const_multiply& x)
    3171             :   {
    3172           1 :     static_cast<Derived&>(*this).enter(x);
    3173           1 :     static_cast<Derived&>(*this).apply(x.left());
    3174           1 :     static_cast<Derived&>(*this).apply(x.right());
    3175           1 :     static_cast<Derived&>(*this).leave(x);
    3176           1 :   }
    3177             : 
    3178           1 :   void apply(const state_formulas::const_multiply_alt& x)
    3179             :   {
    3180           1 :     static_cast<Derived&>(*this).enter(x);
    3181           1 :     static_cast<Derived&>(*this).apply(x.left());
    3182           1 :     static_cast<Derived&>(*this).apply(x.right());
    3183           1 :     static_cast<Derived&>(*this).leave(x);
    3184           1 :   }
    3185             : 
    3186          52 :   void apply(const state_formulas::forall& x)
    3187             :   {
    3188          52 :     static_cast<Derived&>(*this).enter(x);
    3189          52 :     static_cast<Derived&>(*this).apply(x.variables());
    3190          52 :     static_cast<Derived&>(*this).apply(x.body());
    3191          52 :     static_cast<Derived&>(*this).leave(x);
    3192          52 :   }
    3193             : 
    3194          26 :   void apply(const state_formulas::exists& x)
    3195             :   {
    3196          26 :     static_cast<Derived&>(*this).enter(x);
    3197          26 :     static_cast<Derived&>(*this).apply(x.variables());
    3198          26 :     static_cast<Derived&>(*this).apply(x.body());
    3199          26 :     static_cast<Derived&>(*this).leave(x);
    3200          26 :   }
    3201             : 
    3202           2 :   void apply(const state_formulas::infimum& x)
    3203             :   {
    3204           2 :     static_cast<Derived&>(*this).enter(x);
    3205           2 :     static_cast<Derived&>(*this).apply(x.variables());
    3206           2 :     static_cast<Derived&>(*this).apply(x.body());
    3207           2 :     static_cast<Derived&>(*this).leave(x);
    3208           2 :   }
    3209             : 
    3210           1 :   void apply(const state_formulas::supremum& x)
    3211             :   {
    3212           1 :     static_cast<Derived&>(*this).enter(x);
    3213           1 :     static_cast<Derived&>(*this).apply(x.variables());
    3214           1 :     static_cast<Derived&>(*this).apply(x.body());
    3215           1 :     static_cast<Derived&>(*this).leave(x);
    3216           1 :   }
    3217             : 
    3218           1 :   void apply(const state_formulas::sum& x)
    3219             :   {
    3220           1 :     static_cast<Derived&>(*this).enter(x);
    3221           1 :     static_cast<Derived&>(*this).apply(x.variables());
    3222           1 :     static_cast<Derived&>(*this).apply(x.body());
    3223           1 :     static_cast<Derived&>(*this).leave(x);
    3224           1 :   }
    3225             : 
    3226         527 :   void apply(const state_formulas::must& x)
    3227             :   {
    3228         527 :     static_cast<Derived&>(*this).enter(x);
    3229         527 :     static_cast<Derived&>(*this).apply(x.formula());
    3230         527 :     static_cast<Derived&>(*this).apply(x.operand());
    3231         527 :     static_cast<Derived&>(*this).leave(x);
    3232         527 :   }
    3233             : 
    3234         483 :   void apply(const state_formulas::may& x)
    3235             :   {
    3236         483 :     static_cast<Derived&>(*this).enter(x);
    3237         483 :     static_cast<Derived&>(*this).apply(x.formula());
    3238         483 :     static_cast<Derived&>(*this).apply(x.operand());
    3239         483 :     static_cast<Derived&>(*this).leave(x);
    3240         483 :   }
    3241             : 
    3242           0 :   void apply(const state_formulas::yaled& x)
    3243             :   {
    3244           0 :     static_cast<Derived&>(*this).enter(x);
    3245             :     // skip
    3246           0 :     static_cast<Derived&>(*this).leave(x);
    3247           0 :   }
    3248             : 
    3249          11 :   void apply(const state_formulas::yaled_timed& x)
    3250             :   {
    3251          11 :     static_cast<Derived&>(*this).enter(x);
    3252          11 :     static_cast<Derived&>(*this).apply(x.time_stamp());
    3253          11 :     static_cast<Derived&>(*this).leave(x);
    3254          11 :   }
    3255             : 
    3256           0 :   void apply(const state_formulas::delay& x)
    3257             :   {
    3258           0 :     static_cast<Derived&>(*this).enter(x);
    3259             :     // skip
    3260           0 :     static_cast<Derived&>(*this).leave(x);
    3261           0 :   }
    3262             : 
    3263          11 :   void apply(const state_formulas::delay_timed& x)
    3264             :   {
    3265          11 :     static_cast<Derived&>(*this).enter(x);
    3266          11 :     static_cast<Derived&>(*this).apply(x.time_stamp());
    3267          11 :     static_cast<Derived&>(*this).leave(x);
    3268          11 :   }
    3269             : 
    3270         434 :   void apply(const state_formulas::variable& x)
    3271             :   {
    3272         434 :     static_cast<Derived&>(*this).enter(x);
    3273         434 :     static_cast<Derived&>(*this).apply(x.name());
    3274         434 :     static_cast<Derived&>(*this).apply(x.arguments());
    3275         434 :     static_cast<Derived&>(*this).leave(x);
    3276         434 :   }
    3277             : 
    3278         303 :   void apply(const state_formulas::nu& x)
    3279             :   {
    3280         303 :     static_cast<Derived&>(*this).enter(x);
    3281         303 :     static_cast<Derived&>(*this).apply(x.name());
    3282         303 :     static_cast<Derived&>(*this).apply(x.assignments());
    3283         303 :     static_cast<Derived&>(*this).apply(x.operand());
    3284         303 :     static_cast<Derived&>(*this).leave(x);
    3285         303 :   }
    3286             : 
    3287         269 :   void apply(const state_formulas::mu& x)
    3288             :   {
    3289         269 :     static_cast<Derived&>(*this).enter(x);
    3290         269 :     static_cast<Derived&>(*this).apply(x.name());
    3291         269 :     static_cast<Derived&>(*this).apply(x.assignments());
    3292         269 :     static_cast<Derived&>(*this).apply(x.operand());
    3293         269 :     static_cast<Derived&>(*this).leave(x);
    3294         269 :   }
    3295             : 
    3296             :   void apply(const state_formulas::state_formula_specification& x)
    3297             :   {
    3298             :     static_cast<Derived&>(*this).enter(x);
    3299             :     static_cast<Derived&>(*this).apply(x.action_labels());
    3300             :     static_cast<Derived&>(*this).apply(x.formula());
    3301             :     static_cast<Derived&>(*this).leave(x);
    3302             :   }
    3303             : 
    3304        3497 :   void apply(const state_formulas::state_formula& x)
    3305             :   {
    3306        3497 :     static_cast<Derived&>(*this).enter(x);
    3307        3497 :     if (data::is_data_expression(x))
    3308             :     {
    3309          80 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    3310             :     }
    3311        3417 :     else if (data::is_untyped_data_parameter(x))
    3312             :     {
    3313           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    3314             :     }
    3315        3417 :     else if (state_formulas::is_true(x))
    3316             :     {
    3317         388 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    3318             :     }
    3319        3029 :     else if (state_formulas::is_false(x))
    3320             :     {
    3321         238 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    3322             :     }
    3323        2791 :     else if (state_formulas::is_not(x))
    3324             :     {
    3325         180 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    3326             :     }
    3327        2611 :     else if (state_formulas::is_minus(x))
    3328             :     {
    3329           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
    3330             :     }
    3331        2611 :     else if (state_formulas::is_and(x))
    3332             :     {
    3333         274 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    3334             :     }
    3335        2337 :     else if (state_formulas::is_or(x))
    3336             :     {
    3337         163 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    3338             :     }
    3339        2174 :     else if (state_formulas::is_imp(x))
    3340             :     {
    3341          52 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    3342             :     }
    3343        2122 :     else if (state_formulas::is_plus(x))
    3344             :     {
    3345           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
    3346             :     }
    3347        2122 :     else if (state_formulas::is_const_multiply(x))
    3348             :     {
    3349           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
    3350             :     }
    3351        2121 :     else if (state_formulas::is_const_multiply_alt(x))
    3352             :     {
    3353           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
    3354             :     }
    3355        2120 :     else if (state_formulas::is_forall(x))
    3356             :     {
    3357          52 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    3358             :     }
    3359        2068 :     else if (state_formulas::is_exists(x))
    3360             :     {
    3361          26 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    3362             :     }
    3363        2042 :     else if (state_formulas::is_infimum(x))
    3364             :     {
    3365           2 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
    3366             :     }
    3367        2040 :     else if (state_formulas::is_supremum(x))
    3368             :     {
    3369           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
    3370             :     }
    3371        2039 :     else if (state_formulas::is_sum(x))
    3372             :     {
    3373           1 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
    3374             :     }
    3375        2038 :     else if (state_formulas::is_must(x))
    3376             :     {
    3377         527 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    3378             :     }
    3379        1511 :     else if (state_formulas::is_may(x))
    3380             :     {
    3381         483 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    3382             :     }
    3383        1028 :     else if (state_formulas::is_yaled(x))
    3384             :     {
    3385           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    3386             :     }
    3387        1028 :     else if (state_formulas::is_yaled_timed(x))
    3388             :     {
    3389          11 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    3390             :     }
    3391        1017 :     else if (state_formulas::is_delay(x))
    3392             :     {
    3393           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    3394             :     }
    3395        1017 :     else if (state_formulas::is_delay_timed(x))
    3396             :     {
    3397          11 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    3398             :     }
    3399        1006 :     else if (state_formulas::is_variable(x))
    3400             :     {
    3401         434 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    3402             :     }
    3403         572 :     else if (state_formulas::is_nu(x))
    3404             :     {
    3405         303 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    3406             :     }
    3407         269 :     else if (state_formulas::is_mu(x))
    3408             :     {
    3409         269 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    3410             :     }
    3411        3497 :     static_cast<Derived&>(*this).leave(x);
    3412        3497 :   }
    3413             : 
    3414             : };
    3415             : 
    3416             : /// \\brief Traverser class
    3417             : template <typename Derived>
    3418             : struct identifier_string_traverser: public add_traverser_identifier_strings<regular_formulas::identifier_string_traverser, Derived>
    3419             : {
    3420             : };
    3421             : //--- end generated state_formulas::add_traverser_identifier_strings code ---//
    3422             : 
    3423             : //--- start generated state_formulas::add_traverser_regular_formula_expressions code ---//
    3424             : template <template <class> class Traverser, class Derived>
    3425             : struct add_traverser_regular_formula_expressions: public Traverser<Derived>
    3426             : {
    3427             :   typedef Traverser<Derived> super;
    3428             :   using super::enter;
    3429             :   using super::leave;
    3430             :   using super::apply;
    3431             : 
    3432             :   void apply(const state_formulas::true_& x)
    3433             :   {
    3434             :     static_cast<Derived&>(*this).enter(x);
    3435             :     // skip
    3436             :     static_cast<Derived&>(*this).leave(x);
    3437             :   }
    3438             : 
    3439             :   void apply(const state_formulas::false_& x)
    3440             :   {
    3441             :     static_cast<Derived&>(*this).enter(x);
    3442             :     // skip
    3443             :     static_cast<Derived&>(*this).leave(x);
    3444             :   }
    3445             : 
    3446             :   void apply(const state_formulas::not_& x)
    3447             :   {
    3448             :     static_cast<Derived&>(*this).enter(x);
    3449             :     static_cast<Derived&>(*this).apply(x.operand());
    3450             :     static_cast<Derived&>(*this).leave(x);
    3451             :   }
    3452             : 
    3453             :   void apply(const state_formulas::minus& x)
    3454             :   {
    3455             :     static_cast<Derived&>(*this).enter(x);
    3456             :     static_cast<Derived&>(*this).apply(x.operand());
    3457             :     static_cast<Derived&>(*this).leave(x);
    3458             :   }
    3459             : 
    3460             :   void apply(const state_formulas::and_& x)
    3461             :   {
    3462             :     static_cast<Derived&>(*this).enter(x);
    3463             :     static_cast<Derived&>(*this).apply(x.left());
    3464             :     static_cast<Derived&>(*this).apply(x.right());
    3465             :     static_cast<Derived&>(*this).leave(x);
    3466             :   }
    3467             : 
    3468             :   void apply(const state_formulas::or_& x)
    3469             :   {
    3470             :     static_cast<Derived&>(*this).enter(x);
    3471             :     static_cast<Derived&>(*this).apply(x.left());
    3472             :     static_cast<Derived&>(*this).apply(x.right());
    3473             :     static_cast<Derived&>(*this).leave(x);
    3474             :   }
    3475             : 
    3476             :   void apply(const state_formulas::imp& x)
    3477             :   {
    3478             :     static_cast<Derived&>(*this).enter(x);
    3479             :     static_cast<Derived&>(*this).apply(x.left());
    3480             :     static_cast<Derived&>(*this).apply(x.right());
    3481             :     static_cast<Derived&>(*this).leave(x);
    3482             :   }
    3483             : 
    3484             :   void apply(const state_formulas::plus& x)
    3485             :   {
    3486             :     static_cast<Derived&>(*this).enter(x);
    3487             :     static_cast<Derived&>(*this).apply(x.left());
    3488             :     static_cast<Derived&>(*this).apply(x.right());
    3489             :     static_cast<Derived&>(*this).leave(x);
    3490             :   }
    3491             : 
    3492             :   void apply(const state_formulas::const_multiply& x)
    3493             :   {
    3494             :     static_cast<Derived&>(*this).enter(x);
    3495             :     static_cast<Derived&>(*this).apply(x.right());
    3496             :     static_cast<Derived&>(*this).leave(x);
    3497             :   }
    3498             : 
    3499             :   void apply(const state_formulas::const_multiply_alt& x)
    3500             :   {
    3501             :     static_cast<Derived&>(*this).enter(x);
    3502             :     static_cast<Derived&>(*this).apply(x.left());
    3503             :     static_cast<Derived&>(*this).leave(x);
    3504             :   }
    3505             : 
    3506             :   void apply(const state_formulas::forall& x)
    3507             :   {
    3508             :     static_cast<Derived&>(*this).enter(x);
    3509             :     static_cast<Derived&>(*this).apply(x.body());
    3510             :     static_cast<Derived&>(*this).leave(x);
    3511             :   }
    3512             : 
    3513             :   void apply(const state_formulas::exists& x)
    3514             :   {
    3515             :     static_cast<Derived&>(*this).enter(x);
    3516             :     static_cast<Derived&>(*this).apply(x.body());
    3517             :     static_cast<Derived&>(*this).leave(x);
    3518             :   }
    3519             : 
    3520             :   void apply(const state_formulas::infimum& x)
    3521             :   {
    3522             :     static_cast<Derived&>(*this).enter(x);
    3523             :     static_cast<Derived&>(*this).apply(x.body());
    3524             :     static_cast<Derived&>(*this).leave(x);
    3525             :   }
    3526             : 
    3527             :   void apply(const state_formulas::supremum& x)
    3528             :   {
    3529             :     static_cast<Derived&>(*this).enter(x);
    3530             :     static_cast<Derived&>(*this).apply(x.body());
    3531             :     static_cast<Derived&>(*this).leave(x);
    3532             :   }
    3533             : 
    3534             :   void apply(const state_formulas::sum& x)
    3535             :   {
    3536             :     static_cast<Derived&>(*this).enter(x);
    3537             :     static_cast<Derived&>(*this).apply(x.body());
    3538             :     static_cast<Derived&>(*this).leave(x);
    3539             :   }
    3540             : 
    3541             :   void apply(const state_formulas::must& x)
    3542             :   {
    3543             :     static_cast<Derived&>(*this).enter(x);
    3544             :     static_cast<Derived&>(*this).apply(x.formula());
    3545             :     static_cast<Derived&>(*this).apply(x.operand());
    3546             :     static_cast<Derived&>(*this).leave(x);
    3547             :   }
    3548             : 
    3549             :   void apply(const state_formulas::may& x)
    3550             :   {
    3551             :     static_cast<Derived&>(*this).enter(x);
    3552             :     static_cast<Derived&>(*this).apply(x.formula());
    3553             :     static_cast<Derived&>(*this).apply(x.operand());
    3554             :     static_cast<Derived&>(*this).leave(x);
    3555             :   }
    3556             : 
    3557             :   void apply(const state_formulas::yaled& x)
    3558             :   {
    3559             :     static_cast<Derived&>(*this).enter(x);
    3560             :     // skip
    3561             :     static_cast<Derived&>(*this).leave(x);
    3562             :   }
    3563             : 
    3564             :   void apply(const state_formulas::yaled_timed& x)
    3565             :   {
    3566             :     static_cast<Derived&>(*this).enter(x);
    3567             :     // skip
    3568             :     static_cast<Derived&>(*this).leave(x);
    3569             :   }
    3570             : 
    3571             :   void apply(const state_formulas::delay& x)
    3572             :   {
    3573             :     static_cast<Derived&>(*this).enter(x);
    3574             :     // skip
    3575             :     static_cast<Derived&>(*this).leave(x);
    3576             :   }
    3577             : 
    3578             :   void apply(const state_formulas::delay_timed& x)
    3579             :   {
    3580             :     static_cast<Derived&>(*this).enter(x);
    3581             :     // skip
    3582             :     static_cast<Derived&>(*this).leave(x);
    3583             :   }
    3584             : 
    3585             :   void apply(const state_formulas::variable& x)
    3586             :   {
    3587             :     static_cast<Derived&>(*this).enter(x);
    3588             :     // skip
    3589             :     static_cast<Derived&>(*this).leave(x);
    3590             :   }
    3591             : 
    3592             :   void apply(const state_formulas::nu& x)
    3593             :   {
    3594             :     static_cast<Derived&>(*this).enter(x);
    3595             :     static_cast<Derived&>(*this).apply(x.operand());
    3596             :     static_cast<Derived&>(*this).leave(x);
    3597             :   }
    3598             : 
    3599             :   void apply(const state_formulas::mu& x)
    3600             :   {
    3601             :     static_cast<Derived&>(*this).enter(x);
    3602             :     static_cast<Derived&>(*this).apply(x.operand());
    3603             :     static_cast<Derived&>(*this).leave(x);
    3604             :   }
    3605             : 
    3606             :   void apply(const state_formulas::state_formula_specification& x)
    3607             :   {
    3608             :     static_cast<Derived&>(*this).enter(x);
    3609             :     static_cast<Derived&>(*this).apply(x.formula());
    3610             :     static_cast<Derived&>(*this).leave(x);
    3611             :   }
    3612             : 
    3613             :   void apply(const state_formulas::state_formula& x)
    3614             :   {
    3615             :     static_cast<Derived&>(*this).enter(x);
    3616             :     if (data::is_data_expression(x))
    3617             :     {
    3618             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    3619             :     }
    3620             :     else if (data::is_untyped_data_parameter(x))
    3621             :     {
    3622             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    3623             :     }
    3624             :     else if (state_formulas::is_true(x))
    3625             :     {
    3626             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    3627             :     }
    3628             :     else if (state_formulas::is_false(x))
    3629             :     {
    3630             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    3631             :     }
    3632             :     else if (state_formulas::is_not(x))
    3633             :     {
    3634             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    3635             :     }
    3636             :     else if (state_formulas::is_minus(x))
    3637             :     {
    3638             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
    3639             :     }
    3640             :     else if (state_formulas::is_and(x))
    3641             :     {
    3642             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    3643             :     }
    3644             :     else if (state_formulas::is_or(x))
    3645             :     {
    3646             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    3647             :     }
    3648             :     else if (state_formulas::is_imp(x))
    3649             :     {
    3650             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    3651             :     }
    3652             :     else if (state_formulas::is_plus(x))
    3653             :     {
    3654             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
    3655             :     }
    3656             :     else if (state_formulas::is_const_multiply(x))
    3657             :     {
    3658             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
    3659             :     }
    3660             :     else if (state_formulas::is_const_multiply_alt(x))
    3661             :     {
    3662             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
    3663             :     }
    3664             :     else if (state_formulas::is_forall(x))
    3665             :     {
    3666             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    3667             :     }
    3668             :     else if (state_formulas::is_exists(x))
    3669             :     {
    3670             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    3671             :     }
    3672             :     else if (state_formulas::is_infimum(x))
    3673             :     {
    3674             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
    3675             :     }
    3676             :     else if (state_formulas::is_supremum(x))
    3677             :     {
    3678             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
    3679             :     }
    3680             :     else if (state_formulas::is_sum(x))
    3681             :     {
    3682             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
    3683             :     }
    3684             :     else if (state_formulas::is_must(x))
    3685             :     {
    3686             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    3687             :     }
    3688             :     else if (state_formulas::is_may(x))
    3689             :     {
    3690             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    3691             :     }
    3692             :     else if (state_formulas::is_yaled(x))
    3693             :     {
    3694             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    3695             :     }
    3696             :     else if (state_formulas::is_yaled_timed(x))
    3697             :     {
    3698             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    3699             :     }
    3700             :     else if (state_formulas::is_delay(x))
    3701             :     {
    3702             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    3703             :     }
    3704             :     else if (state_formulas::is_delay_timed(x))
    3705             :     {
    3706             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    3707             :     }
    3708             :     else if (state_formulas::is_variable(x))
    3709             :     {
    3710             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    3711             :     }
    3712             :     else if (state_formulas::is_nu(x))
    3713             :     {
    3714             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    3715             :     }
    3716             :     else if (state_formulas::is_mu(x))
    3717             :     {
    3718             :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    3719             :     }
    3720             :     static_cast<Derived&>(*this).leave(x);
    3721             :   }
    3722             : 
    3723             : };
    3724             : 
    3725             : /// \\brief Traverser class
    3726             : template <typename Derived>
    3727             : struct regular_formula_traverser: public add_traverser_regular_formula_expressions<regular_formulas::regular_formula_traverser, Derived>
    3728             : {
    3729             : };
    3730             : //--- end generated state_formulas::add_traverser_regular_formula_expressions code ---//
    3731             : 
    3732             : //--- start generated state_formulas::add_traverser_action_labels code ---//
    3733             : template <template <class> class Traverser, class Derived>
    3734             : struct add_traverser_action_labels: public Traverser<Derived>
    3735             : {
    3736             :   typedef Traverser<Derived> super;
    3737             :   using super::enter;
    3738             :   using super::leave;
    3739             :   using super::apply;
    3740             : 
    3741           0 :   void apply(const state_formulas::true_& x)
    3742             :   {
    3743           0 :     static_cast<Derived&>(*this).enter(x);
    3744             :     // skip
    3745           0 :     static_cast<Derived&>(*this).leave(x);
    3746           0 :   }
    3747             : 
    3748           0 :   void apply(const state_formulas::false_& x)
    3749             :   {
    3750           0 :     static_cast<Derived&>(*this).enter(x);
    3751             :     // skip
    3752           0 :     static_cast<Derived&>(*this).leave(x);
    3753           0 :   }
    3754             : 
    3755           0 :   void apply(const state_formulas::not_& x)
    3756             :   {
    3757           0 :     static_cast<Derived&>(*this).enter(x);
    3758           0 :     static_cast<Derived&>(*this).apply(x.operand());
    3759           0 :     static_cast<Derived&>(*this).leave(x);
    3760           0 :   }
    3761             : 
    3762           0 :   void apply(const state_formulas::minus& x)
    3763             :   {
    3764           0 :     static_cast<Derived&>(*this).enter(x);
    3765           0 :     static_cast<Derived&>(*this).apply(x.operand());
    3766           0 :     static_cast<Derived&>(*this).leave(x);
    3767           0 :   }
    3768             : 
    3769           0 :   void apply(const state_formulas::and_& x)
    3770             :   {
    3771           0 :     static_cast<Derived&>(*this).enter(x);
    3772           0 :     static_cast<Derived&>(*this).apply(x.left());
    3773           0 :     static_cast<Derived&>(*this).apply(x.right());
    3774           0 :     static_cast<Derived&>(*this).leave(x);
    3775           0 :   }
    3776             : 
    3777           0 :   void apply(const state_formulas::or_& x)
    3778             :   {
    3779           0 :     static_cast<Derived&>(*this).enter(x);
    3780           0 :     static_cast<Derived&>(*this).apply(x.left());
    3781           0 :     static_cast<Derived&>(*this).apply(x.right());
    3782           0 :     static_cast<Derived&>(*this).leave(x);
    3783           0 :   }
    3784             : 
    3785           0 :   void apply(const state_formulas::imp& x)
    3786             :   {
    3787           0 :     static_cast<Derived&>(*this).enter(x);
    3788           0 :     static_cast<Derived&>(*this).apply(x.left());
    3789           0 :     static_cast<Derived&>(*this).apply(x.right());
    3790           0 :     static_cast<Derived&>(*this).leave(x);
    3791           0 :   }
    3792             : 
    3793           0 :   void apply(const state_formulas::plus& x)
    3794             :   {
    3795           0 :     static_cast<Derived&>(*this).enter(x);
    3796           0 :     static_cast<Derived&>(*this).apply(x.left());
    3797           0 :     static_cast<Derived&>(*this).apply(x.right());
    3798           0 :     static_cast<Derived&>(*this).leave(x);
    3799           0 :   }
    3800             : 
    3801           0 :   void apply(const state_formulas::const_multiply& x)
    3802             :   {
    3803           0 :     static_cast<Derived&>(*this).enter(x);
    3804           0 :     static_cast<Derived&>(*this).apply(x.right());
    3805           0 :     static_cast<Derived&>(*this).leave(x);
    3806           0 :   }
    3807             : 
    3808           0 :   void apply(const state_formulas::const_multiply_alt& x)
    3809             :   {
    3810           0 :     static_cast<Derived&>(*this).enter(x);
    3811           0 :     static_cast<Derived&>(*this).apply(x.left());
    3812           0 :     static_cast<Derived&>(*this).leave(x);
    3813           0 :   }
    3814             : 
    3815           0 :   void apply(const state_formulas::forall& x)
    3816             :   {
    3817           0 :     static_cast<Derived&>(*this).enter(x);
    3818           0 :     static_cast<Derived&>(*this).apply(x.body());
    3819           0 :     static_cast<Derived&>(*this).leave(x);
    3820           0 :   }
    3821             : 
    3822           0 :   void apply(const state_formulas::exists& x)
    3823             :   {
    3824           0 :     static_cast<Derived&>(*this).enter(x);
    3825           0 :     static_cast<Derived&>(*this).apply(x.body());
    3826           0 :     static_cast<Derived&>(*this).leave(x);
    3827           0 :   }
    3828             : 
    3829           0 :   void apply(const state_formulas::infimum& x)
    3830             :   {
    3831           0 :     static_cast<Derived&>(*this).enter(x);
    3832           0 :     static_cast<Derived&>(*this).apply(x.body());
    3833           0 :     static_cast<Derived&>(*this).leave(x);
    3834           0 :   }
    3835             : 
    3836           0 :   void apply(const state_formulas::supremum& x)
    3837             :   {
    3838           0 :     static_cast<Derived&>(*this).enter(x);
    3839           0 :     static_cast<Derived&>(*this).apply(x.body());
    3840           0 :     static_cast<Derived&>(*this).leave(x);
    3841           0 :   }
    3842             : 
    3843           0 :   void apply(const state_formulas::sum& x)
    3844             :   {
    3845           0 :     static_cast<Derived&>(*this).enter(x);
    3846           0 :     static_cast<Derived&>(*this).apply(x.body());
    3847           0 :     static_cast<Derived&>(*this).leave(x);
    3848           0 :   }
    3849             : 
    3850           0 :   void apply(const state_formulas::must& x)
    3851             :   {
    3852           0 :     static_cast<Derived&>(*this).enter(x);
    3853           0 :     static_cast<Derived&>(*this).apply(x.formula());
    3854           0 :     static_cast<Derived&>(*this).apply(x.operand());
    3855           0 :     static_cast<Derived&>(*this).leave(x);
    3856           0 :   }
    3857             : 
    3858           0 :   void apply(const state_formulas::may& x)
    3859             :   {
    3860           0 :     static_cast<Derived&>(*this).enter(x);
    3861           0 :     static_cast<Derived&>(*this).apply(x.formula());
    3862           0 :     static_cast<Derived&>(*this).apply(x.operand());
    3863           0 :     static_cast<Derived&>(*this).leave(x);
    3864           0 :   }
    3865             : 
    3866           0 :   void apply(const state_formulas::yaled& x)
    3867             :   {
    3868           0 :     static_cast<Derived&>(*this).enter(x);
    3869             :     // skip
    3870           0 :     static_cast<Derived&>(*this).leave(x);
    3871           0 :   }
    3872             : 
    3873           0 :   void apply(const state_formulas::yaled_timed& x)
    3874             :   {
    3875           0 :     static_cast<Derived&>(*this).enter(x);
    3876             :     // skip
    3877           0 :     static_cast<Derived&>(*this).leave(x);
    3878           0 :   }
    3879             : 
    3880           0 :   void apply(const state_formulas::delay& x)
    3881             :   {
    3882           0 :     static_cast<Derived&>(*this).enter(x);
    3883             :     // skip
    3884           0 :     static_cast<Derived&>(*this).leave(x);
    3885           0 :   }
    3886             : 
    3887           0 :   void apply(const state_formulas::delay_timed& x)
    3888             :   {
    3889           0 :     static_cast<Derived&>(*this).enter(x);
    3890             :     // skip
    3891           0 :     static_cast<Derived&>(*this).leave(x);
    3892           0 :   }
    3893             : 
    3894           0 :   void apply(const state_formulas::variable& x)
    3895             :   {
    3896           0 :     static_cast<Derived&>(*this).enter(x);
    3897             :     // skip
    3898           0 :     static_cast<Derived&>(*this).leave(x);
    3899           0 :   }
    3900             : 
    3901           0 :   void apply(const state_formulas::nu& x)
    3902             :   {
    3903           0 :     static_cast<Derived&>(*this).enter(x);
    3904           0 :     static_cast<Derived&>(*this).apply(x.operand());
    3905           0 :     static_cast<Derived&>(*this).leave(x);
    3906           0 :   }
    3907             : 
    3908           0 :   void apply(const state_formulas::mu& x)
    3909             :   {
    3910           0 :     static_cast<Derived&>(*this).enter(x);
    3911           0 :     static_cast<Derived&>(*this).apply(x.operand());
    3912           0 :     static_cast<Derived&>(*this).leave(x);
    3913           0 :   }
    3914             : 
    3915             :   void apply(const state_formulas::state_formula_specification& x)
    3916             :   {
    3917             :     static_cast<Derived&>(*this).enter(x);
    3918             :     static_cast<Derived&>(*this).apply(x.action_labels());
    3919             :     static_cast<Derived&>(*this).apply(x.formula());
    3920             :     static_cast<Derived&>(*this).leave(x);
    3921             :   }
    3922             : 
    3923           0 :   void apply(const state_formulas::state_formula& x)
    3924             :   {
    3925           0 :     static_cast<Derived&>(*this).enter(x);
    3926           0 :     if (data::is_data_expression(x))
    3927             :     {
    3928           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
    3929             :     }
    3930           0 :     else if (data::is_untyped_data_parameter(x))
    3931             :     {
    3932           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
    3933             :     }
    3934           0 :     else if (state_formulas::is_true(x))
    3935             :     {
    3936           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
    3937             :     }
    3938           0 :     else if (state_formulas::is_false(x))
    3939             :     {
    3940           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
    3941             :     }
    3942           0 :     else if (state_formulas::is_not(x))
    3943             :     {
    3944           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
    3945             :     }
    3946           0 :     else if (state_formulas::is_minus(x))
    3947             :     {
    3948           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
    3949             :     }
    3950           0 :     else if (state_formulas::is_and(x))
    3951             :     {
    3952           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
    3953             :     }
    3954           0 :     else if (state_formulas::is_or(x))
    3955             :     {
    3956           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
    3957             :     }
    3958           0 :     else if (state_formulas::is_imp(x))
    3959             :     {
    3960           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
    3961             :     }
    3962           0 :     else if (state_formulas::is_plus(x))
    3963             :     {
    3964           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
    3965             :     }
    3966           0 :     else if (state_formulas::is_const_multiply(x))
    3967             :     {
    3968           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
    3969             :     }
    3970           0 :     else if (state_formulas::is_const_multiply_alt(x))
    3971             :     {
    3972           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
    3973             :     }
    3974           0 :     else if (state_formulas::is_forall(x))
    3975             :     {
    3976           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
    3977             :     }
    3978           0 :     else if (state_formulas::is_exists(x))
    3979             :     {
    3980           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
    3981             :     }
    3982           0 :     else if (state_formulas::is_infimum(x))
    3983             :     {
    3984           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
    3985             :     }
    3986           0 :     else if (state_formulas::is_supremum(x))
    3987             :     {
    3988           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
    3989             :     }
    3990           0 :     else if (state_formulas::is_sum(x))
    3991             :     {
    3992           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
    3993             :     }
    3994           0 :     else if (state_formulas::is_must(x))
    3995             :     {
    3996           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
    3997             :     }
    3998           0 :     else if (state_formulas::is_may(x))
    3999             :     {
    4000           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
    4001             :     }
    4002           0 :     else if (state_formulas::is_yaled(x))
    4003             :     {
    4004           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
    4005             :     }
    4006           0 :     else if (state_formulas::is_yaled_timed(x))
    4007             :     {
    4008           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
    4009             :     }
    4010           0 :     else if (state_formulas::is_delay(x))
    4011             :     {
    4012           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
    4013             :     }
    4014           0 :     else if (state_formulas::is_delay_timed(x))
    4015             :     {
    4016           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
    4017             :     }
    4018           0 :     else if (state_formulas::is_variable(x))
    4019             :     {
    4020           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
    4021             :     }
    4022           0 :     else if (state_formulas::is_nu(x))
    4023             :     {
    4024           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
    4025             :     }
    4026           0 :     else if (state_formulas::is_mu(x))
    4027             :     {
    4028           0 :       static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
    4029             :     }
    4030           0 :     static_cast<Derived&>(*this).leave(x);
    4031           0 :   }
    4032             : 
    4033             : };
    4034             : 
    4035             : /// \\brief Traverser class
    4036             : template <typename Derived>
    4037             : struct action_label_traverser: public add_traverser_action_labels<regular_formulas::action_label_traverser, Derived>
    4038             : {
    4039             : };
    4040             : //--- end generated state_formulas::add_traverser_action_labels code ---//
    4041             : 
    4042             : } // namespace state_formulas
    4043             : 
    4044             : } // namespace mcrl2
    4045             : 
    4046             : #endif // MCRL2_MODAL_FORMULA_TRAVERSER_H