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/eqelm.h
8 : /// \brief The eqelm algorithm.
9 :
10 : #ifndef MCRL2_PBES_EQELM_H
11 : #define MCRL2_PBES_EQELM_H
12 :
13 : #include "mcrl2/pbes/algorithms.h"
14 : #include "mcrl2/pbes/pbes_rewriter_type.h"
15 : #include "mcrl2/pbes/print.h"
16 : #include "mcrl2/pbes/replace.h"
17 : #include "mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace pbes_system
23 : {
24 :
25 : /// \brief Algorithm class for the eqelm algorithm
26 : template <typename Term, typename DataRewriter, typename PbesRewriter>
27 : class pbes_eqelm_algorithm
28 : {
29 : protected:
30 : typedef std::set<data::variable> equivalence_class;
31 :
32 : /// \brief Compares data expressions for equality.
33 : const DataRewriter& m_data_rewriter;
34 :
35 : /// \brief Compares data expressions for equality.
36 : const PbesRewriter& m_pbes_rewriter;
37 :
38 : /// \brief The vertices of the grapth, i.e. the equivalence relations.
39 : /// It stores the equivalence sets for each propositional variable, for example
40 : /// X -> [ {x1, x3}, {x2, x4} ]. Equivalence sets of size 1 are not stored.
41 : std::map<core::identifier_string, std::vector<equivalence_class> > m_vertices;
42 :
43 : /// \brief The edges of the graph.
44 : /// It is a mapping from X to iocc(X).
45 : std::map<core::identifier_string, std::set<propositional_variable_instantiation> > m_edges;
46 :
47 : /// \brief The parameters of the propositional variable declarations.
48 : /// These are stored inside a vector, for efficiency reasons.
49 : std::map<core::identifier_string, std::vector<data::variable> > m_parameters;
50 :
51 : /// \brief Used for determining if a vertex has been visited before.
52 : std::map<core::identifier_string, bool> m_discovered;
53 :
54 : /// \brief Puts all parameters of the same sort in the same equivalence set.
55 4 : std::vector<equivalence_class> compute_equivalence_sets(const propositional_variable& X) const
56 : {
57 4 : std::map< data::sort_expression, equivalence_class> m;
58 15 : for (const auto & i : X.parameters())
59 : {
60 7 : m[i.sort()].insert(i);
61 : }
62 4 : std::vector<equivalence_class> result;
63 8 : for (auto & i : m)
64 : {
65 4 : if (i.second.size() > 1)
66 : {
67 3 : result.push_back(i.second);
68 : }
69 : }
70 8 : return result;
71 4 : }
72 :
73 : /// \brief Prints the vertices of the dependency graph.
74 0 : std::string print_vertices() const
75 : {
76 0 : std::ostringstream out;
77 0 : for (auto i = m_vertices.begin(); i != m_vertices.end(); ++i)
78 : {
79 0 : out << i->first << " -> [ ";
80 0 : const std::vector<equivalence_class>& v = i->second;
81 0 : for (auto j = v.begin(); j != v.end(); ++j)
82 : {
83 0 : if (j != v.begin())
84 : {
85 0 : out << ", ";
86 : }
87 0 : out << core::detail::print_set(*j);
88 : }
89 0 : out << " ]" << std::endl;
90 : }
91 0 : return out.str();
92 0 : }
93 :
94 : /// \brief Prints the edges of the dependency graph.
95 0 : std::string print_edges() const
96 : {
97 0 : std::ostringstream out;
98 0 : for (auto i = m_edges.begin(); i != m_edges.end(); ++i)
99 : {
100 0 : out << i->first << " -> " << core::detail::print_set(i->second) << std::endl;
101 : }
102 0 : return out.str();
103 0 : }
104 :
105 : /// \brief Prints the equivalence classes
106 0 : std::string print_equivalence_classes() const
107 : {
108 0 : std::ostringstream out;
109 0 : for (auto i = m_vertices.begin(); i != m_vertices.end(); ++i)
110 : {
111 0 : out << " vertex " << i->first << ": ";
112 0 : for (auto j = i->second.begin(); j != i->second.end(); ++j)
113 : {
114 0 : out << core::detail::print_set(*j) << " ";
115 : }
116 0 : out << std::endl;
117 : }
118 0 : return out.str();
119 0 : }
120 :
121 : /// \brief Prints the todo list
122 : void log_todo_list(const std::set<core::identifier_string>& todo, const std::string& msg = "") const
123 : {
124 : mCRL2log(log::debug) << msg;
125 : mCRL2log(log::debug) << core::detail::print_set(todo) << "\n";
126 : }
127 :
128 : /// \brief Returns true if the vertex X should propagate its values to Y
129 9 : bool evaluate_guard(const core::identifier_string& /* X */, const propositional_variable_instantiation& /* Y */)
130 : {
131 9 : return true;
132 : }
133 :
134 : /// \brief Returns the index of the element x in the sequence v
135 : template <typename VariableContainer>
136 13 : std::size_t index_of(const data::variable& x, const VariableContainer& v)
137 : {
138 13 : return static_cast<std::size_t>(std::find(v.begin(), v.end(), x) - v.begin());
139 : }
140 :
141 : /// \brief Propagate the equivalence relations given by the substitution vX over the edge Ye.
142 : template <typename Substitution>
143 9 : void update_equivalence_classes(const propositional_variable_instantiation& Ye,
144 : const Substitution& vX,
145 : std::set<core::identifier_string>& todo
146 : )
147 : {
148 9 : const core::identifier_string& Y = Ye.name();
149 9 : std::vector<data::data_expression> e(Ye.parameters().begin(), Ye.parameters().end());
150 :
151 9 : std::vector<equivalence_class>& cY = m_vertices[Y];
152 9 : std::vector<equivalence_class> cY1;
153 15 : for (auto & equiv : cY)
154 : {
155 6 : std::map<data::data_expression, equivalence_class> w;
156 18 : for (const auto & k : equiv)
157 : {
158 12 : std::size_t p = index_of(k, m_parameters[Y]);
159 12 : pbes_system::data_rewriter<DataRewriter> rewr(m_data_rewriter);
160 12 : pbes_system::pbes_expression e_p = rewr(e[p], vX);
161 12 : w[atermpp::down_cast<const data::data_expression>(e_p)].insert(k);
162 : }
163 14 : for (auto & i : w)
164 : {
165 8 : if (i.second.size() > 1)
166 : {
167 4 : cY1.push_back(i.second);
168 : }
169 : }
170 : }
171 9 : if (cY != cY1)
172 : {
173 2 : todo.insert(Y);
174 2 : m_discovered[Y] = true;
175 2 : cY = cY1;
176 : }
177 7 : else if (!m_discovered[Y])
178 : {
179 1 : todo.insert(Y);
180 1 : m_discovered[Y] = true;
181 : }
182 9 : }
183 :
184 : /// \brief Computes a substitution that corresponds to the equivalence relations in X
185 13 : data::mutable_map_substitution<> compute_substitution(const core::identifier_string& X)
186 : {
187 13 : data::mutable_map_substitution<> result;
188 13 : const std::vector<equivalence_class>& cX = m_vertices[X];
189 19 : for (const auto & s : cX)
190 : {
191 12 : for (auto j = ++s.begin(); j != s.end(); ++j)
192 : {
193 6 : result[*j] = *s.begin();
194 : }
195 : }
196 13 : return result;
197 0 : }
198 :
199 : /// \brief Chooses one parameter for every equivalence class, and
200 : /// removes the others. All occurrences of the removed parameters
201 : /// are replaced by the chosen parameter.
202 : inline
203 3 : void apply_equivalence_relations(pbes& p)
204 : {
205 : // first apply the substitutions to the equations
206 7 : for (pbes_equation& eqn: p.equations())
207 : {
208 4 : core::identifier_string X = eqn.variable().name();
209 4 : data::mutable_map_substitution<> sigma = compute_substitution(X);
210 :
211 4 : if (!sigma.empty())
212 : {
213 1 : eqn.formula() = pbes_system::replace_variables_capture_avoiding(eqn.formula(), sigma);
214 : }
215 : }
216 :
217 : // then remove parameters
218 3 : std::map<core::identifier_string, std::vector<std::size_t> > to_be_removed;
219 7 : for (pbes_equation& eqn: p.equations())
220 : {
221 4 : core::identifier_string X = eqn.variable().name();
222 4 : const std::vector<equivalence_class>& eq = m_vertices[X];
223 5 : for (const auto & j : eq)
224 : {
225 2 : for (auto k = ++j.begin(); k != j.end(); ++k)
226 : {
227 1 : to_be_removed[X].push_back(index_of(*k, m_parameters[X]));
228 : }
229 1 : std::sort(to_be_removed[X].begin(), to_be_removed[X].end());
230 : }
231 : }
232 :
233 3 : pbes_system::algorithms::remove_parameters(p, to_be_removed);
234 3 : }
235 :
236 : public:
237 : /// \brief Constructor.
238 : /// \param datar A data rewriter
239 : /// \param pbesr A PBES rewriter
240 3 : pbes_eqelm_algorithm(const DataRewriter& datar, const PbesRewriter& pbesr)
241 3 : : m_data_rewriter(datar),
242 3 : m_pbes_rewriter(pbesr)
243 3 : {}
244 :
245 : /// \brief Runs the eqelm algorithm
246 : /// \param p A pbes
247 : /// \param ignore_initial_state If true, the initial state is ignored.
248 3 : void run(pbes& p, bool ignore_initial_state = false)
249 : {
250 3 : m_vertices.clear();
251 3 : m_edges.clear();
252 3 : std::set<core::identifier_string> todo;
253 :
254 : // compute the vertices and edges of the graph
255 7 : for (pbes_equation& eqn: p.equations())
256 : {
257 4 : core::identifier_string name = eqn.variable().name();
258 4 : m_edges[name] = find_propositional_variable_instantiations(eqn.formula());
259 4 : m_vertices[name] = compute_equivalence_sets(eqn.variable());
260 4 : const data::variable_list& param = eqn.variable().parameters();
261 4 : m_parameters[name] = std::vector<data::variable>(param.begin(), param.end());
262 4 : todo.insert(name);
263 4 : m_discovered[name] = ignore_initial_state;
264 : }
265 :
266 3 : if (!ignore_initial_state)
267 : {
268 3 : todo.clear();
269 3 : propositional_variable_instantiation kappa = p.initial_state();
270 3 : const core::identifier_string& X = kappa.name();
271 3 : data::mutable_map_substitution<> vX = compute_substitution(X);
272 :
273 : // propagate the equivalence relations in X over the edge kappa
274 3 : if (evaluate_guard(X, kappa))
275 : {
276 3 : todo.insert(X);
277 3 : m_discovered[X] = true;
278 3 : update_equivalence_classes(kappa, vX, todo);
279 3 : mCRL2log(log::debug) << "updated equivalence classes using initial state " << kappa << "\n" << print_equivalence_classes();
280 : }
281 3 : }
282 :
283 3 : mCRL2log(log::verbose) << "--- vertices ---\n" << print_vertices();
284 3 : mCRL2log(log::verbose) << "\n--- edges ---\n" << print_edges();
285 3 : mCRL2log(log::debug) << "computed initial equivalence classes\n" << print_equivalence_classes();
286 :
287 : // propagate constraints over the edges until the todo list is empty
288 15 : while (!todo.empty())
289 : {
290 6 : mCRL2log(log::debug) << "todo list = " << core::detail::print_set(todo) << "\n";
291 6 : mCRL2log(log::verbose) << "--- vertices ---\n" << print_vertices();
292 :
293 6 : core::identifier_string X = *todo.begin();
294 6 : todo.erase(X);
295 6 : mCRL2log(log::debug) << "choose todo element " << X << "\n";
296 :
297 : // create a substitution function that corresponds to cX
298 6 : data::mutable_map_substitution<> vX = compute_substitution(X);
299 6 : const std::set<propositional_variable_instantiation>& edges = m_edges[X];
300 12 : for (const auto& Ye : edges)
301 : {
302 : // propagate the equivalence relations in X over the edge Ye
303 6 : if (evaluate_guard(X, Ye))
304 : {
305 6 : update_equivalence_classes(Ye, vX, todo);
306 6 : mCRL2log(log::debug) << "updated equivalence classes using edge " << Ye << "\n" << print_equivalence_classes();
307 : }
308 : }
309 : }
310 3 : apply_equivalence_relations(p);
311 3 : mCRL2log(log::verbose) << "\n--- result ---\n" << print_vertices();
312 3 : }
313 : };
314 :
315 : /// \brief Apply the eqelm algorithm
316 : /// \param p A PBES to which the algorithm is applied.
317 : /// \param rewrite_strategy A data rewrite strategy.
318 : /// \param rewriter_type A PBES rewriter type.
319 : /// \param ignore_initial_state If true, the initial state will be ignored.
320 : inline
321 : void eqelm(pbes& p,
322 : data::rewrite_strategy rewrite_strategy,
323 : pbes_rewriter_type rewriter_type,
324 : bool ignore_initial_state = false
325 : )
326 : {
327 : // data rewriter
328 : data::rewriter datar(p.data(), rewrite_strategy);
329 :
330 : // pbes rewriter
331 : switch (rewriter_type)
332 : {
333 : case simplify:
334 : {
335 : typedef simplify_data_rewriter<data::rewriter> pbes_rewriter;
336 : pbes_rewriter pbesr(datar);
337 : pbes_eqelm_algorithm<pbes_expression, data::rewriter, pbes_rewriter> algorithm(datar, pbesr);
338 : algorithm.run(p, ignore_initial_state);
339 : break;
340 : }
341 : case quantifier_all:
342 : case quantifier_finite:
343 : {
344 : bool enumerate_infinite_sorts = (rewriter_type == quantifier_all);
345 : enumerate_quantifiers_rewriter pbesr(datar, p.data(), enumerate_infinite_sorts);
346 : pbes_eqelm_algorithm<pbes_expression, data::rewriter, enumerate_quantifiers_rewriter> algorithm(datar, pbesr);
347 : algorithm.run(p, ignore_initial_state);
348 : break;
349 : }
350 : default:
351 : { }
352 : }
353 : }
354 :
355 : } // namespace pbes_system
356 :
357 : } // namespace mcrl2
358 :
359 : #endif // MCRL2_PBES_EQELM_H
|
