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/lps/add_binding.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_ADD_BINDING_H
      13             : #define MCRL2_LPS_ADD_BINDING_H
      14             : 
      15             : #include "mcrl2/lps/stochastic_specification.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace lps
      21             : {
      22             : 
      23             : /// \brief Maintains a multiset of bound data variables during traversal
      24             : template <template <class> class Builder, class Derived>
      25             : struct add_data_variable_binding: public data::add_data_variable_binding<Builder, Derived>
      26             : {
      27             :   typedef data::add_data_variable_binding<Builder, Derived> super;
      28             :   using super::apply;
      29             :   using super::enter;
      30             :   using super::leave;
      31             :   using super::increase_bind_count;
      32             :   using super::decrease_bind_count;
      33             : 
      34         597 :   void enter(const action_summand& x)
      35             :   {
      36         597 :     increase_bind_count(x.summation_variables());
      37         597 :   }
      38             : 
      39         597 :   void leave(const action_summand& x)
      40             :   {
      41         597 :     decrease_bind_count(x.summation_variables());
      42         597 :   }
      43             : 
      44        2820 :   void enter(const stochastic_action_summand& x)
      45             :   {
      46        2820 :     increase_bind_count(x.summation_variables());
      47        2820 :     increase_bind_count(x.distribution().variables());
      48        2820 :   }
      49             : 
      50        2820 :   void leave(const stochastic_action_summand& x)
      51             :   {
      52        2820 :     decrease_bind_count(x.summation_variables());
      53        2820 :     decrease_bind_count(x.distribution().variables());
      54        2820 :   }
      55             : 
      56        1317 :   void enter(const deadlock_summand& x)
      57             :   {
      58        1317 :     increase_bind_count(x.summation_variables());
      59        1317 :   }
      60             : 
      61        1317 :   void leave(const deadlock_summand& x)
      62             :   {
      63        1317 :     decrease_bind_count(x.summation_variables());
      64        1317 :   }
      65             : 
      66         259 :   void enter(const linear_process& x)
      67             :   {
      68         259 :     increase_bind_count(x.process_parameters());
      69         259 :   }
      70             : 
      71         259 :   void leave(const linear_process& x)
      72             :   {
      73         259 :     decrease_bind_count(x.process_parameters());
      74         259 :   }
      75             : 
      76         648 :   void enter(const stochastic_linear_process& x)
      77             :   {
      78         648 :     increase_bind_count(x.process_parameters());
      79         648 :   }
      80             : 
      81         648 :   void leave(const stochastic_linear_process& x)
      82             :   {
      83         648 :     decrease_bind_count(x.process_parameters());
      84         648 :   }
      85             : 
      86          51 :   void enter(const specification& x)
      87             :   {
      88          51 :     increase_bind_count(x.global_variables());
      89          51 :   }
      90             : 
      91          51 :   void leave(const specification& x)
      92             :   {
      93          51 :     decrease_bind_count(x.global_variables());
      94          51 :   }
      95             : 
      96         617 :   void enter(const stochastic_specification& x)
      97             :   {
      98         617 :     increase_bind_count(x.global_variables());
      99         617 :   }
     100             : 
     101         617 :   void leave(const stochastic_specification& x)
     102             :   {
     103         617 :     decrease_bind_count(x.global_variables());
     104         617 :   }
     105             : 
     106         647 :   void enter(const stochastic_process_initializer& x)
     107             :   {
     108         647 :     increase_bind_count(x.distribution().variables());
     109         647 :   }
     110             : 
     111         647 :   void leave(const stochastic_process_initializer& x)
     112             :   {
     113         647 :     decrease_bind_count(x.distribution().variables());
     114         647 :   }
     115             : };
     116             : 
     117             : // TODO: get rid of this code duplication
     118             : // special handling for where clauses
     119             : template <template <class> class Builder, class Derived>
     120             : struct add_data_variable_traverser_binding: public add_data_variable_binding<Builder, Derived>
     121             : {
     122             :   typedef add_data_variable_binding<Builder, Derived> super;
     123             :   using super::enter;
     124             :   using super::leave;
     125             :   using super::apply;
     126             :   using super::bound_variables;
     127             :   using super::increase_bind_count;
     128             :   using super::decrease_bind_count;
     129             : 
     130           0 :   void apply(const data::where_clause& x)
     131             :   {
     132           0 :     static_cast<Derived&>(*this).apply(x.declarations());
     133           0 :     static_cast<Derived&>(*this).enter(x);
     134           0 :     static_cast<Derived&>(*this).apply(x.body());
     135           0 :     static_cast<Derived&>(*this).leave(x);
     136           0 :   }
     137             : };
     138             : 
     139             : // special handling for where clauses
     140             : template <template <class> class Builder, class Derived>
     141             : struct add_data_variable_builder_binding: public add_data_variable_binding<Builder, Derived>
     142             : {
     143             :   typedef add_data_variable_binding<Builder, Derived> super;
     144             :   using super::enter;
     145             :   using super::leave;
     146             :   using super::apply;
     147             :   using super::bound_variables;
     148             :   using super::increase_bind_count;
     149             :   using super::decrease_bind_count;
     150             : 
     151             :   template <class T>
     152             :   void apply(T& result,  data::where_clause& x)
     153             :   {
     154             :     data::assignment_expression declarations;
     155             :     static_cast<Derived&>(*this).apply(declarations, x.declarations());
     156             :     static_cast<Derived&>(*this).enter(x);
     157             :     data::make_where_clause(result, [&](data::data_expression& r){ static_cast<Derived&>(*this).apply(r, x.body()); }, declarations);
     158             :     static_cast<Derived&>(*this).leave(x);
     159             :   }
     160             : };
     161             : 
     162             : } // namespace lps
     163             : 
     164             : } // namespace mcrl2
     165             : 
     166             : #endif // MCRL2_LPS_ADD_BINDING_H