mCRL2
Loading...
Searching...
No Matches
liblts_sim.h
Go to the documentation of this file.
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//
11
12#ifndef LIBLTS_SIM_H
13#define LIBLTS_SIM_H
16#include "mcrl2/lts/lts_aut.h"
17#include "mcrl2/lts/lts_fsm.h"
18#include "mcrl2/lts/lts_dot.h"
19
20namespace mcrl2
21{
22namespace lts
23{
24namespace detail
25{
26
27template <class LTS_TYPE>
29{
30 public:
33 sim_partitioner(LTS_TYPE& l);
34
37
40 virtual void partitioning_algorithm();
41
52 std::vector < mcrl2::lts::transition> get_transitions() const;
53
58 std::size_t num_eq_classes() const;
59
67 std::size_t get_eq_class(std::size_t s) const;
68
75 bool in_preorder(std::size_t s,std::size_t t) const;
76
85 bool in_same_class(std::size_t s,std::size_t t) const;
86
87 protected:
88
93
95 {
96 ptrdiff_t next;
97 ptrdiff_t prev;
98 };
99
100 LTS_TYPE& aut;
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;
115 std::vector< std::vector<std::size_t> > pre_exists;
116 std::vector< std::vector<std::size_t> > pre_forall;
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
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
160template <class LTS_TYPE>
162 : aut(l)
163{
164 match = new hash_table3(1000);
165 exists = new hash_table3(1000);
166 forall = new hash_table3(1000);
167}
168
169template <class LTS_TYPE>
171{
172 delete match;
173 delete exists;
174 delete forall;
175}
176
177/* ----------------- PARTITIONING ALGORITHM ------------------------- */
178
179template <class LTS_TYPE>
181{
182 initialise_datastructures();
183 partitioning_algorithmG();
184}
185
186/* Pre : initialise_datastructures called */
187template <class LTS_TYPE>
189{
190 using namespace mcrl2::core;
191
192 bool change;
193 std::size_t i;
194
195 refine(change);
196 update();
197
198 change = true;
199 i = 0;
200 while (change)
201 {
202 change = false;
203
204 /* Set Sigma to Pi and P to Q*/
205 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 P.swap(Q);
212
213 mCRL2log(log::debug) << "--------------------- ITERATION " << i << " ----------------------------------" << std::endl;
214
215 mCRL2log(log::debug) << " iteration " << i << "; number of blocks: " << s_Sigma << std::endl;
216
217 refine(change);
218 if (change)
219 {
220 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 P.swap(Q);
230 }
231 ++i;
232 }
233
234 if (mCRL2logEnabled(log::debug))
235 {
236 mCRL2log(log::debug) << print_Pi_Q();
237 }
238}
239
240template <class LTS_TYPE>
242{
243 // aut.sort_transitions(mcrl2::lts::lbl_tgt_src);
244 // trans_index = aut.get_transition_pre_table();
245 trans_index=transitions_per_outgoing_state_action_pair_reversed(aut.get_transitions(),aut.hidden_label_set());
246
247 std::size_t N = aut.num_states();
248
250 state_buckets.assign(N,sb);
251 state_touched.assign(N,false);
252 block_Pi.assign(N,UNIVERSAL_PART);
253
254 /* put all states in one block */
255 s_Pi = 1;
256 contents_u.push_back(UNIVERSAL_PART);
257 contents_t.push_back(LIST_END);
258 for (std::size_t i = 0; i < N; ++i)
259 {
260 if (i > 0)
261 {
262 state_buckets[i].prev = i-1;
263 }
264 else
265 {
266 state_buckets[i].prev = LIST_END;
267 }
268 if (i < N-1)
269 {
270 state_buckets[i].next = i+1;
271 }
272 else
273 {
274 state_buckets[i].next = LIST_END;
275 }
276 }
277
278 block_touched.assign(s_Pi,false);
279 s_Sigma = s_Pi;
280
281 /* initialise P and children */
282 std::vector<std::size_t> vi;
283 children.assign(s_Sigma,vi);
284 std::vector<bool> vb(s_Sigma,false);
285 P.assign(s_Sigma,vb);
286 for (std::size_t i = 0; i < s_Sigma; ++i)
287 {
288 children[i].push_back(i);
289 P[i][i] = true;
290 }
291
292 mCRL2log(log::debug) << "--------------------- INITIALISATION ---------------------------" << std::endl;
293 mCRL2log(log::debug) << " initialisation; number of blocks: " << s_Sigma << std::endl;
294}
295
296/* ----------------- INITIALISE ------------------------------------- */
297
298template <class LTS_TYPE>
299void sim_partitioner<LTS_TYPE>::initialise_Pi(std::size_t gamma,std::size_t l)
300{
301 std::size_t alpha, a, c;
302 std::vector<std::size_t>::iterator ci, last;
303
304 contents.clear();
305 for (ptrdiff_t i = contents_u[gamma]; i != LIST_END;
306 i = state_buckets[i].next)
307 {
308 contents.push_back(std::size_t(i));
309 }
310 for (ptrdiff_t i = contents_t[gamma]; i != LIST_END;
311 i = state_buckets[i].next)
312 {
313 contents.push_back(std::size_t(i));
314 }
315 last = contents.end();
316 for (ci = contents.begin(); ci != last; ++ci)
317 {
318 c = *ci;
319 /* iterate over the incoming l-transitions of c */
320 using namespace mcrl2::lts;
321 for (outgoing_transitions_per_state_action_t::iterator
322 t=trans_index.lower_bound(std::pair < transition::size_type, transition::size_type >(c,l));
323 t!=trans_index.upper_bound(std::pair < transition::size_type, transition::size_type >(c,l)); ++t)
324 {
325 a = to(t); // As trans_index is reversed, this is actually the state from which the transition t goes.
326 if (!state_touched[a])
327 {
328 alpha = block_Pi[a];
329 touch(a,alpha);
330 if (!block_touched[alpha])
331 {
332 touched_blocks.push_back(alpha);
333 block_touched[alpha] = true;
334 }
335 }
336 }
337 }
338}
339
340template <class LTS_TYPE>
341void sim_partitioner<LTS_TYPE>::initialise_Sigma(std::size_t gamma,std::size_t l)
342{
343 std::vector<std::size_t>::iterator deltai, last;
344 last = children[gamma].end();
345 for (deltai = children[gamma].begin(); deltai != last; ++deltai)
346 {
347 initialise_Pi(*deltai,l);
348 }
349}
350
351/* ----------------- REFINE ----------------------------------------- */
352
353/* PRE: s_Sigma = s_Pi */
354template <class LTS_TYPE>
356{
357 using namespace mcrl2::core;
358 /* Initialise the parent and children functions */
359 std::vector<std::size_t> v;
360 children.assign(s_Pi,v);
361 parent.assign(s_Pi,0);
362 std::size_t alpha;
363 for (alpha = 0; alpha < s_Pi; ++alpha)
364 {
365 children[alpha].push_back(alpha);
366 parent[alpha] = alpha;
367 }
368
369 if (mCRL2logEnabled(log::debug))
370 {
371 mCRL2log(log::debug) << "--------------------- Refine ---------------------------------------" << std::endl;
372 mCRL2log(log::debug) << print_Sigma_P();
373 }
374
375 /* Compute a reverse topological sorting of Sigma w.r.t. P */
376 std::vector<std::size_t> Sort;
377 Sort.reserve(s_Sigma);
378 reverse_topological_sort(Sort);
379
380 if (mCRL2logEnabled(log::debug))
381 {
382 mCRL2log(log::debug) << print_reverse_topological_sort(Sort);
383 }
384
385 /* Some local variables */
386 std::vector<bool> v_false(s_Sigma,false);
387 std::vector<std::size_t>::iterator alphai, last, gammai;
388 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 for (l = 0; l < aut.num_action_labels(); ++l)
394 {
395 mCRL2log(log::debug) << "---------------------------------------------------" << std::endl;
396 mCRL2log(log::debug) << "Label = \"" << mcrl2::lts::pp(aut.action_label(l)) << "\"" << std::endl;
397
398 /* reset the stable function */
399 stable.assign(s_Pi,v_false);
400
401 /* iterate over the reverse topological sorting */
402 for (gammai = Sort.begin(); gammai != Sort.end(); ++gammai)
403 {
404 gamma = *gammai;
405
406 touched_blocks.clear();
407 initialise_Sigma(gamma,l);
408
409 /* iterate over all alpha such that alpha -l->E gamma */
410 last = touched_blocks.end();
411 for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
412 {
413 alpha = *alphai;
414 /* compute stable(alpha,gamma); use a local boolean variable for
415 * efficiency */
416 stable_alpha_gamma = false;
417 stable_alpha = stable.begin() + alpha;
418 P_gamma = P.begin() + gamma;
419 for (delta = 0; delta < s_Sigma && !stable_alpha_gamma; ++delta)
420 {
421 if ((*stable_alpha)[delta] && (*P_gamma)[delta])
422 {
423 stable_alpha_gamma = true;
424 }
425 }
426 (*stable_alpha)[gamma] = stable_alpha_gamma;
427 if (!stable_alpha_gamma)
428 {
429 /* if alpha -l->A gamma then alpha cannot be split */
430 if (contents_u[alpha] != LIST_END)
431 {
432 /* split alpha; new block will be s_Pi */
433 change = true;
434
435 children[parent[alpha]].push_back(s_Pi);
436 parent.push_back(parent[alpha]);
437 stable.push_back(*stable_alpha);
438 block_touched.push_back(false);
439 contents_t.push_back(LIST_END);
440
441 /* assign the untouched contents of alpha to s_Pi */
442 contents_u.push_back(contents_u[alpha]);
443 contents_u[alpha] = LIST_END;
444
445 /* update the block information for the moved states */
446 for (ptrdiff_t i = contents_u[s_Pi]; i != LIST_END;
447 i = state_buckets[i].next)
448 {
449 block_Pi[i] = s_Pi;
450 }
451 ++s_Pi;
452 }
453 stable[alpha][gamma] = true;
454 }
455 untouch(alpha);
456 }
457 }
458 }
459}
460
461template <class LTS_TYPE>
462void sim_partitioner<LTS_TYPE>::reverse_topological_sort(std::vector<std::size_t>& Sort)
463{
464 std::vector<bool> visited(s_Sigma,false);
465 for (std::size_t u = 0; u < s_Sigma; ++u)
466 {
467 if (!visited[u])
468 {
469 dfs_visit(u,visited,Sort);
470 }
471 }
472}
473
474template <class LTS_TYPE>
475void sim_partitioner<LTS_TYPE>::dfs_visit(std::size_t u,std::vector<bool>& visited,
476 std::vector<std::size_t> &Sort)
477{
478 visited[u] = true;
479 for (std::size_t v = 0; v < s_Sigma; ++v)
480 {
481 if (!visited[v] && P[u][v])
482 {
483 dfs_visit(v,visited,Sort);
484 }
485 }
486 Sort.push_back(u);
487}
488
489template <class LTS_TYPE>
490void sim_partitioner<LTS_TYPE>::touch(std::size_t a,std::size_t alpha)
491{
492 state_touched[a] = true;
493 ptrdiff_t p = state_buckets[a].prev;
494 ptrdiff_t n = state_buckets[a].next;
495 if (p == LIST_END)
496 {
497 contents_u[alpha] = n;
498 }
499 else
500 {
501 state_buckets[p].next = n;
502 }
503 if (n != LIST_END)
504 {
505 state_buckets[n].prev = p;
506 }
507 state_buckets[a].prev = LIST_END;
508 state_buckets[a].next = contents_t[alpha];
509 if (contents_t[alpha] != LIST_END)
510 {
511 state_buckets[contents_t[alpha]].prev = a;
512 }
513 contents_t[alpha] = a;
514}
515
516/* PRE: contents_t[alpha] != LIST_END */
517template <class LTS_TYPE>
519{
520 // search linearly for the last element of contents_t[alpha];
521 // untouch every state we encounter along the way
522 ptrdiff_t i = contents_t[alpha];
523 while (state_buckets[i].next != LIST_END)
524 {
525 state_touched[i] = false;
526 i = state_buckets[i].next;
527 }
528 // last element has not been untouched yet
529 state_touched[i] = false;
530
531 // insert the list contents_t[alpha] at the beginning of
532 // contents_u[alpha]
533 state_buckets[i].next = contents_u[alpha];
534 if (contents_u[alpha] != LIST_END)
535 {
536 state_buckets[contents_u[alpha]].prev = i;
537 }
538 contents_u[alpha] = contents_t[alpha];
539 contents_t[alpha] = LIST_END;
540 block_touched[alpha] = false;
541}
542
543/* ----------------- UPDATE ----------------------------------------- */
544
545template <class LTS_TYPE>
547{
548 using namespace mcrl2::core;
549 mCRL2log(log::debug) << "--------------------- Update ---------------------------------------" << std::endl;
550
551 std::size_t l,alpha,gamma;
552 std::vector<std::size_t>::iterator alphai, last;
553
554 induce_P_on_Pi();
555
556 initialise_pre_EA();
557
558 /* Compute the pre_exists and pre_forall functions */
559 for (l = 0; l < aut.num_action_labels(); ++l)
560 {
561 pre_exists[l].reserve(s_Sigma + 1);
562 pre_forall[l].reserve(s_Sigma + 1);
563 pre_exists[l].push_back(exists->get_num_elements());
564 pre_forall[l].push_back(forall->get_num_elements());
565 for (gamma = 0; gamma < s_Sigma; ++gamma)
566 {
567 touched_blocks.clear();
568 initialise_Sigma(gamma,l);
569 last = touched_blocks.end();
570 for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
571 {
572 alpha = *alphai;
573 exists->add(alpha,l,gamma);
574 if (contents_u[alpha] == LIST_END)
575 {
576 forall->add(alpha,l,gamma);
577 }
578 untouch(alpha);
579 }
580 pre_exists[l].push_back(exists->get_num_elements());
581 pre_forall[l].push_back(forall->get_num_elements());
582 }
583 }
584
585 mCRL2log(log::debug) << "------ Filter(false) ------\nExists: ";
586 mCRL2log(log::debug) << print_structure(exists);
587 mCRL2log(log::debug) << "\nForall: ";
588 mCRL2log(log::debug) << print_structure(forall);
589 mCRL2log(log::debug) << "\nSimulation relation: ";
590 mCRL2log(log::debug) << print_relation(s_Pi,Q);
591
592 /* Apply the first filtering to Q */
593 filter(s_Sigma,P,false);
594
595
596 initialise_pre_EA();
597
598 /* Compute the pre_exists and pre_forall functions */
599 for (l = 0; l < aut.num_action_labels(); ++l)
600 {
601 pre_exists[l].reserve(s_Pi + 1);
602 pre_forall[l].reserve(s_Pi + 1);
603 pre_exists[l].push_back(exists->get_num_elements());
604 pre_forall[l].push_back(forall->get_num_elements());
605 for (gamma = 0; gamma < s_Pi; ++gamma)
606 {
607 touched_blocks.clear();
608 initialise_Pi(gamma,l);
609 last = touched_blocks.end();
610 for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
611 {
612 alpha = *alphai;
613 exists->add(alpha,l,gamma);
614 if (contents_u[alpha] == LIST_END)
615 {
616 forall->add(alpha,l,gamma);
617 }
618 untouch(alpha);
619 }
620 pre_exists[l].push_back(exists->get_num_elements());
621 pre_forall[l].push_back(forall->get_num_elements());
622 }
623 }
624
625 mCRL2log(log::debug) << "------ Filter(true) ------\nExists: ";
626 mCRL2log(log::debug) << print_structure(exists);
627 mCRL2log(log::debug) << "\nForall: ";
628 mCRL2log(log::debug) << print_structure(forall);
629 mCRL2log(log::debug) << "\nSimulation relation: ";
630 mCRL2log(log::debug) << print_relation(s_Pi,Q);
631
632 /* Apply the second filtering to Q */
633 filter(s_Pi,Q,true);
634}
635
636template <class LTS_TYPE>
638{
639 /* Initialise the pre_exists and pre_forall data structures */
640 exists->clear();
641 forall->clear();
642 std::vector<std::size_t> v;
643 pre_exists.assign(aut.num_action_labels(),v);
644 pre_forall.assign(aut.num_action_labels(),v);
645}
646
647template <class LTS_TYPE>
649{
650 /* Compute the relation induced on Pi by P, store it in Q */
651 std::vector<bool> v(s_Pi,false);
652 Q.assign(s_Pi,v);
653
654 std::size_t alpha,beta;
655 std::vector< std::vector<bool> >::iterator P_parent_alpha;
656 for (alpha = 0; alpha < s_Pi; ++alpha)
657 {
658 P_parent_alpha = P.begin() + parent[alpha];
659 for (beta = 0; beta < s_Pi; ++beta)
660 {
661 Q[alpha][beta] = (*P_parent_alpha)[parent[beta]];
662 }
663 }
664}
665
666
667/* ----------------- FILTER ----------------------------------------- */
668
669template <class LTS_TYPE>
670void 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 match->clear();
675
676 std::size_t alpha,beta,gamma,delta,l;
678 for (l = 0; l < aut.num_action_labels(); ++l)
679 {
680 for (delta = 0; delta < S; ++delta)
681 {
682 etrans.set_end(pre_exists[l][delta+1]);
683 for (etrans.set(pre_exists[l][delta]); !etrans.is_end(); ++etrans)
684 {
685 beta = etrans.get_x();
686 for (gamma = 0; gamma < S; ++gamma)
687 {
688 if (R[gamma][delta])
689 {
690 match->add(l,beta,gamma);
691 }
692 }
693 }
694 }
695 }
696
698 /* The main for loop */
699 for (l = 0; l < aut.num_action_labels(); ++l)
700 {
701 for (gamma = 0; gamma < S; ++gamma)
702 {
703 atrans.set_end(pre_forall[l][gamma+1]);
704 for (atrans.set(pre_forall[l][gamma]); !atrans.is_end(); ++atrans)
705 {
706 alpha = atrans.get_x();
707 for (beta = 0; beta < s_Pi; ++beta)
708 {
709 if (Q[alpha][beta] && !match->find(l,beta,gamma))
710 {
711 Q[alpha][beta] = false;
712 if (B)
713 {
714 cleanup(alpha,beta);
715 }
716 }
717 }
718 }
719 }
720 }
721}
722
723/* ----------------- CLEANUP ---------------------------------------- */
724
725template <class LTS_TYPE>
726void 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;
732 for (l = 0; l < aut.num_action_labels(); ++l)
733 {
734 alpha1i.set_end(pre_forall[l][alpha+1]);
735 beta1i.set_end(pre_exists[l][beta+1]);
736 for (beta1i.set(pre_exists[l][beta]); !beta1i.is_end(); ++beta1i)
737 {
738 beta1 = beta1i.get_x();
739 match_l_beta1_alpha = false;
740 for (delta = 0; delta < s_Pi && !match_l_beta1_alpha; ++delta)
741 {
742 if (exists->find(beta1,l,delta) && Q[alpha][delta])
743 {
744 match_l_beta1_alpha = true;
745 }
746 }
747 if (!match_l_beta1_alpha)
748 {
749 match->remove(l,beta1,alpha);
750 for (alpha1i.set(pre_forall[l][alpha]); !alpha1i.is_end();
751 ++alpha1i)
752 {
753 alpha1 = alpha1i.get_x();
754 if (Q[alpha1][beta1])
755 {
756 Q[alpha1][beta1] = false;
757 cleanup(alpha1,beta1);
758 }
759 }
760 }
761 }
762 }
763}
764
765/* ----------------- FOR POST-PROCESSING ---------------------------- */
766
767template <class LTS_TYPE>
768std::vector < mcrl2::lts::transition> sim_partitioner<LTS_TYPE>::get_transitions() const
769{
770 using namespace mcrl2::lts;
771
772 std::vector < mcrl2::lts::transition> ts;
773 ts.reserve(forall->get_num_elements());
774
775 std::vector<bool> pre_sim;
776 transition::size_type l,beta,gamma;
779 for (beta = 0; beta < s_Pi; ++beta)
780 {
781 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 pre_sim.assign(s_Pi,false);
789 for (gamma = 0; gamma < s_Pi; ++gamma)
790 {
791 // only consider gammas that are unequal to beta
792 if (gamma != beta && Q[beta][gamma])
793 {
794 alphai.set_end(pre_exists[l][gamma+1]);
795 for (alphai.set(pre_exists[l][gamma]); !alphai.is_end();
796 ++alphai)
797 {
798 pre_sim[alphai.get_x()] = true;
799 }
800 }
801 }
802 gammai.set_end(pre_forall[l][beta+1]);
803 for (gammai.set(pre_forall[l][beta]); !gammai.is_end(); ++gammai)
804 {
805 gamma = gammai.get_x();
806 if (!pre_sim[gamma])
807 {
808 // add the transition gamma -l-> beta
809 ts.push_back(transition(gamma,l,beta));
810 }
811 }
812 }
813 }
814 return ts;
815}
816
817template <class LTS_TYPE>
819{
820 return s_Pi;
821}
822
823template <class LTS_TYPE>
824std::size_t sim_partitioner<LTS_TYPE>::get_eq_class(std::size_t s) const
825{
826 return block_Pi[s];
827}
828
829template <class LTS_TYPE>
830bool sim_partitioner<LTS_TYPE>::in_preorder(std::size_t s,std::size_t t) const
831{
832 return Q[block_Pi[s]][block_Pi[t]];
833}
834
835template <class LTS_TYPE>
836bool sim_partitioner<LTS_TYPE>::in_same_class(std::size_t s,std::size_t t) const
837{
838 return (block_Pi[s] == block_Pi[t]);
839}
840
841/*
842// PRE: FORALL and EXISTS structures on Pi are computed
843void 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
972template <class LTS_TYPE>
974{
975 using namespace mcrl2::core;
976 std::stringstream result;
977 result << print_Sigma() << "Simulation relation: " << print_relation(s_Sigma,P);
978 return result.str();
979}
980
981template <class LTS_TYPE>
983{
984 using namespace mcrl2::core;
985 std::stringstream result;
986 result << print_Pi() << "Simulation relation: " << print_relation(s_Pi,Q);
987 return result.str();
988}
989
990template <class LTS_TYPE>
992{
993 using namespace mcrl2::core;
994 std::stringstream result;
995 std::vector<std::size_t>::iterator ci, last;
996 for (std::size_t b = 0; b < s_Sigma; ++b)
997 {
998 result << "block " << b << ": {";
999 last = children[b].end();
1000 for (ci = children[b].begin(); ci != last; ++ci)
1001 {
1002 result << print_block(*ci);
1003 }
1004 result << "}" << std::endl;
1005 }
1006 return result.str();
1007}
1008
1009template <class LTS_TYPE>
1011{
1012 std::stringstream result;
1013 using namespace mcrl2::core;
1014 for (std::size_t b = 0; b < s_Pi; ++b)
1015 {
1016 result << "block " << b << ": {" << print_block(b) << "}" << std::endl;
1017 }
1018 return result.str();
1019}
1020
1021template <class LTS_TYPE>
1023{
1024 std::stringstream result;
1025 using namespace mcrl2::core;
1026 for (ptrdiff_t i = contents_u[b]; i != LIST_END; i = state_buckets[i].next)
1027 {
1028 result << i << ",";
1029 }
1030 for (ptrdiff_t i = contents_t[b]; i != LIST_END; i = state_buckets[i].next)
1031 {
1032 result << i << ",";
1033 }
1034 return result.str();
1035}
1036
1037template <class LTS_TYPE>
1039 std::vector< std::vector<bool> > &R)
1040{
1041 using namespace mcrl2::core;
1042 std::stringstream result;
1043 result << "{";
1044 std::size_t beta,gamma;
1045 for (beta = 0; beta < s; ++beta)
1046 {
1047 for (gamma = 0; gamma < s; ++gamma)
1048 {
1049 if (R[beta][gamma])
1050 {
1051 result << "(" << beta << "," << gamma << "),";
1052 }
1053 }
1054 }
1055 result << "}" << std::endl;
1056 return result.str();
1057}
1058
1059template <class LTS_TYPE>
1061{
1062 using namespace mcrl2::core;
1063 std::stringstream result;
1064 result << "{";
1065 hash_table3_iterator i(struc);
1066 for (; !i.is_end(); ++i)
1067 {
1068 result << "(" << i.get_x() << "," << mcrl2::lts::pp(aut.action_label(i.get_y()))
1069 << "," << i.get_z() << "),";
1070 }
1071 result << "}";
1072 return result.str();
1073}
1074
1075template <class LTS_TYPE>
1076std::string sim_partitioner<LTS_TYPE>::print_reverse_topological_sort(const std::vector<std::size_t> &Sort)
1077{
1078 using namespace mcrl2::core;
1079 std::stringstream result;
1080 result << "reverse topological sort is: [";
1081 for (std::size_t i = 0; i < Sort.size(); ++i)
1082 {
1083 result << Sort[i];
1084 if (i+1 < Sort.size())
1085 {
1086 result << ",";
1087 }
1088 }
1089 result << "]" << std::endl;
1090 return result.str();
1091}
1092
1093
1094} // namespace detail
1095} // namespace lts
1096} // namespace mcrl2
1097#endif
void set_end(std::size_t i)
void set(std::size_t i)
existential quantification.
Definition exists.h:26
std::vector< ptrdiff_t > contents_t
Definition liblts_sim.h:110
std::string print_reverse_topological_sort(const std::vector< std::size_t > &Sort)
std::vector< std::size_t > touched_blocks
Definition liblts_sim.h:122
std::string print_structure(hash_table3 *struc)
std::size_t get_eq_class(std::size_t s) const
Definition liblts_sim.h:824
void initialise_Sigma(std::size_t gamma, std::size_t l)
Definition liblts_sim.h:341
std::vector< bool > state_touched
Definition liblts_sim.h:104
bool in_same_class(std::size_t s, std::size_t t) const
Definition liblts_sim.h:836
std::vector< std::vector< std::size_t > > pre_forall
Definition liblts_sim.h:116
std::vector< ptrdiff_t > contents_u
Definition liblts_sim.h:111
std::vector< bool > block_touched
Definition liblts_sim.h:105
void dfs_visit(std::size_t u, std::vector< bool > &visited, std::vector< std::size_t > &Sort)
Definition liblts_sim.h:475
void cleanup(std::size_t alpha, std::size_t beta)
Definition liblts_sim.h:726
std::vector< std::vector< bool > > stable
Definition liblts_sim.h:112
std::vector< std::size_t > block_Pi
Definition liblts_sim.h:107
std::string print_relation(std::size_t s, std::vector< std::vector< bool > > &R)
mcrl2::lts::outgoing_transitions_per_state_action_t trans_index
Definition liblts_sim.h:101
std::size_t num_eq_classes() const
Definition liblts_sim.h:818
std::string print_block(std::size_t b)
std::vector< mcrl2::lts::transition > get_transitions() const
Definition liblts_sim.h:768
std::vector< std::vector< std::size_t > > pre_exists
Definition liblts_sim.h:115
std::vector< std::size_t > parent
Definition liblts_sim.h:108
void filter(std::size_t S, std::vector< std::vector< bool > > &R, bool B)
Definition liblts_sim.h:670
std::vector< state_bucket > state_buckets
Definition liblts_sim.h:106
std::vector< std::size_t > contents
Definition liblts_sim.h:123
void touch(std::size_t a, std::size_t alpha)
Definition liblts_sim.h:490
std::vector< std::vector< bool > > P
Definition liblts_sim.h:118
void untouch(std::size_t alpha)
Definition liblts_sim.h:518
std::vector< std::vector< std::size_t > > children
Definition liblts_sim.h:109
void reverse_topological_sort(std::vector< std::size_t > &Sort)
Definition liblts_sim.h:462
std::vector< std::vector< bool > > Q
Definition liblts_sim.h:119
bool in_preorder(std::size_t s, std::size_t t) const
Definition liblts_sim.h:830
void initialise_Pi(std::size_t gamma, std::size_t l)
Definition liblts_sim.h:299
A class containing triples, source label and target representing transitions.
Definition transition.h:43
std::size_t size_type
The type of the elements in a transition.
Definition transition.h:46
#define LIST_END
Definition liblts_sim.h:157
#define UNIVERSAL_PART
Definition liblts_sim.h:158
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
This file contains a class that contains labelled transition systems in aut format.
This file contains a class that contains labelled transition systems in dot format.
This file contains a class that contains labelled transition systems in fsm format.
This file contains some utility functions to manipulate lts's.
normalizer< Function > N(const Function &f)
std::string pp(const abstraction &x)
Definition data.cpp:39
The main LTS namespace.
std::multimap< std::pair< transition::size_type, transition::size_type >, transition::size_type > outgoing_transitions_per_state_action_t
Type for exploring transitions per state and action.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(const std::vector< transition > &trans)
Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Header file for hash table data structure used by the simulation preorder algorithm.
Checks whether condition holds for all types passed as variadic template.
Definition type_traits.h:41