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/small_progress_measures.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_BES_SMALL_PROGRESS_MEASURES_H
13 : #define MCRL2_BES_SMALL_PROGRESS_MEASURES_H
14 :
15 : // TODO: Make it possible to undefine this flag
16 : #define MCRL2_SMALL_PROGRESS_MEASURES_DEBUG
17 :
18 : #include <iomanip>
19 : #include "mcrl2/core/detail/print_utility.h"
20 : #include "mcrl2/pbes/find.h"
21 : #include "mcrl2/pbes/normal_forms.h"
22 : #include "mcrl2/pbes/print.h"
23 :
24 : namespace mcrl2
25 : {
26 :
27 : namespace pbes_system
28 : {
29 :
30 : template <typename T>
31 19 : bool is_odd(T t)
32 : {
33 19 : return t % 2 != 0;
34 : }
35 :
36 : template <typename T>
37 9 : bool is_even(T t)
38 : {
39 9 : return t % 2 == 0;
40 : }
41 :
42 : template <typename InputIterator1, typename InputIterator2>
43 4 : int lexicographical_compare_3way(InputIterator1 first1, InputIterator1 last1,
44 : InputIterator2 first2, InputIterator2 last2)
45 : {
46 9 : while (first1 != last1 && first2 != last2)
47 : {
48 8 : if (*first1 < *first2)
49 : {
50 2 : return -1;
51 : }
52 6 : if (*first2 < *first1)
53 : {
54 1 : return 1;
55 : }
56 5 : ++first1;
57 5 : ++first2;
58 : }
59 1 : if (first2 == last2)
60 : {
61 1 : return !(first1 == last1);
62 : }
63 : else
64 : {
65 0 : return -1;
66 : }
67 : }
68 :
69 : inline
70 7 : bool is_disjunctive(const pbes_expression& x)
71 : {
72 7 : return is_or(x);
73 : }
74 :
75 : inline
76 3 : int maximum_rank(const pbes& b)
77 : {
78 3 : int result = 0;
79 3 : fixpoint_symbol last_symbol;
80 10 : for (auto i = b.equations().begin(); i != b.equations().end(); ++i)
81 : {
82 7 : if (i == b.equations().begin())
83 : {
84 3 : result = i->symbol().is_nu() ? 0 : 1;
85 : }
86 4 : else if (i->symbol() != last_symbol)
87 : {
88 4 : result++;
89 : }
90 7 : last_symbol = i->symbol();
91 : }
92 3 : return result;
93 3 : }
94 :
95 : struct progress_measure
96 : {
97 14 : explicit progress_measure(std::size_t d)
98 14 : : v(d, 0)
99 14 : {}
100 :
101 : // N.B. The special value top is represented by alpha[0] == -1
102 : std::vector<int> v;
103 :
104 20 : bool is_top() const
105 : {
106 20 : return v[0] == -1;
107 : }
108 : };
109 :
110 : inline
111 0 : std::ostream& operator<<(std::ostream& out, const progress_measure& pm)
112 : {
113 0 : if (pm.is_top())
114 : {
115 0 : out << "top";
116 : }
117 : else
118 : {
119 0 : out << core::detail::print_list(pm.v);
120 : }
121 0 : return out;
122 : }
123 :
124 : // increment position m of vector alpha
125 : inline
126 15 : void inc(std::vector<int>& alpha, int m, const std::vector<int>& beta)
127 : {
128 15 : if (alpha[0] == -1)
129 : {
130 2 : return;
131 : }
132 13 : else if (m == -1)
133 : {
134 2 : alpha[0] = -1;
135 2 : return;
136 : }
137 11 : else if (alpha[m] == beta[m])
138 : {
139 4 : alpha[m] = 0;
140 4 : inc(alpha, m - 1, beta);
141 : }
142 : else
143 : {
144 7 : alpha[m]++;
145 : }
146 : }
147 :
148 : /// \brief Vertex of the progress measures graph
149 : struct progress_measures_vertex
150 : {
151 14 : explicit progress_measures_vertex(bool even_ = false, int rank_ = 0, unsigned int d = 1)
152 28 : : even(even_),
153 14 : rank(rank_),
154 14 : alpha(d)
155 14 : {}
156 :
157 : std::vector<progress_measures_vertex*> successors;
158 : bool even;
159 : int rank;
160 : progress_measure alpha;
161 :
162 : #ifdef MCRL2_SMALL_PROGRESS_MEASURES_DEBUG
163 : std::string name;
164 : #endif
165 : };
166 :
167 : // compare the positions with index in [0, ... ,m]
168 : struct compare_progress_measures_vertex
169 : {
170 : unsigned int m;
171 :
172 19 : explicit compare_progress_measures_vertex(unsigned int m_)
173 19 : : m(m_)
174 19 : {}
175 :
176 9 : bool operator()(const progress_measures_vertex* x, const progress_measures_vertex* y) const
177 : {
178 9 : if (x->alpha.is_top())
179 : {
180 1 : return false;
181 : }
182 8 : else if (y->alpha.is_top())
183 : {
184 4 : return true;
185 : }
186 4 : int n = lexicographical_compare_3way(x->alpha.v.begin(), x->alpha.v.begin() + m + 1, y->alpha.v.begin(), y->alpha.v.begin() + m + 1);
187 : //if (n == 0)
188 : //{
189 : // return is_even(x->rank) && is_odd(y->rank);
190 : //}
191 4 : return n < 0;
192 : }
193 : };
194 :
195 : inline
196 0 : std::ostream& operator<<(std::ostream& out, const progress_measures_vertex& v)
197 : {
198 0 : out << " alpha = " << v.alpha;
199 0 : out << " successors = {";
200 0 : for (auto i = v.successors.begin(); i != v.successors.end(); ++i)
201 : {
202 0 : if (i != v.successors.begin())
203 : {
204 0 : out << ", ";
205 : }
206 0 : out << std::string((*i)->name);
207 : }
208 0 : out << "}";
209 0 : out << " rank = " << v.rank;
210 0 : out << " disjunctive = " << std::boolalpha << v.even;
211 0 : return out;
212 : }
213 :
214 : /// \brief Algorithm class for the small progress measures algorithm
215 : class small_progress_measures_algorithm
216 : {
217 : protected:
218 : typedef progress_measures_vertex vertex;
219 : typedef std::map<propositional_variable_instantiation, vertex> vertex_map;
220 :
221 3 : void initialize_vertices()
222 : {
223 : // first build the vertex map without successor information
224 3 : m_d = maximum_rank(m_bes) + 1;
225 3 : unsigned int block_size = 0;
226 3 : int last_rank = 0;
227 3 : fixpoint_symbol last_symbol = fixpoint_symbol::nu();
228 10 : for (const pbes_equation& eqn: m_bes.equations())
229 : {
230 7 : if (eqn.symbol() != last_symbol)
231 : {
232 6 : if (is_even(m_beta.size()))
233 : {
234 4 : m_beta.push_back(0);
235 : }
236 : else
237 : {
238 2 : m_beta.push_back(block_size);
239 : }
240 6 : block_size = 0;
241 6 : last_rank++;
242 6 : last_symbol = eqn.symbol();
243 : }
244 7 : block_size++;
245 7 : m_vertices[propositional_variable_instantiation(eqn.variable().name())] = vertex(is_disjunctive(eqn.formula()), last_rank, m_d);
246 : }
247 3 : if (is_even(m_beta.size()))
248 : {
249 1 : m_beta.push_back(0);
250 : }
251 : else
252 : {
253 2 : m_beta.push_back(block_size);
254 : }
255 :
256 : // add successor information
257 10 : for (const pbes_equation& eqn: m_bes.equations())
258 : {
259 7 : std::set<propositional_variable_instantiation> succ = pbes_system::find_propositional_variable_instantiations(eqn.formula());
260 7 : auto k = m_vertices.find(propositional_variable_instantiation(eqn.variable().name()));
261 7 : std::vector<vertex*>& k_successors = k->second.successors;
262 17 : for (const propositional_variable_instantiation& v: succ)
263 : {
264 10 : k_successors.push_back(&m_vertices[v]);
265 : }
266 :
267 : #ifdef MCRL2_SMALL_PROGRESS_MEASURES_DEBUG
268 7 : k->second.name = std::string(eqn.variable().name());
269 : #endif
270 7 : }
271 3 : }
272 :
273 0 : std::string print_vertices() const
274 : {
275 0 : std::ostringstream out;
276 0 : for (const pbes_equation& eqn: m_bes.equations())
277 : {
278 0 : const vertex& v = m_vertices.find(propositional_variable_instantiation(eqn.variable().name()))->second;
279 0 : out << v.name << " " << v << std::endl;
280 : }
281 0 : return out.str();
282 0 : }
283 :
284 0 : std::string print_vertex(const vertex& v) const
285 : {
286 0 : std::ostringstream out;
287 0 : out << v.name << " (alpha = " << v.alpha << ", rank = " << v.rank << ")";
288 0 : return out.str();
289 0 : }
290 :
291 : /// \brief Logs the neighbors of a vertex
292 0 : std::string print_neighbors(const progress_measures_vertex& v) const
293 : {
294 0 : std::ostringstream out;
295 0 : for (progress_measures_vertex* successor: v.successors)
296 : {
297 0 : out << "\n " << print_vertex(*successor);
298 : }
299 0 : return out.str();
300 0 : }
301 :
302 : vertex_map m_vertices;
303 : int m_d = 0;
304 : const pbes& m_bes;
305 : std::vector<int> m_beta;
306 :
307 : public:
308 3 : explicit small_progress_measures_algorithm(const pbes& b)
309 3 : : m_bes(b)
310 3 : {}
311 :
312 3 : bool run(const propositional_variable_instantiation& first_variable)
313 : {
314 3 : mCRL2log(log::verbose) << "Applying small progress measures.\n";
315 3 : mCRL2log(log::debug) << "BES " << pbes_system::pp(m_bes) << "\n\n";
316 3 : initialize_vertices();
317 3 : mCRL2log(log::debug) << "--- vertices ---\n" << print_vertices();
318 3 : mCRL2log(log::debug) << "\nbeta = " << core::detail::print_list(m_beta) << "\n";
319 : for (;;) // forever
320 : {
321 8 : bool changed = false;
322 27 : for (auto &i: m_vertices)
323 : {
324 19 : vertex& v = i.second;
325 19 : mCRL2log(log::debug) << "\nchoose vertex " << print_vertex(v);
326 19 : int m = v.rank;
327 19 : std::vector<progress_measures_vertex*>::const_iterator j;
328 19 : mCRL2log(log::debug) << "\n neighbors:" << print_neighbors(v);
329 19 : if (v.even)
330 : {
331 6 : j = std::min_element(v.successors.begin(), v.successors.end(), compare_progress_measures_vertex(m));
332 6 : mCRL2log(log::debug) << "\n minimum neighbor " << print_vertex(**j);
333 : }
334 : else
335 : {
336 13 : j = std::max_element(v.successors.begin(), v.successors.end(), compare_progress_measures_vertex(m));
337 13 : mCRL2log(log::debug) << "\n maximum neighbor " << print_vertex(**j);
338 : }
339 19 : std::vector<int> alpha(m_d, 0);
340 19 : const progress_measures_vertex& w = **j;
341 19 : std::copy(w.alpha.v.begin(), w.alpha.v.begin() + m + 1, alpha.begin());
342 19 : if (is_odd(m))
343 : {
344 11 : mCRL2log(log::debug) << "\n inc(" << core::detail::print_list(alpha) << ", " << std::to_string(m) << ") = ";
345 11 : inc(alpha, m, m_beta);
346 11 : mCRL2log(log::debug) << (alpha[0] < 0 ? "top" : core::detail::print_list(alpha));
347 : }
348 :
349 19 : if (!std::equal(alpha.begin(), alpha.end(), v.alpha.v.begin()))
350 : {
351 8 : changed = true;
352 8 : v.alpha.v = alpha;
353 8 : mCRL2log(log::debug) << "\nupdate vertex " << print_vertex(v);
354 : }
355 19 : }
356 8 : if (!changed)
357 : {
358 3 : break;
359 : }
360 5 : }
361 3 : mCRL2log(log::debug) << "\n--- vertices ---\n" << print_vertices();
362 3 : return !m_vertices[first_variable].alpha.is_top();
363 : }
364 : };
365 :
366 : inline
367 3 : bool small_progress_measures(pbes& b)
368 : {
369 3 : propositional_variable_instantiation first(b.equations().front().variable().name());
370 3 : assert(b.equations().front().variable().parameters().empty());
371 3 : make_standard_form(b, true);
372 3 : small_progress_measures_algorithm algorithm(b);
373 6 : return algorithm.run(first);
374 3 : }
375 :
376 : } // namespace pbes_system
377 :
378 : } // namespace mcrl2
379 :
380 : #endif // MCRL2_BES_SMALL_PROGRESS_MEASURES_H
|
