mCRL2
Loading...
Searching...
No Matches
action_label_string.h
Go to the documentation of this file.
1// Author(s): Jan Friso Groote
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
19#ifndef MCRL2_LTS_ACTION_LABEL_STRING_H
20#define MCRL2_LTS_ACTION_LABEL_STRING_H
21
22#include <set>
25
26namespace mcrl2
27{
28namespace lts
29{
30
36class action_label_string: public std::string
37{
38 public:
39
40 /* \brief Default constructor. The label will contain the default string.
41 */
43 {}
44
47
50
51 /* \brief A constructor, where the string s is taken to become the action label.
52 */
53 explicit action_label_string(const std::string& s):std::string(sort_multiactions(s))
54 {}
55
56 /* \brief An auxiliary function to hide actions. Makes a best-effort attempt at
57 parsing the string as an mCRL2 multi-action and hiding the actions
58 with a name in string_vector. If all actions are hidden, the resulting
59 action name will be "tau". The effects of this operation on action
60 labels that are not generated by the pretty printer are undefined. */
61 void hide_actions(const std::vector<std::string>& string_vector)
62 {
63 std::string ns; // New label after hiding.
64 std::string::iterator b = begin(); // Start position of current action.
65 std::string::iterator c = begin(); // End position of current action.
66 while (c != end())
67 {
68 std::string a;
69 // Parse action name into a
70 while (c != end() && *c != '(' && *c != '|')
71 {
72 a.append(1, *c++);
73 }
74 // Skip over parameters of a, if any
75 if (c != end() && *c == '(')
76 {
77 std::size_t nd = 0;
78 do
79 {
80 switch (*c++)
81 {
82 case '(': ++nd; break;
83 case ')': --nd; break;
84 }
85 }
86 while (nd > 0 && c != end());
87 }
88 // Add the appropriate action to the new action label string
89 if (std::find(string_vector.begin(), string_vector.end(), a) == string_vector.end())
90 {
91 if (!ns.empty())
92 {
93 ns.append("|");
94 }
95 ns.append(b, c);
96 }
97 // Skip the multi-action operator, if any
98 if (c != end() && *c == '|')
99 {
100 ++c;
101 }
102 // The start of the next action is pointed to by c.
103 b = c;
104 }
105 if (ns.empty())
106 {
107 assign(tau_action());
108 }
109 else
110 {
111 assign(ns);
112 }
113 }
114
115 /* \brief A comparison operator comparing the action_label_strings in the same way as strings.
116 */
117 bool operator<(const action_label_string& l) const
118 {
119 return std::string(*this)<std::string(l);
120 }
121
122 /* \brief The action label string that represents the internal action.
123 */
125 {
126 static action_label_string tau_action("tau");
127 return tau_action;
128 }
129
130 protected:
136 static std::string sort_multiactions(const std::string& s)
137 {
138 // Split this multiaction in actions a1(...) , a2(...), a3(...)
139 static std::multiset<std::string> split_actions; // Make a static variable to avoid this multiset being created often.
140 assert(split_actions.empty());
141 size_t nested_bracket_counter=0;
142 size_t start_of_current_action=0;
143 for(size_t i=0; i<s.size(); ++i)
144 {
145 const char c=s[i];
146 if (c==')')
147 { if (nested_bracket_counter==0)
148 {
149 throw mcrl2::runtime_error("The transition label is not a proper multiaction (1): " + s);
150 }
151 else
152 {
153 nested_bracket_counter--;
154 }
155 }
156 else if (c=='(')
157 {
158 nested_bracket_counter++;
159 }
160 else if (c=='|' && nested_bracket_counter==0)
161 {
162 split_actions.insert(s.substr(start_of_current_action,i-start_of_current_action));
163 start_of_current_action=i+1;
164 }
165 }
166 if (start_of_current_action==s.size()) // In this case the multiaction ends with a "|".
167 {
168 throw mcrl2::runtime_error("The transition label is not a proper multiaction (2): " + s);
169 }
170 if (split_actions.size()==0) // No actions were split off. No
171 {
172 // This is not a multiaction.
173 return s;
174 }
175 split_actions.insert(s.substr(start_of_current_action,s.size()-start_of_current_action));
176 std::string result;
177 for(const std::string& s: split_actions)
178 {
179 if (result.size()>0)
180 {
181 result.append("|");
182 }
183 result.append(s);
184 }
185 split_actions.clear();
186 return result;
187 }
188
189};
190
191/* \brief A pretty print operator on action labels, returning it as a string.
192*/
193inline std::string pp(const action_label_string& l)
194{
195 return l;
196}
197
198} // namespace lts
199} // namespace mcrl2
200
201namespace std
202{
203
205template<>
206struct hash< mcrl2::lts::action_label_string >
207{
208 std::size_t operator()(const mcrl2::lts::action_label_string& as) const
209 {
210 hash<std::string> hasher;
211 return hasher(as);
212 }
213};
214
215} // namespace std
216
217
218#endif
219
220
This class contains strings to be used as values for action labels in lts's.
static std::string sort_multiactions(const std::string &s)
Sort multiactions in a string.
void hide_actions(const std::vector< std::string > &string_vector)
action_label_string & operator=(const action_label_string &)=default
Copy assignment.
static const action_label_string & tau_action()
action_label_string(const std::string &s)
bool operator<(const action_label_string &l) const
action_label_string(const action_label_string &)=default
Copy constructor.
A class that contains a labelled transition system.
Definition lts.h:83
Standard exception class for reporting runtime errors.
Definition exception.h:27
Exception classes for use in libraries and tools.
std::string pp(const abstraction &x)
Definition data.cpp:39
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
std::size_t operator()(const mcrl2::lts::action_label_string &as) const
String manipulation functions.
#define hash(l, r, m)
Definition tree_set.cpp:23