mCRL2
Loading...
Searching...
No Matches
lts_algorithm.h
Go to the documentation of this file.
1// Author(s): Muck van Weerdenburg, Jan Friso Groote
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
19#ifndef MCRL2_LTS_LTS_ALGORITHM_H
20#define MCRL2_LTS_LTS_ALGORITHM_H
21
34#include "mcrl2/lts/sigref.h"
35
36namespace mcrl2
37{
38namespace lts
39{
40
46template <class LTS_TYPE>
47void reduce(LTS_TYPE& l, lts_equivalence eq);
48
63template <class LTS_TYPE>
64bool destructive_compare(LTS_TYPE& l1,
65 LTS_TYPE& l2,
66 const lts_equivalence eq,
67 const bool generate_counter_examples = false,
68 const std::string& counter_example_file = std::string(),
69 const bool structured_output = false)
70{
71 // Merge this LTS and l and store the result in this LTS.
72 // In the resulting LTS, the initial state i of l will have the
73 // state number i + N where N is the number of states in this
74 // LTS (before the merge).
75
76 switch (eq)
77 {
78 case lts_eq_none:
79 return false;
80 case lts_eq_bisim:
81 {
82 if (generate_counter_examples)
83 {
84 mCRL2log(mcrl2::log::warning) << "A slower partition refinement algorithm is used to generate minimal-depth counter examples.\n";
85 return detail::destructive_bisimulation_compare_minimal_depth(l1, l2, counter_example_file);
86 }
87 return detail::destructive_bisimulation_compare_dnj(l1,l2, false,false,generate_counter_examples,counter_example_file,structured_output);
88 }
89 case lts_eq_bisim_gv:
90 {
91 return detail::destructive_bisimulation_compare(l1,l2, false,false,generate_counter_examples,counter_example_file,structured_output);
92 }
94 {
95 return detail::destructive_bisimulation_compare_gjkw(l1,l2, false,false,generate_counter_examples,counter_example_file,structured_output);
96 }
98 {
99 if (generate_counter_examples)
100 {
101 mCRL2log(mcrl2::log::warning) << "The default branching bisimulation comparison algorithm cannot generate counter examples. A slower partition refinement algorithm (Martens/Groote 2024) is used instead.\n";
102 return detail::destructive_branching_bisimulation_compare_minimal_depth(l1, l2, counter_example_file);
103 }
104 return detail::destructive_bisimulation_compare_dnj(l1,l2, true,false,generate_counter_examples,counter_example_file,structured_output);
105 }
107 {
108 return detail::destructive_bisimulation_compare(l1,l2, true,false,generate_counter_examples,counter_example_file,structured_output);
109 }
111 {
112 return detail::destructive_bisimulation_compare_gjkw(l1,l2, true,false,generate_counter_examples,counter_example_file,structured_output);
113 }
115 {
116 if (generate_counter_examples)
117 {
118 mCRL2log(mcrl2::log::warning) << "The default divergence-preserving branching bisimulation comparison algorithm cannot generate counter examples. Therefore the slower gv algorithm is used instead.\n";
119 return detail::destructive_bisimulation_compare(l1,l2, true,true,generate_counter_examples,counter_example_file,structured_output);
120 }
121 return detail::destructive_bisimulation_compare_dnj(l1,l2, true,true,generate_counter_examples,counter_example_file,structured_output);
122 }
124 {
125 return detail::destructive_bisimulation_compare(l1,l2, true,true,generate_counter_examples,counter_example_file,structured_output);
126 }
128 {
129 return detail::destructive_bisimulation_compare_gjkw(l1,l2, true,true,generate_counter_examples,counter_example_file,structured_output);
130 }
132 {
133 if (generate_counter_examples)
134 {
135 mCRL2log(log::warning) << "Cannot generate counter examples for weak bisimulation\n";
136 }
138 }
140 {
141 if (generate_counter_examples)
142 {
143 mCRL2log(log::warning) << "Cannot generate counter examples for divergence-preserving weak bisimulation\n";
144 }
146 }
147 case lts_eq_sim:
148 {
149 if (generate_counter_examples)
150 {
151 mCRL2log(log::warning) << "Cannot generate counter examples for simulation equivalence\n";
152 }
153 // Run the partitioning algorithm on this merged LTS
154 std::size_t init_l2 = l2.initial_state() + l1.num_states();
155 detail::merge(l1,l2);
156 l2.clear(); // l2 is not needed anymore.
159
160 return sp.in_same_class(l1.initial_state(),init_l2);
161 }
162 case lts_eq_ready_sim:
163 {
164 if (generate_counter_examples)
165 {
166 mCRL2log(log::warning) << "Cannot generate counter examples for ready-simulation equivalence\n";
167 }
168 // Run the partitioning algorithm on this merged LTS
169 std::size_t init_l2 = l2.initial_state() + l1.num_states();
170 detail::merge(l1,l2);
171 l2.clear(); // l2 is not needed anymore.
174
175 return rsp.in_same_class(l1.initial_state(),init_l2);
176 }
177 case lts_eq_trace:
178 {
179 // Determinise first LTS
181 determinise(l1);
182
183 // Determinise second LTS
185 determinise(l2);
186
187 // Trace equivalence now corresponds to bisimilarity
188 if (generate_counter_examples)
189 {
190 return detail::destructive_bisimulation_compare_minimal_depth(l1, l2, counter_example_file);
191 }
192 return detail::destructive_bisimulation_compare(l1, l2, false, false, generate_counter_examples, counter_example_file, structured_output);
193 }
195 {
196 if (generate_counter_examples)
197 {
198 mCRL2log(log::warning) << "Cannot generate counter examples for weak trace equivalence\n";
199 }
200
201 // Eliminate silent steps and determinise first LTS
202 detail::bisimulation_reduce_dnj(l1,true,false);
205 determinise(l1);
206
207 // Eliminate silent steps and determinise second LTS
208 detail::bisimulation_reduce_dnj(l2,true,false);
211 determinise(l2);
212
213 // Weak trace equivalence now corresponds to bisimilarity
214 return detail::destructive_bisimulation_compare(l1,l2,false,false,false,counter_example_file,structured_output);
215 }
217 {
219 }
220 default:
221 throw mcrl2::runtime_error("Comparison for this equivalence is not available");
222 return false;
223 }
224}
225
239template <class LTS_TYPE>
240bool compare(const LTS_TYPE& l1,
241 const LTS_TYPE& l2,
242 const lts_equivalence eq,
243 const bool generate_counter_examples = false,
244 const std::string& counter_example_file = "",
245 const bool structured_output = false);
246
268template <class LTS_TYPE >
269bool destructive_compare(LTS_TYPE& l1,
270 LTS_TYPE& l2,
271 const lts_preorder pre,
272 const bool generate_counter_example,
273 const std::string& counter_example_file = "",
274 const bool structured_output = false,
276 const bool preprocess = true);
277
292template <class LTS_TYPE >
293bool compare(const LTS_TYPE& l1,
294 const LTS_TYPE& l2,
295 const lts_preorder pre,
296 const bool generate_counter_example,
297 const std::string& counter_example_file = "",
298 const bool structured_output = false,
300 const bool preprocess = true);
301
303template <class LTS_TYPE>
304void determinise(LTS_TYPE& l);
305
306
317template <class SL, class AL, class BASE>
318bool reachability_check(lts < SL, AL, BASE>& l, bool remove_unreachable = false)
319{
320 // First calculate which states can be reached, and store this in the array visited.
321 const outgoing_transitions_per_state_t out_trans(l.get_transitions(),l.num_states(),true);
322
323 std::vector < bool > visited(l.num_states(),false);
324 std::stack<std::size_t> todo;
325
326 visited[l.initial_state()]=true;
327 todo.push(l.initial_state());
328
329 while (!todo.empty())
330 {
331 std::size_t state_to_consider=todo.top();
332 todo.pop();
333 // for (const outgoing_pair_t& p: out_trans[state_to_consider])
334 for (detail::state_type i=out_trans.lowerbound(state_to_consider); i<out_trans.upperbound(state_to_consider); ++i)
335 {
336 const outgoing_pair_t& p=out_trans.get_transitions()[i];
337 assert(visited[state_to_consider] && state_to_consider<l.num_states() && to(p)<l.num_states());
338 if (!visited[to(p)])
339 {
340 visited[to(p)]=true;
341 todo.push(to(p));
342 }
343 }
344 }
345
346 // Property: in_visited(s) == true: state s is reachable from the initial state
347
348 // check to see if all states are reachable from the initial state, i.e.
349 // whether all bits are set.
350 bool all_reachable = find(visited.begin(),visited.end(),false)==visited.end();
351
352 if (!all_reachable && remove_unreachable)
353 {
354 // Remove all unreachable states, transitions from such states and labels
355 // that are only used in these transitions.
356
357 std::vector < detail::state_type > state_map(l.num_states());
358 std::vector < detail::state_type > label_map(l.num_action_labels());
359
360 lts < SL, AL, BASE> new_lts=l; // In this way set data specification and action declarations in the new lts.
361 new_lts.clear();
362
363 std::size_t new_nstates = 0;
364 for (std::size_t i=0; i<l.num_states(); i++)
365 {
366 if (visited[i])
367 {
368 state_map[i] = new_nstates;
369 if (l.has_state_info())
370 {
371 new_lts.add_state(l.state_label(i));
372 }
373 else
374 {
375 new_lts.add_state();
376 }
377 new_nstates++;
378 }
379 }
380
381 for (const transition& t: l.get_transitions())
382 {
383 if (visited[t.from()])
384 {
385 label_map[t.label()] = 1;
386 }
387 }
388
389 label_map[0]=1; // Declare the tau action explicitly present.
390 std::size_t new_nlabels = 0;
391 for (std::size_t i=0; i<l.num_action_labels(); i++)
392 {
393 if (label_map[i]>0) // Label i is used.
394 {
395 label_map[i] = new_nlabels;
396 new_lts.add_action(l.action_label(i));
397 new_nlabels++;
398 }
399 }
400
401 for (const transition& t: l.get_transitions())
402 {
403 if (visited[t.from()])
404 {
405 new_lts.add_transition(transition(state_map[t.from()],label_map[t.label()],state_map[t.to()]));
406 }
407 }
408
409 new_lts.set_initial_state(state_map.at(l.initial_state()));
410 l.swap(new_lts);
411 }
412
413 return all_reachable;
414}
415
426template <class SL, class AL, class PROBABILISTIC_STATE, class BASE>
427bool reachability_check(probabilistic_lts < SL, AL, PROBABILISTIC_STATE, BASE>& l, bool remove_unreachable = false)
428{
429 // First calculate which states can be reached, and store this in the array visited.
430 const outgoing_transitions_per_state_t out_trans(l.get_transitions(),l.num_states(),true);
431
432 std::vector < bool > visited(l.num_states(),false);
433 std::stack<std::size_t> todo;
434
435 if (l.initial_probabilistic_state().size()>1) // Target states are in a probabilistic vector.
436 {
437 for(const typename PROBABILISTIC_STATE::state_probability_pair& s: l.initial_probabilistic_state())
438 {
439 visited[s.state()]=true;
440 todo.push(s.state());
441 }
442 }
443 else // it is a singular state;
444 {
445 const typename PROBABILISTIC_STATE::state_t sn=l.initial_probabilistic_state().get();
446 visited[sn]=true;
447 todo.push(sn);
448 }
449
450 while (!todo.empty())
451 {
452 std::size_t state_to_consider=todo.top();
453 todo.pop();
454 // for (const outgoing_pair_t& p: out_trans[state_to_consider])
455 for (detail::state_type i=out_trans.lowerbound(state_to_consider); i<out_trans.upperbound(state_to_consider); ++i)
456 {
457 const outgoing_pair_t& p=out_trans.get_transitions()[i];
458 assert(visited[state_to_consider] && state_to_consider<l.num_states() && to(p)<l.num_probabilistic_states());
459 // Walk through the the states in this probabilistic state.
460 if (l.probabilistic_state(to(p)).size()>1) // Target states are in a probabilistic vector.
461 {
462 for(const typename PROBABILISTIC_STATE::state_probability_pair& pr: l.probabilistic_state(to(p)))
463 {
464 if (!visited[pr.state()])
465 {
466 visited[pr.state()]=true;
467 todo.push(pr.state());
468 }
469 }
470 }
471 else // it is a singular state;
472 {
473 const typename PROBABILISTIC_STATE::state_t sn=l.probabilistic_state(to(p)).get();
474 if (!visited[sn])
475 {
476 visited[sn]=true;
477 todo.push(sn);
478 }
479 }
480 }
481 }
482
483 // Property: in_visited(s) == true: state s is reachable from the initial state
484
485 // check to see if all states are reachable from the initial state, i.e.
486 // whether all bits are set.
487 bool all_reachable = find(visited.begin(),visited.end(),false)==visited.end();
488
489 if (!all_reachable && remove_unreachable)
490 {
491 // Remove all unreachable states, transitions from such states and labels
492 // that are only used in these transitions.
493
494 std::vector < detail::state_type > state_map(l.num_states());
495 std::vector < detail::state_type > label_map(l.num_action_labels());
496
497 probabilistic_lts < SL, AL, PROBABILISTIC_STATE, BASE> new_lts=l; // In this way set data specification and action declarations in the new lts.
498 new_lts.clear();
499
500 std::size_t new_nstates = 0;
501 for (std::size_t i=0; i<l.num_states(); i++)
502 {
503 if (visited[i])
504 {
505 state_map[i] = new_nstates;
506 if (l.has_state_info())
507 {
508 new_lts.add_state(l.state_label(i));
509 }
510 else
511 {
512 new_lts.add_state();
513 }
514 new_nstates++;
515 }
516 }
517
518 for (const transition& t: l.get_transitions())
519 {
520 if (visited[t.from()])
521 {
522 label_map[t.label()] = 1;
523 }
524 }
525
526 label_map[0]=1; // Declare the tau action explicitly present.
527 std::size_t new_nlabels = 0;
528 for (std::size_t i=0; i<l.num_action_labels(); i++)
529 {
530 if (label_map[i]>0) // Label i is used.
531 {
532 label_map[i] = new_nlabels;
533 new_lts.add_action(l.action_label(i));
534 new_nlabels++;
535 }
536 }
537
538 for (const transition& t: l.get_transitions())
539 {
540 if (visited[t.from()])
541 {
542 new_lts.add_transition(transition(state_map[t.from()],label_map[t.label()],t.to()));
543 }
544 }
545
546 PROBABILISTIC_STATE new_initial_state;
547 for (std::size_t i=0; i<l.num_probabilistic_states(); ++i)
548 {
549 new_initial_state.clear();
550 if (l.probabilistic_state(i).size()==0)
551 {
552 new_initial_state.set(state_map[l.probabilistic_state(i).get()]);
553 }
554 else
555 {
556 for(const typename PROBABILISTIC_STATE::state_probability_pair& s: l.probabilistic_state(i))
557 {
558 new_initial_state.add(state_map[s.state()], s.probability());
559 }
560 }
561 new_lts.add_probabilistic_state(new_initial_state);
562 }
563
564 new_initial_state.clear();
565 if (l.initial_probabilistic_state().size()==0)
566 {
567 new_initial_state.set(state_map[l.initial_probabilistic_state().get()]);
568 }
569 else
570 {
571 for(const typename PROBABILISTIC_STATE::state_probability_pair& s: l.initial_probabilistic_state())
572 {
573 new_initial_state.add(state_map[s.state()], s.probability());
574 }
575 }
576 new_lts.set_initial_probabilistic_state(new_initial_state);
577 l.swap(new_lts);
578 }
579
580 return all_reachable;
581}
582
586template <class LTS_TYPE>
587bool is_deterministic(const LTS_TYPE& l);
588
593template <class LTS_TYPE>
594void merge(LTS_TYPE& l1, const LTS_TYPE& l2)
595{
596 detail::merge(l1,l2);
597}
598
599
600/* Here the implementations of the declared functions above are given.
601 Originally these were in a .cpp file, before lts's were templated */
602
603
604
605template <class LTS_TYPE>
606void reduce(LTS_TYPE& l,lts_equivalence eq)
607{
608
609 switch (eq)
610 {
611 case lts_eq_none:
612 return;
613 case lts_eq_bisim:
614 {
615 detail::bisimulation_reduce_dnj(l,false,false);
616 return;
617 }
618 case lts_eq_bisim_gv:
619 {
620 detail::bisimulation_reduce(l,false,false);
621 return;
622 }
624 {
626 return;
627 }
629 {
631 s.run();
632 return;
633 }
635 {
637 return;
638 }
640 {
641 detail::bisimulation_reduce(l,true,false);
642 return;
643 }
645 {
647 return;
648 }
650 {
652 s.run();
653 return;
654 }
656 {
658 return;
659 }
661 {
662 detail::bisimulation_reduce(l,true,true);
663 return;
664 }
666 {
668 return;
669 }
671 {
673 s.run();
674 return;
675 }
677 {
679 return;
680 }
681 /*
682 case lts_eq_weak_bisim_sigref:
683 {
684 {
685 sigref<LTS_TYPE, signature_branching_bisim<LTS_TYPE> > s1(l);
686 s1.run();
687 }
688 detail::reflexive_transitive_tau_closure(l);
689 {
690 sigref<LTS_TYPE, signature_bisim<LTS_TYPE> > s2(l);
691 s2.run();
692 }
693 scc_reduce(l); // Remove tau loops
694 return;
695 }
696 */
698 {
700 return;
701 }
702 /*
703 case lts_eq_divergence_preserving_weak_bisim_sigref:
704 {
705 {
706 sigref<LTS_TYPE, signature_divergence_preserving_branching_bisim<LTS_TYPE> > s1(l);
707 s1.run();
708 }
709 std::size_t divergence_label=detail::mark_explicit_divergence_transitions(l);
710 detail::reflexive_transitive_tau_closure(l);
711 {
712 sigref<LTS_TYPE, signature_bisim<LTS_TYPE> > s2(l);
713 s2.run();
714 }
715 scc_reduce(l); // Remove tau loops
716 detail::unmark_explicit_divergence_transitions(l,divergence_label);
717 return;
718 }
719 */
720 case lts_eq_sim:
721 {
722 // Run the partitioning algorithm on this LTS
725
726 // Clear this LTS, but keep the labels
727 // l.clear_type();
728 l.clear_state_labels();
729 l.clear_transitions();
730
731 // Assign the reduced LTS
732 l.set_num_states(sp.num_eq_classes());
733 l.set_initial_state(sp.get_eq_class(l.initial_state()));
734
735 const std::vector <transition> trans=sp.get_transitions();
736 l.clear_transitions();
737 for (std::vector <transition>::const_iterator i=trans.begin(); i!=trans.end(); ++i)
738 {
739 l.add_transition(*i);
740 }
741 // Remove unreachable parts
742
743 reachability_check(l,true);
744
745 return;
746 }
747 case lts_eq_ready_sim:
748 {
749 // Run the partitioning algorithm on this LTS
752
753 // Clear this LTS, but keep the labels
754 // l.clear_type();
755 l.clear_state_labels();
756 l.clear_transitions();
757
758 // Assign the reduced LTS
759 l.set_num_states(rsp.num_eq_classes());
760 l.set_initial_state(rsp.get_eq_class(l.initial_state()));
761
762 const std::vector <transition> trans=rsp.get_transitions();
763 l.clear_transitions();
764 for (std::vector <transition>::const_iterator i=trans.begin(); i!=trans.end(); ++i)
765 {
766 l.add_transition(*i);
767 }
768 // Remove unreachable parts
769
770 reachability_check(l,true);
771
772 return;
773 }
774 case lts_eq_trace:
776 determinise(l);
778 return;
780 {
784 determinise(l);
786 return;
787 }
788 case lts_red_tau_star:
789 {
793 return;
794 }
796 {
797 determinise(l);
798 return;
799 }
800 default:
801 throw mcrl2::runtime_error("Unknown reduction method.");
802 }
803}
804
805template <class LTS_TYPE>
806bool compare(const LTS_TYPE& l1, const LTS_TYPE& l2, const lts_equivalence eq, const bool generate_counter_examples, const std::string& counter_example_file, const bool structured_output)
807{
808 switch (eq)
809 {
810 case lts_eq_none:
811 return false;
812 default:
813 LTS_TYPE l1_copy(l1);
814 LTS_TYPE l2_copy(l2);
815 return destructive_compare(l1_copy, l2_copy, eq ,generate_counter_examples, counter_example_file, structured_output);
816 }
817 return false;
818}
819
820template <class LTS_TYPE>
821bool compare(const LTS_TYPE& l1, const LTS_TYPE& l2, const lts_preorder pre, const bool generate_counter_example, const std::string& counter_example_file, const bool structured_output, const lps::exploration_strategy strategy, const bool preprocess)
822{
823 LTS_TYPE l1_copy(l1);
824 LTS_TYPE l2_copy(l2);
825 return destructive_compare(l1_copy, l2_copy, pre, generate_counter_example, counter_example_file, structured_output, strategy, preprocess);
826}
827
828template <class LTS_TYPE>
829bool destructive_compare(LTS_TYPE& l1, LTS_TYPE& l2, const lts_preorder pre, const bool generate_counter_example, const std::string& counter_example_file, const bool structured_output, const lps::exploration_strategy strategy, const bool preprocess)
830{
831 switch (pre)
832 {
833 case lts_pre_sim:
834 {
835 // Merge this LTS and l and store the result in this LTS.
836 // In the resulting LTS, the initial state i of l will have the
837 // state number i + N where N is the number of states in this
838 // LTS (before the merge).
839 const std::size_t init_l2 = l2.initial_state() + l1.num_states();
840 detail::merge(l1,l2);
841
842 // We no longer need l, so clear it to save memory
843 l2.clear();
844
845 // Run the partitioning algorithm on this merged LTS
848
849 return sp.in_preorder(l1.initial_state(),init_l2);
850 }
852 {
853 // Merge this LTS and l and store the result in this LTS.
854 // In the resulting LTS, the initial state i of l will have the
855 // state number i + N where N is the number of states in this
856 // LTS (before the merge).
857 const std::size_t init_l2 = l2.initial_state() + l1.num_states();
858 detail::merge(l1,l2);
859
860 // We no longer need l, so clear it to save memory
861 l2.clear();
862
863 // Run the partitioning algorithm on this prepropcessed LTS
866
867 return rsp.in_preorder(l1.initial_state(),init_l2);
868 }
869 case lts_pre_trace:
870 {
871 // Preprocessing: reduce modulo strong bisimulation equivalence.
872 // This is not strictly necessary, but may reduce time/memory
873 // needed for determinisation.
876
877 // Determinise both LTSes. As postprocessing, reduce modulo
878 // strong bisimulation equivalence. This is not strictly
879 // necessary, but may reduce time/memory needed for simulation
880 // preorder checking.
881 determinise(l1);
883
884 determinise(l2);
886
887 // Trace preorder now corresponds to simulation preorder
888 return destructive_compare(l1, l2, lts_pre_sim, generate_counter_example, counter_example_file, structured_output, strategy);
889 }
891 {
892 // Eliminate silent steps of first LTS
893 detail::bisimulation_reduce_dnj(l1,true,false);
895
896 // Eliminate silent steps of second LTS
897 detail::bisimulation_reduce_dnj(l2,true,false);
899
900 // Weak trace preorder now corresponds to strong trace preorder
901 return destructive_compare(l1, l2, lts_pre_trace, generate_counter_example, counter_example_file, structured_output, strategy);
902 }
904 {
905 if (generate_counter_example)
906 {
907 detail::counter_example_constructor cec("counter_example_trace_preorder", counter_example_file, structured_output);
908 return destructive_refinement_checker(l1, l2, refinement_type::trace, false, strategy, preprocess, cec);
909 }
910 return destructive_refinement_checker(l1, l2, refinement_type::trace, false, strategy, preprocess);
911 }
913 {
914 if (generate_counter_example)
915 {
916 detail::counter_example_constructor cec("counter_example_weak_trace_preorder", counter_example_file, structured_output);
917 return destructive_refinement_checker(l1, l2, refinement_type::trace, true, strategy, preprocess, cec);
918 }
919 return destructive_refinement_checker(l1, l2, refinement_type::trace, true, strategy, preprocess);
920 }
922 {
923 if (generate_counter_example)
924 {
925 detail::counter_example_constructor cec("counter_example_failures_refinement", counter_example_file, structured_output);
926 return destructive_refinement_checker(l1, l2, refinement_type::failures, false, strategy, preprocess, cec);
927 }
928 return destructive_refinement_checker(l1, l2, refinement_type::failures, false, strategy, preprocess);
929 }
931 {
932 if (generate_counter_example)
933 {
934 detail::counter_example_constructor cec("counter_example_weak_failures_refinement", counter_example_file, structured_output);
935 return destructive_refinement_checker(l1, l2, refinement_type::failures, true, strategy, preprocess, cec);
936 }
937 return destructive_refinement_checker(l1, l2, refinement_type::failures, true, strategy, preprocess);
938 }
940 {
941 if (generate_counter_example)
942 {
943 detail::counter_example_constructor cec("counter_example_failures_divergence_refinement", counter_example_file, structured_output);
944 return destructive_refinement_checker(l1, l2, refinement_type::failures_divergence, true, strategy, preprocess, cec);
945 }
946 return destructive_refinement_checker(l1, l2, refinement_type::failures_divergence, true, strategy, preprocess);
947 }
948 default:
949 mCRL2log(log::error) << "Comparison for this preorder is not available\n";
950 return false;
951 }
952}
953
954
955template <class LTS_TYPE>
956bool is_deterministic(const LTS_TYPE& l)
957{
958 if (l.num_transitions() == 0)
959 {
960 return true;
961 }
962
963 std::vector<transition> temporary_copy_of_transitions = l.get_transitions();
964 sort_transitions(temporary_copy_of_transitions, l.hidden_label_set(), src_lbl_tgt);
965
966 // Traverse the ordered transitions, and search for two consecutive pairs <s,l,t> and <s,l,t'> with t!=t'.
967 // Such a pair exists iff l is not deterministic.
968 transition& previous_t=temporary_copy_of_transitions[0];
969 bool previous_t_is_valid=false;
970 for(const transition& t: temporary_copy_of_transitions)
971 {
972 if (previous_t_is_valid)
973 {
974 if (previous_t.from()==t.from() &&
975 previous_t.label()==t.label() &&
976 previous_t.to()!=t.to())
977 {
978 return false;
979 }
980 }
981 previous_t=t;
982 previous_t_is_valid=true;
983 }
984 return true;
985}
986
987
988namespace detail
989{
990
991template <class LTS_TYPE>
993 tree_set_store& tss,
994 std::size_t d,
995 std::vector<transition>& d_trans,
996 LTS_TYPE& aut)
997{
998 if (!tss.is_set_empty(d))
999 {
1000 if (tss.is_set_empty(tss.get_set_child_right(d)))
1001 {
1002 // for (outgoing_transitions_per_state_t:: const_iterator
1003 // j=begin.lower_bound(tss.get_set_child_left(d)); j!=begin.upper_bound(tss.get_set_child_left(d)); ++j)
1004 const state_type from=tss.get_set_child_left(d);
1005 // for(const outgoing_pair_t& p: begin[from])
1006 for (detail::state_type i=begin.lowerbound(from); i<begin.upperbound(from); ++i)
1007 {
1008 const outgoing_pair_t& p=begin.get_transitions()[i];
1009 d_trans.push_back(transition(from, aut.apply_hidden_label_map(label(p)), to(p)));
1010 }
1011 }
1012 else
1013 {
1014 get_trans(begin,tss,tss.get_set_child_left(d),d_trans,aut);
1015 get_trans(begin,tss,tss.get_set_child_right(d),d_trans,aut);
1016 }
1017 }
1018}
1019} // namespace detail
1020
1021
1022template <class LTS_TYPE>
1023void determinise(LTS_TYPE& l)
1024{
1025 tree_set_store tss;
1026
1027 std::vector<transition> d_transs;
1028 std::vector<std::ptrdiff_t> d_states;
1029
1030 // create the initial state of the DLTS
1031 d_states.push_back(l.initial_state());
1032 std::ptrdiff_t d_id = tss.set_set_tag(tss.create_set(d_states));
1033 d_states.clear();
1034
1035 const outgoing_transitions_per_state_t begin(l.get_transitions(),l.num_states(),true);
1036
1037 l.clear_transitions();
1038 l.clear_state_labels();
1039 std::size_t d_ntransitions = 0;
1040 std::vector < transition > d_transitions;
1041
1042 std::size_t s;
1043 std::size_t i,to,lbl,n_t;
1044
1045 while (d_id < tss.get_next_tag())
1046 {
1047 // collect the outgoing transitions of every state of DLTS state d_id in
1048 // the vector d_transs
1049 detail::get_trans(begin,tss,tss.get_set(d_id),d_transs,l);
1050
1051 // sort d_transs by label and (if labels are equal) by destination
1052 const detail::compare_transitions_lts compare(l.hidden_label_set());
1053 sort(d_transs.begin(),d_transs.end(),compare);
1054
1055 n_t = d_transs.size();
1056 i = 0;
1057 for (lbl = 0; lbl < l.num_action_labels(); ++lbl)
1058 {
1059 // compute the destination of the transition with label lbl
1060 while (i < n_t && l.apply_hidden_label_map(d_transs[i].label()) < lbl)
1061 {
1062 ++i;
1063 }
1064 while (i < n_t && l.apply_hidden_label_map(d_transs[i].label()) == lbl)
1065 {
1066 to = d_transs[i].to();
1067 d_states.push_back(to);
1068 while (i < n_t && l.apply_hidden_label_map(d_transs[i].label()) == lbl &&
1069 d_transs[i].to() == to)
1070 {
1071 ++i;
1072 }
1073 }
1074 s = tss.create_set(d_states);
1075
1076 // generate the transitions to each of the next states
1077 if (!tss.is_set_empty(s))
1078 {
1079 d_transitions.push_back(transition(d_id,lbl,tss.set_set_tag(s)));
1080
1081 if (d_ntransitions%10000 == 0)
1082 {
1084 "generated " << tss.get_next_tag() << " states and " << d_ntransitions
1085 << " transitions; explored " << d_id << " states" << std::endl;
1086 }
1087 }
1088 d_states.clear();
1089 }
1090 d_transs.clear();
1091 ++d_id;
1092 }
1093
1094
1095 l.set_num_states(d_id,false); // remove the state values, and reset the number of states.
1096 l.set_initial_state(0);
1097
1098 for (const transition& t: d_transitions)
1099 {
1100 l.add_transition(t);
1101 }
1102 assert(is_deterministic(l));
1103}
1104
1105} // namespace lts
1106} // namespace mcrl2
1107
1108#endif // MCRL2_LTS_LTS_ALGORITHM_H
1109
1110
1111
A class that can be used to store counterexample trees and.
const std::vector< CONTENT > & get_transitions() const
std::size_t get_eq_class(std::size_t s) const
Definition liblts_sim.h:824
bool in_same_class(std::size_t s, std::size_t t) const
Definition liblts_sim.h:836
std::size_t num_eq_classes() const
Definition liblts_sim.h:818
std::vector< mcrl2::lts::transition > get_transitions() const
Definition liblts_sim.h:768
bool in_preorder(std::size_t s, std::size_t t) const
Definition liblts_sim.h:830
labels_size_type num_action_labels() const
Gets the number of action labels of this LTS.
Definition lts.h:318
void add_transition(const transition &t)
Add a transition to the lts.
Definition lts.h:544
states_size_type num_states() const
Gets the number of states of this LTS.
Definition lts.h:245
ACTION_LABEL_T action_label(const labels_size_type action) const
Gets the label of an action.
Definition lts.h:470
bool has_state_info() const
Checks whether this LTS has state values associated with its states.
Definition lts.h:636
STATE_LABEL_T state_label(const states_size_type state) const
Gets the label of a state.
Definition lts.h:450
states_size_type add_state(const STATE_LABEL_T &label=STATE_LABEL_T())
Adds a state to this LTS.
Definition lts.h:347
const std::vector< transition > & get_transitions() const
Gets a const reference to the vector of transitions of the current lts.
Definition lts.h:526
labels_size_type add_action(const ACTION_LABEL_T &label)
Adds an action with a label to this LTS.
Definition lts.h:361
void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T &state)
Sets the probabilistic initial state number of this LTS.
const PROBABILISTIC_STATE_T & initial_probabilistic_state() const
Gets the initial state number of this LTS.
void swap(probabilistic_lts &other)
Swap this lts with the supplied supplied LTS.
labels_size_type num_probabilistic_states() const
Gets the number of probabilistic states of this LTS.
void clear()
Clear the transitions system.
states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T &s)
Adds a probabilistic state to this LTS.
const PROBABILISTIC_STATE_T & probabilistic_state(const states_size_type index) const
Gets the probabilistic label of an index.
Signature based reductions for labelled transition systems.
Definition sigref.h:350
void run()
Perform the reduction, modulo the equivalence for which the signature has been passed in as template ...
Definition sigref.h:458
A class containing triples, source label and target representing transitions.
Definition transition.h:43
size_type from() const
The source of the transition.
Definition transition.h:77
size_type label() const
The label of the transition.
Definition transition.h:83
size_type to() const
The target of the transition.
Definition transition.h:90
bool is_set_empty(ptrdiff_t set)
Definition tree_set.cpp:205
ptrdiff_t get_set_child_left(ptrdiff_t set)
Definition tree_set.cpp:185
ptrdiff_t create_set(std::vector< ptrdiff_t > &elems)
Definition tree_set.cpp:139
ptrdiff_t get_set(ptrdiff_t tag)
Definition tree_set.cpp:180
ptrdiff_t get_set_child_right(ptrdiff_t set)
Definition tree_set.cpp:190
ptrdiff_t set_set_tag(ptrdiff_t set)
Definition tree_set.cpp:210
Standard exception class for reporting runtime errors.
Definition exception.h:27
void bisimulation_reduce_gjkw(LTS_TYPE &l, bool branching=false, bool preserve_divergence=false)
Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.
bool destructive_bisimulation_compare_dnj(LTS_TYPE &l1, LTS_TYPE &l2, bool const branching=false, bool const preserve_divergence=false, bool const generate_counter_examples=false, const std::string &="", bool=false)
Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bis...
bool destructive_bisimulation_compare_gjkw(LTS_TYPE &l1, LTS_TYPE &l2, bool branching=false, bool preserve_divergence=false, bool generate_counter_examples=false)
Checks whether the two initial states of two LTSs are strong or branching bisimilar.
void bisimulation_reduce_dnj(LTS_TYPE &l, bool const branching=false, bool const preserve_divergence=false)
Reduce transition system l with respect to strong or (divergence-preserving) branching bisimulation.
O(m log n)-time stuttering equivalence algorithm.
Author(s): # Carlos Gregorio-Rodriguez, Luis LLana, Rafael Martinez-Torres.
This file defines an algorithm for weak bisimulation, by calculating the transitive tau closure and a...
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
Type recording the equivalence reductions supported by the LTS library.
Supperted preorders for LTSes.
@ warning
Definition logger.h:32
void merge(LTS_TYPE &l1, const LTS_TYPE &l2)
bool destructive_branching_bisimulation_compare_minimal_depth(LTS_TYPE &l1, LTS_TYPE &l2, const std::string &counter_example_file)
bool coupled_simulation_compare(LTS_TYPE &l1, LTS_TYPE &l2)
void weak_bisimulation_reduce(LTS_TYPE &l, const bool preserve_divergences=false)
Reduce LTS l with respect to (divergence-preserving) weak bisimulation.
bool destructive_bisimulation_compare_minimal_depth(LTS_TYPE &l1, LTS_TYPE &l2, const std::string &counter_example_file)
std::size_t state_type
type used to store state (numbers and) counts
void bisimulation_reduce(LTS_TYPE &l, const bool branching=false, const bool preserve_divergences=false)
Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.
bool destructive_bisimulation_compare(LTS_TYPE &l1, LTS_TYPE &l2, const bool branching=false, const bool preserve_divergences=false, const bool generate_counter_examples=false, const std::string &counter_example_file="", const bool structured_output=false)
Checks whether the two initial states of two lts's are strong or branching bisimilar.
bool destructive_weak_bisimulation_compare(LTS_TYPE &l1, LTS_TYPE &l2, const bool preserve_divergences=false)
Checks whether the initial states of two LTSs are weakly bisimilar.
void get_trans(const outgoing_transitions_per_state_t &begin, tree_set_store &tss, std::size_t d, std::vector< transition > &d_trans, LTS_TYPE &aut)
void tau_star_reduce(lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &l)
lts_equivalence
LTS equivalence relations.
@ lts_eq_branching_bisim_sigref
@ lts_eq_divergence_preserving_weak_bisim
@ lts_eq_branching_bisim_gjkw
@ lts_eq_branching_bisim_gv
@ lts_eq_divergence_preserving_branching_bisim_sigref
@ lts_eq_divergence_preserving_branching_bisim
@ lts_eq_divergence_preserving_branching_bisim_gjkw
@ lts_eq_divergence_preserving_branching_bisim_gv
bool is_deterministic(const LTS_TYPE &l)
Checks whether this LTS is deterministic.
lts_preorder
LTS preorder relations.
@ lts_pre_failures_refinement
@ lts_pre_failures_divergence_refinement
@ lts_pre_weak_trace_anti_chain
@ lts_pre_weak_failures_refinement
@ lts_pre_trace_anti_chain
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
void sort_transitions(std::vector< transition > &transitions, const std::set< transition::size_type > &hidden_label_set, transition_sort_style ts=src_lbl_tgt)
Sorts the transitions using a sort style.
void determinise(LTS_TYPE &l)
Determinises this LTS.
bool destructive_compare(LTS_TYPE &l1, LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file=std::string(), const bool structured_output=false)
Checks whether this LTS is equivalent to another LTS.
std::pair< std::size_t, bool > reduce(LTS_TYPE &lts, const bool weak_reduction, const bool preserve_divergence, std::size_t l2_init)
Preprocess the LTS for destructive refinement checking.
void merge(LTS_TYPE &l1, const LTS_TYPE &l2)
Merge the second lts into the first lts.
bool reachability_check(lts< SL, AL, BASE > &l, bool remove_unreachable=false)
Checks whether all states in this LTS are reachable from the initial state and remove unreachable sta...
bool destructive_refinement_checker(LTS_TYPE &l1, LTS_TYPE &l2, const refinement_type refinement, const bool weak_reduction, const lps::exploration_strategy strategy, const bool preprocess=true, COUNTER_EXAMPLE_CONSTRUCTOR generate_counter_example=detail::dummy_counter_example_constructor())
This function checks using algorithms in the paper mentioned above whether transition system l1 is in...
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator &i)
From state of an iterator exploring transitions per outgoing state and action.
std::pair< transition::size_type, transition::size_type > outgoing_pair_t
Type for exploring transitions per state.
bool compare(const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file="", const bool structured_output=false)
Checks whether this LTS is equivalent to another LTS.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Implementation of LTS reductions using the signature refinement approach of S. Blom and S....