Line data Source code
1 : // Author(s): Bas Ploeger
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 liblts_sim.h
10 : /// \brief Header file for the simulation preorder algorithm
11 :
12 : #ifndef LIBLTS_SIM_H
13 : #define LIBLTS_SIM_H
14 : #include "mcrl2/lts/lts_utilities.h"
15 : #include "mcrl2/lts/detail/sim_hashtable.h"
16 : #include "mcrl2/lts/lts_aut.h"
17 : #include "mcrl2/lts/lts_fsm.h"
18 : #include "mcrl2/lts/lts_dot.h"
19 :
20 : namespace mcrl2
21 : {
22 : namespace lts
23 : {
24 : namespace detail
25 : {
26 :
27 : template <class LTS_TYPE>
28 : class sim_partitioner
29 : {
30 : public:
31 : /** Creates a partitioner for an LTS.
32 : * \param[in] l Pointer to the LTS. */
33 : sim_partitioner(LTS_TYPE& l);
34 :
35 : /** Destroys this partitioner. */
36 : ~sim_partitioner();
37 :
38 : /** Computes the simulation equivalence classes and preorder
39 : * relations of the LTS. */
40 : virtual void partitioning_algorithm();
41 :
42 : /** Gives the transition relation on the computed equivalence
43 : * classes of the LTS. The label numbers of the transitions
44 : * correspond to the label numbers of the LTS that was passed as an
45 : * argument to the constructor of this partitioner.
46 : * The state numbers of the transitions are the equivalence class
47 : * numbers which range from 0 upto (and excluding) \ref num_eq_classes().
48 : *
49 : * \pre The simulation equivalence classes have been computed.
50 : * \return A vector containing the transitions between the
51 : * simulation equivalence classes. */
52 : std::vector < mcrl2::lts::transition> get_transitions() const;
53 :
54 : /** Gives the number of simulation equivalence classes of the LTS.
55 : * \pre The simulation equivalence classes have been computed.
56 : * \return The number of simulation equivalence classes of the LTS.
57 : */
58 : std::size_t num_eq_classes() const;
59 :
60 : /** Gives the equivalence class number of a state.
61 : * The equivalence class numbers range from 0 upto (and excluding)
62 : * \ref num_eq_classes().
63 : * \pre The simulation equivalence classes have been computed.
64 : * \param[in] s A state number.
65 : * \return The number of the equivalence class to which \e s
66 : * belongs. */
67 : std::size_t get_eq_class(std::size_t s) const;
68 :
69 : /** Returns whether one state is simulated by another state.
70 : * \pre The simulation preorder has been computed.
71 : * \param[in] s A state number.
72 : * \param[in] t A state number.
73 : * \retval true if \e s is simulated by \e t;
74 : * \retval false otherwise. */
75 : bool in_preorder(std::size_t s,std::size_t t) const;
76 :
77 : /** Returns whether two states are in the same simulation
78 : * equivalence class.
79 : * \pre The simulation equivalence classes have been computed.
80 : * \param[in] s A state number.
81 : * \param[in] t A state number.
82 : * \retval true if \e s and \e t are in the same simulation
83 : * equivalence class;
84 : * \retval false otherwise. */
85 : bool in_same_class(std::size_t s,std::size_t t) const;
86 :
87 : protected:
88 :
89 : /** Computes the simulation equivalence classes and preorder
90 : * relations of the LTS.
91 : * \pre : initialise_datastructures called */
92 : void partitioning_algorithmG();
93 :
94 : struct state_bucket
95 : {
96 : ptrdiff_t next;
97 : ptrdiff_t prev;
98 : };
99 :
100 : LTS_TYPE& aut;
101 : mcrl2::lts::outgoing_transitions_per_state_action_t trans_index;
102 : std::size_t s_Sigma;
103 : std::size_t s_Pi;
104 : std::vector<bool> state_touched;
105 : std::vector<bool> block_touched;
106 : std::vector<state_bucket> state_buckets;
107 : std::vector<std::size_t> block_Pi;
108 : std::vector<std::size_t> parent;
109 : std::vector< std::vector<std::size_t> > children;
110 : std::vector<ptrdiff_t> contents_t;
111 : std::vector<ptrdiff_t> contents_u;
112 : std::vector< std::vector<bool> > stable;
113 : hash_table3* exists;
114 : hash_table3* forall;
115 : std::vector< std::vector<std::size_t> > pre_exists;
116 : std::vector< std::vector<std::size_t> > pre_forall;
117 : hash_table3* match;
118 : std::vector< std::vector<bool> > P;
119 : std::vector< std::vector<bool> > Q;
120 :
121 : /* auxiliary variables */
122 : std::vector<std::size_t> touched_blocks;
123 : std::vector<std::size_t> contents;
124 :
125 : void initialise_datastructures();
126 : //void read_partition_from_file(char *parfile);
127 :
128 : void refine(bool& change);
129 : void update();
130 : //void update_lts();
131 :
132 : void touch(std::size_t a,std::size_t alpha);
133 : void untouch(std::size_t alpha);
134 :
135 : void reverse_topological_sort(std::vector<std::size_t>& Sort);
136 : void dfs_visit(std::size_t u,std::vector<bool>& visited,
137 : std::vector<std::size_t>& Sort);
138 :
139 : void initialise_Sigma(std::size_t gamma,std::size_t l);
140 : void initialise_Pi(std::size_t gamma,std::size_t l);
141 : void filter(std::size_t S,std::vector< std::vector<bool> >& R,bool B);
142 : void cleanup(std::size_t alpha,std::size_t beta);
143 : void initialise_pre_EA();
144 : void induce_P_on_Pi();
145 :
146 : std::string print_Sigma_P();
147 : std::string print_Pi_Q();
148 : std::string print_Sigma();
149 : std::string print_Pi();
150 : std::string print_relation(std::size_t s,std::vector< std::vector<bool> >& R);
151 : std::string print_block(std::size_t b);
152 : std::string print_structure(hash_table3* struc);
153 : std::string print_reverse_topological_sort(const std::vector<std::size_t>& Sort);
154 : };
155 :
156 :
157 : #define LIST_END (-1)
158 : #define UNIVERSAL_PART (0)
159 :
160 : template <class LTS_TYPE>
161 54 : sim_partitioner<LTS_TYPE>::sim_partitioner(LTS_TYPE& l)
162 54 : : aut(l)
163 : {
164 54 : match = new hash_table3(1000);
165 54 : exists = new hash_table3(1000);
166 54 : forall = new hash_table3(1000);
167 54 : }
168 :
169 : template <class LTS_TYPE>
170 54 : sim_partitioner<LTS_TYPE>::~sim_partitioner()
171 : {
172 54 : delete match;
173 54 : delete exists;
174 54 : delete forall;
175 108 : }
176 :
177 : /* ----------------- PARTITIONING ALGORITHM ------------------------- */
178 :
179 : template <class LTS_TYPE>
180 38 : void sim_partitioner<LTS_TYPE>::partitioning_algorithm()
181 : {
182 38 : initialise_datastructures();
183 38 : partitioning_algorithmG();
184 38 : }
185 :
186 : /* Pre : initialise_datastructures called */
187 : template <class LTS_TYPE>
188 54 : void sim_partitioner<LTS_TYPE>::partitioning_algorithmG()
189 : {
190 : using namespace mcrl2::core;
191 :
192 : bool change;
193 : std::size_t i;
194 :
195 54 : refine(change);
196 54 : update();
197 :
198 54 : change = true;
199 54 : i = 0;
200 145 : while (change)
201 : {
202 91 : change = false;
203 :
204 : /* Set Sigma to Pi and P to Q*/
205 91 : s_Sigma = s_Pi;
206 : /* The following statement simultaneously assigns P to Q and Q to P.
207 : * The assignment of Q to P is safe because Q is not used in
208 : * refine() and will be freshly computed at the start of update().
209 : * The advantage of using swap() is that it is executed in constant
210 : * time. */
211 91 : P.swap(Q);
212 :
213 91 : mCRL2log(log::debug) << "--------------------- ITERATION " << i << " ----------------------------------" << std::endl;
214 :
215 91 : mCRL2log(log::debug) << " iteration " << i << "; number of blocks: " << s_Sigma << std::endl;
216 :
217 91 : refine(change);
218 91 : if (change)
219 : {
220 37 : update();
221 : }
222 : else
223 : {
224 : /* No blocks were split by refine(), so update() need not be
225 : * called. However, we do need to swap P and Q again: Q currently
226 : * contains the P-relation of the previous iteration (due to the
227 : * call to swap() prior to the call to refine()) but we want it to
228 : * contain that of the current iteration! */
229 54 : P.swap(Q);
230 : }
231 91 : ++i;
232 : }
233 :
234 54 : if (mCRL2logEnabled(log::debug))
235 : {
236 0 : mCRL2log(log::debug) << print_Pi_Q();
237 : }
238 54 : }
239 :
240 : template <class LTS_TYPE>
241 54 : void sim_partitioner<LTS_TYPE>::initialise_datastructures()
242 : {
243 : // aut.sort_transitions(mcrl2::lts::lbl_tgt_src);
244 : // trans_index = aut.get_transition_pre_table();
245 54 : trans_index=transitions_per_outgoing_state_action_pair_reversed(aut.get_transitions(),aut.hidden_label_set());
246 :
247 54 : std::size_t N = aut.num_states();
248 :
249 54 : state_bucket sb = { LIST_END, LIST_END };
250 54 : state_buckets.assign(N,sb);
251 54 : state_touched.assign(N,false);
252 54 : block_Pi.assign(N,UNIVERSAL_PART);
253 :
254 : /* put all states in one block */
255 54 : s_Pi = 1;
256 54 : contents_u.push_back(UNIVERSAL_PART);
257 54 : contents_t.push_back(LIST_END);
258 666 : for (std::size_t i = 0; i < N; ++i)
259 : {
260 612 : if (i > 0)
261 : {
262 558 : state_buckets[i].prev = i-1;
263 : }
264 : else
265 : {
266 54 : state_buckets[i].prev = LIST_END;
267 : }
268 612 : if (i < N-1)
269 : {
270 558 : state_buckets[i].next = i+1;
271 : }
272 : else
273 : {
274 54 : state_buckets[i].next = LIST_END;
275 : }
276 : }
277 :
278 54 : block_touched.assign(s_Pi,false);
279 54 : s_Sigma = s_Pi;
280 :
281 : /* initialise P and children */
282 54 : std::vector<std::size_t> vi;
283 54 : children.assign(s_Sigma,vi);
284 54 : std::vector<bool> vb(s_Sigma,false);
285 54 : P.assign(s_Sigma,vb);
286 108 : for (std::size_t i = 0; i < s_Sigma; ++i)
287 : {
288 54 : children[i].push_back(i);
289 54 : P[i][i] = true;
290 : }
291 :
292 54 : mCRL2log(log::debug) << "--------------------- INITIALISATION ---------------------------" << std::endl;
293 54 : mCRL2log(log::debug) << " initialisation; number of blocks: " << s_Sigma << std::endl;
294 54 : }
295 :
296 : /* ----------------- INITIALISE ------------------------------------- */
297 :
298 : template <class LTS_TYPE>
299 9482 : void sim_partitioner<LTS_TYPE>::initialise_Pi(std::size_t gamma,std::size_t l)
300 : {
301 : std::size_t alpha, a, c;
302 9482 : std::vector<std::size_t>::iterator ci, last;
303 :
304 9482 : contents.clear();
305 34235 : for (ptrdiff_t i = contents_u[gamma]; i != LIST_END;
306 24753 : i = state_buckets[i].next)
307 : {
308 24753 : contents.push_back(std::size_t(i));
309 : }
310 9711 : for (ptrdiff_t i = contents_t[gamma]; i != LIST_END;
311 229 : i = state_buckets[i].next)
312 : {
313 229 : contents.push_back(std::size_t(i));
314 : }
315 9482 : last = contents.end();
316 34464 : for (ci = contents.begin(); ci != last; ++ci)
317 : {
318 24982 : c = *ci;
319 : /* iterate over the incoming l-transitions of c */
320 : using namespace mcrl2::lts;
321 24982 : for (outgoing_transitions_per_state_action_t::iterator
322 24982 : t=trans_index.lower_bound(std::pair < transition::size_type, transition::size_type >(c,l));
323 30538 : t!=trans_index.upper_bound(std::pair < transition::size_type, transition::size_type >(c,l)); ++t)
324 : {
325 5556 : a = to(t); // As trans_index is reversed, this is actually the state from which the transition t goes.
326 5556 : if (!state_touched[a])
327 : {
328 5154 : alpha = block_Pi[a];
329 5154 : touch(a,alpha);
330 5154 : if (!block_touched[alpha])
331 : {
332 2730 : touched_blocks.push_back(alpha);
333 2730 : block_touched[alpha] = true;
334 : }
335 : }
336 : }
337 : }
338 9482 : }
339 :
340 : template <class LTS_TYPE>
341 5077 : void sim_partitioner<LTS_TYPE>::initialise_Sigma(std::size_t gamma,std::size_t l)
342 : {
343 5077 : std::vector<std::size_t>::iterator deltai, last;
344 5077 : last = children[gamma].end();
345 11848 : for (deltai = children[gamma].begin(); deltai != last; ++deltai)
346 : {
347 6771 : initialise_Pi(*deltai,l);
348 : }
349 5077 : }
350 :
351 : /* ----------------- REFINE ----------------------------------------- */
352 :
353 : /* PRE: s_Sigma = s_Pi */
354 : template <class LTS_TYPE>
355 145 : void sim_partitioner<LTS_TYPE>::refine(bool& change)
356 : {
357 : using namespace mcrl2::core;
358 : /* Initialise the parent and children functions */
359 145 : std::vector<std::size_t> v;
360 145 : children.assign(s_Pi,v);
361 145 : parent.assign(s_Pi,0);
362 : std::size_t alpha;
363 830 : for (alpha = 0; alpha < s_Pi; ++alpha)
364 : {
365 685 : children[alpha].push_back(alpha);
366 685 : parent[alpha] = alpha;
367 : }
368 :
369 145 : if (mCRL2logEnabled(log::debug))
370 : {
371 0 : mCRL2log(log::debug) << "--------------------- Refine ---------------------------------------" << std::endl;
372 0 : mCRL2log(log::debug) << print_Sigma_P();
373 : }
374 :
375 : /* Compute a reverse topological sorting of Sigma w.r.t. P */
376 145 : std::vector<std::size_t> Sort;
377 145 : Sort.reserve(s_Sigma);
378 145 : reverse_topological_sort(Sort);
379 :
380 145 : if (mCRL2logEnabled(log::debug))
381 : {
382 0 : mCRL2log(log::debug) << print_reverse_topological_sort(Sort);
383 : }
384 :
385 : /* Some local variables */
386 145 : std::vector<bool> v_false(s_Sigma,false);
387 145 : std::vector<std::size_t>::iterator alphai, last, gammai;
388 145 : std::vector< std::vector<bool> >::iterator stable_alpha, P_gamma;
389 : bool stable_alpha_gamma;
390 : std::size_t gamma, delta, l;
391 :
392 : /* The main loop */
393 764 : for (l = 0; l < aut.num_action_labels(); ++l)
394 : {
395 619 : mCRL2log(log::debug) << "---------------------------------------------------" << std::endl;
396 619 : mCRL2log(log::debug) << "Label = \"" << mcrl2::lts::pp(aut.action_label(l)) << "\"" << std::endl;
397 :
398 : /* reset the stable function */
399 619 : stable.assign(s_Pi,v_false);
400 :
401 : /* iterate over the reverse topological sorting */
402 3787 : for (gammai = Sort.begin(); gammai != Sort.end(); ++gammai)
403 : {
404 3168 : gamma = *gammai;
405 :
406 3168 : touched_blocks.clear();
407 3168 : initialise_Sigma(gamma,l);
408 :
409 : /* iterate over all alpha such that alpha -l->E gamma */
410 3168 : last = touched_blocks.end();
411 4246 : for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
412 : {
413 1078 : alpha = *alphai;
414 : /* compute stable(alpha,gamma); use a local boolean variable for
415 : * efficiency */
416 1078 : stable_alpha_gamma = false;
417 1078 : stable_alpha = stable.begin() + alpha;
418 1078 : P_gamma = P.begin() + gamma;
419 10462 : for (delta = 0; delta < s_Sigma && !stable_alpha_gamma; ++delta)
420 : {
421 9384 : if ((*stable_alpha)[delta] && (*P_gamma)[delta])
422 : {
423 32 : stable_alpha_gamma = true;
424 : }
425 : }
426 1078 : (*stable_alpha)[gamma] = stable_alpha_gamma;
427 1078 : if (!stable_alpha_gamma)
428 : {
429 : /* if alpha -l->A gamma then alpha cannot be split */
430 1046 : if (contents_u[alpha] != LIST_END)
431 : {
432 : /* split alpha; new block will be s_Pi */
433 195 : change = true;
434 :
435 195 : children[parent[alpha]].push_back(s_Pi);
436 195 : parent.push_back(parent[alpha]);
437 195 : stable.push_back(*stable_alpha);
438 195 : block_touched.push_back(false);
439 195 : contents_t.push_back(LIST_END);
440 :
441 : /* assign the untouched contents of alpha to s_Pi */
442 195 : contents_u.push_back(contents_u[alpha]);
443 195 : contents_u[alpha] = LIST_END;
444 :
445 : /* update the block information for the moved states */
446 1458 : for (ptrdiff_t i = contents_u[s_Pi]; i != LIST_END;
447 1263 : i = state_buckets[i].next)
448 : {
449 1263 : block_Pi[i] = s_Pi;
450 : }
451 195 : ++s_Pi;
452 : }
453 1046 : stable[alpha][gamma] = true;
454 : }
455 1078 : untouch(alpha);
456 : }
457 : }
458 : }
459 145 : }
460 :
461 : template <class LTS_TYPE>
462 145 : void sim_partitioner<LTS_TYPE>::reverse_topological_sort(std::vector<std::size_t>& Sort)
463 : {
464 145 : std::vector<bool> visited(s_Sigma,false);
465 830 : for (std::size_t u = 0; u < s_Sigma; ++u)
466 : {
467 685 : if (!visited[u])
468 : {
469 587 : dfs_visit(u,visited,Sort);
470 : }
471 : }
472 145 : }
473 :
474 : template <class LTS_TYPE>
475 685 : void sim_partitioner<LTS_TYPE>::dfs_visit(std::size_t u,std::vector<bool>& visited,
476 : std::vector<std::size_t> &Sort)
477 : {
478 685 : visited[u] = true;
479 6956 : for (std::size_t v = 0; v < s_Sigma; ++v)
480 : {
481 6271 : if (!visited[v] && P[u][v])
482 : {
483 98 : dfs_visit(v,visited,Sort);
484 : }
485 : }
486 685 : Sort.push_back(u);
487 685 : }
488 :
489 : template <class LTS_TYPE>
490 5154 : void sim_partitioner<LTS_TYPE>::touch(std::size_t a,std::size_t alpha)
491 : {
492 5154 : state_touched[a] = true;
493 5154 : ptrdiff_t p = state_buckets[a].prev;
494 5154 : ptrdiff_t n = state_buckets[a].next;
495 5154 : if (p == LIST_END)
496 : {
497 2865 : contents_u[alpha] = n;
498 : }
499 : else
500 : {
501 2289 : state_buckets[p].next = n;
502 : }
503 5154 : if (n != LIST_END)
504 : {
505 1463 : state_buckets[n].prev = p;
506 : }
507 5154 : state_buckets[a].prev = LIST_END;
508 5154 : state_buckets[a].next = contents_t[alpha];
509 5154 : if (contents_t[alpha] != LIST_END)
510 : {
511 2424 : state_buckets[contents_t[alpha]].prev = a;
512 : }
513 5154 : contents_t[alpha] = a;
514 5154 : }
515 :
516 : /* PRE: contents_t[alpha] != LIST_END */
517 : template <class LTS_TYPE>
518 2730 : void sim_partitioner<LTS_TYPE>::untouch(std::size_t alpha)
519 : {
520 : // search linearly for the last element of contents_t[alpha];
521 : // untouch every state we encounter along the way
522 2730 : ptrdiff_t i = contents_t[alpha];
523 5154 : while (state_buckets[i].next != LIST_END)
524 : {
525 2424 : state_touched[i] = false;
526 2424 : i = state_buckets[i].next;
527 : }
528 : // last element has not been untouched yet
529 2730 : state_touched[i] = false;
530 :
531 : // insert the list contents_t[alpha] at the beginning of
532 : // contents_u[alpha]
533 2730 : state_buckets[i].next = contents_u[alpha];
534 2730 : if (contents_u[alpha] != LIST_END)
535 : {
536 125 : state_buckets[contents_u[alpha]].prev = i;
537 : }
538 2730 : contents_u[alpha] = contents_t[alpha];
539 2730 : contents_t[alpha] = LIST_END;
540 2730 : block_touched[alpha] = false;
541 2730 : }
542 :
543 : /* ----------------- UPDATE ----------------------------------------- */
544 :
545 : template <class LTS_TYPE>
546 91 : void sim_partitioner<LTS_TYPE>::update()
547 : {
548 : using namespace mcrl2::core;
549 91 : mCRL2log(log::debug) << "--------------------- Update ---------------------------------------" << std::endl;
550 :
551 : std::size_t l,alpha,gamma;
552 91 : std::vector<std::size_t>::iterator alphai, last;
553 :
554 91 : induce_P_on_Pi();
555 :
556 91 : initialise_pre_EA();
557 :
558 : /* Compute the pre_exists and pre_forall functions */
559 485 : for (l = 0; l < aut.num_action_labels(); ++l)
560 : {
561 394 : pre_exists[l].reserve(s_Sigma + 1);
562 394 : pre_forall[l].reserve(s_Sigma + 1);
563 394 : pre_exists[l].push_back(exists->get_num_elements());
564 394 : pre_forall[l].push_back(forall->get_num_elements());
565 2175 : for (gamma = 0; gamma < s_Sigma; ++gamma)
566 : {
567 1781 : touched_blocks.clear();
568 1781 : initialise_Sigma(gamma,l);
569 1781 : last = touched_blocks.end();
570 2501 : for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
571 : {
572 720 : alpha = *alphai;
573 720 : exists->add(alpha,l,gamma);
574 720 : if (contents_u[alpha] == LIST_END)
575 : {
576 714 : forall->add(alpha,l,gamma);
577 : }
578 720 : untouch(alpha);
579 : }
580 1781 : pre_exists[l].push_back(exists->get_num_elements());
581 1781 : pre_forall[l].push_back(forall->get_num_elements());
582 : }
583 : }
584 :
585 91 : mCRL2log(log::debug) << "------ Filter(false) ------\nExists: ";
586 91 : mCRL2log(log::debug) << print_structure(exists);
587 91 : mCRL2log(log::debug) << "\nForall: ";
588 91 : mCRL2log(log::debug) << print_structure(forall);
589 91 : mCRL2log(log::debug) << "\nSimulation relation: ";
590 91 : mCRL2log(log::debug) << print_relation(s_Pi,Q);
591 :
592 : /* Apply the first filtering to Q */
593 91 : filter(s_Sigma,P,false);
594 :
595 :
596 91 : initialise_pre_EA();
597 :
598 : /* Compute the pre_exists and pre_forall functions */
599 485 : for (l = 0; l < aut.num_action_labels(); ++l)
600 : {
601 394 : pre_exists[l].reserve(s_Pi + 1);
602 394 : pre_forall[l].reserve(s_Pi + 1);
603 394 : pre_exists[l].push_back(exists->get_num_elements());
604 394 : pre_forall[l].push_back(forall->get_num_elements());
605 3105 : for (gamma = 0; gamma < s_Pi; ++gamma)
606 : {
607 2711 : touched_blocks.clear();
608 2711 : initialise_Pi(gamma,l);
609 2711 : last = touched_blocks.end();
610 3508 : for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
611 : {
612 797 : alpha = *alphai;
613 797 : exists->add(alpha,l,gamma);
614 797 : if (contents_u[alpha] == LIST_END)
615 : {
616 684 : forall->add(alpha,l,gamma);
617 : }
618 797 : untouch(alpha);
619 : }
620 2711 : pre_exists[l].push_back(exists->get_num_elements());
621 2711 : pre_forall[l].push_back(forall->get_num_elements());
622 : }
623 : }
624 :
625 91 : mCRL2log(log::debug) << "------ Filter(true) ------\nExists: ";
626 91 : mCRL2log(log::debug) << print_structure(exists);
627 91 : mCRL2log(log::debug) << "\nForall: ";
628 91 : mCRL2log(log::debug) << print_structure(forall);
629 91 : mCRL2log(log::debug) << "\nSimulation relation: ";
630 91 : mCRL2log(log::debug) << print_relation(s_Pi,Q);
631 :
632 : /* Apply the second filtering to Q */
633 91 : filter(s_Pi,Q,true);
634 91 : }
635 :
636 : template <class LTS_TYPE>
637 182 : void sim_partitioner<LTS_TYPE>::initialise_pre_EA()
638 : {
639 : /* Initialise the pre_exists and pre_forall data structures */
640 182 : exists->clear();
641 182 : forall->clear();
642 182 : std::vector<std::size_t> v;
643 182 : pre_exists.assign(aut.num_action_labels(),v);
644 182 : pre_forall.assign(aut.num_action_labels(),v);
645 182 : }
646 :
647 : template <class LTS_TYPE>
648 107 : void sim_partitioner<LTS_TYPE>::induce_P_on_Pi()
649 : {
650 : /* Compute the relation induced on Pi by P, store it in Q */
651 107 : std::vector<bool> v(s_Pi,false);
652 107 : Q.assign(s_Pi,v);
653 :
654 : std::size_t alpha,beta;
655 107 : std::vector< std::vector<bool> >::iterator P_parent_alpha;
656 754 : for (alpha = 0; alpha < s_Pi; ++alpha)
657 : {
658 647 : P_parent_alpha = P.begin() + parent[alpha];
659 6880 : for (beta = 0; beta < s_Pi; ++beta)
660 : {
661 6233 : Q[alpha][beta] = (*P_parent_alpha)[parent[beta]];
662 : }
663 : }
664 107 : }
665 :
666 :
667 : /* ----------------- FILTER ----------------------------------------- */
668 :
669 : template <class LTS_TYPE>
670 182 : void sim_partitioner<LTS_TYPE>::filter(std::size_t S,std::vector< std::vector<bool> > &R,
671 : bool B)
672 : {
673 : /* Initialise the match function */
674 182 : match->clear();
675 :
676 : std::size_t alpha,beta,gamma,delta,l;
677 182 : hash_table3_iterator etrans(exists);
678 970 : for (l = 0; l < aut.num_action_labels(); ++l)
679 : {
680 5280 : for (delta = 0; delta < S; ++delta)
681 : {
682 4492 : etrans.set_end(pre_exists[l][delta+1]);
683 6009 : for (etrans.set(pre_exists[l][delta]); !etrans.is_end(); ++etrans)
684 : {
685 1517 : beta = etrans.get_x();
686 15998 : for (gamma = 0; gamma < S; ++gamma)
687 : {
688 14481 : if (R[gamma][delta])
689 : {
690 2510 : match->add(l,beta,gamma);
691 : }
692 : }
693 : }
694 : }
695 : }
696 :
697 182 : hash_table3_iterator atrans(forall);
698 : /* The main for loop */
699 970 : for (l = 0; l < aut.num_action_labels(); ++l)
700 : {
701 5280 : for (gamma = 0; gamma < S; ++gamma)
702 : {
703 4492 : atrans.set_end(pre_forall[l][gamma+1]);
704 5890 : for (atrans.set(pre_forall[l][gamma]); !atrans.is_end(); ++atrans)
705 : {
706 1398 : alpha = atrans.get_x();
707 16898 : for (beta = 0; beta < s_Pi; ++beta)
708 : {
709 15500 : if (Q[alpha][beta] && !match->find(l,beta,gamma))
710 : {
711 1047 : Q[alpha][beta] = false;
712 1047 : if (B)
713 : {
714 20 : cleanup(alpha,beta);
715 : }
716 : }
717 : }
718 : }
719 : }
720 : }
721 182 : }
722 :
723 : /* ----------------- CLEANUP ---------------------------------------- */
724 :
725 : template <class LTS_TYPE>
726 28 : void sim_partitioner<LTS_TYPE>::cleanup(std::size_t alpha,std::size_t beta)
727 : {
728 : std::size_t l,alpha1,beta1,delta;
729 : bool match_l_beta1_alpha;
730 28 : hash_table3_iterator alpha1i(forall);
731 28 : hash_table3_iterator beta1i(exists);
732 203 : for (l = 0; l < aut.num_action_labels(); ++l)
733 : {
734 175 : alpha1i.set_end(pre_forall[l][alpha+1]);
735 175 : beta1i.set_end(pre_exists[l][beta+1]);
736 204 : for (beta1i.set(pre_exists[l][beta]); !beta1i.is_end(); ++beta1i)
737 : {
738 29 : beta1 = beta1i.get_x();
739 29 : match_l_beta1_alpha = false;
740 843 : for (delta = 0; delta < s_Pi && !match_l_beta1_alpha; ++delta)
741 : {
742 814 : if (exists->find(beta1,l,delta) && Q[alpha][delta])
743 : {
744 1 : match_l_beta1_alpha = true;
745 : }
746 : }
747 29 : if (!match_l_beta1_alpha)
748 : {
749 28 : match->remove(l,beta1,alpha);
750 43 : for (alpha1i.set(pre_forall[l][alpha]); !alpha1i.is_end();
751 15 : ++alpha1i)
752 : {
753 15 : alpha1 = alpha1i.get_x();
754 15 : if (Q[alpha1][beta1])
755 : {
756 8 : Q[alpha1][beta1] = false;
757 8 : cleanup(alpha1,beta1);
758 : }
759 : }
760 : }
761 : }
762 : }
763 28 : }
764 :
765 : /* ----------------- FOR POST-PROCESSING ---------------------------- */
766 :
767 : template <class LTS_TYPE>
768 5 : std::vector < mcrl2::lts::transition> sim_partitioner<LTS_TYPE>::get_transitions() const
769 : {
770 : using namespace mcrl2::lts;
771 :
772 5 : std::vector < mcrl2::lts::transition> ts;
773 5 : ts.reserve(forall->get_num_elements());
774 :
775 5 : std::vector<bool> pre_sim;
776 : transition::size_type l,beta,gamma;
777 5 : hash_table3_iterator alphai(exists);
778 5 : hash_table3_iterator gammai(forall);
779 65 : for (beta = 0; beta < s_Pi; ++beta)
780 : {
781 409 : for (l = 0; l < aut.num_action_labels(); ++l)
782 : {
783 : // there is an l-transition from alpha to beta iff:
784 : // - alpha -l->A [beta]
785 : // - not Exists gamma : beta Q gamma /\ alpha -l->E gamma
786 : // first compute for which alpha the latter statement does not
787 : // hold
788 349 : pre_sim.assign(s_Pi,false);
789 9978 : for (gamma = 0; gamma < s_Pi; ++gamma)
790 : {
791 : // only consider gammas that are unequal to beta
792 9629 : if (gamma != beta && Q[beta][gamma])
793 : {
794 49 : alphai.set_end(pre_exists[l][gamma+1]);
795 62 : for (alphai.set(pre_exists[l][gamma]); !alphai.is_end();
796 13 : ++alphai)
797 : {
798 13 : pre_sim[alphai.get_x()] = true;
799 : }
800 : }
801 : }
802 349 : gammai.set_end(pre_forall[l][beta+1]);
803 434 : for (gammai.set(pre_forall[l][beta]); !gammai.is_end(); ++gammai)
804 : {
805 85 : gamma = gammai.get_x();
806 85 : if (!pre_sim[gamma])
807 : {
808 : // add the transition gamma -l-> beta
809 83 : ts.push_back(transition(gamma,l,beta));
810 : }
811 : }
812 : }
813 : }
814 10 : return ts;
815 5 : }
816 :
817 : template <class LTS_TYPE>
818 5 : std::size_t sim_partitioner<LTS_TYPE>::num_eq_classes() const
819 : {
820 5 : return s_Pi;
821 : }
822 :
823 : template <class LTS_TYPE>
824 5 : std::size_t sim_partitioner<LTS_TYPE>::get_eq_class(std::size_t s) const
825 : {
826 5 : return block_Pi[s];
827 : }
828 :
829 : template <class LTS_TYPE>
830 33 : bool sim_partitioner<LTS_TYPE>::in_preorder(std::size_t s,std::size_t t) const
831 : {
832 33 : return Q[block_Pi[s]][block_Pi[t]];
833 : }
834 :
835 : template <class LTS_TYPE>
836 16 : bool sim_partitioner<LTS_TYPE>::in_same_class(std::size_t s,std::size_t t) const
837 : {
838 16 : return (block_Pi[s] == block_Pi[t]);
839 : }
840 :
841 : /*
842 : // PRE: FORALL and EXISTS structures on Pi are computed
843 : void sim_partitione<LTS_TYPE>r::update_nfa()
844 : {
845 : std::vector< std::vector<std::size_t> > v(s_Pi);
846 : std::vector< std::vector< std::vector<std::size_t> > > post_trans(L,v);
847 :
848 : std::vector<bool> pre_sim;
849 : std::size_t l,beta,alpha,gamma;
850 : hash_table3_iterator alphai(exists);
851 : hash_table3_iterator gammai(forall);
852 : for (beta = 0; beta < s_Pi; ++beta)
853 : {
854 : for (l = 0; l < aut.num_action_labels(); ++l)
855 : {
856 : // there is an l-transition from alpha to beta iff:
857 : // - alpha -l->A [beta]
858 : // - not Exists gamma : beta Q gamma /\ alpha -l->E gamma
859 : // first compute for which alpha the latter statement does not
860 : // hold
861 : pre_sim.assign(s_Pi,false);
862 : for (gamma = 0; gamma < s_Pi; ++gamma)
863 : {
864 : // only consider gammas that are unequal to beta
865 : if (gamma != beta && Q[beta][gamma])
866 : {
867 : alphai.set_end(pre_exists[l][gamma+1]);
868 : for (alphai.set(pre_exists[l][gamma]); !alphai.is_end();
869 : ++alphai)
870 : {
871 : pre_sim[alphai.get_x()] = true;
872 : }
873 : }
874 : }
875 : gammai.set_end(pre_forall[l][beta+1]);
876 : for (gammai.set(pre_forall[l][beta]); !gammai.is_end(); ++gammai)
877 : {
878 : gamma = gammai.get_x();
879 : if (!pre_sim[gamma])
880 : {
881 : post_trans[l][gamma].push_back(beta);
882 : }
883 : }
884 : }
885 : }
886 :
887 : std::vector<transition> *trans = new std::vector<transition> ();
888 : std::vector<bool> *final = new std::vector<bool> ();
889 :
890 : // Do a breadth first search over the computed graph to assign ids to
891 : // the reachable blocks and construct the final transition relation
892 : std::vector<std::size_t>::iterator post_it,post_last;
893 : std::queue<std::size_t> todo;
894 : std::vector<std::size_t> block_id(s_Pi,s_Pi);
895 : todo.push(block_Pi[aut.initial_state()]);
896 : block_id[block_Pi[aut.initial_state()]] = 0;
897 : std::size_t n_s = 1;
898 : std::size_t n_f = 0;
899 : if (aut.is_final(aut.initial_state()))
900 : {
901 : final->push_back(true);
902 : ++n_f;
903 : }
904 : else
905 : {
906 : final->push_back(false);
907 : }
908 : while (!todo.empty())
909 : {
910 : // visit todo.front()
911 : beta = todo.front();
912 : for (l = 0; l < L; ++l)
913 : {
914 : post_last = post_trans[l][beta].end();
915 : for (post_it = post_trans[l][beta].begin(); post_it != post_last;
916 : ++post_it)
917 : {
918 : alpha = *post_it;
919 : if (block_id[alpha] == s_Pi)
920 : {
921 : todo.push(alpha);
922 : block_id[alpha] = n_s;
923 : ++n_s;
924 : if (aut.is_final(contents_u[alpha]))
925 : {
926 : final->push_back(true);
927 : ++n_f;
928 : }
929 : else
930 : {
931 : final->push_back(false);
932 : }
933 : }
934 : transition t = {block_id[beta], l, block_id[alpha]};
935 : trans->push_back(t);
936 : }
937 : }
938 : todo.pop();
939 : }
940 :
941 : // assign the new transition relation to aut
942 : aut.clear_transition_relation();
943 : aut.clear_final();
944 : aut.set_num_states(n_s);
945 : aut.set_num_transitions(trans->size());
946 : aut.set_num_final(n_f);
947 : aut.set_init(0);
948 : aut.set_trans(trans);
949 : aut.set_final(final);
950 :
951 : // assign the simulation relation to aut
952 : aut.init_simulation_relation();
953 : for (beta = 0; beta < s_Pi; ++beta)
954 : {
955 : // only consider reachable blocks
956 : if (block_id[beta] < s_Pi)
957 : {
958 : for (gamma = 0; gamma < s_Pi; ++gamma)
959 : {
960 : if (block_id[gamma] < s_Pi && Q[beta][gamma])
961 : {
962 : aut.add_simulation(block_id[beta],block_id[gamma]);
963 : }
964 : }
965 : }
966 : }
967 : }
968 : */
969 :
970 : /* ----------------- FOR DEBUGGING ---------------------------------- */
971 :
972 : template <class LTS_TYPE>
973 0 : std::string sim_partitioner<LTS_TYPE>::print_Sigma_P()
974 : {
975 : using namespace mcrl2::core;
976 0 : std::stringstream result;
977 0 : result << print_Sigma() << "Simulation relation: " << print_relation(s_Sigma,P);
978 0 : return result.str();
979 0 : }
980 :
981 : template <class LTS_TYPE>
982 0 : std::string sim_partitioner<LTS_TYPE>::print_Pi_Q()
983 : {
984 : using namespace mcrl2::core;
985 0 : std::stringstream result;
986 0 : result << print_Pi() << "Simulation relation: " << print_relation(s_Pi,Q);
987 0 : return result.str();
988 0 : }
989 :
990 : template <class LTS_TYPE>
991 0 : std::string sim_partitioner<LTS_TYPE>::print_Sigma()
992 : {
993 : using namespace mcrl2::core;
994 0 : std::stringstream result;
995 0 : std::vector<std::size_t>::iterator ci, last;
996 0 : for (std::size_t b = 0; b < s_Sigma; ++b)
997 : {
998 0 : result << "block " << b << ": {";
999 0 : last = children[b].end();
1000 0 : for (ci = children[b].begin(); ci != last; ++ci)
1001 : {
1002 0 : result << print_block(*ci);
1003 : }
1004 0 : result << "}" << std::endl;
1005 : }
1006 0 : return result.str();
1007 0 : }
1008 :
1009 : template <class LTS_TYPE>
1010 0 : std::string sim_partitioner<LTS_TYPE>::print_Pi()
1011 : {
1012 0 : std::stringstream result;
1013 : using namespace mcrl2::core;
1014 0 : for (std::size_t b = 0; b < s_Pi; ++b)
1015 : {
1016 0 : result << "block " << b << ": {" << print_block(b) << "}" << std::endl;
1017 : }
1018 0 : return result.str();
1019 0 : }
1020 :
1021 : template <class LTS_TYPE>
1022 0 : std::string sim_partitioner<LTS_TYPE>::print_block(std::size_t b)
1023 : {
1024 0 : std::stringstream result;
1025 : using namespace mcrl2::core;
1026 0 : for (ptrdiff_t i = contents_u[b]; i != LIST_END; i = state_buckets[i].next)
1027 : {
1028 0 : result << i << ",";
1029 : }
1030 0 : for (ptrdiff_t i = contents_t[b]; i != LIST_END; i = state_buckets[i].next)
1031 : {
1032 0 : result << i << ",";
1033 : }
1034 0 : return result.str();
1035 0 : }
1036 :
1037 : template <class LTS_TYPE>
1038 0 : std::string sim_partitioner<LTS_TYPE>::print_relation(std::size_t s,
1039 : std::vector< std::vector<bool> > &R)
1040 : {
1041 : using namespace mcrl2::core;
1042 0 : std::stringstream result;
1043 0 : result << "{";
1044 : std::size_t beta,gamma;
1045 0 : for (beta = 0; beta < s; ++beta)
1046 : {
1047 0 : for (gamma = 0; gamma < s; ++gamma)
1048 : {
1049 0 : if (R[beta][gamma])
1050 : {
1051 0 : result << "(" << beta << "," << gamma << "),";
1052 : }
1053 : }
1054 : }
1055 0 : result << "}" << std::endl;
1056 0 : return result.str();
1057 0 : }
1058 :
1059 : template <class LTS_TYPE>
1060 0 : std::string sim_partitioner<LTS_TYPE>::print_structure(hash_table3* struc)
1061 : {
1062 : using namespace mcrl2::core;
1063 0 : std::stringstream result;
1064 0 : result << "{";
1065 0 : hash_table3_iterator i(struc);
1066 0 : for (; !i.is_end(); ++i)
1067 : {
1068 0 : result << "(" << i.get_x() << "," << mcrl2::lts::pp(aut.action_label(i.get_y()))
1069 0 : << "," << i.get_z() << "),";
1070 : }
1071 0 : result << "}";
1072 0 : return result.str();
1073 0 : }
1074 :
1075 : template <class LTS_TYPE>
1076 0 : std::string sim_partitioner<LTS_TYPE>::print_reverse_topological_sort(const std::vector<std::size_t> &Sort)
1077 : {
1078 : using namespace mcrl2::core;
1079 0 : std::stringstream result;
1080 0 : result << "reverse topological sort is: [";
1081 0 : for (std::size_t i = 0; i < Sort.size(); ++i)
1082 : {
1083 0 : result << Sort[i];
1084 0 : if (i+1 < Sort.size())
1085 : {
1086 0 : result << ",";
1087 : }
1088 : }
1089 0 : result << "]" << std::endl;
1090 0 : return result.str();
1091 0 : }
1092 :
1093 :
1094 : } // namespace detail
1095 : } // namespace lts
1096 : } // namespace mcrl2
1097 : #endif
|
