state_formula_rename.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_MODAL_FORMULA_STATE_FORMULA_RENAME_H
#define MCRL2_MODAL_FORMULA_STATE_FORMULA_RENAME_H
 
#include "mcrl2/modal_formula/replace.h"
 
namespace mcrl2
{
 
namespace state_formulas
{
 
template <typename IdentifierGenerator>
struct state_formula_predicate_variable_rename_builder: public state_formulas::state_formula_builder<state_formula_predicate_variable_rename_builder<IdentifierGenerator> >
{
  typedef state_formulas::state_formula_builder<state_formula_predicate_variable_rename_builder<IdentifierGenerator> > super;
  using super::enter;
  using super::leave;
  using super::update;
  using super::apply;
 
  IdentifierGenerator& generator;
 
  std::deque<std::pair<core::identifier_string, core::identifier_string> > replacements;
 
  state_formula_predicate_variable_rename_builder(IdentifierGenerator& generator)
    : generator(generator)
  {}
 
  core::identifier_string push(const core::identifier_string& n)
  {
    core::identifier_string new_name = generator(n);
    replacements.push_front(std::make_pair(n, new_name));
    return new_name;
  }
 
  void pop()
  {
    replacements.pop_front();
  }
 
  template <class T>
  void apply(T& result, const variable& x)
  {
    core::identifier_string new_name = x.name();
    for (std::deque<std::pair<core::identifier_string, core::identifier_string> >::iterator i = replacements.begin(); i != replacements.end(); ++i)
    {
      if (i->first == x.name())
      {
        new_name = i->second;
        break;
      }
    }
    result = variable(new_name, x.arguments());
  }
 
  template <class T>
  void apply(T& result, const mu& x)
  {
    core::identifier_string new_name = push(x.name());
    state_formula new_formula;
    apply(new_formula, x.operand());
    pop();
    make_mu(result, new_name, x.assignments(), new_formula);
  }
 
  template <class T>
  void apply(T& result, const nu& x)
  {
    core::identifier_string new_name = push(x.name());
    state_formula new_formula;
    apply(new_formula, x.operand());
    pop();
    make_nu(result, new_name, x.assignments(), new_formula);
  }
};
 
template <typename IdentifierGenerator>
state_formula_predicate_variable_rename_builder<IdentifierGenerator> make_state_formula_predicate_variable_rename_builder(IdentifierGenerator& generator)
{
  return state_formula_predicate_variable_rename_builder<IdentifierGenerator>(generator);
}
 
template <typename IdentifierGenerator>
state_formula rename_predicate_variables(const state_formula& f, IdentifierGenerator& generator)
{
  state_formula result;
  make_state_formula_predicate_variable_rename_builder(generator).apply(result, f);
  return result;
}
 
struct state_formula_variable_rename_builder: public state_formulas::sort_expression_builder<state_formula_variable_rename_builder>
{
  typedef state_formulas::sort_expression_builder<state_formula_variable_rename_builder> super;
 
  using super::enter;
  using super::leave;
  using super::update;
  using super::apply;
 
  const std::set<core::identifier_string>& forbidden_identifiers;
 
  std::map<core::identifier_string, core::identifier_string> generated_identifiers;
 
  utilities::number_postfix_generator generator;
 
  core::identifier_string create_name(const core::identifier_string& x)
  {
    std::map<core::identifier_string, core::identifier_string>::iterator i = generated_identifiers.find(x);
    if (i != generated_identifiers.end())
    {
      return i->second;
    }
    std::string name = generator(std::string(x));
    generated_identifiers[x] = core::identifier_string(name);
    return core::identifier_string(name);
  }
 
  state_formula_variable_rename_builder(const std::set<core::identifier_string>& forbidden_identifiers_)
    : forbidden_identifiers(forbidden_identifiers_)
  {
    for (const core::identifier_string& id: forbidden_identifiers)
    {
      generator.add_identifier(std::string(id));
    }
  }
 
  // do not traverse sorts
  template <class T>
  void apply(T& result, const data::sort_expression& x)
  {
    result = x;
  }
 
  template <class T>
  void apply(T& result, const data::variable& x)
  {
    using utilities::detail::contains;
    if (!contains(forbidden_identifiers, x.name()))
    {
      result = x;
      return;
    }
    data::make_variable(result, create_name(x.name()), x.sort());
  }
};
 
inline
state_formula rename_variables(const state_formula& f, const std::set<core::identifier_string>& forbidden_identifiers)
{
  state_formula result;
  state_formula_variable_rename_builder(forbidden_identifiers).apply(result, f);
  return result;
}
 
} // namespace state_formulas
 
} // namespace mcrl2
 
#endif // MCRL2_MODAL_FORMULA_STATE_FORMULA_RENAME_H