Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/pbes/anonymize.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_ANONYMIZE_H
      13             : #define MCRL2_PBES_ANONYMIZE_H
      14             : 
      15             : #include "mcrl2/data/anonymize.h"
      16             : #include "mcrl2/pbes/builder.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : namespace detail {
      23             : 
      24             : template <typename Derived>
      25             : struct anonymize_builder: public add_sort_expressions<data::detail::anonymize_builder, Derived>
      26             : {
      27             :   typedef add_sort_expressions<data::detail::anonymize_builder, Derived> super;
      28             :   using super::enter;
      29             :   using super::leave;
      30             :   using super::update;
      31             :   using super::apply;
      32             :   using super::add_name;
      33             :   using super::derived;
      34             : 
      35             :   std::map<core::identifier_string, core::identifier_string> propositional_variable_name_substitution;
      36             : 
      37           0 :   void update(pbes& x)
      38             :   {
      39           0 :     super::update(x.data());
      40           0 :     super::update(x);
      41           0 :   }
      42             : 
      43           0 :   void enter(const propositional_variable& x)
      44             :   {
      45           0 :     add_name(x.name(), propositional_variable_name_substitution, "X");
      46           0 :   }
      47             : 
      48             :   template <class T>
      49           0 :   void apply(T& result, const propositional_variable& x)
      50             :   {
      51           0 :     derived().enter(x);
      52           0 :     data::variable_list parameters;
      53           0 :     derived().apply(parameters, x.parameters());
      54           0 :     make_propositional_variable(result,propositional_variable_name_substitution[x.name()], parameters);
      55           0 :     derived().leave(x);
      56           0 :   }
      57             : 
      58           0 :   void enter(const propositional_variable_instantiation& x)
      59             :   {
      60           0 :     add_name(x.name(), propositional_variable_name_substitution, "X");
      61           0 :   }
      62             : 
      63             :   template <class T>
      64           0 :   void apply(T& result, const propositional_variable_instantiation& x)
      65             :   {
      66           0 :     derived().enter(x);
      67           0 :     data::data_expression_list parameters;
      68           0 :     derived().apply(parameters, x.parameters());
      69           0 :     make_propositional_variable_instantiation(result, propositional_variable_name_substitution[x.name()], parameters);
      70           0 :     derived().leave(x);
      71           0 :   }
      72             : };
      73             : 
      74             : struct anonymize_builder_instance: public anonymize_builder<anonymize_builder_instance>
      75             : {
      76             : };
      77             : 
      78             : } // namespace detail
      79             : 
      80             : inline
      81           0 : void anonymize(pbes& pbesspec)
      82             : {
      83           0 :   detail::anonymize_builder_instance f;
      84           0 :   f.update(pbesspec);
      85           0 : }
      86             : 
      87             : } // namespace pbes_system
      88             : 
      89             : } // namespace mcrl2
      90             : 
      91             : #endif // MCRL2_PBES_ANONYMIZE_H