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/data/xyz_identifier_generator.h
10 : /// \brief Class that generates identifiers in the range X, Y, Z, X0, Y0, Z0, X1, ...
11 :
12 : #ifndef MCRL2_DATA_XYZ_IDENTIFIER_GENERATOR_H
13 : #define MCRL2_DATA_XYZ_IDENTIFIER_GENERATOR_H
14 :
15 : #include "mcrl2/data/set_identifier_generator.h"
16 :
17 : namespace mcrl2
18 : {
19 :
20 : namespace data
21 : {
22 :
23 : /// \brief Identifier generator that generates names from the range X, Y, Z, X0, Y0, Z0, X1, ...
24 : class xyz_identifier_generator: public multiset_identifier_generator
25 : {
26 : protected:
27 : /// \brief The index of the last generated identifier.
28 : int m_index;
29 :
30 : /// \brief The character of the last generated identifier.
31 : char m_char; // character of last generated identifier
32 :
33 : /// \brief Returns the next name in the range X, Y, Z, X0, Y0, Z0, X1, ...
34 : /// \return The next name in the range X, Y, Z, X0, Y0, Z0, X1, ...
35 309 : std::string next()
36 : {
37 309 : switch (m_char)
38 : {
39 112 : case 'X' :
40 : {
41 112 : m_char = 'Y';
42 112 : break;
43 : }
44 60 : case 'Y' :
45 : {
46 60 : m_char = 'Z';
47 60 : break;
48 : }
49 137 : case 'Z' :
50 : {
51 137 : m_char = 'X';
52 137 : m_index++;
53 137 : break;
54 : }
55 : }
56 618 : return m_index < 0 ? std::string(1, m_char) : m_char + std::to_string(m_index);
57 : }
58 :
59 : public:
60 : /// \brief Constructor.
61 138 : xyz_identifier_generator()
62 138 : : m_index(-2), m_char('Z')
63 138 : {}
64 :
65 : /// \brief Constructor.
66 : /// \param ids a set of identifiers to use as context
67 151 : xyz_identifier_generator(const std::set<core::identifier_string>& ids)
68 151 : : m_index(-2), m_char('Z')
69 : {
70 151 : add_identifiers(ids);
71 151 : }
72 :
73 : /// \brief Returns hint if it isn't in the context yet. Else the next available
74 : /// identifier in the range X, Y, Z, X0, Y0, Z0, X1, ... is returned.
75 : /// \param hint A string
76 : /// \param add_to_context If true, the generated identifier is added to the context,
77 : /// it is not added otherwise.
78 : /// \return A fresh identifier.
79 118 : core::identifier_string operator()(const std::string& hint, bool add_to_context = true)
80 : {
81 118 : core::identifier_string result(hint);
82 :
83 118 : if (m_identifiers.find(hint) != m_identifiers.end())
84 : {
85 105 : m_index = -2;
86 105 : m_char = 'Z';
87 : do
88 : {
89 309 : result = core::identifier_string(next());
90 : }
91 309 : while (m_identifiers.find(result) != m_identifiers.end());
92 : }
93 :
94 118 : if (add_to_context)
95 : {
96 118 : add_identifier(result);
97 : }
98 118 : return result;
99 0 : }
100 : };
101 :
102 : } // namespace data
103 :
104 : } // namespace mcrl2
105 :
106 : #endif // MCRL2_DATA_XYZ_IDENTIFIER_GENERATOR_H
|