12#ifndef MCRL2_LPS_DETAIL_SPECIFICATION_PROPERTY_MAP_H
13#define MCRL2_LPS_DETAIL_SPECIFICATION_PROPERTY_MAP_H
17#include <boost/algorithm/string/split.hpp>
18#include <boost/algorithm/string/trim.hpp>
51template <
typename Specification = specification>
88 std::string
print(
const std::set<std::multiset<process::action_label> >& v)
const
90 std::set<std::string> elements;
91 for (
const auto& s: v)
93 elements.insert(
print(s));
103 if (property ==
"summand_count")
107 else if (property ==
"tau_summand_count")
111 else if (property ==
"delta_summand_count")
115 else if (property ==
"declared_free_variables")
119 else if (property ==
"declared_free_variable_names")
123 else if (property ==
"declared_free_variable_count")
127 else if (property ==
"used_free_variables")
131 else if (property ==
"used_free_variable_names")
135 else if (property ==
"used_free_variable_count")
139 else if (property ==
"process_parameters")
143 else if (property ==
"process_parameter_names")
147 else if (property ==
"process_parameter_count")
151 else if (property ==
"declared_action_labels")
155 else if (property ==
"declared_action_label_count")
159 else if (property ==
"used_action_labels")
163 else if (property ==
"used_action_label_count")
167 else if (property ==
"used_multi_actions")
171 else if (property ==
"used_multi_action_count")
175 return "ERROR: unknown property " +
property +
" encountered!";
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)
187 std::multiset<process::action_label> labels;
190 labels.insert(a.label());
192 result.insert(labels);
199 std::set<process::action_label> result;
200 for (
auto i = spec.process().action_summands().begin(); i != spec.process().action_summands().end(); ++i)
204 result.insert(a.label());
212 std::size_t result = 0;
213 auto const& summands = spec.process().action_summands();
214 for (
auto i = summands.begin(); i != summands.end(); ++i)
240 std::size_t summand_count = spec.process().summand_count();
241 std::size_t action_summand_count = spec.process().action_summands().size();
243 std::size_t delta_summand_count = spec.process().deadlock_summands().size();
244 const std::set<data::variable>& declared_free_variables = spec.global_variables();
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());
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());
276 using super::operator[];
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";
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.
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....
std::string print(const deadlock &x) const
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
const core::identifier_string & name() const
A property map containing properties of an LPS specification.
std::string pp(const identifier_string &x)
std::string pp(const action_summand &x)
std::set< data::variable > find_free_variables(const lps::deadlock &x)
std::string pp(const action_label &x)
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...