Line data Source code
1 : // Author(s): Wieger Wesselink
2 : //
3 : // Distributed under the Boost Software License, Version 1.0.
4 : // (See accompanying file LICENSE_1_0.txt or copy at
5 : // http://www.boost.org/LICENSE_1_0.txt)
6 : //
7 : /// \file mcrl2/pbes/parelm.h
8 : /// \brief The parelm algorithm.
9 :
10 : #ifndef MCRL2_PBES_PARELM_H
11 : #define MCRL2_PBES_PARELM_H
12 :
13 : #include "mcrl2/pbes/algorithms.h"
14 : #include "mcrl2/pbes/detail/find_free_variables.h"
15 : #include "mcrl2/utilities/detail/iota.h"
16 : #include "mcrl2/utilities/reachable_nodes.h"
17 :
18 : namespace mcrl2::pbes_system {
19 :
20 : namespace detail {
21 :
22 : /// \brief Finds the index of a variable in a sequence
23 : /// \param variables A sequence of data variables
24 : /// \param d A data variable
25 : /// \return The index of \p d in \p v, or -1 if the variable wasn't found
26 : inline
27 117 : int variable_index(const data::variable_list& variables, const data::variable& d)
28 : {
29 117 : int index = 0;
30 781 : for (const data::variable& v: variables)
31 : {
32 767 : if (v == d)
33 : {
34 103 : return index;
35 : }
36 664 : index++;
37 : }
38 14 : return -1;
39 : }
40 :
41 : } // namespace detail
42 :
43 : /// \brief Algorithm class for the parelm algorithm
44 : class pbes_parelm_algorithm
45 : {
46 : protected:
47 : /// \brief The graph type of the dependency graph
48 : typedef boost::adjacency_list<boost::setS, boost::vecS, boost::directedS> graph;
49 :
50 : /// \brief The vertex type of the dependency graph
51 : typedef boost::graph_traits<graph>::vertex_descriptor vertex_descriptor;
52 :
53 : /// \brief The edge type of the dependency graph
54 : typedef boost::graph_traits<graph>::edge_descriptor edge_descriptor;
55 :
56 : struct parelm_dependency_traverser: public pbes_expression_traverser<parelm_dependency_traverser>
57 : {
58 : typedef pbes_expression_traverser<parelm_dependency_traverser> super;
59 : using super::enter;
60 : using super::leave;
61 : using super::apply;
62 :
63 : graph& G;
64 : const std::map<core::identifier_string, std::size_t>& propvar_offsets;
65 :
66 : core::identifier_string X;
67 : data::variable_list Xparams;
68 : std::multiset<data::variable> bound_variables;
69 :
70 1 : parelm_dependency_traverser(graph& G_, const std::map<core::identifier_string, std::size_t>& propvar_offsets_)
71 1 : : G(G_), propvar_offsets(propvar_offsets_)
72 1 : {}
73 :
74 6 : void enter(const forall& x)
75 : {
76 12 : for (const data::variable& v: x.variables())
77 : {
78 6 : bound_variables.insert(v);
79 : }
80 6 : }
81 :
82 6 : void leave(const forall& x)
83 : {
84 12 : for (const data::variable& v: x.variables())
85 : {
86 6 : bound_variables.erase(v);
87 : }
88 6 : }
89 :
90 0 : void enter(const exists& x)
91 : {
92 0 : for (const data::variable& v: x.variables())
93 : {
94 0 : bound_variables.insert(v);
95 : }
96 0 : }
97 :
98 0 : void leave(const exists& x)
99 : {
100 0 : for (const data::variable& v: x.variables())
101 : {
102 0 : bound_variables.erase(v);
103 : }
104 0 : }
105 :
106 11 : void apply(const propositional_variable_instantiation& x)
107 : {
108 : using utilities::detail::contains;
109 :
110 11 : const core::identifier_string& Y = x.name();
111 11 : int Yindex = 0;
112 132 : for (const data::data_expression& e: x.parameters())
113 : {
114 243 : for (const data::variable& var: data::find_free_variables(e))
115 : {
116 122 : if (contains(bound_variables, var))
117 : {
118 13 : continue;
119 : }
120 109 : int Xindex = detail::variable_index(Xparams, var);
121 109 : if (Xindex < 0)
122 : {
123 14 : continue;
124 : }
125 : // parameter (Y, Yindex) is influenced by (X, Xindex)
126 95 : boost::add_edge(propvar_offsets.at(Y) + Yindex, propvar_offsets.at(X) + Xindex, G);
127 121 : }
128 121 : Yindex++;
129 : }
130 11 : }
131 :
132 2 : void apply(const pbes_equation& eqn)
133 : {
134 2 : X = eqn.variable().name();
135 2 : Xparams = eqn.variable().parameters();
136 2 : super::apply(eqn);
137 2 : }
138 : };
139 :
140 : /// \brief Finds unbound variables in a pbes expression
141 : /// \param t A PBES expression
142 : /// \param bound_variables A sequence of data variables
143 : /// \return The unbound variables in \p t that are not contained in \p bound_variables
144 2 : static std::set<data::variable> unbound_variables(const pbes_expression& t, const data::variable_list& bound_variables)
145 : {
146 2 : bool search_propositional_variables = false;
147 2 : return detail::find_free_variables(t, bound_variables, search_propositional_variables);
148 : }
149 :
150 : /// \brief Finds the predicate variable to which the data parameter with the given index belongs.
151 : /// Here index refers to the cumulative index in the array obtained by concatening all parameters
152 : /// of the predicate variables in the pbes \p p.
153 : /// \param p A pbes
154 : /// \param index A positive number
155 : /// \return The name of the predicate variable that corresponds with \p index
156 0 : static core::identifier_string find_predicate_variable(const pbes& p, std::size_t index)
157 : {
158 0 : std::size_t offset = 0;
159 0 : for (const pbes_equation& eqn: p.equations())
160 : {
161 0 : std::size_t size = eqn.variable().parameters().size();
162 0 : if (offset + size > index)
163 : {
164 0 : return eqn.variable().name();
165 : }
166 0 : offset += eqn.variable().parameters().size();
167 : }
168 0 : return core::identifier_string("<not found>");
169 : }
170 :
171 1 : static void compute_dependency_graph(const pbes& p, const std::map<core::identifier_string, std::size_t>& propvar_offsets, graph& G)
172 : {
173 1 : parelm_dependency_traverser f(G, propvar_offsets);
174 3 : for (const pbes_equation& eqn: p.equations())
175 : {
176 2 : f.apply(eqn);
177 : }
178 1 : }
179 :
180 : public:
181 : /// \brief Runs the parelm algorithm. The pbes \p is modified by the algorithm
182 : /// \param p A pbes
183 1 : void run(pbes& p)
184 : {
185 1 : data::variable_list global_variables(p.global_variables().begin(), p.global_variables().end());
186 1 : std::vector<data::variable> predicate_variables;
187 :
188 : // compute a mapping from propositional variable names to offsets
189 1 : std::size_t offset = 0;
190 1 : std::map<core::identifier_string, std::size_t> propvar_offsets;
191 3 : for (pbes_equation& eqn: p.equations())
192 : {
193 2 : propvar_offsets[eqn.variable().name()] = offset;
194 2 : offset += eqn.variable().parameters().size();
195 2 : predicate_variables.insert(predicate_variables.end(), eqn.variable().parameters().begin(), eqn.variable().parameters().end());
196 : }
197 1 : std::size_t N = offset; // # variables
198 :
199 : // compute the initial set v of significant variables
200 1 : std::set<std::size_t> significant_variables;
201 1 : offset = 0;
202 3 : for (pbes_equation& eqn: p.equations())
203 : {
204 10 : for (const data::variable& w: unbound_variables(eqn.formula(), global_variables))
205 : {
206 8 : int k = detail::variable_index(eqn.variable().parameters(), w);
207 8 : if (k < 0)
208 : {
209 0 : throw mcrl2::runtime_error("<variable error>" + data::pp(w));
210 : }
211 8 : significant_variables.insert(offset + k);
212 2 : }
213 2 : offset += eqn.variable().parameters().size();
214 : }
215 :
216 1 : graph G(N);
217 1 : compute_dependency_graph(p, propvar_offsets, G);
218 :
219 : // compute the indices s of the parameters that need to be removed
220 1 : std::vector<std::size_t> r = utilities::reachable_nodes(G, significant_variables.begin(), significant_variables.end());
221 1 : std::sort(r.begin(), r.end());
222 1 : std::vector<std::size_t> q(N);
223 1 : utilities::detail::iota(q.begin(), q.end(), 0);
224 1 : std::vector<std::size_t> s;
225 1 : std::set_difference(q.begin(), q.end(), r.begin(), r.end(), std::back_inserter(s));
226 :
227 : // create a map that specifies the parameters that need to be removed
228 1 : std::map<core::identifier_string, std::vector<std::size_t> > removals;
229 1 : std::size_t index = 0;
230 1 : auto sfirst = s.begin();
231 3 : for (pbes_equation& eqn: p.equations())
232 : {
233 2 : std::size_t maxindex = index + eqn.variable().parameters().size();
234 17 : auto slast = std::find_if(sfirst, s.end(), [&](std::size_t i) { return i >= maxindex; });
235 2 : if (slast > sfirst)
236 : {
237 2 : std::vector<std::size_t> w(sfirst, slast);
238 16 : std::transform(w.begin(), w.end(), w.begin(), [&](std::size_t i) { return i - index; });
239 2 : removals[eqn.variable().name()] = w;
240 2 : }
241 2 : index = maxindex;
242 2 : sfirst = slast;
243 : }
244 :
245 1 : if (mCRL2logEnabled(log::debug))
246 : {
247 0 : print_dependencies(p, predicate_variables, significant_variables, G);
248 : }
249 :
250 : // print verbose output
251 1 : if (mCRL2logEnabled(log::verbose))
252 : {
253 0 : print_removed_parameters(predicate_variables, propvar_offsets, removals);
254 : }
255 :
256 : // remove the parameters
257 1 : pbes_system::algorithms::remove_parameters(p, removals);
258 1 : }
259 :
260 0 : void print_removed_parameters(const std::vector<data::variable>& predicate_variables,
261 : const std::map<core::identifier_string, std::size_t>& propvar_offsets,
262 : const std::map<core::identifier_string, std::vector<std::size_t>>& removals) const
263 : {
264 0 : mCRL2log(log::verbose) << "\nremoving the following parameters:" << std::endl;
265 0 : for (auto& removal: removals)
266 : {
267 0 : core::identifier_string X1 = removal.first;
268 0 : for (std::size_t j: removal.second)
269 : {
270 0 : data::variable v1 = predicate_variables[j + propvar_offsets.at(X1)];
271 0 : mCRL2log(log::verbose) << "(" + core::pp(X1) + ", " + data::pp(v1) + ")\n";
272 0 : }
273 0 : }
274 0 : }
275 :
276 0 : static void print_dependencies(const pbes& p, const std::vector<data::variable>& predicate_variables, const std::set<std::size_t>& significant_variables, const graph& G)
277 : {
278 0 : mCRL2log(log::debug) << "\ninfluential parameters:" << std::endl;
279 0 : for (std::size_t i: significant_variables)
280 : {
281 0 : core::identifier_string X1 = find_predicate_variable(p, i);
282 0 : data::variable v1 = predicate_variables[i];
283 0 : mCRL2log(log::debug) << "(" + core::pp(X1) + ", " + data::pp(v1) + ")\n";
284 0 : }
285 0 : mCRL2log(log::debug) << "\ndependencies:" << std::endl;
286 : typedef boost::graph_traits<graph>::edge_iterator edge_iterator;
287 0 : std::pair<edge_iterator, edge_iterator> e = edges(G);
288 0 : edge_iterator first = e.first;
289 0 : edge_iterator last = e.second;
290 0 : for (; first != last; ++first)
291 : {
292 0 : edge_descriptor f = *first;
293 0 : std::size_t i1 = boost::source(f, G);
294 0 : core::identifier_string X1 = find_predicate_variable(p, i1);
295 0 : data::variable v1 = predicate_variables[i1];
296 0 : std::size_t i2 = boost::target(f, G);
297 0 : core::identifier_string X2 = find_predicate_variable(p, i2);
298 0 : data::variable v2 = predicate_variables[i2];
299 0 : std::string left = "(" + core::pp(X1) + ", " + data::pp(v1) + ")";
300 0 : std::string right = "(" + core::pp(X2) + ", " + data::pp(v2) + ")";
301 0 : mCRL2log(log::debug) << left << " -> " << right << std::endl;
302 0 : }
303 0 : }
304 : };
305 :
306 : /// \brief Apply the parelm algorithm
307 : /// \param p A PBES to which the algorithm is applied
308 : inline
309 0 : void parelm(pbes& p)
310 : {
311 : pbes_parelm_algorithm algorithm;
312 0 : algorithm.run(p);
313 0 : }
314 :
315 : } // namespace mcrl2::pbes_system
316 :
317 : #endif // MCRL2_PBES_PARELM_H
|
