mCRL2
Loading...
Searching...
No Matches
liblts_bisim.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//
10
11#ifndef _LIBLTS_BISIM_H
12#define _LIBLTS_BISIM_H
13#include <fstream>
18#include "mcrl2/lts/lts_aut.h"
19#include "mcrl2/lts/lts_fsm.h"
20#include "mcrl2/lts/lts_dot.h"
21
22namespace mcrl2
23{
24namespace lts
25{
26namespace detail
27{
28
29template < class LTS_TYPE>
31{
32
33 public:
54 LTS_TYPE& l,
55 const bool branching=false,
56 const bool preserve_divergence=false,
57 const bool generate_counter_examples=false)
58 : max_state_index(0),
59 aut(l),
61 store_counter_info(generate_counter_examples)
62 {
63 assert(branching || !preserve_divergence);
64 mCRL2log(log::verbose) << (preserve_divergence?"Divergence preserving b":"B") <<
65 (branching?"ranching b":"") << "isimulation partitioner created for "
66 << l.num_states() << " states and " <<
67 l.num_transitions() << " transitions\n";
68
69 if (generate_counter_examples)
70 {
71 outgoing_transitions = transitions_per_outgoing_state_action_pair(aut.get_transitions(), aut.hidden_label_set());
72 }
73
74 create_initial_partition(branching,preserve_divergence);
76 }
77
78
81
94 void replace_transition_system(const bool branching, const bool preserve_divergences)
95 {
96 // Put all the non inert transitions in a set. Add the transitions that form a self
97 // loop. Such transitions only exist in case divergence preserving branching bisimulation is
98 // used. A set is used to remove double occurrences of transitions.
99 std::set < transition > resulting_transitions;
100
101 for (const transition& i: aut.get_transitions())
102 {
103 const bool is_transition_i_hidden=aut.is_tau(aut.apply_hidden_label_map(i.label()));
104 if (!branching ||
105 !is_transition_i_hidden ||
106 get_eq_class(i.from())!=get_eq_class(i.to()) ||
107 (preserve_divergences && i.from()==i.to()))
108 {
109 resulting_transitions.insert(
111 get_eq_class(i.from()),
112// In the line below all hidden transitions are replaced by an explicit tau. It is possible to
113// always use i.label() where the resulting transition is only implicitly hidden. This has as effect that
114// the labels of non inert hidden transitions are preserved (e.g. for use in counter examples) but that
115// there are possibly multiple hidden transitions between states, leading to a larger number of
116// transitions than strictly necessary.
117 (is_transition_i_hidden?aut.tau_label_index():i.label()),
118 get_eq_class(i.to())));
119 }
120 }
121 // Remove the old transitions
122 aut.clear_transitions();
123
124 // Copy the transitions from the set into the transition system.
125 for (const transition& t: resulting_transitions)
126 {
127 aut.add_transition(t);
128 }
129
130 // Merge the states, by setting the state labels of each state to the concatenation of the state labels of its
131 // equivalence class.
132 if (aut.has_state_info()) /* If there are no state labels this step can be ignored */
133 {
134 /* Create a vector for the new labels */
135 std::vector<typename LTS_TYPE::state_label_t> new_labels(num_eq_classes());
136
137 for(std::size_t i=aut.num_states(); i>0; )
138 {
139 --i;
140 const std::size_t new_index=get_eq_class(i);
141 new_labels[new_index] = new_labels[new_index] + aut.state_label(i);
142 }
143
144 aut.set_num_states(num_eq_classes());
145 for(std::size_t i=0; i<num_eq_classes(); ++i)
146 {
147 aut.set_state_label(i,new_labels[i]);
148 }
149 }
150 else
151 {
152 aut.set_num_states(num_eq_classes());
153 }
154
155 aut.set_initial_state(get_eq_class(aut.initial_state()));
156 }
157
161 std::size_t num_eq_classes() const
162 {
163 return max_state_index;
164 }
165
166
170 std::size_t get_eq_class(const std::size_t s) const
171 {
172 assert(s<block_index_of_a_state.size());
173 return blocks[block_index_of_a_state[s]].state_index;
174 }
175
176
182 bool in_same_class(const std::size_t s, const std::size_t t) const
183 {
184 return get_eq_class(s)==get_eq_class(t);
185 }
186
187
196 mcrl2::state_formulas::state_formula counter_formula(const std::size_t s, const std::size_t t);
197
198 private:
199
200 typedef std::size_t block_index_type;
201 typedef std::size_t state_type;
202 typedef std::size_t label_type;
203
205 LTS_TYPE& aut;
208
210 {
212 std::vector < state_type > inert_transitions; // Only the target state is interesting.
213
215 : state(s)
216 {}
217 non_bottom_state(const state_type s, const std::vector < state_type > &it)
218 : state(s), inert_transitions(it)
219 {}
220 };
221
222 struct block
223 {
224 state_type state_index; // The state number that represent the states in this block
225 block_index_type block_index; // The sequence number of this block.
226 block_index_type parent_block_index; // Index of the parent block.
227 // If there is no parent block, this refers to the block
228 // itself.
229 std::vector < state_type > bottom_states; // The non bottom states must be ordered
230 // on tau reachability. The deepest
231 // states occur first in the vector.
232 std::vector < non_bottom_state > non_bottom_states;
233 // The non_inert transitions are grouped per label. The (non-inert) transitions
234 // with tau labels are at the end of this vector.
235 std::vector < transition > non_inert_transitions;
236
237 void swap(block& b)
238 {
239 state_type state_index1=b.state_index;
241 state_index=state_index1;
242
243 block_index_type block_index1=b.block_index;
245 block_index=block_index1;
246
247 block_index_type parent_block_index1=b.parent_block_index;
249 parent_block_index=parent_block_index1;
250
254 }
255 };
256
257 std::vector < block > blocks;
258
259 // std::vector < bool > block_is_active; // Indicates whether this is still a block in the partition.
260 // Blocks that are split become inactive.
261 std::vector < state_type > block_index_of_a_state;
262 std::vector < bool > block_flags;
263 std::vector < bool > block_is_in_to_be_processed;
264 std::vector < bool > state_flags;
265
266 std::vector< block_index_type > to_be_processed;
267 std::vector< block_index_type > BL;
268
269 // Counter example information based on "Computing Distinguishing Formulas for Branching Bisimulation", 1991 by Henri Korver
270 // Given a block B that is split using action alpha and block B' into blocks L and R, with P as the partition just before this split, then
271 // right_child[B] = R
272 std::map < block_index_type, block_index_type > right_child;
273 // split_by_action[B] = alpha,
274 std::map < block_index_type, label_type > split_by_action;
275 // split_by_block[B] = B',
276 std::map < block_index_type, block_index_type > split_by_block;
277 // r_alpha[R] = { C \in P | \exists_{s \in R, s' \in C} : s -a-> s'} and
278 std::map < block_index_type, std::set < block_index_type > > r_alpha;
279 // r_tau[R] = { C \in P | \exists_{s \in R, s' \in C} : s -tau-> s' && C != B}.
280 std::map < block_index_type, std::set < block_index_type > > r_tauP;
281 // map from source state and action to target state, makes generating counterexample info easier
283
284 // A counter for creating fresh variables
286
287
289 const bool preserve_divergences)
290
291 {
292 to_be_processed.clear();
293
294 block initial_partition;
295
296 // First store the bottom and non bottom states.
297 sort_transitions(aut.get_transitions(), aut.hidden_label_set(), mcrl2::lts::src_lbl_tgt);
298
299 state_type last_non_stored_state_number=0;
300 bool bottom_state=true;
301 std::vector < state_type > current_inert_transitions;
302
303 {
304 // Reserve enough space, such that no reallocations of the vector are required when adding transitions.
305 // For this purpose, first the number of inert transitions must be counted, to avoid reserving too much
306 // space. This for instance leads to a waste of memory (terabytes for reducing 30M states), especially,
307 // when calculating ia strong bisimulation reduction.
308 std::size_t initial_partition_non_inert_counter=0;
309 std::size_t current_inert_transition_counter=0;
310 const std::vector<transition> & trans=aut.get_transitions();
311 for (std::vector<transition>::const_iterator r=trans.begin(); r!=trans.end(); ++r)
312 {
313 const transition t= *r;
314 if (branching && aut.is_tau(aut.apply_hidden_label_map(t.label())))
315 {
316 if (preserve_divergences && t.from()==t.to())
317 {
318 initial_partition_non_inert_counter++;
319 }
320 else
321 {
322 current_inert_transition_counter++;
323 }
324 }
325 }
326 current_inert_transitions.reserve(initial_partition_non_inert_counter);
327 initial_partition.non_inert_transitions.reserve(current_inert_transition_counter);
328 }
329
330 const std::vector<transition>& trans=aut.get_transitions();
331 for (std::vector<transition>::const_iterator r=trans.begin(); r!=trans.end(); ++r)
332 {
333 const transition t=* r;
334
335 if (branching && aut.is_tau(aut.apply_hidden_label_map(t.label())))
336 {
337 if (preserve_divergences && t.from()==t.to())
338 {
339 initial_partition.non_inert_transitions.push_back(transition(t.from(),aut.tau_label_index(),t.to()));
340 }
341 else
342 {
343 current_inert_transitions.push_back(t.to());
344 bottom_state=false;
345 }
346 }
347 std::vector<transition>::const_iterator next_i=r;
348 ++next_i;
349 if (next_i==trans.end() || t.from()!=next_i->from())
350 {
351 // store the current from state
352 for (; last_non_stored_state_number<t.from(); ++last_non_stored_state_number)
353 {
354 initial_partition.bottom_states.push_back(last_non_stored_state_number);
355 }
356
357 if (bottom_state)
358 {
359 initial_partition.bottom_states.push_back(t.from());
360 }
361 else
362 {
363 initial_partition.non_bottom_states.push_back(non_bottom_state(t.from()));
364 current_inert_transitions.swap(initial_partition.non_bottom_states.back().inert_transitions);
365 bottom_state=true;
366 }
367 assert(last_non_stored_state_number==t.from());
368 last_non_stored_state_number++;
369 }
370 }
371
372 for (; last_non_stored_state_number<aut.num_states(); ++last_non_stored_state_number)
373 {
374 initial_partition.bottom_states.push_back(last_non_stored_state_number);
375 }
376
377 // Sort the non-bottom states such that the deepest states occur first.
378 // Raise an exception if there is a non trivial tau loop.
379
381
382 // Store the non-inert transitions (i.e. the non tau transitions)
383 sort_transitions(aut.get_transitions(), aut.hidden_label_set(), mcrl2::lts::lbl_tgt_src);
384 const std::vector<transition> & trans1=aut.get_transitions();
385 for (std::vector<transition>::const_iterator r=trans1.begin(); r!=trans1.end(); ++r)
386 {
387 const transition t= *r;
388 if (!branching || !aut.is_tau(aut.apply_hidden_label_map(t.label())))
389 {
390 // Note that by sorting the transitions first, the non_inert_transitions are grouped per label.
391 initial_partition.non_inert_transitions.push_back(t);
392 }
393 }
394
395 // block_is_active.push_back(true);
396 initial_partition.block_index=0;
397 initial_partition.state_index=0;
399 initial_partition.parent_block_index=0;
400 blocks.push_back(block());
401 blocks.back().swap(initial_partition);
402 block_index_of_a_state=std::vector < block_index_type >(aut.num_states(),0);
403 block_flags.push_back(false);
404 state_flags=std::vector < bool >(aut.num_states(),false);
405 block_is_in_to_be_processed.push_back(false);
406 to_be_processed.clear();
407 BL.clear();
408 } // end create_initial_partition
409
410// Refine the partition until the partition has become stable
411#ifndef NDEBUG
412 void refine_partition_until_it_becomes_stable(const bool branching, const bool preserve_divergence)
413#else
414 void refine_partition_until_it_becomes_stable(const bool, const bool)
415#endif
416 {
417#ifndef NDEBUG
418 std::size_t consistency_check_counter=1;
419 std::size_t consistency_check_barrier=1;
420#endif
421 bool partition_is_unstable=true; // This boolean indicates that the partition becomes unstable
422 // because an inert transition becomes non inert.
423 while (!to_be_processed.empty() || partition_is_unstable)
424 {
425#ifndef NDEBUG
426 // Avoid checking too often. This is too time consuming, even in debug mode.
427 consistency_check_counter++;
428 if (consistency_check_counter>=consistency_check_barrier)
429 {
430 consistency_check_counter=0;
431 consistency_check_barrier=consistency_check_barrier*2;
433 }
434#endif
435 if (to_be_processed.empty() && partition_is_unstable)
436 {
437 // Put all blocks in to_be_processed;
438 for (block_index_type i=0; i< blocks.size(); ++i)
439 {
440 to_be_processed.push_back(i);
441 }
442 block_is_in_to_be_processed=std::vector < bool >(blocks.size(),true);
443 partition_is_unstable=false;
444 }
445
446 const block_index_type splitter_index=to_be_processed.back();
447 // assert(block_is_in_to_be_processed[splitter_index]||!block_is_active[splitter_index]);
448 to_be_processed.pop_back();
449 block_is_in_to_be_processed[splitter_index]=false;
450
451 // Split with the splitter block, unless it is to_be_processed as we have to reconsider it
452 // completely anyhow at some later point.
453
454 // Walk through the non_inert_transitions via a natural number, because
455 // the blocks and the non_inert_transitions can move around in memory. This makes it
456 // unsafe to use interators.
457
458 for (std::size_t i=0; i<blocks[splitter_index].non_inert_transitions.size(); ++i)
459 {
460 // The flag of the starting state of *i is raised and its block is added to BL;
461
462 assert(blocks[splitter_index].non_inert_transitions[i].from()<aut.num_states());
463 state_flags[blocks[splitter_index].non_inert_transitions[i].from()]=true;
464 const block_index_type marked_block_index=block_index_of_a_state[blocks[splitter_index].non_inert_transitions[i].from()];
465 if (block_flags[marked_block_index]==false)
466 {
467 block_flags[marked_block_index]=true;
468 BL.push_back(marked_block_index);
469 }
470
471 // If the label of the next action is different, we must carry out the splitting.
472 if ((i+1)==blocks[splitter_index].non_inert_transitions.size() ||
473 aut.apply_hidden_label_map(blocks[splitter_index].non_inert_transitions[i].label())!=
474 aut.apply_hidden_label_map(blocks[splitter_index].non_inert_transitions[i+1].label()))
475 {
476 // We consider BL which contains references to all blocks from which a state from splitter
477 // can be reached. If not all flags of the non bottom states in a block in BL are set, the
478 // non flagged non bottom states are moved to a new block.
479
480 split_the_blocks_in_BL(partition_is_unstable,aut.apply_hidden_label_map(blocks[splitter_index].non_inert_transitions[i].label()),splitter_index);
481
482 }
483
484 }
485 }
486#ifndef NDEBUG
488#endif
489 block_flags.clear();
491 state_flags.clear();
492 to_be_processed.clear();
493 BL.clear();
494 }
495
496
497
499
501 bool& partition_is_unstable,
502 const label_type splitter_label,
503 const block_index_type splitter_block)
504 {
505 for (std::vector < block_index_type > :: const_iterator i1=BL.begin();
506 i1!=BL.end(); ++i1)
507 {
508 // assert(block_is_active[*i1]);
509 block_flags[*i1]=false;
510 std::vector < state_type > flagged_states;
511 std::vector < state_type > non_flagged_states;
512 std::vector < state_type > i1_bottom_states;
513 i1_bottom_states.swap(blocks[*i1].bottom_states);
514
515 for (std::vector < state_type >::const_iterator j=i1_bottom_states.begin();
516 j!=i1_bottom_states.end(); ++j)
517 {
518 if (state_flags[*j])
519 {
520 // state is flagged.
521 flagged_states.push_back(*j);
522 }
523 else
524 {
525 // state is not flagged. It will be moved to a new block.
526 non_flagged_states.push_back(*j);
528 }
529 }
530 assert(!flagged_states.empty()||!blocks[*i1].non_bottom_states.empty()||i1_bottom_states.empty());
531 block_index_type reset_state_flags_block=*i1;
532
533 if (!non_flagged_states.empty())
534 {
535 // There are flagged and non flagged states. So, the block must be split.
536 // Move the unflagged states to the new block.
537
538 if (mCRL2logEnabled(log::debug))
539 {
540 const std::size_t m = static_cast<std::size_t>(std::pow(10.0, std::floor(std::log10(static_cast<double>((blocks.size()+1)/2)))));
541 if ((blocks.size()+1)/2 % m==0)
542 {
543 mCRL2log(log::debug) << "Bisimulation partitioner: create block " << (blocks.size()+1)/2 << std::endl;
544 }
545 }
546
547 // Create a first new block.
548 blocks.push_back(block());
549 block_index_type new_block1=blocks.size()-1;
550 // block_is_active.push_back(true);
551 blocks.back().state_index=max_state_index;
553 blocks.back().block_index=new_block1;
554 blocks.back().parent_block_index=*i1;
555
556 non_flagged_states.swap(blocks.back().bottom_states);
557 // Put the indices of first split block to to_be_processed.
558 to_be_processed.push_back(blocks.back().block_index);
559 block_is_in_to_be_processed.push_back(true);
560
561 // Create a second new block.
562 blocks.push_back(block());
563 block_index_type new_block2=blocks.size()-1;
564 // block_is_active.push_back(true);
565 blocks.back().state_index=blocks[*i1].state_index;
566 blocks.back().block_index=new_block2;
567 reset_state_flags_block=new_block2;
568 blocks.back().parent_block_index=*i1;
569
570 // Move the flagged states to the second block, and let the block index of these states refer to this block.
571 flagged_states.swap(blocks.back().bottom_states);
572 std::vector < state_type > &reference_to_flagged_states_of_block2=blocks.back().bottom_states;
573 for (std::vector < state_type >::const_iterator j=reference_to_flagged_states_of_block2.begin();
574 j!=reference_to_flagged_states_of_block2.end(); ++j)
575 {
576 block_index_of_a_state[*j]=new_block2;
577 }
578
579 // NOTES: new_block1 = R, new_block2 = L
580 // Store counter formula info
582 {
583 right_child[*i1] = new_block1;
584 split_by_action[*i1] = splitter_label;
585 split_by_block[*i1] = splitter_block;
586
587 // compute r_alpha[new_block1]
588 std::set<block_index_type> reachable_blocks = {};
589 for (state_type source_state : blocks[new_block1].bottom_states)
590 {
591 for (outgoing_transitions_per_state_action_t::const_iterator i = outgoing_transitions.lower_bound(std::pair<state_type, label_type>(source_state, splitter_label));
592 i != outgoing_transitions.upper_bound(std::pair<state_type, label_type>(source_state, splitter_label)); ++i)
593 {
594 state_type target_state = to(i);
595 block_index_type target_block = block_index_of_a_state[target_state];
596 reachable_blocks.insert(target_block == new_block1 || target_block == new_block2 ? *i1 : target_block);
597 }
598 }
599 r_alpha[new_block1] = reachable_blocks;
600
601 if (branching) {
602 // compute r_tau[new_block1]
603 std::set<block_index_type> tau_reachable_blocks = {};
604 for (state_type source_state : blocks[new_block1].bottom_states)
605 {
606 for (label_type lab = 0; lab < aut.num_action_labels(); ++lab)
607 {
608 if (aut.is_tau(aut.apply_hidden_label_map(lab)))
609 {
610 for (outgoing_transitions_per_state_action_t::const_iterator i = outgoing_transitions.lower_bound(std::pair<state_type, label_type>(source_state, lab));
611 i != outgoing_transitions.upper_bound(std::pair<state_type, label_type>(source_state, lab)); ++i)
612 {
613 state_type target_state = to(i);
614 block_index_type target_block = block_index_of_a_state[target_state];
615 if (!(target_block == *i1 || target_block == new_block1 || target_block == new_block2))
616 {
617 tau_reachable_blocks.insert(target_block);
618 }
619 }
620 }
621 }
622 }
623 r_tauP[new_block1] = tau_reachable_blocks;
624 }
625 }
626
627 // Put the indices of second split block to to_be_processed.
628 to_be_processed.push_back(blocks.back().block_index);
629 block_is_in_to_be_processed.push_back(true);
630
631 // reset the flag of block *i1, which is being split.
633 // block_is_active[*i1]=false;
634
635 // The flag fields of the new blocks is set to false;
636 block_flags.push_back(false);
637 block_flags.push_back(false);
638
639 // Declare already some space for transitions, such that we can
640 // put inert transitions that become non inert in there when investigating
641 // the non bottom states. After investigating the non bottom states,
642 // the transitions are split over the vectors below.
643
644 std::vector < transition > flagged_non_inert_transitions;
645 std::vector < transition > non_flagged_non_inert_transitions;
646 // Reserve enough space for transitions to be copied. Otherwise, resizing may lead to
647 // lot of unneccesary copying...
648 flagged_non_inert_transitions.reserve(blocks[*i1].non_inert_transitions.size());
649 non_flagged_non_inert_transitions.reserve(blocks[*i1].non_inert_transitions.size());
650
651 // Next we scan the non-bottom states of *i1. If for some non-bottom state the flag is not raised
652 // and if none of the outgoing P-inert transitions leads to a state in the old block then this
653 // state becomes a non bottom state of B2.
654
655 std::vector < non_bottom_state > flagged_non_bottom_states;
656 std::vector < non_bottom_state > non_flagged_non_bottom_states;
657 std::vector < non_bottom_state > i1_non_bottom_states;
658 i1_non_bottom_states.swap(blocks[*i1].non_bottom_states);
659 for (typename std::vector < non_bottom_state >::iterator k=i1_non_bottom_states.begin();
660 k!=i1_non_bottom_states.end(); ++k)
661 {
662 const std::vector < state_type > &inert_transitions=k->inert_transitions;
663 if (!state_flags[k->state])
664 {
665 bool all_transitions_end_in_unflagged_block=true;
666 for (std::vector < state_type > :: const_iterator l=inert_transitions.begin();
667 all_transitions_end_in_unflagged_block && l!=inert_transitions.end(); ++l)
668 {
669 if (block_index_of_a_state[*l]!= new_block1)
670 {
671 block_index_of_a_state[*l]=new_block2;
672 all_transitions_end_in_unflagged_block=false;
673 }
674 }
675 if (all_transitions_end_in_unflagged_block)
676 {
677 // Move *k to the non flagged block. Swap the inert transitions to avoid copying.
678 non_bottom_state s(k->state);
679 s.inert_transitions.swap(k->inert_transitions);
680 non_flagged_non_bottom_states.push_back(s);
681 block_index_of_a_state[k->state]=new_block1;
682 continue;
683 }
684 }
685 // Move *k to the flagged block; note that the transitions can have become
686 // non-inert. So, investigate them separately.
687 std::vector < state_type > remaining_inert_transitions;
688 for (std::vector < state_type > :: const_iterator l=inert_transitions.begin();
689 l!=inert_transitions.end(); ++l)
690 {
691 if (block_index_of_a_state[*l]==new_block1)
692 {
693 // The transition *l (*k,tau_label,*l) becomes a non inert transition in the new
694 // block.
695 non_flagged_non_inert_transitions.push_back(transition(k->state,aut.tau_label_index(),*l));
696 }
697 else
698 {
699 // The transition represented by *l remains an inert transition.
700 block_index_of_a_state[*l]=new_block2;
701 remaining_inert_transitions.push_back(*l);
702 }
703 }
704 if (remaining_inert_transitions.empty()) // The last outgoing inert tau transition just became non inert.
705 // k->state has become a bottom state. Otherwise it remains
706 // a non bottom state.
707 {
708 blocks[new_block2].bottom_states.push_back(k->state);
709 block_index_of_a_state[k->state]=new_block2;
710 partition_is_unstable=true;
711 }
712 else
713 {
714 flagged_non_bottom_states.push_back(non_bottom_state(k->state,remaining_inert_transitions));
715 block_index_of_a_state[k->state]=new_block2;
716 }
717 }
718 non_flagged_non_bottom_states.swap(blocks[new_block1].non_bottom_states);
719 flagged_non_bottom_states.swap(blocks[new_block2].non_bottom_states);
720
721 // Finally the non-inert transitions are distributed over both blocks in the obvious way.
722 // Note that this must be done after all states are properly put into a new block.
723
724 assert(*i1 < blocks.size());
725 std::vector < transition > i1_non_inert_transitions;
726 i1_non_inert_transitions.swap(blocks[*i1].non_inert_transitions);
727 for (std::vector < transition >::iterator k=i1_non_inert_transitions.begin();
728 k!=i1_non_inert_transitions.end(); ++k)
729 {
730 if (block_index_of_a_state[k->to()]==new_block1)
731 {
732 non_flagged_non_inert_transitions.push_back(*k);
733 }
734 else
735 {
736 block_index_of_a_state[k->to()]=new_block2;
737 flagged_non_inert_transitions.push_back(*k);
738 }
739 }
740
741 // Only put the parts that we need to store. Avoid that reserved space for
742 // current_inert_transition_counter and flagged_non_inert_transitions is stored
743 // in the non_inert_transitions in both blocks. Therefore, we do not use a copy
744 // constructor, but put elements in there one by one.
745 // The two lines below were old code, wasting memory bandwidth.
746 // non_flagged_non_inert_transitions.swap(blocks[new_block1].non_inert_transitions);
747 // flagged_non_inert_transitions.swap(blocks[new_block2].non_inert_transitions);
748
749 blocks[new_block1].non_inert_transitions.reserve(non_flagged_non_inert_transitions.size());
750 for(std::vector < transition > ::const_iterator i=non_flagged_non_inert_transitions.begin();
751 i!=non_flagged_non_inert_transitions.end(); i++)
752 {
753 blocks[new_block1].non_inert_transitions.push_back(*i);
754 }
755
756 blocks[new_block2].non_inert_transitions.reserve(flagged_non_inert_transitions.size());
757 for(std::vector < transition > ::const_iterator i=flagged_non_inert_transitions.begin();
758 i!=flagged_non_inert_transitions.end(); i++)
759 {
760 blocks[new_block2].non_inert_transitions.push_back(*i);
761 }
762 }
763 else
764 {
765 // Nothing changed, so put the bottom states back again.
766 i1_bottom_states.swap(blocks[*i1].bottom_states);
767 }
768 // reset the state flags
769 std::vector < state_type > &flagged_states_to_be_unflagged=blocks[reset_state_flags_block].bottom_states;
770 for (std::vector < state_type >::const_iterator j=flagged_states_to_be_unflagged.begin();
771 j!=flagged_states_to_be_unflagged.end(); ++j)
772 {
773 state_flags[*j]=false;
774 }
775
776 std::vector < non_bottom_state > &flagged_states_to_be_unflagged1=blocks[reset_state_flags_block].non_bottom_states;
777 for (typename std::vector < non_bottom_state >::const_iterator j=flagged_states_to_be_unflagged1.begin();
778 j!=flagged_states_to_be_unflagged1.end(); ++j)
779 {
780 state_flags[j->state]=false;
781 }
782 }
783 BL.clear();
784 }
785
787 const state_type s,
788 std::map < state_type, std::vector < state_type > >& inert_transition_map,
789 std::vector < non_bottom_state >& new_non_bottom_states,
790 std::set < state_type >& visited)
791 {
792 if (inert_transition_map.count(s)>0) // The state s is a bottom state. We need not to investigate these.
793 {
794 if (visited.count(s)==0)
795 {
796 visited.insert(s);
797 std::vector < state_type> &inert_transitions=inert_transition_map[s];
798 for (std::vector < state_type>::const_iterator j=inert_transitions.begin();
799 j!=inert_transitions.end(); j++)
800 {
801 order_recursively_on_tau_reachability(*j,inert_transition_map,new_non_bottom_states,visited);
802 }
803 new_non_bottom_states.push_back(non_bottom_state(s));
804 inert_transitions.swap(new_non_bottom_states.back().inert_transitions);
805 }
806 }
807 }
808
809 void order_on_tau_reachability(std::vector < non_bottom_state > &non_bottom_states)
810 {
811 std::set < state_type > visited;
812 std::map < state_type, std::vector < state_type > > inert_transition_map;
813 for (typename std::vector < non_bottom_state >::iterator i=non_bottom_states.begin();
814 i!=non_bottom_states.end(); ++i)
815 {
816 i->inert_transitions.swap(inert_transition_map[i->state]);
817 }
818 std::vector < non_bottom_state > new_non_bottom_states;
819
820 for (typename std::vector < non_bottom_state >::const_iterator i=non_bottom_states.begin();
821 i!=non_bottom_states.end(); ++i)
822 {
823 order_recursively_on_tau_reachability(i->state, inert_transition_map, new_non_bottom_states, visited);
824 }
825 new_non_bottom_states.swap(non_bottom_states);
826 }
827
833 mcrl2::state_formulas::state_formula conjunction(std::set<mcrl2::state_formulas::state_formula> terms) const
834 {
835 return utilities::detail::join<mcrl2::state_formulas::state_formula>(terms.begin(), terms.end(),
837 { return mcrl2::state_formulas::and_(a, b); }, mcrl2::state_formulas::true_());
838 }
839
847 {
849 }
850
858 {
861 }
862
876 {
877 std::string var = "X" + std::to_string(fresh_var_counter++);
881
884
885 if (aut.is_tau(aut.apply_hidden_label_map(a)))
886 {
887 until = mcrl2::state_formulas::or_(phi2, until);
888 }
889 return until;
890 }
891
892 /* \brief Creates a state formula that distinguishes states in block B1 from state in block B2.
893 \details Based on "Computing Distinguishing Formulas for Branching Bisimulation", 1991 by Henri Korver.
894 Variable names used below correspond to definitions in this paper.
895 \param[in] B1 The block on which the resulting formula must be true.
896 \param[in] B2 The block on which the resulting formula must be false.
897 \return A distinguishing state formula.
898 */
900 {
901 // First find the smallest block containing both B1 and B2.
902 // Find all blocks containing B1.
903 std::set < block_index_type > blocks_containing_B1;
904 block_index_type B1p = B1;
905 blocks_containing_B1.insert(B1p);
906 while (blocks[B1p].parent_block_index != B1p)
907 {
908 B1p = blocks[B1p].parent_block_index;
909 blocks_containing_B1.insert(B1p);
910 }
911
912 // Go up the block tree from B2 until we find a block that contains B1.
913 block_index_type DB = B2;
914 while (blocks_containing_B1.count(DB) == 0)
915 {
916 assert(blocks[DB].parent_block_index != DB);
917 DB = blocks[DB].parent_block_index;
918 }
919
920 // Now DB is the smallest block containing both B1 and B2.
921
922 const block_index_type R = right_child.at(DB);
923 const label_type a = split_by_action.at(DB);
924 const block_index_type Bp = split_by_block.at(DB);
925
926 // We distinguish Bp with every block in r_alpha[R]
927 std::set<mcrl2::state_formulas::state_formula> Gamma2;
928 for (block_index_type PPB : r_alpha.at(R))
929 {
930 Gamma2.insert(counter_formula_aux(Bp, PPB));
931 }
933
935 if (branching)
936 {
937 // We distinguish DB with every block in r_tauP[R]
938 std::set<mcrl2::state_formulas::state_formula> Gamma1;
939 for (block_index_type PPB : r_tauP.at(R))
940 {
941 Gamma1.insert(counter_formula_aux(DB, PPB));
942 }
944
945 // In case a == tau, we also need to distinguish Bp with R
946 if (aut.is_tau(aut.apply_hidden_label_map(a)))
947 {
949 }
950
951 Phi = until_formula(Phi1, a, Phi2);
952 }
953 else
954 {
955 Phi = mcrl2::state_formulas::may(create_regular_formula(aut.action_label(a)), Phi2);
956 }
957
958 if (blocks_containing_B1.count(R) == 0)
959 {
960 return Phi;
961 }
962 else
963 {
964 return mcrl2::state_formulas::not_(Phi);
965 }
966 }
967
968
969#ifndef NDEBUG
970 // The method below is intended to check the consistency of the internal data
971 // structure. Its sole purpose is to detect programming errors. It has no
972 // side effects on the data structure. If a problem occurs, execution halts with
973 // an assert.
974
976 const bool branching,
977 const bool preserve_divergence) const
978 {
979 state_type total_number_of_states=0;
980 std::size_t total_number_of_transitions=0;
981
982 assert(!blocks.empty());
983 std::set < block_index_type > block_indices;
984
985 assert(block_index_of_a_state.size()==aut.num_states());
986 for (typename std::vector < block >::const_iterator i=blocks.begin();
987 i!=blocks.end(); ++i)
988 {
989 // Check the block_index.
990 assert(i->block_index<blocks.size());
991 assert(block_indices.count(i->block_index)==0);
992 block_indices.insert(i->block_index);
993
994 // Check the bottom states.
995 const std::vector < state_type > &i_bottom_states=i->bottom_states;
996
997 for (std::vector < state_type >::const_iterator j=i_bottom_states.begin();
998 j!=i_bottom_states.end(); ++j)
999 {
1000 total_number_of_states++;
1001 assert(*j<aut.num_states());
1002 // Check that the block number of the state is maintained properly.
1003 assert(block_index_of_a_state[*j]==i->block_index);
1004 }
1005
1006 // Check the non bottom states. In particular check that there is no tau loop
1007 // in these non bottom states.
1008 const std::vector < non_bottom_state > &i_non_bottom_states=i->non_bottom_states;
1009 std::set < state_type > visited;
1010 std::set < state_type > local_bottom_states;
1011 for (typename std::vector < non_bottom_state >::const_iterator j=i_non_bottom_states.begin();
1012 j!=i_non_bottom_states.end(); ++j)
1013 {
1014 local_bottom_states.insert(j->state);
1015 }
1016
1017 for (typename std::vector < non_bottom_state >::const_iterator j=i_non_bottom_states.begin();
1018 j!=i_non_bottom_states.end(); ++j)
1019 {
1020 total_number_of_states++;
1021 assert(j->state<aut.num_states());
1022 // Check that the block number of the state is maintained properly.
1023 assert(block_index_of_a_state[j->state]==i->block_index);
1024 const std::vector < state_type > &j_inert_transitions=j->inert_transitions;
1025 for (std::vector < state_type >::const_iterator k=j_inert_transitions.begin();
1026 k!=j_inert_transitions.end(); k++)
1027 {
1028 total_number_of_transitions++;
1029 assert(*k<aut.num_states());
1030 // Check that the inert transitions are well ordered.
1031 assert(visited.count(*k)>0 || local_bottom_states.count(*k)==0);
1032 }
1033 visited.insert(j->state);
1034 }
1035
1036 // Check the non_inert_transitions. It is required that the transitions
1037 // are grouped per label, and that tau transitions must be inert.
1038
1039 const std::vector < transition > &i_non_inert_transitions=i->non_inert_transitions;
1040 std::set < label_type > observed_action_labels;
1041 for (std::vector < transition >::const_iterator j=i_non_inert_transitions.begin();
1042 j!=i_non_inert_transitions.end(); ++j)
1043 {
1044 total_number_of_transitions++;
1045 assert(j->to()<aut.num_states());
1046 assert(j->from()<aut.num_states());
1047
1048 // Check proper grouping of action labels.
1049 std::vector < transition >::const_iterator j_next=j;
1050 j_next++;
1051 if (j_next==i_non_inert_transitions.end() || (aut.apply_hidden_label_map(j->label())!=aut.apply_hidden_label_map(j_next->label())))
1052 {
1053 assert(observed_action_labels.count(aut.apply_hidden_label_map(j->label()))==0);
1054 observed_action_labels.insert(aut.apply_hidden_label_map(j->label()));
1055 }
1056
1057 // Check whether tau transition in non inert transition vector is inert.
1058 if (!preserve_divergence && branching && aut.is_tau(aut.apply_hidden_label_map(j->label())))
1059 {
1060 assert(j->to()!=j->from());
1061 }
1062
1063 // Check whether the target state of the transition is in the current block.
1064 assert(block_index_of_a_state[j->to()]==i->block_index);
1065 }
1066 }
1067
1068 // Check total number of states and transitions.
1069 assert(total_number_of_states==aut.num_states());
1070 assert(total_number_of_transitions==aut.num_transitions());
1071
1072 // Check block_index_of_a_state
1073 assert(block_index_of_a_state.size()==aut.num_states());
1074 for (std::vector < state_type >::const_iterator i=block_index_of_a_state.begin();
1075 i!=block_index_of_a_state.end(); ++i)
1076 {
1077 assert(blocks[*i].block_index== *i);
1078 }
1079
1080 // Check block_flags that the block flags are all set to false
1081 for (std::vector < bool >::const_iterator i=block_flags.begin();
1082 i!=block_flags.end(); ++i)
1083 {
1084 assert(!*i);
1085 }
1086
1087 // Check that state_flags are all false.
1088 for (std::vector < bool >::const_iterator i=state_flags.begin();
1089 i!=state_flags.end(); ++i)
1090 {
1091 assert(!*i);
1092 }
1093
1094 // Check to_be_processed
1095 // Check block_is_in_to_be_processed
1096 std::vector < bool > temporary_block_is_in_to_be_processed(blocks.size(),false);
1097
1098 for (std::vector< block_index_type > ::const_iterator i=to_be_processed.begin();
1099 i!=to_be_processed.end(); ++i)
1100 {
1101 temporary_block_is_in_to_be_processed[*i]=true;
1102 }
1103 for (state_type i=0; i<blocks.size(); ++i)
1104 {
1105 assert(!block_is_in_to_be_processed[i] || temporary_block_is_in_to_be_processed[i]);
1106 }
1107
1108 // Check that BL is empty.
1109 assert(BL.empty());
1110
1111 }
1112
1113#endif // not NDEBUG
1114
1115};
1116
1117
1123template < class LTS_TYPE>
1124void bisimulation_reduce(
1125 LTS_TYPE& l,
1126 const bool branching = false,
1127 const bool preserve_divergences = false);
1128
1129
1142template < class LTS_TYPE>
1143bool destructive_bisimulation_compare(
1144 LTS_TYPE& l1,
1145 LTS_TYPE& l2,
1146 const bool branching = false,
1147 const bool preserve_divergences = false,
1148 const bool generate_counter_examples = false,
1149 const std::string& counter_example_file = "",
1150 const bool structured_output = false);
1151
1152
1167template < class LTS_TYPE>
1168bool bisimulation_compare(
1169 const LTS_TYPE& l1,
1170 const LTS_TYPE& l2,
1171 const bool branching = false,
1172 const bool preserve_divergences = false,
1173 const bool generate_counter_examples = false,
1174 const std::string& counter_example_file = "",
1175 const bool structured_output = false);
1176
1177
1178
1179
1180
1181template < class LTS_TYPE>
1183 const std::size_t s, const std::size_t t)
1184{
1185 if (get_eq_class(s)==get_eq_class(t))
1186 {
1187 throw mcrl2::runtime_error("Requesting a counter state formula for two bisimilar states. Such a state formula is not useful.");
1188 }
1189
1190 return counter_formula_aux(block_index_of_a_state[s], block_index_of_a_state[t]);
1191}
1192
1193
1194template < class LTS_TYPE>
1195void bisimulation_reduce(LTS_TYPE& l,
1196 const bool branching /*=false */,
1197 const bool preserve_divergences /*=false */)
1198{
1199 // First, remove tau loops in case of branching bisimulation.
1200 if (branching)
1201 {
1202 scc_reduce(l,preserve_divergences);
1203 }
1204
1205 // Secondly, apply the branching bisimulation reduction algorithm. If there are no tau's,
1206 // this will automatically yield strong bisimulation.
1207 detail::bisim_partitioner<LTS_TYPE> bisim_part(l, branching, preserve_divergences);
1208
1209 // Assign the reduced LTS
1210 bisim_part.replace_transition_system(branching,preserve_divergences);
1211}
1212
1213template < class LTS_TYPE>
1215 const LTS_TYPE& l1,
1216 const LTS_TYPE& l2,
1217 const bool branching /* =false*/,
1218 const bool preserve_divergences /*=false*/,
1219 const bool generate_counter_examples /*= false*/,
1220 const std::string& /* counter_example_file = ""*/,
1221 const bool structured_output /* = false */)
1222{
1223 LTS_TYPE l1_copy(l1);
1224 LTS_TYPE l2_copy(l2);
1225 return destructive_bisimulation_compare(l1_copy,l2_copy,branching,preserve_divergences,
1226 generate_counter_examples, structured_output);
1227}
1228
1241template < class LTS_TYPE>
1243 LTS_TYPE& l1,
1244 LTS_TYPE& l2,
1245 const bool branching /* =false*/,
1246 const bool preserve_divergences /*=false*/,
1247 const bool generate_counter_examples /* = false */,
1248 const std::string& counter_example_file /*= ""*/,
1249 const bool /*structured_output = false */)
1250{
1251 std::size_t init_l2 = l2.initial_state() + l1.num_states();
1253 l2.clear(); // No use for l2 anymore.
1254
1255 // First remove tau loops in case of branching bisimulation.
1256 if (branching)
1257 {
1259 scc_part.replace_transition_system(preserve_divergences);
1260 init_l2 = scc_part.get_eq_class(init_l2);
1261 }
1262
1263 detail::bisim_partitioner<LTS_TYPE> bisim_part(l1, branching, preserve_divergences, generate_counter_examples);
1264 if (generate_counter_examples && !bisim_part.in_same_class(l1.initial_state(), init_l2))
1265 {
1266 mcrl2::state_formulas::state_formula counter_example_formula = bisim_part.counter_formula(l1.initial_state(), init_l2);
1267
1268 std::string filename = "Counterexample.mcf";
1269 if (!counter_example_file.empty())
1270 {
1271 filename = counter_example_file;
1272 }
1273 std::ofstream counter_file(filename);
1274 counter_file << mcrl2::state_formulas::pp(counter_example_formula);
1275 counter_file.close();
1276 mCRL2log(mcrl2::log::info) << "Saved counterexample to: \"" << filename << "\"" << std::endl;
1277
1278 }
1279 return bisim_part.in_same_class(l1.initial_state(),init_l2);
1280}
1281
1282
1283}
1284}
1285}
1286#endif
Read-only balanced binary tree of terms.
A list of aterm objects.
Definition aterm_list.h:24
\brief The multi action for action formulas
\brief A timed multi-action
const process::action_list & actions() const
This class contains strings to be used as values for action labels in lts's.
mcrl2::state_formulas::state_formula conjunction(std::set< mcrl2::state_formulas::state_formula > terms) const
conjunction Creates a conjunction of state formulas
regular_formulas::regular_formula create_regular_formula(const mcrl2::lts::action_label_string &a) const
create_regular_formula Creates a regular formula that represents action a
regular_formulas::regular_formula create_regular_formula(const mcrl2::lps::multi_action &a) const
create_regular_formula Creates a regular formula that represents action a
std::vector< bool > block_is_in_to_be_processed
std::map< block_index_type, block_index_type > right_child
std::vector< block_index_type > BL
bool in_same_class(const std::size_t s, const std::size_t t) const
Returns whether two states are in the same bisimulation equivalence class.
mcrl2::state_formulas::state_formula until_formula(const mcrl2::state_formulas::state_formula &phi1, const label_type &a, const mcrl2::state_formulas::state_formula &phi2)
until_formula Creates a state formula that corresponds to the until operator phi1phi2 from HMLU
std::size_t get_eq_class(const std::size_t s) const
Gives the bisimulation equivalence class number of a state.
bisim_partitioner(LTS_TYPE &l, const bool branching=false, const bool preserve_divergence=false, const bool generate_counter_examples=false)
Creates a bisimulation partitioner for an LTS.
~bisim_partitioner()=default
Destroys this partitioner.
std::map< block_index_type, std::set< block_index_type > > r_tauP
std::map< block_index_type, label_type > split_by_action
std::size_t num_eq_classes() const
Gives the number of bisimulation equivalence classes of the LTS.
void order_recursively_on_tau_reachability(const state_type s, std::map< state_type, std::vector< state_type > > &inert_transition_map, std::vector< non_bottom_state > &new_non_bottom_states, std::set< state_type > &visited)
std::vector< block_index_type > to_be_processed
std::map< block_index_type, block_index_type > split_by_block
void replace_transition_system(const bool branching, const bool preserve_divergences)
Replaces the transition relation of the current lts by the transitions of the bisimulation reduced tr...
void order_on_tau_reachability(std::vector< non_bottom_state > &non_bottom_states)
void split_the_blocks_in_BL(bool &partition_is_unstable, const label_type splitter_label, const block_index_type splitter_block)
void refine_partition_until_it_becomes_stable(const bool branching, const bool preserve_divergence)
void create_initial_partition(const bool branching, const bool preserve_divergences)
std::vector< state_type > block_index_of_a_state
std::map< block_index_type, std::set< block_index_type > > r_alpha
mcrl2::state_formulas::state_formula counter_formula_aux(const block_index_type B1, const block_index_type B2)
mcrl2::state_formulas::state_formula counter_formula(const std::size_t s, const std::size_t t)
Creates a state formula that distinguishes state s from state t.
void check_internal_consistency_of_the_partitioning_data_structure(const bool branching, const bool preserve_divergence) const
outgoing_transitions_per_state_action_t outgoing_transitions
This class contains an scc partitioner removing inert tau loops.
Definition liblts_scc.h:128
std::size_t get_eq_class(const std::size_t s) const
Gives the equivalence class number of a state. The equivalence class numbers range from 0 upto (and e...
Definition liblts_scc.h:307
void replace_transition_system(const bool preserve_divergence_loops)
The lts for which this partioner is created is replaced by the lts modulo the calculated partition.
Definition liblts_scc.h:248
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
\brief An action label
Standard exception class for reporting runtime errors.
Definition exception.h:27
\brief The and operator for state formulas
\brief The may operator for state formulas
\brief The mu operator for state formulas
\brief The not operator for state formulas
\brief The or operator for state formulas
\brief The value true for state formulas
\brief The state formula variable
#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.
@ verbose
Definition logger.h:35
bool bisimulation_compare(const LTS_TYPE &l1, const 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.
void merge(LTS_TYPE &l1, const LTS_TYPE &l2)
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.
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.
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(const std::vector< transition > &trans)
Provide the transitions as a multimap accessible per from state and label.
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.
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.
void scc_reduce(LTS_TYPE &l, const bool preserve_divergence_loops=false)
Definition liblts_scc.h:362
void pp(const T &t, std::ostream &out)
Prints the object t to a stream.
Definition print.h:668
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Add your file description here.
std::vector< transition > non_inert_transitions
std::vector< non_bottom_state > non_bottom_states
non_bottom_state(const state_type s, const std::vector< state_type > &it)