mCRL2
Loading...
Searching...
No Matches
specification_property_map.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_LPS_DETAIL_SPECIFICATION_PROPERTY_MAP_H
13#define MCRL2_LPS_DETAIL_SPECIFICATION_PROPERTY_MAP_H
14
17#include <boost/algorithm/string/split.hpp>
18#include <boost/algorithm/string/trim.hpp>
19
20namespace mcrl2
21{
22
23namespace lps
24{
25
26namespace detail
27{
28
51template <typename Specification = specification>
52class specification_property_map: protected mcrl2::data::detail::data_property_map<specification_property_map<Specification> >
53{
54 protected:
55
56 // Allow base class access to protected functions
58
60
61 using super::m_data;
62 using super::names;
63 using super::print;
67
68 std::string print(const process::action_label& l) const
69 {
70 return core::pp(l.name());
71 }
72
73 std::string print(const process::action& a) const
74 {
75 return process::pp(a);
76 }
77
78 std::string print(const deadlock& x) const
79 {
80 return lps::pp(x);
81 }
82
83 std::string print(const multi_action& x) const
84 {
85 return lps::pp(x);
86 }
87
88 std::string print(const std::set<std::multiset<process::action_label> >& v) const
89 {
90 std::set<std::string> elements;
91 for (const auto& s: v)
92 {
93 elements.insert(print(s));
94 }
95 return utilities::string_join(elements, "; ");
96 }
97
98 // super class compare functions
99 using super::compare;
100
101 std::string compare_property(std::string property, std::string x, std::string y) const
102 {
103 if (property == "summand_count")
104 {
105 return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
106 }
107 else if (property == "tau_summand_count")
108 {
109 return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
110 }
111 else if (property == "delta_summand_count")
112 {
113 return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
114 }
115 else if (property == "declared_free_variables")
116 {
117 return compare(property, parse_set_string(x), parse_set_string(y));
118 }
119 else if (property == "declared_free_variable_names")
120 {
121 return compare(property, parse_set_string(x), parse_set_string(y));
122 }
123 else if (property == "declared_free_variable_count")
124 {
125 return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
126 }
127 else if (property == "used_free_variables")
128 {
129 return compare(property, parse_set_string(x), parse_set_string(y));
130 }
131 else if (property == "used_free_variable_names")
132 {
133 return compare(property, parse_set_string(x), parse_set_string(y));
134 }
135 else if (property == "used_free_variable_count")
136 {
137 return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
138 }
139 else if (property == "process_parameters")
140 {
141 return compare(property, parse_set_string(x), parse_set_string(y));
142 }
143 else if (property == "process_parameter_names")
144 {
145 return compare(property, parse_set_string(x), parse_set_string(y));
146 }
147 else if (property == "process_parameter_count")
148 {
149 return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
150 }
151 else if (property == "declared_action_labels")
152 {
153 return compare(property, parse_set_string(x), parse_set_string(y));
154 }
155 else if (property == "declared_action_label_count")
156 {
157 return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
158 }
159 else if (property == "used_action_labels")
160 {
161 return compare(property, parse_set_string(x), parse_set_string(y));
162 }
163 else if (property == "used_action_label_count")
164 {
165 return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
166 }
167 else if (property == "used_multi_actions")
168 {
170 }
171 else if (property == "used_multi_action_count")
172 {
173 return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
174 }
175 return "ERROR: unknown property " + property + " encountered!";
176 }
177
178 //--------------------------------------------//
179 // compute functions
180 //--------------------------------------------//
181 // TODO: the compute functions can be combined for efficiency
182 std::set<std::multiset<process::action_label> > compute_used_multi_actions(const Specification& spec) const
183 {
184 std::set<std::multiset<process::action_label> > result;
185 for (auto i = spec.process().action_summands().begin(); i != spec.process().action_summands().end(); ++i)
186 {
187 std::multiset<process::action_label> labels;
188 for (const process::action& a: i->multi_action().actions())
189 {
190 labels.insert(a.label());
191 }
192 result.insert(labels);
193 }
194 return result;
195 }
196
197 std::set<process::action_label> compute_used_action_labels(const Specification& spec) const
198 {
199 std::set<process::action_label> result;
200 for (auto i = spec.process().action_summands().begin(); i != spec.process().action_summands().end(); ++i)
201 {
202 for (const process::action& a: i->multi_action().actions())
203 {
204 result.insert(a.label());
205 }
206 }
207 return result;
208 }
209
210 std::size_t compute_tau_summand_count(const Specification& spec) const
211 {
212 std::size_t result = 0;
213 auto const& summands = spec.process().action_summands();
214 for (auto i = summands.begin(); i != summands.end(); ++i)
215 {
216 if (i->is_tau())
217 {
218 result++;
219 }
220 }
221 return result;
222 }
223
224 std::set<data::variable> compute_used_free_variables(const Specification& spec) const
225 {
226 return lps::find_free_variables(spec.process());
227 }
228
229 public:
232 specification_property_map(const std::string& text)
233 : super(text)
234 {}
235
238 specification_property_map(const Specification& spec)
239 {
240 std::size_t summand_count = spec.process().summand_count();
241 std::size_t action_summand_count = spec.process().action_summands().size();
242 std::size_t tau_summand_count = compute_tau_summand_count(spec);
243 std::size_t delta_summand_count = spec.process().deadlock_summands().size();
244 const std::set<data::variable>& declared_free_variables = spec.global_variables();
245 std::set<data::variable> used_free_variables = compute_used_free_variables(spec);
246 auto const& params = spec.process().process_parameters();
247 std::set<data::variable> process_parameters(params.begin(), params.end());
248 auto const& action_labels = spec.action_labels();
249 std::set<process::action_label> declared_action_labels(action_labels.begin(),action_labels.end());
250 std::set<process::action_label> used_action_labels = compute_used_action_labels(spec);
251 auto used_multi_actions = compute_used_multi_actions(spec);
252
253 m_data["summand_count" ] = print(summand_count);
254 m_data["action_summand_count" ] = print(action_summand_count);
255 m_data["tau_summand_count" ] = print(tau_summand_count);
256 m_data["delta_summand_count" ] = print(delta_summand_count);
257 m_data["declared_free_variables" ] = print(declared_free_variables, false);
258 m_data["declared_free_variable_names"] = print(names(declared_free_variables), false);
259 m_data["declared_free_variable_count"] = print(declared_free_variables.size());
260 m_data["used_free_variables" ] = print(used_free_variables, false);
261 m_data["used_free_variable_names" ] = print(names(used_free_variables), false);
262 m_data["used_free_variable_count" ] = print(used_free_variables.size());
263 m_data["process_parameters" ] = print(process_parameters, false);
264 m_data["process_parameter_names" ] = print(names(process_parameters), false);
265 m_data["process_parameter_count" ] = print(process_parameters.size());
266 m_data["declared_action_labels" ] = print(declared_action_labels, false);
267 m_data["declared_action_label_count" ] = print(declared_action_labels.size());
268 m_data["used_action_labels" ] = print(used_action_labels, false);
269 m_data["used_action_label_count" ] = print(used_action_labels.size());
270 m_data["used_multi_actions" ] = print(used_multi_actions);
271 m_data["used_multi_action_count" ] = print(used_multi_actions.size());
272 }
273
274 using super::to_string;
275 using super::data;
276 using super::operator[];
277
279 {
280 return super::compare(other);
281 }
282
284 std::string info() const
285 {
286 std::ostringstream out;
287 out << "Number of action summands : " << (*this)["action_summand_count" ] << "\n";
288 out << "Number of deadlock/delta summands : " << (*this)["delta_summand_count" ] << "\n";
289 out << "Number of tau-summands : " << (*this)["tau_summand_count" ] << "\n";
290 out << "Number of declared global variables : " << (*this)["declared_free_variable_count"] << "\n";
291 out << "Number of process parameters : " << (*this)["process_parameter_count" ] << "\n";
292 out << "Number of declared action labels : " << (*this)["declared_action_label_count" ] << "\n";
293 out << "Number of used actions : " << (*this)["used_action_label_count" ] << "\n";
294 out << "Number of used multi-actions : " << (*this)["used_multi_action_count" ] << "\n";
295 return out.str();
296 }
297};
298
299} // namespace detail
300
301} // namespace lps
302
303} // namespace mcrl2
304
305#endif // MCRL2_LPS_DETAIL_SPECIFICATION_PROPERTY_MAP_H
Base class for storing properties of mCRL2 types. Properties are (key, value) pairs stored as strings...
unsigned int parse_unsigned_int(std::string const &text) const
const std::map< std::string, std::string > & data() const
Returns the stored properties.
std::set< core::identifier_string > names(const Container &v) const
Collects the names of the elements of the container. The name of element x is retrieved by x....
std::string compare(const std::string &property, unsigned int x, unsigned int y) const
Compares two integers, and returns a message if they are different. If if they are equal the empty st...
std::map< std::string, std::string > m_data
Contains a normalized string representation of the properties.
std::string print(std::size_t n) const
std::set< std::multiset< std::string > > parse_set_multiset_string(std::string const &text) const
std::set< std::string > parse_set_string(std::string const &text) const
std::string to_string() const
Returns a string representation of the properties.
Represents a deadlock.
Definition deadlock.h:26
Stores the following properties of a linear process specification:
std::string compare(const specification_property_map< Specification > &other) const
unsigned int parse_unsigned_int(std::string const &text) const
std::set< core::identifier_string > names(const Container &v) const
Collects the names of the elements of the container. The name of element x is retrieved by x....
specification_property_map(const Specification &spec)
Constructor Initializes the specification_property_map with a linear process specification.
std::map< std::string, std::string > m_data
Contains a normalized string representation of the properties.
std::string compare_property(std::string property, std::string x, std::string y) const
data::detail::data_property_map< specification_property_map > super
std::string print(const process::action &a) const
std::string print(const multi_action &x) const
std::set< std::multiset< std::string > > parse_set_multiset_string(std::string const &text) const
std::set< std::string > parse_set_string(std::string const &text) const
std::string print(const std::set< std::multiset< process::action_label > > &v) const
std::set< std::multiset< process::action_label > > compute_used_multi_actions(const Specification &spec) const
specification_property_map(const std::string &text)
Constructor. The strings may appear in a random order, and not all of them need to be present.
std::string info() const
Returns a textual overview of some properties of an LPS.
std::size_t compute_tau_summand_count(const Specification &spec) const
std::string print(const process::action_label &l) const
std::set< data::variable > compute_used_free_variables(const Specification &spec) const
std::set< process::action_label > compute_used_action_labels(const Specification &spec) const
\brief A timed multi-action
\brief An action label
const core::identifier_string & name() const
A property map containing properties of an LPS specification.
std::string pp(const identifier_string &x)
Definition core.cpp:26
std::string pp(const action_summand &x)
Definition lps.cpp:26
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:54
std::string pp(const action_label &x)
Definition process.cpp:36
std::string string_join(const Container &c, const std::string &separator)
Joins a sequence of strings. This is a replacement for boost::algorithm::join, since it gives stack o...
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
The class specification.