xyz_identifier_generator.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_DATA_XYZ_IDENTIFIER_GENERATOR_H
#define MCRL2_DATA_XYZ_IDENTIFIER_GENERATOR_H
 
#include "mcrl2/data/set_identifier_generator.h"
 
namespace mcrl2
{
 
namespace data
{
 
class xyz_identifier_generator: public multiset_identifier_generator
{
  protected:
    int m_index;
 
    char m_char; // character of last generated identifier
 
    std::string next()
    {
      switch (m_char)
      {
        case 'X' :
        {
          m_char = 'Y';
          break;
        }
        case 'Y' :
        {
          m_char = 'Z';
          break;
        }
        case 'Z' :
        {
          m_char = 'X';
          m_index++;
          break;
        }
      }
      return m_index < 0 ? std::string(1, m_char) : m_char + std::to_string(m_index);
    }
 
  public:
    xyz_identifier_generator()
      : m_index(-2), m_char('Z')
    {}
 
   xyz_identifier_generator(const std::set<core::identifier_string>& ids)
      : m_index(-2), m_char('Z')
    {
      add_identifiers(ids);
    }
 
    core::identifier_string operator()(const std::string& hint, bool add_to_context = true)
    {
      core::identifier_string result(hint);
 
      if (m_identifiers.find(hint) != m_identifiers.end())
      {
        m_index = -2;
        m_char = 'Z';
        do
        {
          result = core::identifier_string(next());
        }
        while (m_identifiers.find(result) != m_identifiers.end());
      }
 
      if (add_to_context)
      {
        add_identifier(result);
      }
      return result;
    }
};
 
} // namespace data
 
} // namespace mcrl2
 
#endif // MCRL2_DATA_XYZ_IDENTIFIER_GENERATOR_H