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/pbes/detail/pbes_property_map.h
10 : /// \brief A property map containing properties of an LPS specification.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_PBES_PROPERTY_MAP_H
13 : #define MCRL2_PBES_DETAIL_PBES_PROPERTY_MAP_H
14 :
15 : #include "mcrl2/data/detail/data_property_map.h"
16 : #include "mcrl2/pbes/pbes.h"
17 : #include <boost/algorithm/string/split.hpp>
18 : #include <boost/algorithm/string/trim.hpp>
19 :
20 : namespace mcrl2
21 : {
22 :
23 : namespace pbes_system
24 : {
25 :
26 : namespace detail
27 : {
28 :
29 : /// \brief Stores the following properties of a linear process specification:
30 : /// <table>
31 : /// <tr><th>property </th><th>description </th><th>format </th></tr>
32 : /// <tr><td>equation_count </td><td>The number of equation </td><td>NUMBER </td></tr>
33 : /// <tr><td>mu_equation_count </td><td>The number of mu equations </td><td>NUMBER </td></tr>
34 : /// <tr><td>nu_equation_count </td><td>The number of nu equations </td><td>NUMBER </td></tr>
35 : /// <tr><td>block_nesting_depth </td><td>The number of mu/nu alternations </td><td>NUMBER </td></tr>
36 : /// <tr><td>declared_free_variables </td><td>The declared free variables </td><td>PARAMLIST </td></tr>
37 : /// <tr><td>declared_free_variable_names</td><td>The names of the declared free variables</td><td>NAME, ..., NAME </td></tr>
38 : /// <tr><td>declared_variable_count </td><td>The number of declared free variables </td><td>NUMBER </td></tr>
39 : /// <tr><td>used_free_variables </td><td>The used free variables </td><td>PARAMLIST </td></tr>
40 : /// <tr><td>used_free_variables_names </td><td>The names of the used free variables </td><td>NAME, ..., NAME </td></tr>
41 : /// <tr><td>used_free_variable_count </td><td>The number of used free variables </td><td>NUMBER </td></tr>
42 : /// <tr><td>binding_variables </td><td>The binding variables </td><td>NAME(PARAMLIST), ..., NAME(PARAMLIST)</td></tr>
43 : /// <tr><td>binding_variable_names </td><td>The names of the binding variables </td><td>NAME, ..., NAME </td></tr>
44 : /// <tr><td>occurring_variables </td><td>The occurring variables </td><td>NUMBER </td></tr>
45 : /// <tr><td>occurring_variable_names </td><td>The names of the occurring variables </td><td>NAME(PARAMLIST), ..., NAME(PARAMLIST)</td></tr>
46 : /// </table>
47 : /// where <tt>PARAMLIST</tt> is defined as <tt>NAME:SORT, ... ,NAME:SORT</tt>.
48 : class pbes_property_map : public mcrl2::data::detail::data_property_map< pbes_property_map >
49 : {
50 : protected:
51 :
52 : // Allow base class access to protected functions
53 : friend class data::detail::data_property_map< pbes_property_map >;
54 :
55 : typedef data::detail::data_property_map< pbes_property_map > super;
56 :
57 : using super::print;
58 :
59 77 : std::string print(const propositional_variable& v) const
60 : {
61 77 : return pbes_system::pp(v);
62 : }
63 :
64 : // super class compare functions
65 : using super::compare;
66 :
67 36 : std::string compare_property(const std::string& property, const std::string& x, const std::string& y) const
68 : {
69 36 : if (property == "equation_count")
70 : {
71 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
72 : }
73 35 : else if (property == "mu_equation_count")
74 : {
75 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
76 : }
77 34 : else if (property == "nu_equation_count")
78 : {
79 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
80 : }
81 33 : else if (property == "block_nesting_depth")
82 : {
83 0 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
84 : }
85 33 : else if (property == "declared_free_variables")
86 : {
87 2 : return compare(property, parse_set_string(x), parse_set_string(y));
88 : }
89 32 : else if (property == "declared_free_variable_names")
90 : {
91 2 : return compare(property, parse_set_string(x), parse_set_string(y));
92 : }
93 31 : else if (property == "declared_variable_count")
94 : {
95 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
96 : }
97 30 : else if (property == "used_free_variables")
98 : {
99 2 : return compare(property, parse_set_string(x), parse_set_string(y));
100 : }
101 29 : else if (property == "used_free_variables_names")
102 : {
103 2 : return compare(property, parse_set_string(x), parse_set_string(y));
104 : }
105 28 : else if (property == "used_free_variable_count")
106 : {
107 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
108 : }
109 27 : else if (property == "binding_variables")
110 : {
111 44 : return compare(property, parse_set_string(x), parse_set_string(y));
112 : }
113 5 : else if (property == "binding_variable_names")
114 : {
115 6 : return compare(property, parse_set_string(x), parse_set_string(y));
116 : }
117 2 : else if (property == "occurring_variables")
118 : {
119 2 : return compare(property, parse_set_string(x), parse_set_string(y));
120 : }
121 1 : else if (property == "occurring_variable_names")
122 : {
123 2 : return compare(property, parse_set_string(x), parse_set_string(y));
124 : }
125 0 : return "ERROR: unknown property " + property + " encountered!";
126 : }
127 :
128 : //--------------------------------------------//
129 : // compute functions
130 : //--------------------------------------------//
131 : /// \brief Computes the number of mu and nu equations and returns them as a pair
132 23 : std::pair<std::size_t, std::size_t> compute_equation_counts(const pbes& p) const
133 : {
134 23 : std::size_t mu_count = 0;
135 23 : std::size_t nu_count = 0;
136 62 : for (const pbes_equation& eqn: p.equations())
137 : {
138 39 : if (eqn.symbol().is_mu())
139 : {
140 15 : mu_count++;
141 : }
142 : else
143 : {
144 24 : nu_count++;
145 : }
146 : }
147 46 : return std::make_pair(mu_count, nu_count);
148 : }
149 :
150 : // number of changes from mu to nu or vice versa
151 23 : std::size_t compute_block_nesting_depth(const pbes& p) const
152 : {
153 23 : std::size_t block_nesting_depth = 0;
154 23 : bool last_symbol_is_mu = false;
155 :
156 62 : for (auto i = p.equations().begin(); i != p.equations().end(); ++i)
157 : {
158 39 : if (i != p.equations().begin())
159 : {
160 16 : if (i->symbol().is_mu() != last_symbol_is_mu)
161 : {
162 10 : block_nesting_depth++;
163 : }
164 : }
165 39 : last_symbol_is_mu = i->symbol().is_mu();
166 : }
167 23 : return block_nesting_depth;
168 : }
169 :
170 : public:
171 : /// \brief Constructor.
172 : /// The strings may appear in a random order, and not all of them need to be present
173 24 : pbes_property_map(const std::string& text)
174 24 : : super(text)
175 24 : {}
176 :
177 : /// \brief Constructor
178 : /// Initializes the pbes_property_map with a linear process specification
179 23 : explicit pbes_property_map(const pbes& p)
180 23 : {
181 23 : std::pair<std::size_t, std::size_t> equation_counts = compute_equation_counts(p);
182 23 : std::size_t block_nesting_depth = compute_block_nesting_depth(p);
183 23 : const std::set<data::variable>& declared_free_variables = p.global_variables();
184 23 : std::set<data::variable> used_free_variables = pbes_system::find_free_variables(p);
185 23 : std::set<propositional_variable> binding_variables = p.binding_variables();
186 23 : std::set<propositional_variable> occurring_variables = p.occurring_variables();
187 :
188 23 : m_data["equation_count" ] = print(equation_counts.first + equation_counts.second);
189 23 : m_data["mu_equation_count" ] = print(equation_counts.first);
190 23 : m_data["nu_equation_count" ] = print(equation_counts.second);
191 23 : m_data["block_nesting_depth" ] = print(block_nesting_depth);
192 23 : m_data["declared_free_variables" ] = print(declared_free_variables, false);
193 23 : m_data["declared_free_variable_names"] = print(names(declared_free_variables), false);
194 23 : m_data["declared_variable_count" ] = print(declared_free_variables.size());
195 23 : m_data["used_free_variables" ] = print(used_free_variables, false);
196 23 : m_data["used_free_variables_names" ] = print(names(used_free_variables), false);
197 23 : m_data["used_free_variable_count" ] = print(used_free_variables.size());
198 23 : m_data["binding_variables" ] = print(binding_variables, false);
199 23 : m_data["binding_variable_names" ] = print(names(binding_variables), false);
200 23 : m_data["occurring_variables" ] = print(occurring_variables, false);
201 23 : m_data["occurring_variable_names" ] = print(names(occurring_variables), false);
202 23 : }
203 :
204 : using super::to_string;
205 : using super::data;
206 :
207 24 : std::string compare(const pbes_property_map& other) const
208 : {
209 24 : return super::compare(other);
210 : }
211 : };
212 :
213 : } // namespace detail
214 :
215 : } // namespace pbes_system
216 :
217 : } // namespace mcrl2
218 :
219 : #endif // MCRL2_PBES_DETAIL_PBES_PROPERTY_MAP_H
|