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/state_formula_rename.h
      10             : /// \brief Add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_STATE_FORMULA_RENAME_H
      13             : #define MCRL2_MODAL_FORMULA_STATE_FORMULA_RENAME_H
      14             : 
      15             : #include "mcrl2/modal_formula/replace.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace state_formulas
      21             : {
      22             : 
      23             : /// Visitor that renames predicate variables using the specified identifier generator.
      24             : /// \post In the generated formula, all predicate variables have different names.
      25             : template <typename IdentifierGenerator>
      26             : struct state_formula_predicate_variable_rename_builder: public state_formulas::state_formula_builder<state_formula_predicate_variable_rename_builder<IdentifierGenerator> >
      27             : {
      28             :   typedef state_formulas::state_formula_builder<state_formula_predicate_variable_rename_builder<IdentifierGenerator> > super;
      29             :   using super::enter;
      30             :   using super::leave;
      31             :   using super::update;
      32             :   using super::apply;
      33             : 
      34             :   /// \brief An identifier generator
      35             :   IdentifierGenerator& generator;
      36             : 
      37             :   /// \brief A stack of replacements. It may contain pairs with identical values.
      38             :   std::deque<std::pair<core::identifier_string, core::identifier_string> > replacements;
      39             : 
      40             :   /// \brief Constructor
      41             :   /// \param generator A generator for fresh identifiers
      42         144 :   state_formula_predicate_variable_rename_builder(IdentifierGenerator& generator)
      43         144 :     : generator(generator)
      44         144 :   {}
      45             : 
      46             :   /// \brief Generates a new name for n, and adds a replacement to the replacement stack.
      47             :   /// \param n A
      48             :   /// \return The new name.
      49         120 :   core::identifier_string push(const core::identifier_string& n)
      50             :   {
      51         120 :     core::identifier_string new_name = generator(n);
      52         120 :     replacements.push_front(std::make_pair(n, new_name));
      53         120 :     return new_name;
      54           0 :   }
      55             : 
      56             :   /// \brief Removes the last added replacement.
      57         120 :   void pop()
      58             :   {
      59         120 :     replacements.pop_front();
      60         120 :   }
      61             : 
      62             :   /// \brief Visit var node.
      63             :   /// \param x A variable.
      64             :   /// \return The result of visiting the node
      65             :   template <class T>
      66         111 :   void apply(T& result, const variable& x)
      67             :   {
      68         111 :     core::identifier_string new_name = x.name();
      69         125 :     for (std::deque<std::pair<core::identifier_string, core::identifier_string> >::iterator i = replacements.begin(); i != replacements.end(); ++i)
      70             :     {
      71         125 :       if (i->first == x.name())
      72             :       {
      73         111 :         new_name = i->second;
      74         111 :         break;
      75             :       }
      76             :     }
      77         111 :     result = variable(new_name, x.arguments());
      78         111 :   }
      79             : 
      80             :   /// \brief Visit mu node.
      81             :   /// \param x The mu state variable.
      82             :   /// \return The result of visiting the node
      83             :   template <class T>
      84          69 :   void apply(T& result, const mu& x)
      85             :   {
      86          69 :     core::identifier_string new_name = push(x.name());
      87          69 :     state_formula new_formula;
      88          69 :     apply(new_formula, x.operand());
      89          69 :     pop();
      90          69 :     make_mu(result, new_name, x.assignments(), new_formula);
      91          69 :   }
      92             : 
      93             :   /// \brief Visit nu node.
      94             :   /// \param x The visited nu node.
      95             :   /// \return The result of visiting the node
      96             :   template <class T>
      97          51 :   void apply(T& result, const nu& x)
      98             :   {
      99          51 :     core::identifier_string new_name = push(x.name());
     100          51 :     state_formula new_formula;
     101          51 :     apply(new_formula, x.operand());
     102          51 :     pop();
     103          51 :     make_nu(result, new_name, x.assignments(), new_formula);
     104          51 :   }
     105             : };
     106             : 
     107             : /// \brief Utility function for creating a state_formula_predicate_variable_rename_builder.
     108             : /// \param generator A generator for fresh identifiers
     109             : /// \return a state_formula_predicate_variable_rename_builder
     110             : template <typename IdentifierGenerator>
     111         144 : state_formula_predicate_variable_rename_builder<IdentifierGenerator> make_state_formula_predicate_variable_rename_builder(IdentifierGenerator& generator)
     112             : {
     113         144 :   return state_formula_predicate_variable_rename_builder<IdentifierGenerator>(generator);
     114             : }
     115             : 
     116             : /// \brief Renames predicate variables of the formula f using the specified identifier generator.
     117             : /// \post predicate variables within the same scope have different names
     118             : /// \param f A modal formula
     119             : /// \param generator A generator for fresh identifiers
     120             : /// \return The rename result
     121             : template <typename IdentifierGenerator>
     122         144 : state_formula rename_predicate_variables(const state_formula& f, IdentifierGenerator& generator)
     123             : {
     124         144 :   state_formula result;
     125         144 :   make_state_formula_predicate_variable_rename_builder(generator).apply(result, f);
     126         144 :   return result;
     127           0 : }
     128             : 
     129             : /// Visitor that renames variables using the specified identifier generator. Also bound variables are renamed!
     130             : struct state_formula_variable_rename_builder: public state_formulas::sort_expression_builder<state_formula_variable_rename_builder>
     131             : {
     132             :   typedef state_formulas::sort_expression_builder<state_formula_variable_rename_builder> super;
     133             : 
     134             :   using super::enter;
     135             :   using super::leave;
     136             :   using super::update;
     137             :   using super::apply;
     138             : 
     139             :   /// \brief The set of identifiers that may not be used as a variable name.
     140             :   const std::set<core::identifier_string>& forbidden_identifiers;
     141             : 
     142             :   std::map<core::identifier_string, core::identifier_string> generated_identifiers;
     143             : 
     144             :   utilities::number_postfix_generator generator;
     145             : 
     146          86 :   core::identifier_string create_name(const core::identifier_string& x)
     147             :   {
     148          86 :     std::map<core::identifier_string, core::identifier_string>::iterator i = generated_identifiers.find(x);
     149          86 :     if (i != generated_identifiers.end())
     150             :     {
     151          54 :       return i->second;
     152             :     }
     153          32 :     std::string name = generator(std::string(x));
     154          32 :     generated_identifiers[x] = core::identifier_string(name);
     155          32 :     return core::identifier_string(name);
     156          32 :   }
     157             : 
     158             :   /// \brief Constructor
     159         142 :   state_formula_variable_rename_builder(const std::set<core::identifier_string>& forbidden_identifiers_)
     160         142 :     : forbidden_identifiers(forbidden_identifiers_)
     161             :   {
     162       10218 :     for (const core::identifier_string& id: forbidden_identifiers)
     163             :     {
     164       10076 :       generator.add_identifier(std::string(id));
     165             :     }
     166         142 :   }
     167             : 
     168             :   // do not traverse sorts
     169             :   template <class T>
     170         256 :   void apply(T& result, const data::sort_expression& x)
     171             :   {
     172         256 :     result = x;
     173         256 :   }
     174             : 
     175             :   template <class T>
     176          86 :   void apply(T& result, const data::variable& x)
     177             :   {
     178             :     using utilities::detail::contains;
     179          86 :     if (!contains(forbidden_identifiers, x.name()))
     180             :     {
     181           0 :       result = x;
     182           0 :       return;
     183             :     }
     184          86 :     data::make_variable(result, create_name(x.name()), x.sort());
     185             :   }
     186             : };
     187             : 
     188             : /// \brief Renames all data variables in the formula f such that the forbidden identifiers are not used.
     189             : /// \param f A modal formula.
     190             : /// \param forbidden_identifiers Set of identifiers strings, which are renamed. 
     191             : /// \return The rename result.
     192             : inline
     193         142 : state_formula rename_variables(const state_formula& f, const std::set<core::identifier_string>& forbidden_identifiers)
     194             : {
     195         142 :   state_formula result;
     196         142 :   state_formula_variable_rename_builder(forbidden_identifiers).apply(result, f);
     197         142 :   return result;
     198           0 : }
     199             : 
     200             : } // namespace state_formulas
     201             : 
     202             : } // namespace mcrl2
     203             : 
     204             : #endif // MCRL2_MODAL_FORMULA_STATE_FORMULA_RENAME_H