mCRL2
Loading...
Searching...
No Matches
liblts_bisim_gjkw.cpp
Go to the documentation of this file.
1// Author(s): David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
2//
3// Copyright: see the accompanying file COPYING or copy at
4// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
5//
6// Distributed under the Boost Software License, Version 1.0.
7// (See accompanying file LICENSE_1_0.txt or copy at
8// http://www.boost.org/LICENSE_1_0.txt)
9
22
23#include "mcrl2/lts/detail/liblts_bisim_gjkw.h"
24#include "mcrl2/lts/detail/coroutine.h"
25#include "mcrl2/lts/lts_aut.h"
26#include "mcrl2/lts/lts_fsm.h"
27#include "mcrl2/lts/lts_utilities.h"
28
29#define PARANOID_CHECK
30
31namespace mcrl2
32{
33namespace lts
34{
35namespace detail
36{
37namespace bisim_gjkw
38{
39
40
41
42
43
44/* ************************************************************************* */
45/* */
46/* R E F I N A B L E P A R T I T I O N */
47/* */
48/* ************************************************************************* */
49
50
51
52
53
54block_t* block_t::refinable_first = nullptr;
55state_type block_t::nr_of_blocks = 0;
56constln_t* constln_t::nontrivial_first = nullptr;
57 #ifndef NDEBUG
58 // These variables are only accessed in debug mode. In release mode,
59 // accessing them would lead to a linker error.
60 state_info_const_ptr state_info_entry::s_i_begin;
61 state_info_const_ptr state_info_entry::s_i_end;
62 permutation_const_iter_t block_t::perm_begin;
63 #endif
70block_t* block_t::split_off_blue(permutation_iter_t const blue_nonbottom_end)
71{ assert(unmarked_nonbottom_end() >= blue_nonbottom_end);
72 assert(unmarked_nonbottom_begin() <= blue_nonbottom_end);
73 assert(0 != unmarked_bottom_size());
74 permutation_iter_t const splitpoint = blue_nonbottom_end +
75 unmarked_bottom_size(); assert(splitpoint < end()); assert(begin() < splitpoint);
76 #ifndef NDEBUG
77 unsigned const max_counter = check_complexity::log_n -
78 /* It is not necessary to reset the nottoblue counters; these counters */ check_complexity::ilog2((state_type) (splitpoint - begin()));
79 /* are anyway only valid for the maybe-blue states. */ assert((state_type) (splitpoint - begin()) <= size()/2);
80 #endif
81 if (state_type swapcount = std::min(unmarked_bottom_size(),
82 (state_type) (marked_nonbottom_end() - blue_nonbottom_end));
83 0 != swapcount)
84 {
85 // vector swap the states:
86 permutation_iter_t pos1=blue_nonbottom_end, pos2=unmarked_bottom_end();
87 state_info_ptr const temp = *pos1;
88 for (;;)
89 {
90 --pos2; mCRL2complexity(*pos2, add_work(check_complexity::
91 Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29, max_counter), );
92 *pos1 = *pos2;
93 (*pos1)->pos = pos1;
94 ++pos1;
95 if (0 == --swapcount) break;
96 *pos2 = *pos1;
97 (*pos2)-> pos = pos2;
98 }
99 *pos2 = temp;
100 (*pos2)->pos = pos2;
101 }
102
103 // create a new block for the blue states
104 block_t* const NewB = new block_t(constln(), begin(), splitpoint);
105 #ifndef NDEBUG
106 NewB->work_counter = work_counter;
107 #endif
108 if (BLOCK_NO_SEQNR != seqnr())
109 {
110 NewB->assign_seqnr();
111 }
112 // NewB->set_begin(begin());
113 NewB->set_bottom_begin(blue_nonbottom_end);
114 NewB->set_marked_nonbottom_begin(blue_nonbottom_end);
115 // NewB->set_marked_bottom_begin(splitpoint);
116 /* NewB->set_end(splitpoint); */ assert(NewB->to_constln.empty());
117 /* NewB->set_inert_begin(?); */ mCRL2complexity(NewB, add_work(check_complexity::
118 /* NewB->set_inert_end(?); */ Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29, max_counter), );
119 for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
120 { // mCRL2complexity(*s_iter, ...) -- optimized to the above call.
121 (*s_iter)->block = NewB;
122 }
123
124 // adapt the old block: it only keeps the red states
125 // set_end(end());
126 set_bottom_begin(marked_bottom_begin());
127 // set_marked_bottom_begin(marked_bottom_begin());
128 set_marked_nonbottom_begin(marked_bottom_begin());
129 set_begin(splitpoint);
130
131 constln()->make_nontrivial();
132
133 return NewB;
134}
135
149block_t* block_t::split_off_red(permutation_iter_t const red_nonbottom_begin)
150{ assert(marked_nonbottom_begin() == red_nonbottom_begin);
151 assert(marked_nonbottom_end() >= red_nonbottom_begin);
152 assert(0 != marked_size());
153 permutation_iter_t const splitpoint = red_nonbottom_begin +
154 unmarked_bottom_size(); assert(begin() < splitpoint); assert(splitpoint < end());
155 #ifndef NDEBUG
156 unsigned const max_counter = check_complexity::log_n -
157 /* It is not necessary to reset the nottoblue counters; these counters */ check_complexity::ilog2((state_type) (end() - splitpoint));
158 /* are anyway only valid for the maybe-blue states. */ assert((state_type) (end() - splitpoint) <= size() / 2);
159 #endif
160 if (state_type swapcount = std::min(unmarked_bottom_size(),
161 (state_type) (marked_nonbottom_end() - red_nonbottom_begin));
162 0 != swapcount)
163 {
164 // vector swap the states:
165 permutation_iter_t pos1=red_nonbottom_begin,pos2=unmarked_bottom_end();
166 state_info_ptr const temp = *pos1;
167 for (;;)
168 { mCRL2complexity(*pos1, add_work(check_complexity::
169 Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29, max_counter), );
170 *pos1 = *--pos2;
171 (*pos1)->pos = pos1;
172 ++pos1;
173 if (0 == --swapcount) break;
174 *pos2 = *pos1;
175 (*pos2)->pos = pos2;
176 }
177 *pos2 = temp;
178 (*pos2)->pos = pos2;
179 }
180 // create a new block for the red states
181 block_t* const NewB = new block_t(constln(), splitpoint, end());
182 #ifndef NDEBUG
183 NewB->work_counter = work_counter;
184 #endif
185 if (BLOCK_NO_SEQNR != seqnr())
186 {
187 NewB->assign_seqnr();
188 }
189 // NewB->set_end(end());
190 NewB->set_marked_bottom_begin(marked_bottom_begin());
191 NewB->set_bottom_begin(marked_bottom_begin());
192 NewB->set_marked_nonbottom_begin(marked_bottom_begin());
193 /* NewB->set_begin(splitpoint); */ assert(NewB->to_constln.empty());
194 /* NewB->set_inert_begin(?); */ mCRL2complexity(NewB, add_work(check_complexity::
195 /* NewB->set_inert_end(?); */ Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29, max_counter), );
196 for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
197 { // mCRL2complexity(*s_iter, ...) -- optimized to the above call.
198 (*s_iter)->block = NewB;
199 }
200
201 // adapt the old block: it only keeps the blue states
202 // set_begin(begin());
203 set_marked_nonbottom_begin(red_nonbottom_begin);
204 set_bottom_begin(red_nonbottom_begin);
205 set_marked_bottom_begin(splitpoint);
206 set_end(splitpoint);
207
208 constln()->make_nontrivial();
209
210 return NewB;
211}
212 #ifndef NDEBUG
221 void part_state_t::print_block(const char* const message,
222 const block_t* const B,
223 permutation_const_iter_t begin,
224 permutation_const_iter_t const end) const
225 {
226 if (0 != end - begin)
227 {
228 mCRL2log(log::debug) << "\t\t" << message
229 << (1 < end-begin ? "s:\n" : ":\n");
230 do
231 {
232 mCRL2log(log::debug) << "\t\t\t"
233 << (*begin)->debug_id();
234 if (B != (*begin)->block)
235 {
236 mCRL2log(log::debug) << ", inconsistent: "
237 "points to " << (*begin)->block->debug_id();
238 }
239 if (begin != (*begin)->pos)
240 {
241 mCRL2log(log::debug)
242 << ", inconsistent pointer to state_info_entry";
243 }
244 mCRL2log(log::debug) << '\n';
245 }
246 while (++begin != end);
247 }
248 }
249
255 void part_state_t::print_part(const part_trans_t& part_tr) const
256 {
257 assert(permutation.begin() < permutation.end());
258 for (const constln_t* C = permutation.front()->constln(); ; )
259 {
260 mCRL2log(log::debug) << C->debug_id() << ":\n";
261 assert(C->begin() < C->end());
262 for (const block_t* B = (*C->begin())->block; ; )
263 {
264 mCRL2log(log::debug) << "\t" << B->debug_id();
265 if (C != B->constln())
266 {
267 mCRL2log(log::debug) << ", inconsistent: "
268 "points to " << B->constln()->debug_id();
269 }
270 mCRL2log(log::debug) << ":\n";
271 print_block("Non-bottom state", B, B->nonbottom_begin(),
272 B->nonbottom_end());
273 print_block("Bottom state", B, B->bottom_begin(),
274 B->bottom_end());
275 mCRL2log(log::debug) << "\t\tThis block has ";
276 if (B->inert_end() == part_tr.B_to_C_begin())
277 {
278 mCRL2log(log::debug)
279 << "no transitions to its own constellation.\n";
280 assert(B->inert_begin() == B->inert_end());
281 }
282 else
283 {
284 assert(B->inert_end() ==
285 B->inert_end()[-1].B_to_C_slice->end);
286 assert(B->inert_end()[-1].B_to_C_slice->from_block() == B);
287 assert(B->inert_end()[-1].B_to_C_slice->to_constln() == C);
288 mCRL2log(log::debug) << B->inert_end() -
289 B->inert_end()[-1].B_to_C_slice->begin
290 <<" transition(s) to its own constellation,\n\t\tof which "
291 << B->inert_end() - B->inert_begin()
292 << (1 == B->inert_end() - B->inert_begin()
293 ? " is inert.\n" : " are inert.\n");
294 }
295 // go to next block
296 if (C->end() == B->end()) break;
297 B = (*B->end())->block;
298 }
299 // go to next constellation
300 if (permutation.end() == C->end()) break;
301 C = (*C->end())->constln();
302 }
303 }
304
309 void part_state_t::print_trans() const
310 {
311 fixed_vector<state_info_entry>::const_iterator const state_info_end =
312 state_info.end() - 1;
313 for (fixed_vector<state_info_entry>::const_iterator state_iter =
314 state_info.begin(); state_info_end != state_iter; ++state_iter)
315 {
316 // print transitions out of state
317 succ_const_iter_t succ_constln_iter = state_iter->succ_begin();
318 if (state_iter->succ_end() != succ_constln_iter)
319 {
320 mCRL2log(log::debug) << state_iter->debug_id()
321 << ":\n";
322 assert(state_iter->succ_begin() <=
323 state_iter->inert_succ_begin());
324 assert(state_iter->inert_succ_begin() <=
325 state_iter->inert_succ_end());
326 assert(state_iter->succ_begin()==state_iter->inert_succ_begin()
327 || *state_iter->inert_succ_begin()[-1].target->constln() <=
328 *state_iter->constln());
329 assert(state_iter->succ_begin()==state_iter->inert_succ_begin()
330 || state_iter->inert_succ_begin()[-1].target->block !=
331 state_iter->block);
332 assert(state_iter->inert_succ_begin() ==
333 state_iter->inert_succ_end() ||
334 (state_iter->inert_succ_begin()->target->block ==
335 state_iter->block &&
336 state_iter->inert_succ_end()[-1].target->block ==
337 state_iter->block));
338 assert(state_iter->succ_end() == state_iter->inert_succ_end()||
339 *state_iter->constln() <
340 *state_iter->inert_succ_end()->target->constln());
341 do
342 {
343 // print transitions to a constellation
344 mCRL2log(log::debug) << "\ttransitions to "
345 << succ_constln_iter->target->constln()->debug_id()
346 << ":\n";
347 succ_const_iter_t s_iter = succ_constln_iter;
348 // set succ_constln_iter to the end of the transitions to
349 // this constellation
350 succ_constln_iter=succ_entry::slice_end(succ_constln_iter);
351 for ( ;s_iter != succ_constln_iter ;++s_iter)
352 {
353 mCRL2log(log::debug) << "\t\tto "
354 << s_iter->target->debug_id();
355 if (state_iter->inert_succ_begin() <= s_iter &&
356 s_iter < state_iter->inert_succ_end())
357 {
358 mCRL2log(log::debug) << " (inert)";
359 }
360 if (state_iter->current_constln() == s_iter)
361 {
362 mCRL2log(log::debug)
363 << " <- current_constln";
364 }
365 mCRL2log(log::debug) << '\n';
366 assert(s_iter->B_to_C->pred->succ == s_iter);
367 assert(s_iter->B_to_C->pred->source == &*state_iter);
368 }
369 }
370/* ************************************************************************* */ while (state_iter->succ_end() != succ_constln_iter);
371/* */ if (state_iter->current_constln() == state_iter->succ_end())
372/* T R A N S I T I O N S */ {
373/* */ mCRL2log(log::debug)
374/* ************************************************************************* */ << "\t\t<- current_constln\n";
375 }
376 }
377 }
378 }
379 #endif // ifndef NDEBUG
392void part_trans_t::split_inert_to_C(block_t* const SpB)
393{
394 // if there are no inert transitions
395 if (SpB->inert_begin() == SpB->inert_end())
396 {
397 if (SpB->inert_end() != B_to_C.begin())
398 {
399 // There are noninert transitions from SpB to its old
400 // constellation: they all go to SpC.
401 SpB->SetFromRed(SpB->inert_end()[-1].B_to_C_slice);
402 // There are no more transitions from SpB to its own constellation
403 SpB->set_inert_begin(B_to_C.begin());
404 SpB->set_inert_end(B_to_C.begin());
405 }
406 return;
407 }
408 B_to_C_desc_iter_t const slice = SpB->inert_begin()->B_to_C_slice;
409 // if all transitions are inert
410 if (slice->begin == SpB->inert_begin())
411 {
412 return;
413 }
414
415 // now the slice actually has to be split
416 B_to_C_desc_iter_t new_slice;
417 // select the smaller number of swaps to decide which part should be the
418 // new one:
419 if(SpB->inert_begin() - slice->begin < slice->end - SpB->inert_begin())
420 {
421 // fewer noninert transitions
422 SpB->to_constln.emplace_front(slice->begin, SpB->inert_begin());
423 new_slice = SpB->to_constln.begin();
424 /* SpB->SetFromRed(new_slice); */ assert(new_slice->from_block() == SpB);
425 slice->begin = SpB->inert_begin();
426 #ifndef NDEBUG
427 new_slice->work_counter = slice->work_counter;
428 // We actually change the pointers in the new slice (i. e. the pointers of
429 // the non-inert transitions) because there are fewer of them; however, we
430 // still have to assign this work to the inert transitions.
431 mCRL2complexity(slice, add_work(check_complexity::
432 Register_that_inert_transitions_from_s_go_to_NewC_B_to_C_2_17,
433 check_complexity::log_n-check_complexity::ilog2(SpB->size())), );
434 #endif
435 }
436 else
437 {
438 // fewer (or equal) inert transitions
439 SpB->to_constln.emplace_back(SpB->inert_begin(), slice->end);
440 new_slice = std::prev(SpB->to_constln.end());
441 slice->end = SpB->inert_begin();
442 SpB->SetFromRed(slice);
443 #ifndef NDEBUG
444 new_slice->work_counter = slice->work_counter;
445 mCRL2complexity(new_slice, add_work(check_complexity::
446 Register_that_inert_transitions_from_s_go_to_NewC_B_to_C_2_17,
447 check_complexity::log_n-check_complexity::ilog2(SpB->size())), );
448 #endif
449 }
450 // set the slice pointers of the smaller part to the new slice:
451 for (B_to_C_iter_t iter = new_slice->begin; new_slice->end != iter; ++iter)
452 { // mCRL2complexity(...) -- optimized to the above calls.
453 assert(B_to_C.end() > iter); assert(iter->pred->succ->B_to_C == iter);
454 iter->B_to_C_slice = new_slice;
455 }
456}
457
458
474succ_iter_t part_trans_t::change_to_C(pred_iter_t const pred_iter, ONLY_IF_DEBUG( constln_t* const SpC, constln_t* const NewC, )
475 bool const first_transition_of_state, bool const first_transition_of_block)
476{ assert(pred_iter<pred.end()); assert(pred_iter->succ->B_to_C->pred==pred_iter);
477 // adapt the B_to_C array:
478 // always move the transition to the beginning of the slice (this will make
479 // it easier because inert transitions are stored at the end of a slice).
480 B_to_C_iter_t const old_B_to_C_pos = pred_iter->succ->B_to_C;
481 B_to_C_desc_iter_t const old_B_to_C_slice = old_B_to_C_pos->B_to_C_slice;
482 B_to_C_iter_t const new_B_to_C_pos = old_B_to_C_slice->begin; assert(new_B_to_C_pos < B_to_C.end());
483 B_to_C_desc_iter_t new_B_to_C_slice; assert(new_B_to_C_pos->pred->succ->B_to_C == new_B_to_C_pos);
484 if (first_transition_of_block)
485 {
486 // create a new slice in B_to_C for the transitions from RfnB to NewC
487 block_t* const RfnB = pred_iter->source->block;
488 RfnB->to_constln.emplace_back(new_B_to_C_pos, new_B_to_C_pos);
489 new_B_to_C_slice = std::prev(RfnB->to_constln.end());
490 #ifndef NDEBUG
491 new_B_to_C_slice->work_counter = old_B_to_C_slice->work_counter;
492 #endif
493 RfnB->SetFromRed(old_B_to_C_slice);
494 }
495 else
496 {
497 new_B_to_C_slice = new_B_to_C_pos[-1].B_to_C_slice;
498 }
499 ++new_B_to_C_slice->end;
500 ++old_B_to_C_slice->begin; assert(new_B_to_C_slice->end == old_B_to_C_slice->begin);
501 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
502 {
503 // this was the last transition from RfnB to SpC
504 block_t* const RfnB = pred_iter->source->block;
505 if (RfnB->inert_end() == old_B_to_C_slice->begin)
506 { assert(RfnB->inert_begin() == RfnB->inert_end());
507 // this was the last transition from RfnB to its own constellation
508 RfnB->set_inert_begin(B_to_C.begin());
509 RfnB->set_inert_end(B_to_C.begin());
510 } assert(RfnB->to_constln.begin() == old_B_to_C_slice);
511 RfnB->to_constln.erase(old_B_to_C_slice);
512 }
513 swap_B_to_C(pred_iter->succ, new_B_to_C_pos->pred->succ);
514 new_B_to_C_pos->B_to_C_slice = new_B_to_C_slice;
515 // adapt the outgoing transition array:
516 // move the transition to the beginning
517 succ_iter_t const old_out_pos = pred_iter->succ; assert(succ.end() > old_out_pos);
518 assert(old_out_pos->B_to_C->pred->succ == old_out_pos);
519 /* move to beginning */ assert(*NewC < *SpC);
520 succ_iter_t const new_out_pos = old_out_pos->slice_begin();
521 swap_out(pred_iter, new_out_pos->B_to_C->pred);
522 if (succ_iter_t const old_slice_end = succ_entry::slice_end(old_out_pos);
523 old_slice_end > new_out_pos + 1)
524 {
525 // the following assignment might assign an illegal transition if the
526 // old slice becomes empty -- but then it doesn't hurt, because it will
527 // be overwritten below. However, Visual Studio C complains.
528 old_slice_end[-1].set_slice_begin_or_before_end(new_out_pos + 1); assert(old_slice_end - 1 == new_out_pos->slice_begin_or_before_end());
529 } else
530 { assert(old_slice_end - 1 == new_out_pos);
531 assert(old_slice_end-1==old_slice_end[-1].slice_begin_or_before_end());
532 }
533 if (first_transition_of_state)
534 {
535 new_out_pos->set_slice_begin_or_before_end(new_out_pos);
536 }
537 else
538 { assert(pred_iter->source->current_constln() == new_out_pos);
539 new_out_pos->set_slice_begin_or_before_end(
540 new_out_pos[-1].slice_begin_or_before_end());
541 }
542 return new_out_pos + 1;
543}
544
545
555bool part_trans_t::split_s_inert_out(state_info_ptr s ONLY_IF_DEBUG( , constln_t* OldC )
556 )
557{
558 constln_t* NewC = s->constln(); assert(*NewC < *OldC); assert(NewC->sort_key + OldC->size() == OldC->sort_key);
559 assert(OldC->end() == NewC->begin() || NewC->end() == OldC->begin());
560 succ_iter_t split = s->inert_succ_begin(), to_C_end = s->inert_succ_end(); assert(s->succ_begin() == to_C_end ||
561 to_C_end[-1].slice_begin_or_before_end() < to_C_end);
562 succ_iter_t to_C_begin = s->succ_begin() == to_C_end ? to_C_end
563 : to_C_end[-1].slice_begin_or_before_end();
564 //< If s has no transitions to OldC at all, then to_C_begin may be the
565 // beginning of the constln_slice for transitions to another
566 // constellation. We will check that later.
567 bool result = to_C_begin < split; assert(to_C_begin <= split); assert(split <= to_C_end);
568 assert(succ.end() == split || split->B_to_C->pred->succ == split);
569 assert(succ.end() == to_C_end || to_C_end->B_to_C->pred->succ == to_C_end);
570 assert(succ.end() == to_C_begin ||
571 to_C_begin->B_to_C->pred->succ == to_C_begin);
572 if (!result) ;
573 else if (split < to_C_end)
574 {
575 // s has both inert and non-inert transitions
576 #ifndef NDEBUG
577 /* the out-transitions of s also have to be swapped. */ unsigned const max_counter = check_complexity::log_n -
578 /* Actually only B_to_C and the target need to be swapped, as the */ check_complexity::ilog2(NewC->size());
579 /* constln_slices are (still) identical. */ assert(*NewC < *OldC);
580 #endif
581 trans_type swapcount = std::min(to_C_end - split, split - to_C_begin);
582 split = to_C_end - split + to_C_begin; assert(0 != swapcount);
583
584 succ_iter_t pos1 = to_C_begin, pos2 = to_C_end;
585 state_info_ptr temp_target = pos1->target;
586 B_to_C_iter_t temp_B_to_C = pos1->B_to_C;
587 for (;;)
588 {
589 --pos2; mCRL2complexity(pos2->B_to_C->pred, add_work(check_complexity::
590 Register_that_inert_transitions_from_s_go_to_NewC_swap_2_17,
591 max_counter), );
592 pos1->target = pos2->target;
593 pos1->B_to_C = pos2->B_to_C;
594 pos1->B_to_C->pred->succ = pos1;
595 ++pos1;
596 if (0 == --swapcount) break;
597 pos2->target = pos1->target;
598 pos2->B_to_C = pos1->B_to_C;
599 pos2->B_to_C->pred->succ = pos2;
600 }
601 pos2->target = temp_target;
602 pos2->B_to_C = temp_B_to_C;
603 pos2->B_to_C->pred->succ = pos2;
604
605 s->set_inert_succ_begin_and_end(to_C_begin, split); assert(s->succ_begin() == s->inert_succ_begin() ||
606 *s->inert_succ_begin()[-1].target->constln() < *NewC);
607 assert(s->inert_succ_begin()->target->block == s->block);
608 assert(s->inert_succ_end()[-1].target->block == s->block);
609 assert(s->inert_succ_end() < s->succ_end());
610 /* set the pointer to the slice for the inert transitions. */ assert(OldC == s->inert_succ_end()->target->constln());
611 to_C_end[-1].set_slice_begin_or_before_end(split);
612 split[-1].set_slice_begin_or_before_end(to_C_begin);
613 for (succ_iter_t succ_iter = split - 1; to_C_begin != succ_iter; )
614 {
615 --succ_iter; mCRL2complexity(succ_iter->B_to_C->pred,add_work(check_complexity::
616 Register_that_inert_transitions_from_s_go_to_NewC_succ_2_17,
617 max_counter), );
618 assert(succ.end() > succ_iter);
619 assert(succ_iter->B_to_C->pred->succ == succ_iter);
620 succ_iter->set_slice_begin_or_before_end(split - 1);
621 }
622 }
623 else if (*to_C_begin->target->constln() > *NewC)
624 {
625 // s has (noninert) transitions to OldC, but no (inert)
626 /* transitions to NewC. */ assert(to_C_begin->target->constln() == OldC);
627 s->set_inert_succ_begin_and_end(to_C_begin, to_C_begin); assert(s->succ_begin() == s->inert_succ_begin() ||
628 *s->inert_succ_begin()[-1].target->constln() < *NewC);
629 assert(s->succ_end() > s->inert_succ_end()); assert(to_C_end == split);
630 assert(OldC == s->inert_succ_end()->target->constln());
631 }
632 else
633 {
634 // s actually hasn't got transitions to OldC at all, so `result`
635 // should not be true.
636 result = false;
637 }
638 #ifndef NDEBUG
639 if (succ_iter_t succ_iter = s->succ_begin(); succ_iter != s->succ_end())
640 {
641 do
642 {
643 assert(succ_iter->B_to_C->pred->source == s);
644 }
645 while (++succ_iter != s->succ_end());
646 assert(s->succ_begin() == s->inert_succ_begin() ||
647 *s->inert_succ_begin()[-1].target->constln() < *NewC);
648 assert(s->inert_succ_begin() == s->inert_succ_end() ||
649 (s->inert_succ_begin()->target->block == s->block &&
650 s->inert_succ_end()[-1].target->block == s->block));
651 assert(s->inert_succ_end() == s->succ_end() ||
652 *NewC < *s->inert_succ_end()->target->constln());
653 }
654 #endif // ifndef NDEBUG
655 return result;
656}
657
658
666void part_trans_t::new_blue_block_created(block_t* const RfnB,
667 block_t* const NewB)
668{ assert(RfnB->constln()==NewB->constln()); assert(NewB->end()==RfnB->begin());
669 NewB->set_inert_begin_and_end(B_to_C.begin(), B_to_C.begin());
670 #ifndef NDEBUG
671 unsigned const max_counter = check_complexity::log_n -
672 check_complexity::ilog2(NewB->size());
673 mCRL2complexity(NewB, add_work(check_complexity::
674 /* for all outgoing transitions of NewB */ Move_Blue_or_Red_to_a_new_block_states_3_29, max_counter), );
675 #endif
676 for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
677 { // mCRL2complexity(*s_iter, ...) -- optimized to the above call
678 for (succ_iter_t succ_iter = (*s_iter)->succ_begin();
679 (*s_iter)->succ_end() != succ_iter; ++succ_iter)
680 { mCRL2complexity(succ_iter->B_to_C->pred,add_work(check_complexity::
681 Move_Blue_or_Red_to_a_new_block_succ_3_29, max_counter), );
682 /* Move the transition to a new slice: */ assert(succ.end()>succ_iter); assert(succ_iter->B_to_C->pred->succ==succ_iter);
683 B_to_C_iter_t const old_pos = succ_iter->B_to_C;
684 B_to_C_desc_iter_t const old_B_to_C_slice = old_pos->B_to_C_slice;
685 B_to_C_iter_t const after_new_pos = old_B_to_C_slice->end; assert(B_to_C.end() > old_pos);
686 assert(old_pos->pred->succ->B_to_C == old_pos);
687 assert(B_to_C.end() == after_new_pos ||
688 after_new_pos->pred->succ->B_to_C == after_new_pos);
689 B_to_C_desc_iter_t new_B_to_C_slice;
690 if (B_to_C.end() == after_new_pos ||
691 after_new_pos->pred->source->block != NewB ||
692 after_new_pos->pred->succ->target->constln() !=
693 succ_iter->target->constln())
694 {
695 // create a new B_to_C-slice
696 // this can only happen when the first transition from
697 // *s_iter to a new constellation is handled.
698 if (!old_B_to_C_slice->needs_postprocessing())
699 {
700 // (During primary refinement [Line 2.23]: There is no need
701 // to put the FromRed-slice of the new blue block into
702 // position like in new_red_block_created(), as only the
703 // red subblock will be refined further in Line 2.24.)
704 // During postprocessing:
705 // the old_B_to_C_slice does not need postprocessing, so
706 // its corresponding new slice should be in a similar
707 // position near the beginning of the list of slices.
708 NewB->to_constln.emplace_front(after_new_pos,
709 after_new_pos); // new_B_to_C_slice is not yet fully initialised, therefore
710 new_B_to_C_slice = NewB->to_constln.begin(); // the assertion fails:
711 // assert(new_B_to_C_slice->from_block() == NewB);
712 }
713 else
714 {
715 // During postprocessing:
716 // the old_B_to_C_slice needs postprocessing, so also the
717 // new_B_to_C_slice will need postprocessing.
718 NewB->to_constln.emplace_back(after_new_pos,after_new_pos);
719 new_B_to_C_slice = std::prev(NewB->to_constln.end());
720 }
721 #ifndef NDEBUG
722 new_B_to_C_slice->work_counter = old_B_to_C_slice->work_counter;
723 #endif
724 if (RfnB->inert_end() == after_new_pos)
725 {
726 /* this is the first transition from NewB to its own */ assert(NewB->inert_begin() == B_to_C.begin());
727 /* constellation. Adapt the pointers accordingly. */ assert(NewB->inert_end() == B_to_C.begin());
728 NewB->set_inert_end(after_new_pos);
729 NewB->set_inert_begin(after_new_pos);
730 }
731 }
732 else
733 {
734 // the slice at after_new_pos is already the correct one
735 new_B_to_C_slice = after_new_pos->B_to_C_slice;
736 }
737 --new_B_to_C_slice->begin;
738 --old_B_to_C_slice->end; assert(new_B_to_C_slice->begin == old_B_to_C_slice->end);
739 B_to_C_iter_t new_pos = after_new_pos - 1; assert(B_to_C.end() > new_pos);
740 assert(new_pos->pred->succ->B_to_C == new_pos);
741 if (RfnB->inert_end() == after_new_pos)
742 {
743 // The transition goes from NewB to the constellation of
744 // RfnB and NewB.
745 if (RfnB->inert_begin() <= old_pos)
746 {
747 // The transition is inert and has to be moved over the
748 // non-inert transitions of NewB.
749 NewB->set_inert_begin(NewB->inert_begin() - 1);
750 new_pos = NewB->inert_begin();
751 // old_pos --> new_pos --> new_B_to_C_slice->begin -->
752 // old_pos
753 swap3_B_to_C(succ_iter, new_pos->pred->succ,
754 new_B_to_C_slice->begin->pred->succ);
755 }
756 else
757 {
758 // The transition is non-inert, but it has to be moved
759 // over the inert transitions of RfnB.
760 RfnB->set_inert_begin(RfnB->inert_begin() - 1);
761 // old_pos --> new_pos --> RfnB->inert_begin() -> old_pos
762 swap3_B_to_C(succ_iter, new_pos->pred->succ,
763 RfnB->inert_begin()->pred->succ);
764 }
765 RfnB->set_inert_end(RfnB->inert_end() - 1);
766 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
767 {
768 // This was the last transition from RfnB to its own
769 // constellation.
770 RfnB->set_inert_begin(B_to_C.begin());
771 RfnB->set_inert_end(B_to_C.begin());
772
773 RfnB->to_constln.erase(old_B_to_C_slice);
774 }
775 }
776 else
777 {
778 // The transition goes from NewB to a constellation that
779 // does not contain RfnB or NewB. No special treatment is
780 // required.
781 swap_B_to_C(succ_iter, new_pos->pred->succ);
782 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
783 {
784 RfnB->to_constln.erase(old_B_to_C_slice);
785 }
786 }
787 new_pos->B_to_C_slice = new_B_to_C_slice;
788 }
789 }
790 #ifndef NDEBUG
791 if (RfnB->inert_begin() == RfnB->inert_end() &&
792 RfnB->inert_end() != B_to_C.begin() &&
793 (RfnB->inert_end()[-1].pred->source->block != RfnB ||
794 RfnB->inert_end()[-1].pred->succ->target->constln()
795 != RfnB->constln()))
796 {
797 assert(0 && "The old block has no transitions to its own "
798 "constellation, but its inert_begin and "
799 "inert_end pointers are not set to B_to_C.begin()");
800 }
801 if (RfnB->inert_end() != B_to_C.begin())
802 {
803 assert(RfnB->inert_end()[-1].pred->source->block == RfnB);
804 assert(RfnB->inert_end()[-1].pred->succ->target->constln() ==
805 RfnB->constln());
806 }
807 if (NewB->inert_begin() == NewB->inert_end() &&
808 NewB->inert_end() != B_to_C.begin() &&
809 (NewB->inert_end()[-1].pred->source->block != NewB ||
810 NewB->inert_end()[-1].pred->succ->target->constln()
811 != NewB->constln()))
812 {
813 assert(0 && "The new block has no transitions to its own "
814 "constellation, but its inert_begin and "
815 "inert_end pointers are not set to B_to_C.begin()");
816 }
817 if (NewB->inert_end() != B_to_C.begin())
818 {
819 assert(NewB->inert_end()[-1].pred->source->block == NewB);
820 assert(NewB->inert_end()[-1].pred->succ->target->constln() ==
821 NewB->constln());
822 }
823 #endif
824}
825
826
837void part_trans_t::new_red_block_created(block_t* const RfnB,
838 block_t* const NewB, bool const postprocessing)
839{ assert(RfnB->constln()==NewB->constln()); assert(NewB->begin()==RfnB->end());
840 NewB->set_inert_begin_and_end(B_to_C.begin(), B_to_C.begin());
841 bool old_fromred_invalid = false;
842 #ifndef NDEBUG
843 unsigned const max_counter = check_complexity::log_n -
844 check_complexity::ilog2(NewB->size());
845 mCRL2complexity(NewB, add_work(check_complexity::
846 /* for all outgoing transitions of NewB */ Move_Blue_or_Red_to_a_new_block_states_3_29, max_counter), );
847 #endif
848 for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
849 { // mCRL2complexity(*s_iter, ...) -- optimized to the above call
850 for (succ_iter_t succ_iter = (*s_iter)->succ_begin();
851 (*s_iter)->succ_end() != succ_iter; ++succ_iter)
852 { mCRL2complexity(succ_iter->B_to_C->pred,add_work(check_complexity::
853 Move_Blue_or_Red_to_a_new_block_succ_3_29, max_counter), );
854 /* Move the transition to a new slice: */ assert(succ.end()>succ_iter); assert(succ_iter->B_to_C->pred->succ==succ_iter);
855 B_to_C_iter_t const old_pos = succ_iter->B_to_C;
856 B_to_C_desc_iter_t const old_B_to_C_slice = old_pos->B_to_C_slice;
857 B_to_C_iter_t new_pos = old_B_to_C_slice->begin; assert(B_to_C.end() > old_pos); assert(old_pos->pred->succ->B_to_C == old_pos);
858 assert(B_to_C.end() > new_pos); assert(new_pos->pred->succ->B_to_C == new_pos);
859 B_to_C_desc_iter_t new_B_to_C_slice;
860 if (B_to_C.begin() == new_pos ||
861 new_pos[-1].pred->source->block != NewB ||
862 new_pos[-1].pred->succ->target->constln() !=
863 succ_iter->target->constln())
864 {
865 // create a new B_to_C-slice
866 // this can only happen when the first transition from
867 // *s_iter to a new constellation is handled.
868 if (!postprocessing ? !old_fromred_invalid &&
869 RfnB->to_constln.begin() == old_B_to_C_slice
870 : !old_B_to_C_slice->needs_postprocessing())
871 {
872 // During primary refinement (Line 2.23):
873 // The old B_to_C_slice is in the FromRed-position, i. e.
874 // it contains the transitions to SpC. So the new slice
875 // also contains the transitions to SpC.
876 // During postprocessing:
877 // The old_B_to_C_slice does not need postprocessing, so
878 // its corresponding new slice should be in a similar
879 // position near the beginning of the list of slices.
880 NewB->to_constln.emplace_front(new_pos, new_pos); // new_B_to_C_slice is not yet fully initialised, therefore
881 new_B_to_C_slice = NewB->to_constln.begin(); // the assertion fails:
882 // assert(new_B_to_C_slice->from_block() == NewB);
883 }
884 else
885 {
886 // During primary refinement (Line 2.23):
887 // The old_B_to_C_slice is not in the FromRed-position. The
888 // corresponding slice of NewB should be moved into a
889 // position that does not change a potential FromRed-slice
890 // there.
891 // During postprocessing:
892 // The old_B_to_C_slice needs postprocessing, so also the
893 // new_B_to_C_slice will need postprocessing.
894 NewB->to_constln.emplace_back(new_pos, new_pos);
895 new_B_to_C_slice = std::prev(NewB->to_constln.end());
896 }
897 #ifndef NDEBUG
898 new_B_to_C_slice->work_counter = old_B_to_C_slice->work_counter;
899 #endif
900 if (RfnB->inert_end() == old_B_to_C_slice->end)
901 {
902 /* this is the first transition from NewB to its own */ assert(NewB->inert_begin() == B_to_C.begin());
903 /* constellation. Adapt the pointers accordingly. */ assert(NewB->inert_end() == B_to_C.begin());
904 NewB->set_inert_end(new_pos);
905 NewB->set_inert_begin(new_pos);
906 }
907 }
908 else
909 {
910 // the slice before new_pos is already the correct one
911 new_B_to_C_slice = new_pos[-1].B_to_C_slice;
912 }
913 ++new_B_to_C_slice->end;
914 ++old_B_to_C_slice->begin; assert(new_B_to_C_slice->end == old_B_to_C_slice->begin);
915 if (RfnB->inert_end() == old_B_to_C_slice->end)
916 {
917 // The transition goes from NewB to the constellation of
918 // RfnB and NewB.
919 NewB->set_inert_end(NewB->inert_end() + 1);
920 if (RfnB->inert_begin() <= old_pos)
921 {
922 // The transition is inert and has to be moved over the
923 // non-inert transitions of RfnB.
924 // old_pos --> new_pos --> RfnB->inert_begin() --> old_pos
925 swap3_B_to_C(succ_iter, new_pos->pred->succ,
926 RfnB->inert_begin()->pred->succ);
927 RfnB->set_inert_begin(RfnB->inert_begin() + 1);
928 }
929 else
930 {
931 // The transition is non-inert, but it has to be moved
932 // over the inert transitions of NewB.
933 new_pos = NewB->inert_begin();
934 NewB->set_inert_begin(NewB->inert_begin() + 1);
935 // old_pos --> new_pos --> NewB->inert_end() - 1 -> old_pos
936 swap3_B_to_C(succ_iter, new_pos->pred->succ,
937 NewB->inert_end()[-1].pred->succ);
938 }
939 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
940 {
941 // This was the last transition from RfnB to its own
942 // constellation.
943 RfnB->set_inert_begin(B_to_C.begin());
944 RfnB->set_inert_end(B_to_C.begin());
945
946 if (!old_fromred_invalid &&
947 RfnB->to_constln.begin() == old_B_to_C_slice)
948 {
949 old_fromred_invalid = true;
950 }
951 RfnB->to_constln.erase(old_B_to_C_slice);
952 }
953 }
954 else
955 {
956 // The transition goes from NewB to a constellation that
957 // does not contain RfnB or NewB. No special treatment is
958 // required.
959 swap_B_to_C(succ_iter, new_pos->pred->succ);
960 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
961 {
962 if (!old_fromred_invalid &&
963 RfnB->to_constln.begin() == old_B_to_C_slice)
964 {
965 old_fromred_invalid = true;
966 }
967 RfnB->to_constln.erase(old_B_to_C_slice);
968 }
969 }
970 new_pos->B_to_C_slice = new_B_to_C_slice;
971 }
972 }
973 #ifndef NDEBUG
974 if (RfnB->inert_begin() == RfnB->inert_end() &&
975 RfnB->inert_end() != B_to_C.begin() &&
976 (RfnB->inert_end()[-1].pred->source->block != RfnB ||
977 RfnB->inert_end()[-1].pred->succ->target->constln()
978 != RfnB->constln()))
979 {
980 assert(0 && "The old block has no transitions to its own "
981 "constellation, but its inert_begin and "
982 "inert_end pointers are not set to B_to_C.begin()");
983 }
984 if (RfnB->inert_end() != B_to_C.begin())
985 {
986 assert(RfnB->inert_end()[-1].pred->source->block == RfnB);
987 assert(RfnB->inert_end()[-1].pred->succ->target->constln() ==
988 RfnB->constln());
989 }
990 if (NewB->inert_begin() == NewB->inert_end() &&
991 NewB->inert_end() != B_to_C.begin() &&
992 (NewB->inert_end()[-1].pred->source->block != NewB ||
993 NewB->inert_end()[-1].pred->succ->target->constln()
994 != NewB->constln()))
995 {
996 assert(0 && "The new block has no transitions to its own "
997 "constellation, but its inert_begin and "
998 "inert_end pointers are not set to B_to_C.begin()");
999 }
1000 if (NewB->inert_end() != B_to_C.begin())
1001 {
1002 assert(NewB->inert_end()[-1].pred->source->block == NewB);
1003 assert(NewB->inert_end()[-1].pred->succ->target->constln() ==
1004 NewB->constln());
1005 }
1006 #endif
1007}
1008 #ifndef NDEBUG
1019 void part_trans_t::assert_stability(const part_state_t& part_st) const
1020 {
1021 #ifdef PARANOID_CHECK
1022 std::vector<state_info_const_ptr> part_st_predecessors;
1023 #endif
1024 // count the nontrivial constellations (to check later whether every
1025 // nontrivial constellation is reachable from the first nontrivial
1026 // constellation)
1027 state_type nr_of_nontrivial_constellations = 0;
1028 const constln_t* C = constln_t::get_some_nontrivial();
1029 if (nullptr != C)
1030 {
1031 for (;;)
1032 {
1033 ++nr_of_nontrivial_constellations;
1034 if (C->get_nontrivial_next() == C) break;
1035 C = C->get_nontrivial_next();
1036 assert(nullptr != C);
1037 }
1038 }
1039
1040 // for all constellations C do
1041 C = part_st.permutation.front()->constln();
1042 assert(C->begin() == part_st.permutation.begin());
1043 for (;;)
1044 {
1045 // assert some properties of constellation C
1046 assert(C->begin() < C->end());
1047 assert(C->postprocess_begin == C->postprocess_end);
1048 unsigned const max_C = check_complexity::log_n -
1049 check_complexity::ilog2(C->size());
1050 const block_t* B = (*C->begin())->block;
1051 assert(C->begin() == B->begin());
1052 if (C->is_trivial())
1053 {
1054 // a trivial constellation contains exactly one block
1055 assert(B->end() == C->end());
1056 }
1057 else
1058 {
1059 // a nontrivial constellation contains at least two blocks
1060 assert(B->end() < C->end());
1061 --nr_of_nontrivial_constellations;
1062 }
1063 // for all blocks B in C do
1064 for (;;)
1065 {
1066 // assert some properties of block B
1067 assert(B->constln() == C);
1068 assert(B->nonbottom_begin() <= B->nonbottom_end());
1069 assert(B->marked_nonbottom_begin()==B->marked_nonbottom_end());
1070 assert(B->bottom_begin() < B->bottom_end());
1071 assert(B->marked_bottom_begin() == B->marked_bottom_end());
1072 assert(!B->is_refinable());
1073 assert(B->inert_begin() <= B->inert_end());
1074 unsigned const max_B = check_complexity::log_n -
1075 check_complexity::ilog2(B->size());
1076 mCRL2complexity(B, no_temporary_work(max_C, max_B), );
1077 // count inert transitions in block
1078 state_type nr_of_inert_successors =
1079 B->inert_end()-B->inert_begin();
1080 permutation_const_iter_t s_iter;
1081 #ifdef PARANOID_CHECK
1082 state_type nr_of_inert_predecessors=nr_of_inert_successors;
1083 // make sure that every non-bottom state can reach some
1084 // bottom state in the block. This is done using
1085 // a simple graph algorithm for reachability. The
1086 // algorithm should mark every source of an inert
1087 // transition exactly once. For this, we misuse the field
1088 // state_info_entry::notblue: It is == STATE_TYPE_MAX if
1089 // and only if the state has been marked.
1090
1091 // Because we run through the bottom states and their
1092 // predecessor transitions anyway, we also verify a few
1093 // other properties, in particular everything we want to
1094 // verify about inert predecessor transitions.
1095
1096 // for all bottom states s in B do
1097 assert(part_st_predecessors.empty());
1098 part_st_predecessors.reserve(B->nonbottom_end() -
1099 B->nonbottom_begin());
1100 s_iter = B->bottom_begin();
1101 do
1102 {
1103 state_info_const_ptr const s = *s_iter;
1104 nr_of_inert_predecessors -=
1105 s->inert_pred_end() - s->inert_pred_begin();
1106 // for all inert predecessors pred of s do
1107 for (pred_const_iter_t pred_iter=s->inert_pred_begin();
1108 pred_iter < s->inert_pred_end(); ++pred_iter)
1109 {
1110 // assert some properties of the predecessor
1111 // transition
1112 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1113 from_block() == B);
1114 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1115 to_constln() == C);
1116 assert(pred_iter->succ->target == s);
1117
1118 state_info_const_ptr const pred=pred_iter->source;
1119 // if pred is not yet marked as predecessor then
1120 if (STATE_TYPE_MAX != pred->notblue)
1121 {
1122 // assert some properties of the predecessor
1123 // state
1124 assert(pred->block == B);
1125 assert(pred->pos < B->nonbottom_end());
1126 // mark pred as predecessor
1127 const_cast<state_type&>(pred->notblue) =
1128 STATE_TYPE_MAX;
1129 // add pred to the list of predecessors
1130 part_st_predecessors.push_back(pred);
1131 // end if
1132 }
1133 // end for
1134 }
1135 // end for
1136 }
1137 while(++s_iter < B->bottom_end());
1138
1139 // Now that we have collected the predecessors of the
1140 // bottom states, we have to extend this set to their
1141 // indirect predecessors.
1142
1143 // for all states s in the list of predecessors do
1144 for (std::vector<state_info_const_ptr>::iterator s_iter =
1145 part_st_predecessors.begin();
1146 s_iter < part_st_predecessors.end(); ++s_iter)
1147 {
1148 state_info_const_ptr const s = *s_iter;
1149 nr_of_inert_predecessors -=
1150 s->inert_pred_end() - s->inert_pred_begin();
1151 // for all inert predecessors pred of s do
1152 for (pred_const_iter_t pred_iter=s->inert_pred_begin();
1153 pred_iter < s->inert_pred_end(); ++pred_iter)
1154 {
1155 // assert some properties of the predecessor
1156 // transition
1157 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1158 from_block() == B);
1159 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1160 to_constln() == C);
1161 assert(pred_iter->succ->target == s);
1162
1163 state_info_const_ptr const pred=pred_iter->source;
1164 // if pred is not yet marked as predecessor then
1165 if (STATE_TYPE_MAX != pred->notblue)
1166 {
1167 // assert some properties of the predecessor
1168 // state
1169 assert(pred->block == B);
1170 assert(pred->pos < B->nonbottom_end());
1171 // mark pred as predecessor
1172 const_cast<state_type&>(pred->notblue) =
1173 STATE_TYPE_MAX;
1174 // add pred to the list of predecessors
1175 part_st_predecessors.push_back(pred);
1176 // end if
1177 }
1178 // end for
1179 }
1180 // end for
1181 }
1182 assert(part_st_predecessors.size() == (std::size_t)
1183 (B->nonbottom_end() - B->nonbottom_begin()));
1184 part_st_predecessors.clear();
1185 assert(0 == nr_of_inert_predecessors);
1186 // now all nonbottom states should have
1187 // s->notblue == STATE_TYPE_MAX.
1188 #endif
1189 // verify to_constln list:
1190 bool to_own_constln = false;
1191 for (B_to_C_desc_const_iter_t iter = B->to_constln.begin();
1192 B->to_constln.end() != iter; ++iter)
1193 {
1194 assert(iter->from_block() == B);
1195 mCRL2complexity(iter, no_temporary_work(
1196 check_complexity::log_n -
1197 check_complexity::ilog2(iter->to_constln()->size())), );
1198 if (iter->to_constln() == C)
1199 {
1200 assert(!to_own_constln);
1201 to_own_constln = true;
1202 assert(iter->begin <= B->inert_begin());
1203 assert(iter->end == B->inert_end());
1204 }
1205 }
1206 if (!to_own_constln)
1207 {
1208 assert(B->nonbottom_begin() == B->nonbottom_end());
1209 assert(B->inert_begin() == B_to_C_begin());
1210 assert(B->inert_end() == B_to_C_begin());
1211 }
1212
1213 // for all states s in B do
1214 s_iter = B->begin();
1215 do
1216 {
1217 state_info_const_ptr const s = *s_iter;
1218 // assert some properties of state s
1219 assert(s->pos == s_iter);
1220 assert(s->block == B);
1221 assert(s->pred_begin() <= s->inert_pred_begin());
1222 assert(s->inert_pred_begin() <= s->inert_pred_end());
1223 assert(s->inert_pred_end() == s->pred_end());
1224 assert(s->succ_begin() <= s->inert_succ_begin());
1225 assert(s->inert_succ_begin() <= s->inert_succ_end());
1226 assert(s->inert_succ_end() <= s->succ_end());
1227 assert(s->succ_begin() == s->current_constln() ||
1228 s->succ_end() == s->current_constln() ||
1229 *s->current_constln()[-1].target->constln() <
1230 *s->current_constln()->target->constln());
1231 mCRL2complexity(s, no_temporary_work(max_B,
1232 s_iter >= B->bottom_begin()), );
1233 // count reachable constellations
1234 state_type nr_of_reachable_constlns = B->to_constln.size();
1235
1236 // for all constln-slices of successors of s do
1237 if (succ_const_iter_t succ_iter = s->succ_begin();
1238 succ_iter < s->succ_end())
1239 {
1240 for (;;)
1241 {
1242 succ_const_iter_t before_end =
1243 succ_iter->slice_begin_or_before_end();
1244 succ_const_iter_t slice_end = before_end + 1;
1245 assert(succ_iter < slice_end);
1246 assert(before_end->slice_begin_or_before_end() ==
1247 succ_iter);
1248 const constln_t* const targetC =
1249 succ_iter->target->constln();
1250 // for all noninert transitions in the
1251 // constln-slice do
1252 if (targetC == C)
1253 {
1254 assert(s->inert_succ_end() == slice_end);
1255 slice_end = s->inert_succ_begin();
1256 }
1257 for (; succ_iter < slice_end; ++succ_iter)
1258 {
1259 // assert some properties of the successor
1260 // transition
1261 assert(succ_iter->target->block != B);
1262 assert(succ_iter->target->constln()==targetC);
1263 if (succ_iter != before_end)
1264 {
1265 assert(succ_iter->
1266 slice_begin_or_before_end()==before_end);
1267 }
1268 assert(succ_iter->B_to_C < B->inert_begin() ||
1269 B->inert_end() <= succ_iter->B_to_C);
1270 assert(succ_iter->B_to_C->B_to_C_slice->
1271 from_block() == B);
1272 assert(succ_iter->B_to_C->B_to_C_slice->
1273 to_constln() == targetC);
1274 assert(succ_iter->B_to_C->pred->succ ==
1275 succ_iter);
1276 assert(succ_iter->B_to_C->pred->source == s);
1277 mCRL2complexity(succ_iter->B_to_C->pred,
1278 no_temporary_work(max_B, check_complexity::
1279 log_n - check_complexity::ilog2(
1280 succ_iter->target->constln()->size()),
1281 check_complexity::log_n - check_complexity::
1282 ilog2(succ_iter->target->block->size()),
1283 s_iter >= B->bottom_begin()), );
1284 // end for
1285 }
1286 // if we have reached the inert transitions then
1287 if (targetC == C)
1288 {
1289 // for all inert transitions in the
1290 // constln-slice do
1291 for (slice_end = s->inert_succ_end();
1292 succ_iter < slice_end; ++succ_iter)
1293 {
1294 // assert some properties of inert
1295 // transitions
1296 assert(succ_iter->target->block == B);
1297 if (succ_iter != before_end)
1298 {
1299 assert(before_end == succ_iter->
1300 slice_begin_or_before_end());
1301 }
1302 assert(B->inert_begin() <=
1303 succ_iter->B_to_C);
1304 assert(succ_iter->B_to_C < B->inert_end());
1305 assert(succ_iter->B_to_C->B_to_C_slice->
1306 from_block() == B);
1307 assert(succ_iter->B_to_C->B_to_C_slice->
1308 to_constln() == targetC);
1309 assert(succ_iter->B_to_C->pred->succ ==
1310 succ_iter);
1311 assert(succ_iter->B_to_C->pred->source==s);
1312 mCRL2complexity(succ_iter->B_to_C->pred,
1313 no_temporary_work(max_B,
1314 max_C, max_B, false), );
1315 // end for
1316 }
1317 // end if
1318 }
1319 else
1320 {
1321 --nr_of_reachable_constlns;
1322 }
1323 // end for
1324 if (s->succ_end() <= succ_iter) break;
1325 assert(0 != nr_of_reachable_constlns);
1326 assert(*targetC < *succ_iter->target->constln());
1327 }
1328 }
1329 // if s is a nonbottom state then
1330 if (s_iter < B->bottom_begin())
1331 {
1332 assert(s->inert_succ_begin() < s->inert_succ_end());
1333 nr_of_inert_successors -=
1334 s->inert_succ_end() - s->inert_succ_begin();
1335 // the following assertion is necessary because s must
1336 // have a transition to its own constellation (namely
1337 // an inert one), but this constln_slice is not
1338 // counted.
1339 assert(0 != nr_of_reachable_constlns);
1340
1341 #ifdef PARANOID_CHECK
1342 // assert that s can reach a bottom state
1343 assert(STATE_TYPE_MAX == s->notblue);
1344 const_cast<state_type&>(s->notblue) = 1;
1345 #endif
1346 }
1347 else
1348 {
1349 // (s is a bottom state.)
1350 // assert that not too few constellations are
1351 // reachable.
1352 assert((state_type) to_own_constln ==
1353 nr_of_reachable_constlns);
1354 assert(s->inert_succ_begin() == s->inert_succ_end());
1355 // the following assertions are necessary because it
1356 // could be that the state has no transition to its own
1357 // constellation.
1358 assert(s->succ_begin() == s->inert_succ_begin() ||
1359 *s->inert_succ_begin()[-1].target->constln() <= *C);
1360 assert(s->inert_succ_end() == s->succ_end() ||
1361 *s->inert_succ_end()->target->constln() > *C);
1362 }
1363
1364 // for all noninert predecessors of s do
1365 for (pred_const_iter_t pred_iter=s->noninert_pred_begin();
1366 pred_iter < s->noninert_pred_end(); ++pred_iter)
1367 {
1368 // assert some properties of the predecessor
1369 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1370 from_block() != B);
1371 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1372 to_constln() == C);
1373 assert(pred_iter->succ->target == s);
1374 assert(pred_iter->source->block != B);
1375 // end for
1376 }
1377 #ifndef PARANOID_CHECK
1378 // for all inert predecessors of s do
1379 for (pred_const_iter_t pred_iter=s->inert_pred_begin();
1380 pred_iter < s->inert_pred_end(); ++pred_iter)
1381 {
1382 // assert some properties of the predecessor
1383 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1384 from_block() == B);
1385 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1386 to_constln() == C);
1387 assert(pred_iter->succ->target == s);
1388 assert(pred_iter->source->block == B);
1389 assert(pred_iter->source->pos<B->nonbottom_end());
1390 // end for
1391 }
1392 #endif
1393 // end for (all states s in B)
1394 }
1395 while (++s_iter < B->end());
1396 assert(0 == nr_of_inert_successors);
1397 // end for (all blocks B in C)
1398/* ************************************************************************* */ if (B->end() == C->end()) break;
1399/* */ assert(B->end() < C->end());
1400/* A L G O R I T H M S */ assert(B->end() == (*B->end())->block->begin());
1401/* */ B = (*B->end())->block;
1402/* ************************************************************************* */ }
1403 // end for (all constellations C)
1404 if (C->end() == part_st.permutation.end()) break;
1405 assert(C->end() < part_st.permutation.end());
1406 assert(C->end() == (*C->end())->constln()->begin());
1407 C = (*C->end())->constln();
1408/*===========================================================================*/ }
1409/* initialisation helper */ assert(0 == nr_of_nontrivial_constellations);
1410/*===========================================================================*/ return;
1411 }
1412 #endif
1414template<class LTS_TYPE>
1415bisim_partitioner_gjkw_initialise_helper<LTS_TYPE>::
1416bisim_partitioner_gjkw_initialise_helper(LTS_TYPE& l, bool const branching,
1417 bool const preserve_divergence)
1418 : aut(l),
1419 nr_of_states(l.num_states()),
1420 orig_nr_of_states(l.num_states()),
1421 nr_of_transitions(l.num_transitions()),
1422 noninert_out_per_state(l.num_states(), 0),
1423 inert_out_per_state(l.num_states(), 0),
1424 noninert_in_per_state(l.num_states(), 0),
1425 inert_in_per_state(l.num_states(), 0),
1426 noninert_out_per_block(1, 0),
1427 inert_out_per_block(1, 0),
1428 states_per_block(1, l.num_states()),
1429 nr_of_nonbottom_states(0)
1430{
1431 // log::logger::set_reporting_level(log::debug);
1432
1433 mCRL2log(log::verbose) << "O(m log n) "
1434 << (preserve_divergence ? "Divergence preserving b" : "B")
1435 << (branching ? "ranching b" : "")
1436 << "isimulation partitioner created for " << l.num_states()
1437 << " states and " << l.num_transitions()
1438 << " transitions [GJKW 2017]\n";
1439 // Iterate over the transitions and collect new states
1440 for (const transition& t: aut.get_transitions())
1441 {
1442 if (!branching || !aut.is_tau(aut.apply_hidden_label_map(t.label())) ||
1443 (preserve_divergence && t.from() == t.to()))
1444 {
1445 // (possibly) create new state
1446 Key const k(aut.apply_hidden_label_map(t.label()), t.to());
1447 std::pair<typename std::unordered_map<Key, state_type,
1448 KeyHasher>::iterator,bool> extra_state = extra_kripke_states.
1449 insert(std::make_pair(k, nr_of_states));
1450 if (extra_state.second)
1451 {
1452 noninert_in_per_state.push_back(0);
1453 inert_in_per_state.push_back(0);
1454 noninert_out_per_state.push_back(0);
1455 inert_out_per_state.push_back(0);
1456
1457 // (possibly) create new block
1458 std::pair<std::unordered_map<label_type, state_type>::iterator,
1459 bool> const action_block = action_block_map.insert(
1460 std::make_pair(aut.apply_hidden_label_map(t.label()),
1461 states_per_block.size()));
1462 if (action_block.second)
1463 {
1464 noninert_out_per_block.push_back(0);
1465 inert_out_per_block.push_back(0);
1466 states_per_block.push_back(0);
1467 }
1468
1469 ++noninert_in_per_state[t.to()];
1470 ++noninert_out_per_state[nr_of_states];
1471 ++noninert_out_per_block[action_block.first->second];
1472 ++states_per_block[action_block.first->second];
1473 ++nr_of_states;
1474 ++nr_of_transitions;
1475 }
1476 ++noninert_in_per_state[extra_state.first->second];
1477 ++noninert_out_per_state[t.from()];
1478 ++noninert_out_per_block[0];
1479 }
1480 else
1481 {
1482 ++inert_in_per_state[t.to()];
1483 if (1 == ++inert_out_per_state[t.from()])
1484 {
1485 // this is the first inert outgoing transition of t.from()
1486 ++nr_of_nonbottom_states;
1487 }
1488 ++inert_out_per_block[0];
1489 }
1490 }
1491 mCRL2log(log::verbose) << "Number of extra states: "
1492 << extra_kripke_states.size() << "\n";
1493 #ifndef NDEBUG
1494 check_complexity::init(nr_of_states);
1495 #endif
1496}
1497
1498
1500template<class LTS_TYPE>
1501inline void bisim_partitioner_gjkw_initialise_helper<LTS_TYPE>::
1502init_transitions(part_state_t& part_st, part_trans_t& part_tr,
1503 bool const branching, bool const preserve_divergence)
1504{ assert(part_st.state_size() == get_nr_of_states());
1505 assert(part_tr.trans_size() == get_nr_of_transitions());
1506 // initialise blocks and B_to_C slices
1507 permutation_iter_t begin = part_st.permutation.begin();
1508 constln_t* const constln = new constln_t(get_nr_of_states(), begin,
1509 part_st.permutation.end(), part_tr.B_to_C_end());
1510 if (1 < states_per_block.size())
1511 {
1512 constln->make_nontrivial();
1513 }
1514 std::vector<block_t*> blocks(states_per_block.size());
1515 B_to_C_iter_t B_to_C_begin = part_tr.B_to_C.begin();
1516 for (state_type B = 0; B < states_per_block.size(); ++B)
1517 {
1518 permutation_iter_t const end = begin + states_per_block[B];
1519 blocks[B] = new block_t(constln, begin, end);
1520 if (0 == noninert_out_per_block[B] && 0 == inert_out_per_block[B])
1521 {
1522 blocks[B]->set_inert_begin_and_end(part_tr.B_to_C.begin(),
1523 part_tr.B_to_C.begin()); assert(blocks[B]->to_constln.empty());
1524 }
1525 else
1526 {
1527 blocks[B]->set_inert_begin_and_end(B_to_C_begin +
1528 noninert_out_per_block[B],
1529 B_to_C_begin + noninert_out_per_block[B] +
1530 inert_out_per_block[B]);
1531 blocks[B]->to_constln.emplace_back(B_to_C_begin,
1532 blocks[B]->inert_end());
1533 B_to_C_desc_iter_t const slice =
1534 std::prev(blocks[B]->to_constln.end()); assert(B_to_C_begin < slice->end);
1535 for (; slice->end != B_to_C_begin; ++B_to_C_begin)
1536 {
1537 B_to_C_begin->B_to_C_slice = slice;
1538 }
1539 }
1540 begin = end;
1541 } assert(part_st.permutation.end() == begin);
1542 /* only block 0 has a sequence number and non-bottom states: */ assert(part_tr.B_to_C.end() == B_to_C_begin);
1543 blocks[0]->assign_seqnr();
1544 blocks[0]->set_bottom_begin(blocks[0]->begin() + nr_of_nonbottom_states);
1545 blocks[0]->set_marked_nonbottom_begin(blocks[0]->bottom_begin());
1546
1547 // initialise states and succ slices
1548 part_st.state_info.front().set_pred_begin(part_tr.pred.begin());
1549 part_st.state_info.front().set_succ_begin(part_tr.succ.begin());
1550 for (state_type s = 0; get_nr_of_states() != s; ++s)
1551 {
1552 part_st.state_info[s].set_pred_end(part_st.state_info[s].pred_begin() +
1553 noninert_in_per_state[s] + inert_in_per_state[s]);
1554 part_st.state_info[s].set_inert_pred_begin(part_st.state_info[s].
1555 pred_begin() + noninert_in_per_state[s]);
1556 // part_st.state_info[s+1].set_pred_begin(part_st.state_info[s].
1557 // pred_end());
1558
1559 succ_iter_t succ_iter = part_st.state_info[s].succ_begin();
1560 succ_iter_t succ_end = succ_iter +
1561 noninert_out_per_state[s] + inert_out_per_state[s];
1562 part_st.state_info[s].set_succ_end(succ_end);
1563 part_st.state_info[s].set_current_constln(succ_end);
1564 part_st.state_info[s].set_inert_succ_begin_and_end(part_st.
1565 state_info[s].succ_begin() + noninert_out_per_state[s], succ_end);
1566 if (succ_iter < succ_end)
1567 {
1568 --succ_end;
1569 for (; succ_iter < succ_end; ++succ_iter)
1570 {
1571 succ_iter->set_slice_begin_or_before_end(succ_end);
1572 } assert(succ_iter == succ_end);
1573 succ_end->set_slice_begin_or_before_end(
1574 part_st.state_info[s].succ_begin());
1575 } else assert(succ_end == succ_iter);
1576 if (s < aut.num_states())
1577 {
1578 // s is not an extra Kripke state. It is in block 0.
1579 part_st.state_info[s].block = blocks[0];
1580 if (0 != inert_out_per_state[s])
1581 {
1582 /* non-bottom state: */ assert(0 != nr_of_nonbottom_states);
1583 --nr_of_nonbottom_states;
1584 part_st.state_info[s].pos = blocks[0]->begin() +
1585 nr_of_nonbottom_states;
1586 }
1587 else
1588 { // The following assertion is incomplete; only the second
1589 // bottom state: // assertion (after the assignment) makes sure that not too
1590 // many states become part of this slice.
1591 assert(0 != states_per_block[0]);
1592 --states_per_block[0];
1593 part_st.state_info[s].pos = blocks[0]->begin() +
1594 states_per_block[0]; assert(part_st.state_info[s].pos >= blocks[0]->bottom_begin());
1595 }
1596 *part_st.state_info[s].pos = &part_st.state_info[s];
1597 // part_st.state_info[s].notblue = 0;
1598 }
1599 }
1600
1601 // initialise transitions (and finalise extra Kripke states)
1602 for (const transition& t: aut.get_transitions())
1603 {
1604 if (!branching || !aut.is_tau(aut.apply_hidden_label_map(t.label())) ||
1605 (preserve_divergence && t.from() == t.to()))
1606 {
1607 // take transition through an extra intermediary state
1608 Key const k(aut.apply_hidden_label_map(t.label()), t.to());
1609 state_type const extra_state = extra_kripke_states[k];
1610 if (0 != noninert_out_per_state[extra_state])
1611 {
1612 state_type const extra_block =
1613 action_block_map[aut.apply_hidden_label_map(t.label())];
1614 // now initialise extra_state correctly
1615 part_st.state_info[extra_state].block = blocks[extra_block]; assert(0 != states_per_block[extra_block]);
1616 --states_per_block[extra_block];
1617 part_st.state_info[extra_state].pos = blocks[extra_block]->
1618 begin() + states_per_block[extra_block];
1619 *part_st.state_info[extra_state].pos =
1620 &part_st.state_info[extra_state];
1621 // part_st.state_info[extra_state].notblue = 0;
1622
1623 // state extra_state has exactly one outgoing transition,
1624 // namely a noninert transition to to t.to(). It has to be
1625 /* initialised now. */ assert(0 != noninert_in_per_state[t.to()]);
1626 --noninert_in_per_state[t.to()];
1627 pred_iter_t const t_pred =
1628 part_st.state_info[t.to()].noninert_pred_begin() +
1629 noninert_in_per_state[t.to()];
1630 --noninert_out_per_state[extra_state]; assert(0 == noninert_out_per_state[extra_state]);
1631 succ_iter_t const t_succ =
1632 part_st.state_info[extra_state].succ_begin(); assert(0 != noninert_out_per_block[extra_block]);
1633 B_to_C_iter_t const t_B_to_C =
1634 blocks[extra_block]->inert_begin() -
1635 noninert_out_per_block[extra_block]--;
1636 t_pred->source = &part_st.state_info[extra_state];
1637 t_pred->succ = t_succ;
1638 t_succ->target = &part_st.state_info[t.to()];
1639 t_succ->B_to_C = t_B_to_C;
1640 // t_B_to_C->B_to_C_slice = (already initialised);
1641 t_B_to_C->pred = t_pred;
1642 }
1643 /* noninert transition from t.from() to extra_state */ assert(0 != noninert_in_per_state[extra_state]);
1644 --noninert_in_per_state[extra_state];
1645 pred_iter_t const t_pred =
1646 part_st.state_info[extra_state].noninert_pred_begin() +
1647 noninert_in_per_state[extra_state]; assert(0 != noninert_out_per_state[t.from()]);
1648 --noninert_out_per_state[t.from()];
1649 succ_iter_t const t_succ=part_st.state_info[t.from()].succ_begin()+
1650 noninert_out_per_state[t.from()]; assert(0 != noninert_out_per_block[0]);
1651 B_to_C_iter_t const t_B_to_C = blocks[0]->inert_begin() -
1652 noninert_out_per_block[0]--;
1653
1654 t_pred->source = &part_st.state_info[t.from()];
1655 t_pred->succ = t_succ;
1656 t_succ->target = &part_st.state_info[extra_state];
1657 t_succ->B_to_C = t_B_to_C;
1658 // t_B_to_C->B_to_C_slice = (already initialised);
1659 t_B_to_C->pred = t_pred;
1660 }
1661 else
1662 {
1663 /* inert transition from t.from() to t.to() */ assert(0 != inert_in_per_state[t.to()]);
1664 --inert_in_per_state[t.to()];
1665 pred_iter_t const t_pred =
1666 part_st.state_info[t.to()].inert_pred_begin() +
1667 inert_in_per_state[t.to()]; assert(0 != inert_out_per_state[t.from()]);
1668 --inert_out_per_state[t.from()];
1669 succ_iter_t const t_succ =
1670 part_st.state_info[t.from()].inert_succ_begin() +
1671 inert_out_per_state[t.from()]; assert(0 != inert_out_per_block[0]);
1672 --inert_out_per_block[0];
1673 B_to_C_iter_t const t_B_to_C = blocks[0]->inert_begin() +
1674 inert_out_per_block[0];
1675
1676 t_pred->source = &part_st.state_info[t.from()];
1677 t_pred->succ = t_succ;
1678 t_succ->target = &part_st.state_info[t.to()];
1679 t_succ->B_to_C = t_B_to_C;
1680 // t_B_to_C->B_to_C_slice = (already initialised);
1681 t_B_to_C->pred = t_pred;
1682 }
1683 }
1684 noninert_out_per_state.clear(); inert_out_per_state.clear();
1685 noninert_in_per_state.clear(); inert_in_per_state.clear();
1686 noninert_out_per_block.clear(); inert_out_per_block.clear();
1687 states_per_block.clear();
1688
1689 aut.clear_transitions();
1690
1691 mCRL2log(log::verbose) << "Size of the resulting Kripke structure: "
1692 << get_nr_of_states() << " states and "
1693 << get_nr_of_transitions() << " transitions.\n";
1694}
1695
1712template <class LTS_TYPE>
1713void bisim_partitioner_gjkw_initialise_helper<LTS_TYPE>::
1714 replace_transition_system(const part_state_t& part_st, ONLY_IF_DEBUG( const bool branching, )
1715 const bool preserve_divergence)
1716{
1717 std::unordered_map <state_type, Key> to_lts_map;
1718 // obtain a map from state to <action, state> pair from extra_kripke_states
1719 for (typename std::unordered_map<Key, state_type, KeyHasher>::iterator it =
1720 extra_kripke_states.begin(); it != extra_kripke_states.end(); ++it)
1721 {
1722 to_lts_map.insert(std::make_pair(it->second, it->first));
1723 }
1724 extra_kripke_states.clear();
1725
1726 label_type const tau_label = aut.tau_label_index();
1727 // In the following loop, we visit a bottom state of each block and take
1728 // its transitions. As the partition is (assumed to be) stable, in this
1729 // way we visit each transition of a lumped state exactly once.
1730 for (permutation_const_iter_t s_iter = part_st.permutation.begin();
1731 part_st.permutation.end() != s_iter; ++s_iter)
1732 {
1733 block_t *B = (*s_iter)->block;
1734 // forward to last state of block, i. e. to a bottom state:
1735 s_iter = B->end() - 1; assert(B->bottom_end() > s_iter); assert(B->bottom_begin() <= s_iter);
1736 assert(B->end() == B->constln()->end());
1737 state_type const s_eq = B->seqnr();
1738 if (BLOCK_NO_SEQNR == s_eq)
1739 {
1740 break;
1741 }
1742
1743 for (succ_const_iter_t succ_iter = (*s_iter)->succ_begin();
1744 (*s_iter)->succ_end() != succ_iter; )
1745 {
1746 if (state_type t_eq = succ_iter->target->block->seqnr();
1747 BLOCK_NO_SEQNR != t_eq)
1748 { assert(branching);
1749 // We have a transition that originally was inert.
1750 if (s_eq == t_eq)
1751 {
1752 // The transition is still inert.
1753 if (!preserve_divergence)
1754 {
1755 // As we do not preserve divergence, we do not add it.
1756 // Nor will we add other transitions to the same
1757 // constellation.
1758 succ_iter = succ_entry::slice_end(succ_iter);
1759 continue;
1760 }
1761 if (*s_iter != succ_iter->target)
1762 {
1763 // The transition was not a self-loop to start with.
1764 // So we do not add it either.
1765 ++succ_iter;
1766 continue;
1767 }
1768 } assert((label_type) -1 != tau_label);
1769 aut.add_transition(transition(s_eq, tau_label, t_eq));
1770 }
1771 else
1772 {
1773 state_type const tgt_id = succ_iter->target -
1774 &part_st.state_info.front();
1775 // We have a non-inert transition to an intermediary state.
1776 // Look up the label and where the transition from the
1777 // intermediary state goes.
1778 Key const k = to_lts_map.find(tgt_id)->second;
1779 t_eq = part_st.state_info[k.second].block->seqnr(); assert(BLOCK_NO_SEQNR != t_eq);
1780 aut.add_transition(transition(s_eq, k.first, t_eq)); // The target state could also be found through the pointer
1781 // structure (but we also need the labels, which are not stored
1782 // in the refinable partition):
1783 assert(&part_st.state_info[k.second]==succ_iter->target->succ_begin()->target);
1784 assert(1 == succ_iter->target->succ_end() - succ_iter->target->succ_begin());
1785 }
1786 // Skip over other transitions from the same state to the same
1787 // constellation -- they would be mapped to the same resulting
1788 // transition.
1789 succ_iter = succ_entry::slice_end(succ_iter);
1790 }
1791 }
1792
1793 // Merge the states, by setting the state labels of each state to the concatenation of the state labels of its
1794 // equivalence class.
1795
1796 if (aut.has_state_info()) /* If there are no state labels this step can be ignored */
1797 {
1798 /* Create a vector for the new labels */
1799 std::vector<typename LTS_TYPE::state_label_t> new_labels(block_t::nr_of_blocks);
1800
1801 for(std::size_t i=aut.num_states(); i>0; )
1802 {
1803 --i;
1804 const std::size_t new_index=part_st.block(i)->seqnr(); /* get_eq_class(i) */
1805 new_labels[new_index] = new_labels[new_index] + aut.state_label(i);
1806 }
1807
1808 aut.set_num_states(block_t::nr_of_blocks);
1809 for(std::size_t i=0; i<block_t::nr_of_blocks; ++i)
1810 {
1811 aut.set_state_label(i,new_labels[i]);
1812 }
1813 }
1814 else
1815 {
1816 aut.set_num_states(block_t::nr_of_blocks);
1817 }
1818
1819 aut.set_initial_state(part_st.block(aut.initial_state())->seqnr());
1820}
1821
1822} // end namespace bisim_gjkw
1823
1824
1825
1826/*=============================================================================
1827= dbStutteringEquivalence -- Algorithm 2 in [GJKW 2017] =
1828=============================================================================*/
1829
1830
1831
1832template <class LTS_TYPE>
1833void bisim_partitioner_gjkw<LTS_TYPE>::create_initial_partition_gjkw(
1834 bool const branching, bool const preserve_divergence)
1835{
1836 // 2.2: P := P_0, i. e. the initial, cycle-free partition; C = {S}
1837 // and
1838 // 2.3: Initialise all temporary data
1839 init_helper.init_transitions(part_st, part_tr, branching,
1840 preserve_divergence);
1841}
1842
1843
1844template <class LTS_TYPE>
1845void bisim_partitioner_gjkw<LTS_TYPE>::
1846 refine_partition_until_it_becomes_stable_gjkw()
1847{
1848 #ifndef NDEBUG
1849 if (mCRL2logEnabled(log::debug))
1850 {
1851 part_st.print_part(part_tr);
1852 part_st.print_trans();
1853 }
1854
1855 part_tr.assert_stability(part_st);
1856 #endif
1857 // 2.4: while C contains a nontrivial constellation SpC do
1858 while (nullptr != bisim_gjkw::constln_t::get_some_nontrivial())
1859 { // check_complexity::add_work is called below, after SpB has been found
1860 bisim_gjkw::constln_t* const SpC =
1861 bisim_gjkw::constln_t::get_some_nontrivial();
1862 // 2.5: Choose a small splitter block SpB subset of SpC from P,
1863 // i.e. |SpB| <= 1/2*|SpC|
1864 // and
1865 // 2.6: Create a new constellation NewC and move SpB from SpC to NewC
1866 // and
1867 // 2.7: C := partition C where SpB is removed from SpC and NewC is
1868 // added
1869 bisim_gjkw::block_t* const SpB = SpC->split_off_small_block();
1870 bisim_gjkw::constln_t* const NewC = SpB->constln();
1871 #ifndef NDEBUG
1872 unsigned const max_counter = check_complexity::log_n -
1873 /*-------------------- find predecessors of SpB ---------------------*/ check_complexity::ilog2(SpB->size());
1874 #endif
1875 /* 2.8: Mark block SpB as refinable */ mCRL2complexity(SpB, add_work(check_complexity::
1876 /* 2.9: Mark all states of SpB as predecessors */ while_C_contains_a_nontrivial_constellation_2_4, max_counter), );
1877 /* we deviate from the published algorithm: only states with a */ assert(nullptr == bisim_gjkw::block_t::get_some_refinable());
1878 // transition to SpC will be marked. SpB will be split separately.
1879 // 2.17: Register that the transitions from s to inert_out(s) go to
1880 // NewC (instead of SpC)
1881 // (Before we enter the loop, we already adapt the ``B_to_C''
1882 // transition array.)
1883 part_tr.split_inert_to_C(SpB);
1884 // 2.10: for all s in SpB do
1885 /* We have to walk through the states from end to beginning so */ mCRL2complexity(SpB,
1886 /* we can mark state s if necessary. Marking will move s to a */ add_work(check_complexity::for_all_s_in_SpB_2_10, max_counter), );
1887 // position that has already been visited.
1888 for (bisim_gjkw::permutation_iter_t s_iter = SpB->end();
1889 SpB->begin() != s_iter; )
1890 {
1891 --s_iter;
1892 bisim_gjkw::state_info_ptr const s = *s_iter; // mCRL2complexity(s, ...) -- optimized to the above call.
1893 // 2.11: for all s_prime in noninert_in(s) do
1894 for (bisim_gjkw::pred_iter_t pred_iter = s->noninert_pred_begin();
1895 s->noninert_pred_end() != pred_iter; ++pred_iter)
1896 { mCRL2complexity(pred_iter, add_work(
1897 check_complexity::for_all_s_prime_in_pred_s_2_11, max_counter), );
1898 assert(part_tr.pred_end() > pred_iter);
1899 assert(pred_iter->succ->B_to_C->pred == pred_iter);
1900 bisim_gjkw::state_info_ptr const s_prime = pred_iter->source;
1901 // 2.12: Mark the block of s_prime as refinable
1902 bool const first_transition_of_block =
1903 s_prime->block->make_refinable();
1904 // 2.13: Mark s_prime as predecessor of SpB
1905 bool const first_transition_of_state =
1906 s_prime->block->mark(s_prime);
1907 // 2.14: Register that s_prime->s goes to NewC (instead of SpC)
1908 // and
1909 // 2.15: Store whether s' still has some transition to SpC\SpB
1910 s_prime->set_current_constln(part_tr.change_to_C(pred_iter, ONLY_IF_DEBUG( SpC, NewC, )
1911 first_transition_of_state, first_transition_of_block));
1912 // 2.16: end for
1913 }
1914 // 2.17: Register that the transitions from s to inert_out(s) go to
1915 // NewC (instead of SpC)
1916 // (Here, we only adapt the ``succ'' transition array.)
1917 if (part_tr.split_s_inert_out(s ONLY_IF_DEBUG( , SpC )
1918 ))
1919 {
1920 // 2.18: Store whether s still has some transition to SpC\SpB
1921 // we deviate from the explanation of the published
1922 // algorithm: we store this information by marking states
1923 // with transitions to SpC.
1924 SpB->mark(s);
1925 }
1926 // 2.19: end for
1927 }
1928
1929 // second pass through the predecessors to correct the pointers to the
1930 // constln_slices
1931 for (bisim_gjkw::permutation_iter_t s_iter = SpB->begin();
1932 SpB->end() != s_iter; ++s_iter)
1933 {
1934 bisim_gjkw::state_info_ptr const s = *s_iter;
1935 for (bisim_gjkw::pred_iter_t pred_iter = s->noninert_pred_begin();
1936 s->noninert_pred_end() != pred_iter; ++pred_iter)
1937 {
1938 bisim_gjkw::succ_iter_t succ = pred_iter->succ;
1939 bisim_gjkw::succ_iter_t before_end =
1940 pred_iter->source->current_constln() - 1;
1941 if (succ != before_end)
1942 { assert(succ<before_end); assert(succ>=before_end->slice_begin_or_before_end());
1943 assert(succ->slice_begin_or_before_end() ==
1944 before_end->slice_begin_or_before_end());
1945 succ->set_slice_begin_or_before_end(before_end);
1946 }
1947 }
1948 }
1949 #ifndef NDEBUG
1950 // The following tests cannot be executed during the above loops
1951 // because a state s_prime may have multiple transitions to SpB.
1952 for (bisim_gjkw::permutation_const_iter_t s_iter = SpB->begin();
1953 SpB->end() != s_iter; ++s_iter)
1954 {
1955 bisim_gjkw::state_info_ptr const s = *s_iter;
1956 for (bisim_gjkw::pred_const_iter_t pred_iter=s->noninert_pred_begin();
1957 s->noninert_pred_end() != pred_iter; ++pred_iter)
1958 {
1959 bisim_gjkw::state_info_const_ptr const s_prime = pred_iter->source;
1960 // check consistency of s_prime->current_constln()
1961 assert(s_prime->succ_begin() == s_prime->current_constln() ||
1962 *s_prime->current_constln()[-1].target->constln() <= *SpC);
1963 assert(s_prime->succ_end() == s_prime->current_constln() ||
1964 *SpC <= *s_prime->current_constln()->target->constln());
1965 // s_prime must have a transition to the new constellation
1966 assert(s_prime->succ_begin() < s_prime->current_constln());
1967 assert(s_prime->current_constln()[-1].target->constln() == NewC);
1968 // check consistency of s_prime->inert_succ_begin() and
1969 // s_prime->inert_succ_end()
1970 assert(s_prime->succ_begin() == s_prime->inert_succ_begin() ||
1971 *s_prime->inert_succ_begin()[-1].target->constln() <=
1972 *s_prime->constln());
1973 assert(s_prime->succ_begin() == s_prime->inert_succ_begin() ||
1974 s_prime->inert_succ_begin()[-1].target->block !=
1975 s_prime->block);
1976 assert(s_prime->inert_succ_begin()==s_prime->inert_succ_end()||
1977 (s_prime->inert_succ_begin()->target->block ==
1978 s_prime->block &&
1979 s_prime->inert_succ_end()[-1].target->block ==
1980 s_prime->block));
1981 assert(s_prime->succ_end() == s_prime->inert_succ_end() ||
1982 *s_prime->constln() <
1983 *s_prime->inert_succ_end()->target->constln());
1984 }
1985 // check consistency of s->inert_succ_begin() and
1986 // s->inert_succ_end()
1987 assert(s->succ_begin() == s->inert_succ_begin() ||
1988 *s->inert_succ_begin()[-1].target->constln() < *s->constln());
1989 assert(s->inert_succ_begin() == s->inert_succ_end() ||
1990 /*------------------ stabilise the partition again ------------------*/ (s->inert_succ_begin()->target->block == s->block &&
1991 s->inert_succ_end()[-1].target->block == s->block));
1992 /* deviation from the published algorithm: we first refine the */ assert(s->succ_end() == s->inert_succ_end() ||
1993 /* splitter according to the marking of states (marked states have a */ *s->constln() < *s->inert_succ_end()->target->constln());
1994 /* transition to SpC). */ }
1995 #endif // ifndef NDEBUG
1996 if (0 != SpB->marked_size())
1997 {
1998 if (1 == SpB->size())
1999 {
2000 // if the block only contains a single state, the refinement
2001 // would be trivial anyway (and it cannot find new bottom
2002 // states).
2003 SpB->set_marked_bottom_begin(SpB->bottom_end());
2004 }
2005 else
2006 {
2007 bisim_gjkw::block_t* RedB = refine(SpB, SpC, nullptr, false);
2008 if (0 != RedB->unmarked_bottom_size())
2009 {
2010 postprocess_new_bottom(RedB);
2011 }
2012 else
2013 {
2014 RedB->set_marked_bottom_begin(RedB->bottom_end());
2015 }
2016 }
2017 }
2018
2019 // 2.20: for all refinable blocks RfnB do
2020 while (nullptr != bisim_gjkw::block_t::get_some_refinable())
2021 {
2022 bisim_gjkw::block_t* const RfnB =
2023 bisim_gjkw::block_t::get_some_refinable();
2024 // 2.21: Mark block RfnB as non-refinable
2025 RfnB->make_nonrefinable();
2026 #ifndef NDEBUG
2027 // The work in this loop has to be assigned to the B_to_C-
2028 // slice that contains the transitions from RfnB to NewC.
2029 // Note that this is not FromRed, so we have to find it in a
2030 // different way. First find a marked state:
2031 bisim_gjkw::permutation_iter_t s_mark_iter = RfnB->marked_bottom_begin();
2032 if (s_mark_iter == RfnB->marked_bottom_end())
2033 {
2034 s_mark_iter = RfnB->marked_nonbottom_begin();
2035 assert(s_mark_iter < RfnB->marked_nonbottom_end());
2036 }
2037 // Now, using the current_constln pointer of s, find a
2038 // transition to NewC.
2039 bisim_gjkw::succ_iter_t to_NewC =
2040 std::prev((*s_mark_iter)->current_constln());
2041 assert((*s_mark_iter)->succ_begin() <= to_NewC);
2042 assert(to_NewC->target->constln() == NewC);
2043 mCRL2complexity(to_NewC->B_to_C->B_to_C_slice, add_work(
2044 check_complexity::for_all_refinable_blocks_RfnB_2_20, max_counter), );
2045 #endif
2046 if (1 == RfnB->size())
2047 {
2048 // if the block only contains a single state, the refinement
2049 // would be trivial anyway (and it cannot find new bottom
2050 // states).
2051 RfnB->set_marked_bottom_begin(RfnB->bottom_end());
2052 continue;
2053 }
2054 // 2.22: <RedB, BlueB> := Refine(RfnB, NewC, {marked states in
2055 // RfnB}, {})
2056 bisim_gjkw::block_t* RedB = refine(RfnB, NewC, nullptr, false);
2057 // 2.23: if RedB contains new bottom states then
2058 if (0 != RedB->unmarked_bottom_size())
2059 {
2060 // 2.24: RedB := PostprocessNewBottom(RedB, BlueB)
2061 RedB = postprocess_new_bottom(RedB);
2062 if (nullptr == RedB) continue;
2063 // 2.25: end if
2064 }
2065 // 2.30: Unmark all states of the original RfnB as predecessors
2066 // (first part) This needs to be done to make sure the call to
2067 // Refine in line 2.26 does not regard some states as marked.
2068 else
2069 {
2070 RedB->set_marked_bottom_begin(RedB->bottom_end());
2071 }
2072 assert(0 == RedB->marked_size());
2073 if (1 == RedB->size() || nullptr == RedB->FromRed(SpC))
2074 {
2075 // If the block only contains a single state or has no
2076 // transitions to SpC, the refinement would be trivial anyway
2077 // (and it cannot find new bottom states).
2078 continue;
2079 }
2080
2081 // 2.26: <RedB, BlueB> := Refine(RedB, SpC\SpB, {}, {transitions
2082 // from RedB to SpC\SpB})
2083 RedB = refine(RedB, SpC, RedB->FromRed(SpC), false ONLY_IF_DEBUG( , NewC )
2084 );
2085 // 2.27: if RedB contains new bottom states then
2086 if (0 != RedB->unmarked_bottom_size())
2087 {
2088 // 2.28: PostprocessNewBottom(RedB, BlueB)
2089 postprocess_new_bottom(RedB);
2090 // 2.29: endif
2091 }
2092 // 2.30: Unmark all states of the original RfnB as predecessors
2093 // if postprocess_new_bottom is called, that procedure already
2094 // unmarks the new bottom states.
2095 else
2096 {
2097 RedB->set_marked_bottom_begin(RedB->bottom_end());
2098 } assert(0 == RedB->marked_size());
2099 // 2.31: end for
2100 }
2101 #ifndef NDEBUG
2102 if (mCRL2logEnabled(log::debug))
2103 {
2104 part_st.print_part(part_tr);
2105 part_st.print_trans();
2106 }
2107
2108 /* 2.32: end while */ part_tr.assert_stability(part_st);
2109 #endif
2110 }
2111 // 2.33: return P
2112 // (this happens implicitly, through the bisim_partitioner_gjkw object
2113 // data)
2114 mCRL2log(log::verbose) << "number of blocks in the quotient: "
2115 << bisim_gjkw::block_t::nr_of_blocks << '\n';
2116}
2117 #ifndef NDEBUG
2118 namespace bisim_gjkw
2119 {
2120/*=============================================================================
2121= Refine -- Algorithm 3 in [GJKW 2017] =
2122=============================================================================*/
2135 static void blue_is_smaller(block_t* BlueB, block_t* RedB,
2136 const constln_t* NewC)
2137 {
2138 assert(nullptr != RedB);
2139 if (nullptr != BlueB)
2140 {
2141 assert(BlueB->size() <= RedB->size());
2142 unsigned const max_NewB = nullptr == BlueB ? 0
2143 : check_complexity::log_n-check_complexity::ilog2(BlueB->size());
2144 for (permutation_iter_t i = BlueB->begin(); BlueB->end() != i; ++i)
2145 {
2146 state_info_ptr s = *i;
2147 mCRL2complexity(s, finalise_work(check_complexity::
2148 while_Test_is_not_empty_3_6l_s_is_blue_3_11l,
2149 check_complexity::refine_bottom_state_3_6l,
2150 max_NewB), );
2151 mCRL2complexity(s, finalise_work(check_complexity::
2152 while_Blue_contains_unvisited_states_3_15l,
2153 check_complexity::refine_visited_state_3_15,
2154 max_NewB), );
2155 for (succ_iter_t succ = s->succ_begin(); s->succ_end() != succ;
2156 ++succ)
2157 {
2158 mCRL2complexity(succ->B_to_C->pred,finalise_work(
2159 check_complexity::
2160 if___s_prime_has_transition_to_SpC_3_23l,
2161 check_complexity::
2162 refine_outgoing_transition_3_6_or_23l, max_NewB), );
2163 }
2164 for (pred_iter_t pred = s->pred_begin(); s->pred_end() != pred;
2165 ++pred)
2166 {
2167 mCRL2complexity(pred, finalise_work(check_complexity::
2168 for_all_s_prime_in_pred_s_setminus_Red_3_18l,
2169 check_complexity::refine_incoming_transition_3_18,
2170 max_NewB), );
2171 }
2172 }
2173 }
2174 // cancel work counters for the red states, and also measure the work
2175 // done in the blue coroutine on states that turned out to be red.
2176 unsigned const max_NewC = nullptr == NewC ? 0
2177 : check_complexity::log_n - check_complexity::ilog2(NewC->size());
2178 for (permutation_iter_t i = RedB->begin(); RedB->end() != i; ++i)
2179 {
2180 state_info_ptr s = *i;
2181 mCRL2complexity(s, cancel_work(check_complexity::
2182 while_Red_contains_unvisited_states_3_15r), );
2183 for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
2184 {
2185 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2186 check_complexity::while_FromRed_is_not_empty_3_6r), );
2187 // the following counter should only be set for transitions to
2188 // the splitter constellation. For others transitions, no
2189 // (temporary) work should have been done.
2190 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2191 check_complexity::
2192 while_Test_is_not_empty_3_6l_s_is_red_3_9l,
2193 check_complexity::
2194 refine_outgoing_transition_to_marked_state_3_6l,
2195 succ->target->constln() == NewC ? max_NewC : 0), );
2196 // the following counter only gets 1 during postprocessing, at
2197 // a time when state s is already stored as bottom state.
2198 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2199 check_complexity::
2200 while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing,
2201 check_complexity::
2202 refine_outgoing_transition_postprocess_new_bottom_3_6l,
2203 1), );
2204 // the following counter only gets 1 before postprocessing, at
2205 // the same time as when it is discovered to be a new bottom
2206 // state
2207 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2208 check_complexity::if___s_prime_has_transition_to_SpC_3_23l,
2209 check_complexity::
2210 refine_outgoing_transition_from_new_bottom_3_23l, 1), );
2211 }
2212 for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
2213 {
2214 mCRL2complexity(pred, cancel_work(check_complexity::
2215 for_all_s_prime_in_pred_s_3_18r), );
2216 }
2217 }
2218 // check the balance between useful and cancelled work:
2219 check_complexity::check_temporary_work();
2220 }
2221
2229 static void red_is_smaller(block_t* BlueB, block_t* RedB)
2230 {
2231 assert(nullptr != BlueB);
2232 assert(nullptr != RedB);
2233 assert(BlueB->size() >= RedB->size());
2234 for (permutation_iter_t i = BlueB->begin(); BlueB->end() != i; ++i)
2235 {
2236 state_info_ptr s = *i;
2237 mCRL2complexity(s, cancel_work(check_complexity::
2238 while_Test_is_not_empty_3_6l_s_is_blue_3_11l), );
2239 mCRL2complexity(s, cancel_work(check_complexity::
2240 while_Blue_contains_unvisited_states_3_15l), );
2241 for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
2242 {
2243 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2244 check_complexity::
2245 if___s_prime_has_transition_to_SpC_3_23l), );
2246 }
2247 for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
2248 {
2249 mCRL2complexity(pred, cancel_work(check_complexity::
2250 for_all_s_prime_in_pred_s_setminus_Red_3_18l), );
2251 }
2252 }
2253 unsigned const max_NewB = check_complexity::log_n -
2254 check_complexity::ilog2(RedB->size());
2255 for (permutation_iter_t i = RedB->begin(); RedB->end() != i; ++i)
2256 {
2257 state_info_ptr s = *i;
2258 mCRL2complexity(s, finalise_work(check_complexity::
2259 while_Red_contains_unvisited_states_3_15r,
2260 check_complexity::refine_visited_state_3_15, max_NewB), );
2261 for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
2262 {
2263 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2264 check_complexity::while_FromRed_is_not_empty_3_6r,
2265 check_complexity::
2266 refine_outgoing_transition_3_6_or_23l, max_NewB), );
2267 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2268 check_complexity::
2269 while_Test_is_not_empty_3_6l_s_is_red_3_9l), );
2270 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2271 check_complexity::
2272 while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing), );
2273 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2274 check_complexity::
2275 if___s_prime_has_transition_to_SpC_3_23l), );
2276 }
2277 for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
2278 {
2279 mCRL2complexity(pred, finalise_work(check_complexity::
2280 for_all_s_prime_in_pred_s_3_18r,
2281 check_complexity::refine_incoming_transition_3_18,
2282 max_NewB), );
2283 }
2284 }
2285 check_complexity::check_temporary_work();
2286 }
2287
2288 } // end namespace bisim_gjkw
2289 #endif
2359
2360template <class LTS_TYPE>
2361bisim_gjkw::block_t* bisim_partitioner_gjkw<LTS_TYPE>::refine(
2362 bisim_gjkw::block_t* const RfnB, const bisim_gjkw::constln_t* const SpC,
2363 const bisim_gjkw::B_to_C_descriptor* const FromRed,
2364 bool const postprocessing ONLY_IF_DEBUG( , const bisim_gjkw::constln_t* NewC )
2365 )
2366{
2367 #ifndef NDEBUG
2368 if (nullptr != FromRed)
2369 {
2370 assert(FromRed->from_block() == RfnB);
2371 assert(FromRed->to_constln() == SpC);
2372 assert(nullptr != SpC);
2373 assert(0 == RfnB->marked_size());
2374 }
2375 else
2376 {
2377 assert(0 != RfnB->marked_size());
2378 }
2379 assert(1 < RfnB->size());
2380 #endif
2381 // 3.2: if RfnB subseteq SpC then return RfnB
2382 if (RfnB->constln() == SpC)
2383 {
2384 // Mark all bottom states to indicate there are no new bottom states.
2385 RfnB->set_marked_nonbottom_begin(RfnB->nonbottom_end());
2386 RfnB->set_marked_bottom_begin(RfnB->bottom_begin());
2387 return RfnB;
2388 }
2389 // 3.3: Test := {bottom states}\Red, ...
2390 // 3.4: Spend the same amount of work on either coroutine:
2391 // and
2392 // 3.39: RedB := RfnB or RedB := NewB , respectively
2393 #ifndef NDEBUG
2394 bisim_gjkw::permutation_iter_t const red_end = RfnB->end();
2395 #endif
2396 bisim_gjkw::block_t* RedB;
2397
2398 COROUTINES_SECTION
2399 // common variables
2400 bisim_gjkw::permutation_iter_t notblue_initialised_end =
2401 RfnB->nonbottom_begin();
2402 bool FromRed_is_empty = nullptr == FromRed;
2403
2404 // variables for the blue coroutine
2405 bisim_gjkw::permutation_iter_t blue_visited_end;
2406 bisim_gjkw::state_info_ptr blue_s;
2407 bisim_gjkw::pred_iter_t blue_pred_iter;
2408 bisim_gjkw::state_info_ptr blue_s_prime;
2409 bisim_gjkw::permutation_iter_t blue_blue_nonbottom_end;
2410 bisim_gjkw::succ_const_iter_t blue_begin;
2411 bisim_gjkw::succ_const_iter_t blue_end;
2412
2413 // variables for the red coroutine
2414 bisim_gjkw::B_to_C_iter_t red_fromred_visited_begin;
2415 bisim_gjkw::permutation_iter_t red_visited_begin;
2416 bisim_gjkw::state_info_ptr red_s;
2417 bisim_gjkw::pred_iter_t red_pred_iter;
2418
2419 COROUTINE_LABELS( (REFINE_BLUE_PREDECESSOR_HANDLED)
2420 (REFINE_BLUE_TESTING)
2421 (REFINE_BLUE_STATE_HANDLED)
2422 (REFINE_BLUE_COLLECT_BOTTOM)
2423 (REFINE_RED_COLLECT_FROMRED)
2424 (REFINE_RED_PREDECESSOR_HANDLED)
2425 (REFINE_RED_STATE_HANDLED))
2426
2427/*--------------------------- handle blue states ----------------------------*/
2428
2429
2461
2462 COROUTINE assert(RfnB->nonbottom_begin() == notblue_initialised_end);
2463 // we have to decide which unmarked bottom states are blue. So we
2464 // walk over all of them and check whether they have a transition
2465 // to SpC or not.
2466 // 3.3: ..., Blue := {}
2467 blue_visited_end = RfnB->unmarked_bottom_begin();
2468 // 3.5l: whenever |Blue| > |RfnB|/2 do Abort this coroutine
2469 // nothing needs to be done now, as |Blue| = 0 here.
2470
2471 /* - - - - - - - collect blue bottom states - - - - - - - */
2472
2473 // 3.6l: while Test is not empty and FromRed is not empty do
2474 // We use the variable blue_visited_end in this loop to
2475 // indicate the boundary between blue states (namely those
2476 // in the interval [RfnB->unmarked_bottom_begin(),
2477 // blue_visited_end) ) and Test states (namely those in
2478 // [blue_visited_end, RfnB->unmarked_bottom_end()) ).
2479 COROUTINE_WHILE (REFINE_BLUE_COLLECT_BOTTOM,
2480 RfnB->unmarked_bottom_end() > blue_visited_end)
2481 {
2482 if (FromRed_is_empty)
2483 {
2484 // 3.14l: Blue := Blue union Test
2485 // done implicitly: we now regard all unmarked
2486 // bottom states as blue, i. e. the whole
2487 // interval [RfnB->unmarked_bottom_begin(),
2488 // RfnB->unmarked_bottom_end()).
2489 // 3.5l: whenever |Blue|>|RfnB|/2 do Abort this coroutine
2490 // In this case, Test may not yet be empty, so here we
2491 // have to check the condition of Line 3.5l.
2492 if (RfnB->unmarked_bottom_size() > RfnB->size() / 2)
2493 {
2494 ABORT_THIS_COROUTINE();
2495 }
2496 break;
2497 }
2498 // 3.7l: Choose s in Test
2499 blue_s = *blue_visited_end;
2500 // 3.8l: if s --> SpC then
2501 if (blue_s->surely_has_transition_to(SpC))
2502 {
2503 // 3.9l: Move s from Test to Red
2504 // The state s is not blue. Move it to the slice of
2505 // non-blue bottom states.
2506 RfnB->set_marked_bottom_begin(
2507 RfnB->marked_bottom_begin() - 1);
2508 bisim_gjkw::swap_permutation(blue_visited_end,
2509 RfnB->marked_bottom_begin());
2510 // 3.5r: whenever |Red|>|RfnB|/2 do Abort the red coroutine
2511 if (RfnB->marked_size() > RfnB->size() / 2)
2512 {
2513 ABORT_OTHER_COROUTINE();
2514 }
2515 #ifndef NDEBUG
2516 // The state is red. Depending on the context of refinement, the work done
2517 // on this state is attributed to one or another element of the Kripke
2518 // structure.
2519 if (postprocessing)
2520 {
2521 // refine() has been called from line 4.14. During postprocessing, the
2522 // work is ascribed to the transitions from s to SpC.
2523 // Using the current_constln pointer of s, find a transition to SpC.
2524 // The work has to be ascribed to the transitions from s to SpC.
2525 bisim_gjkw::succ_iter_t to_SpC = blue_s->current_constln();
2526 if (to_SpC == blue_s->succ_end() || to_SpC->target->constln() != SpC)
2527 {
2528 assert(blue_s->succ_begin() < to_SpC);
2529 --to_SpC;
2530 assert(to_SpC->target->constln() == SpC);
2531 }
2532 bisim_gjkw::succ_entry::slice_add_work_to_transns(to_SpC,
2533 check_complexity::
2534 while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing, 1);
2535 }
2536 else
2537 {
2538 // refine() has been called from line 2.26, and RfnB is a block with a
2539 // transition to SpB. The state has been marked because of these
2540 // transitions (which are not transitions to SpC!).
2541 // code similar to the case if (postprocessing).
2542 bisim_gjkw::succ_iter_t to_NewC = blue_s->current_constln();
2543 if (to_NewC == blue_s->succ_end() || to_NewC->target->constln() == SpC)
2544 {
2545 assert(blue_s->succ_begin() < to_NewC);
2546 --to_NewC;
2547 assert(to_NewC->target->constln() != SpC);
2548 }
2549 bisim_gjkw::succ_entry::slice_add_work_to_transns(to_NewC,
2550 check_complexity::while_Test_is_not_empty_3_6l_s_is_red_3_9l, 1);
2551 }
2552 #endif
2553 // 3.10l: else
2554 }
2555 else
2556 { assert(blue_s->surely_has_no_transition_to(SpC));
2557 // 3.11l: Move s from Test to Blue
2558 ++blue_visited_end;
2559 // 3.5l: whenever |Blue|>|RfnB|/2 do Abort this coroutine
2560 if ((state_type) (blue_visited_end -
2561 RfnB->unmarked_bottom_begin()) > RfnB->size() / 2)
2562 {
2563 ABORT_THIS_COROUTINE();
2564 } mCRL2complexity(blue_s, add_work(
2565 check_complexity::while_Test_is_not_empty_3_6l_s_is_blue_3_11l, 1), );
2566 // 3.12l: end if
2567 }
2568 // 3.13l: end while
2569 }
2570 END_COROUTINE_WHILE; assert(RfnB->constln() != SpC);
2571
2572 if (0 == RfnB->unmarked_bottom_size())
2573 {
2574 // all bottom states are red, so there cannot be any blue
2575 // states.
2576 RfnB->set_marked_nonbottom_begin(RfnB->marked_nonbottom_end());
2577 // RfnB->set_marked_bottom_begin(RfnB->bottom_begin());
2578 RedB = RfnB; ONLY_IF_DEBUG( blue_is_smaller(nullptr, RedB, NewC); )
2579 TERMINATE_COROUTINE_SUCCESSFULLY();
2580 }
2581
2582 /* - - - - - - - - visit blue states - - - - - - - - */
2583
2584 // 3.15l: while Blue contains unvisited states do
2585 blue_visited_end = RfnB->unmarked_bottom_begin();
2586 blue_blue_nonbottom_end = RfnB->unmarked_nonbottom_begin();
2587 COROUTINE_DO_WHILE (REFINE_BLUE_STATE_HANDLED,
2588 blue_visited_end != blue_blue_nonbottom_end)
2589 {
2590 // 3.16l: Choose an unvisited s in Blue
2591 blue_s = *blue_visited_end; assert(blue_visited_end < blue_blue_nonbottom_end ||
2592 (RfnB->unmarked_bottom_begin() <= blue_visited_end &&
2593 RfnB->unmarked_bottom_end() > blue_visited_end));
2594 assert(RfnB->unmarked_nonbottom_begin() <= blue_blue_nonbottom_end);
2595 assert(blue_blue_nonbottom_end <= notblue_initialised_end);
2596 /* 3.17l: Mark s as visited */ assert(RfnB->unmarked_nonbottom_end() >= notblue_initialised_end);
2597 ++blue_visited_end;
2598 // 3.18l: for all s_prime in inert_in(s) \ Red do
2599 COROUTINE_FOR (REFINE_BLUE_PREDECESSOR_HANDLED,
2600 blue_pred_iter = blue_s->inert_pred_begin(),
2601 blue_s->inert_pred_end()!=blue_pred_iter, ++blue_pred_iter)
2602 {
2603 blue_s_prime = blue_pred_iter->source;
2604 if (blue_s_prime->pos >= RfnB->marked_nonbottom_begin())
2605 { mCRL2complexity(blue_pred_iter, add_work(
2606 check_complexity::for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2607 continue;
2608 }
2609 // 3.19l: if notblue(s_prime) undefined then
2610 if (blue_s_prime->pos >= notblue_initialised_end)
2611 {
2612 // 3.20l: notblue(s_prime) := |inert_out(s_prime)|
2613 blue_s_prime->notblue = blue_s_prime->inert_succ_end()-
2614 blue_s_prime->inert_succ_begin();
2615 bisim_gjkw::swap_permutation(blue_s_prime->pos,
2616 notblue_initialised_end);
2617 ++notblue_initialised_end;
2618 // 3.21l: end if
2619 }
2620 // 3.22l: notblue(s_prime) := notblue(s_prime) - 1
2621 --blue_s_prime->notblue;
2622 // 3.23l: if notblue(s_prime) == 0 && ...
2623 if (0 != blue_s_prime->notblue)
2624 { mCRL2complexity(blue_pred_iter, add_work(
2625 check_complexity::for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2626 continue;
2627 }
2628 // 3.23l: ... && (FromRed == {} ||
2629 // out_noninert(s_prime) intersect SpC == {}) then
2630 if (!FromRed_is_empty)
2631 {
2632 if (blue_s_prime->surely_has_transition_to(SpC))
2633 { mCRL2complexity(blue_pred_iter, add_work(
2634 check_complexity::for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2635 continue;
2636 }
2637 if (!blue_s_prime->surely_has_no_transition_to(SpC))
2638 {
2639 // It is not yet known whether s_prime has a
2640 // transition to SpC or not. Execute the slow test
2641 // now.
2642 COROUTINE_FOR (REFINE_BLUE_TESTING,
2643 (blue_begin = blue_s_prime->succ_begin(),
2644 blue_end = blue_s_prime->succ_end() ),
2645 blue_begin < blue_end, (void) 0)
2646 {
2647 // binary search for transitions from s_prime
2648 // to constellation SpC.
2649 bisim_gjkw::succ_const_iter_t const mid =
2650 blue_begin + (blue_end - blue_begin) / 2;
2651 if (*SpC <= *mid->target->constln())
2652 {
2653 blue_end = mid->slice_begin();
2654 }
2655 if (*mid->target->constln() <= *SpC)
2656 {
2657 blue_begin =
2658 bisim_gjkw::succ_entry::slice_end(mid);
2659 }
2660 #ifndef NDEBUG
2661 bisim_gjkw::succ_entry::slice_add_work_to_transns(mid,
2662 check_complexity::if___s_prime_has_transition_to_SpC_3_23l, 1);
2663 #endif
2664 }
2665 END_COROUTINE_FOR;
2666 if (blue_begin != blue_end)
2667 { mCRL2complexity(blue_pred_iter, add_work(
2668 check_complexity::for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2669 continue;
2670 }
2671 }
2672 }
2673 // 3.24l: Blue := Blue union {s_prime}
2674 bisim_gjkw::swap_permutation(blue_s_prime->pos,
2675 blue_blue_nonbottom_end);
2676 ++blue_blue_nonbottom_end;
2677 // 3.5l: whenever |Blue|>|RfnB| / 2 do Abort this coroutine
2678 if (blue_blue_nonbottom_end -
2679 RfnB->unmarked_nonbottom_begin() +
2680 RfnB->unmarked_bottom_size() > RfnB->size() / 2)
2681 {
2682 ABORT_THIS_COROUTINE();
2683 }
2684 // 3.25l: end if
2685 // this is implicit in the `continue` statements above.
2686 /* 3.26l: end for */ mCRL2complexity(blue_pred_iter, add_work(
2687 check_complexity::for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2688 }
2689 END_COROUTINE_FOR;
2690 /* 3.27l: end while */ mCRL2complexity(blue_s, add_work(
2691 check_complexity::while_Blue_contains_unvisited_states_3_15l, 1), );
2692 if (RfnB->unmarked_bottom_end() == blue_visited_end)
2693 {
2694 blue_visited_end = RfnB->unmarked_nonbottom_begin();
2695 }
2696 }
2697 END_COROUTINE_DO_WHILE;
2698
2699 /* - - - - - - - - split off blue block - - - - - - - - */
2700
2701 // 3.28l: Abort the other coroutine
2702 ABORT_OTHER_COROUTINE();
2703 // All non-blue states are red.
2704 // 3.29l: Move Blue to a new block NewB
2705 // and
2706 // 3.30l: Destroy all temporary data
2707 bisim_gjkw::block_t* const NewB =
2708 RfnB->split_off_blue(blue_blue_nonbottom_end);
2709 part_tr.new_blue_block_created(RfnB, NewB);
2710 #ifndef NDEBUG
2711 unsigned const max_counter = check_complexity::log_n -
2712 check_complexity::ilog2(NewB->size());
2713 mCRL2complexity(NewB,
2714 add_work(check_complexity::for_all_s_in_NewB_3_31, max_counter), );
2715 #endif
2716 // 3.31l: for all s in NewB do
2717 for (bisim_gjkw::permutation_iter_t s_iter = NewB->begin();
2718 NewB->end() != s_iter; ++s_iter)
2719 {
2720 blue_s = *s_iter; // mCRL2complexity(s, ...) -- optimized to the above call.
2721 // 3.32l: for all s_prime in inert_in(s) \ NewB do
2722 for (blue_pred_iter = blue_s->inert_pred_begin();
2723 blue_s->inert_pred_end()!=blue_pred_iter; ++blue_pred_iter)
2724 { mCRL2complexity(blue_pred_iter, add_work(
2725 check_complexity::for_all_s_prime_in_pred_s_3_32l, max_counter), );
2726 assert(part_tr.pred_end() > blue_pred_iter);
2727 assert(blue_pred_iter->succ->B_to_C->pred == blue_pred_iter);
2728 blue_s_prime = blue_pred_iter->source;
2729 if (blue_s_prime->block == NewB) { continue; } assert(blue_s_prime->block == RfnB);
2730 // 3.33l: s_prime --> s is no longer inert
2731 part_tr.make_noninert(blue_pred_iter->succ);
2732 // 3.34l: if |inert_out(s_prime)| == 0 then
2733 if (blue_s_prime->inert_succ_begin() ==
2734 blue_s_prime->inert_succ_end())
2735 {
2736 // 3.35l: s_prime is a new bottom state
2737 RfnB->set_marked_nonbottom_begin(
2738 RfnB->bottom_begin() - 1);
2739 RfnB->set_bottom_begin(RfnB->marked_nonbottom_begin());
2740 swap_permutation(blue_s_prime->pos,
2741 RfnB->bottom_begin()); // assert("blue_s_prime has a transition to SpC");
2742 // 3.36l: end if
2743 }
2744 // 3.37l: end for
2745 }
2746 // 3.38l: end for
2747 }
2748
2749 RedB = RfnB; ONLY_IF_DEBUG( blue_is_smaller(NewB, RedB, NewC); )
2750 END_COROUTINE
2751
2752/*---------------------------- handle red states ----------------------------*/
2753
2781
2782 COROUTINE
2783 // 3.5r: whenever |Red| > |RfnB|/2 then Abort this coroutine
2784 if (RfnB->marked_size() > RfnB->size()/2) ABORT_THIS_COROUTINE();
2785 // The red block contains at most RfnB->size() -
2786 // RfnB->unmarked_bottom_size() + FromRed->size() states. If that
2787 // is <= RfnB->size() / 2, we could abort the other coroutine
2788 // immediately. We don't do it here because we want to investigate
2789 // the effect of this and similar heuristics more systematically.
2790
2791 /* - - - - - - - collect states from FromRed - - - - - - - */
2792
2793 // 3.6r: while FromRed != {} do
2794 if (nullptr != FromRed)
2795 { assert(FromRed->from_block() == RfnB);
2796 red_fromred_visited_begin = FromRed->end; assert(RfnB->inert_end() <= FromRed->begin ||
2797 (RfnB->inert_begin() >= red_fromred_visited_begin &&
2798 RfnB->inert_end() > red_fromred_visited_begin));
2799 COROUTINE_WHILE (REFINE_RED_COLLECT_FROMRED,
2800 FromRed->begin != red_fromred_visited_begin)
2801 {
2802 // 3.10r (order of lines changed): FromRed := FromRed \ {s --> t}
2803 // We can change the order of lines because the
2804 // coroutine is not interrupted in between.
2805 --red_fromred_visited_begin;
2806 // 3.7r: Choose s --> t in FromRed
2807 bisim_gjkw::state_info_ptr const red_s =
2808 red_fromred_visited_begin->pred->source; assert(RfnB->begin() <= red_s->pos);
2809 /* 3.8r: Test := Test \ {s} */ assert(red_s->pos < RfnB->end());
2810 // and
2811 // 3.9r: Red := Red union {s}
2812 if (red_s->pos < notblue_initialised_end)
2813 {
2814 // The non-bottom state has a transition to a blue
2815 // state, so notblue is initialised; however, now it is
2816 // revealed to be red anyway.
2817 bisim_gjkw::swap_permutation(red_s->pos,
2818 --notblue_initialised_end);
2819 }
2820 if (RfnB->mark(red_s) &&
2821 // 3.5r: whenever |Red| > |RfnB|/2 do Abort this coroutine
2822 RfnB->marked_size() > RfnB->size() / 2)
2823 {
2824 ABORT_THIS_COROUTINE();
2825 }
2826 /* 3.13r: end while */ mCRL2complexity(red_fromred_visited_begin->pred,
2827 add_work(check_complexity::while_FromRed_is_not_empty_3_6r, 1), );
2828 }
2829 END_COROUTINE_WHILE;
2830
2831 // The shared variable FromRed_is_empty is set to true as soon
2832 // as FromRed should be considered empty. (From that moment
2833 // on, no slow tests are needed any more.)
2834 FromRed_is_empty = true;
2835 } assert(FromRed_is_empty); assert(0 != RfnB->marked_size());
2836
2837 /* - - - - - - - - visit red states - - - - - - - - */
2838
2839 red_visited_begin = RfnB->marked_bottom_end();
2840 if (RfnB->marked_bottom_begin() == red_visited_begin)
2841 {
2842 // It may happen that all found states are non-bottom states.
2843 // (In that case, some of these states will become new bottom
2844 // states.)
2845 red_visited_begin = RfnB->marked_nonbottom_end();
2846 }
2847 // 3.15r: while Red contains unvisited states do
2848 COROUTINE_DO_WHILE(REFINE_RED_STATE_HANDLED,
2849 RfnB->marked_nonbottom_begin() != red_visited_begin)
2850 {
2851 // 3.17r (order of lines changed): Mark s as visited
2852 --red_visited_begin; assert(RfnB->marked_bottom_begin() <= red_visited_begin ||
2853 (RfnB->marked_nonbottom_begin() <= red_visited_begin &&
2854 RfnB->marked_nonbottom_end() > red_visited_begin));
2855 // 3.16r: Choose an unvisited s in Red
2856 red_s = *red_visited_begin;
2857 // 3.18r: for all s_prime in inert_in(s) do
2858 COROUTINE_FOR (REFINE_RED_PREDECESSOR_HANDLED,
2859 red_pred_iter = red_s->inert_pred_begin(),
2860 red_s->inert_pred_end() != red_pred_iter, ++red_pred_iter)
2861 {
2862 bisim_gjkw::state_info_ptr const s_prime =
2863 red_pred_iter->source;
2864 // 3.24r: Red := Red union {s_prime}
2865 if (s_prime->pos < notblue_initialised_end)
2866 {
2867 // The state has a transition to a blue state, so
2868 // notblue is initialised; however, now it is revealed
2869 // to be red anyway.
2870 bisim_gjkw::swap_permutation(s_prime->pos,
2871 --notblue_initialised_end);
2872 }
2873 if (RfnB->mark_nonbottom(s_prime) &&
2874 // 3.5r: whenever |Red| > |RfnB|/2 do Abort this coroutine
2875 RfnB->marked_size() > RfnB->size() / 2)
2876 {
2877 ABORT_THIS_COROUTINE();
2878 }
2879 /* 3.26r: end for */ mCRL2complexity(red_pred_iter,
2880 add_work(check_complexity::for_all_s_prime_in_pred_s_3_18r, 1), );
2881 }
2882 END_COROUTINE_FOR;
2883 /* 3.27r: end while */ mCRL2complexity(red_s, add_work(
2884 check_complexity::while_Red_contains_unvisited_states_3_15r, 1), );
2885 if (RfnB->marked_bottom_begin() == red_visited_begin)
2886 {
2887 red_visited_begin = RfnB->marked_nonbottom_end();
2888 }
2889 }
2890 END_COROUTINE_DO_WHILE;
2891
2892 /* - - - - - - - - split off red block - - - - - - - - */
2893
2894 // 3.28r: Abort the other coroutine
2895 ABORT_OTHER_COROUTINE();
2896 // All non-red states are blue.
2897 // 3.29r: Move Red to a new block RedB
2898 // and
2899 // 3.30r: Destroy all temporary data
2900 RedB = RfnB->split_off_red(RfnB->marked_nonbottom_begin());
2901 part_tr.new_red_block_created(RfnB, RedB, postprocessing);
2902 #ifndef NDEBUG
2903 unsigned const max_counter = check_complexity::log_n -
2904 check_complexity::ilog2(RedB->size());
2905 mCRL2complexity(RedB,
2906 add_work(check_complexity::for_all_s_in_NewB_3_31, max_counter), );
2907 #endif
2908 // 3.31r: for all non-bottom s in RedB do
2909 // we have to run through the states backwards because
2910 // otherwise, we might miss out some states.
2911 for (bisim_gjkw::permutation_iter_t s_iter = RedB->nonbottom_end();
2912 RedB->nonbottom_begin() != s_iter; )
2913 {
2914 --s_iter;
2915 red_s = *s_iter; // mCRL2complexity(s, ...) -- optimized to the above call.
2916 // 3.32r: for all s_prime in inert_out(s) \ RedB do
2917 for (bisim_gjkw::succ_iter_t
2918 succ_iter = red_s->inert_succ_begin();
2919 red_s->inert_succ_end()!=succ_iter; ++succ_iter)
2920 { mCRL2complexity(succ_iter->B_to_C->pred, add_work(
2921 check_complexity::for_all_s_prime_in_succ_s_3_32r, max_counter), );
2922 assert(part_tr.succ_end() > succ_iter);
2923 assert(succ_iter->B_to_C->pred->succ == succ_iter);
2924 if (bisim_gjkw::state_info_ptr const s_prime =
2925 succ_iter->target;
2926 s_prime->block == RedB)
2927 {
2928 continue;
2929 } else assert(s_prime->block == RfnB);
2930 // 3.33r: s --> s_prime is no longer inert
2931 part_tr.make_noninert(succ_iter);
2932 // 3.34r: end for
2933 }
2934 // 3.35r: if |inert_out(s)| == 0 then
2935 if (red_s->inert_succ_begin() == red_s->inert_succ_end())
2936 {
2937 // 3.36r: s is a new bottom state
2938 RedB->set_marked_nonbottom_begin(RedB->bottom_begin() - 1);
2939 RedB->set_bottom_begin(RedB->marked_nonbottom_begin());
2940 swap_permutation(red_s->pos, RedB->bottom_begin()); // assert("red_s has a transition to SpC");
2941 // 3.37r: end if
2942 }
2943 // 3.38r: end for
2944 } assert(RfnB->end() < red_end);
2945 ONLY_IF_DEBUG( red_is_smaller(RfnB, RedB); )
2946 END_COROUTINE
2947 END_COROUTINES_SECTION
2948
2949
2950 /* 3.41 P := partition P where NewB is added and the states in NewB are */ assert(RedB->end() == red_end);
2951 // removed from RfnB
2952 // done through adapting the data structures in the coroutines.
2953 // 3.42: return <RedB, BlueB> (with old and new bottom states separated)
2954 // The separation is indicated by marking the old bottom states.
2955 // Only RedB is returned explicitly, as most calls to Refine only use
2956 // RedB.
2957 return RedB;
2958}
2959
2960
2961
2962/*=============================================================================
2963= PostprocessNewBottom -- Algorithm 4 in [GJKW 2017] =
2964=============================================================================*/
2965
2966
2967
2973class constln_ptr_less
2974{
2975 public:
2976 bool operator() (const bisim_gjkw::constln_t* a,
2977 const bisim_gjkw::constln_t* b) const
2978 {
2979 return *a < *b;
2980 }
2981};
2982
2983
2984typedef std::set<bisim_gjkw::constln_t*, constln_ptr_less> R_map_t;
2985
2986
3003template <class LTS_TYPE>
3004bisim_gjkw::block_t* bisim_partitioner_gjkw<LTS_TYPE>::postprocess_new_bottom(
3005 bisim_gjkw::block_t* RedB
3006 /* , bisim_gjkw::block_t* BlueB */)
3007{ assert(0 != RedB->unmarked_bottom_size());
3008 assert(RedB->marked_nonbottom_begin() == RedB->marked_nonbottom_end());
3009 /*------- collect constellations reachable from new bottom states -------*/
3010
3011 // 4.3: <ResultB, RfnB> := Refine(RedB, cosplit(RedB, BlueB), {old bottom
3012 // states in RedB}, {})
3013 bisim_gjkw::block_t* ResultB;
3014 bisim_gjkw::block_t* RfnB;
3015 #ifndef NDEBUG
3016 bisim_gjkw::permutation_const_iter_t blue_begin = RedB->begin();
3017 #endif
3018 if (0 != RedB->marked_bottom_size())
3019 {
3020 // postprocessing == false is required here because we need to keep
3021 // ResultB->FromRed().
3022 ResultB = refine(RedB, nullptr, nullptr, false); assert(nullptr != ResultB); assert(0 == ResultB->unmarked_bottom_size());
3023 // 4.26: Destroy all temporary data
3024 // As part of this line, we unmark all states.
3025 ResultB->set_marked_bottom_begin(ResultB->bottom_end()); assert(ResultB->begin() > blue_begin);
3026 RfnB = ResultB->begin()[-1]->block;
3027 }
3028 else
3029 {
3030 RfnB = RedB;
3031 ResultB = nullptr;
3032 } assert(ResultB != RfnB); assert(RfnB->begin() == blue_begin);
3033 // do not refine a trivial block
3034 if (1 == RfnB->size())
3035 { assert(0 == RfnB->marked_size());
3036 return ResultB;
3037 }
3038 // 4.2: Create an empty search tree R of constellations
3039 R_map_t R;
3040Line_4_4:
3041 /* 4.4: for all constellations C not in R reachable from RfnB do */ assert(0 == RfnB->marked_bottom_size());
3042 while (!RfnB->to_constln.front().needs_postprocessing())
3043 {
3044 bisim_gjkw::B_to_C_desc_iter_t const new_slice =
3045 RfnB->to_constln.begin(); // try to assign the work to the transitions from bottom states in RfnB to C.
3046 #ifndef NDEBUG
3047 if (!new_slice->add_work_to_bottom_transns(check_complexity::
3048 for_all_transitions_from_bottom_states_a_priori_4_4, 1))
3049 {
3050 // It didn't work out -- now assign it temporarily to the
3051 // B_to_C slice itself.
3052 mCRL2complexity(new_slice, add_work(check_complexity::
3053 for_all_constellations_C_not_in_R_from_RfnB_4_4, 1), );
3054 }
3055 #endif
3056 bisim_gjkw::constln_t* const C = new_slice->to_constln();
3057 // 4.5: Add C to R
3058 if (!R.insert(C).second) //< complexity log(n)
3059 { assert(0 && "The constellation already was in R");
3060 }
3061 // 4.6: Register that the transitions from RfnB to C need
3062 /* postprocessing */ assert(C->postprocess_begin == C->postprocess_end);
3063 C->postprocess_begin = new_slice->begin;
3064 C->postprocess_end = new_slice->end; assert(C->postprocess_begin < C->postprocess_end);
3065 // move the set of transitions to the end of the list
3066 RfnB->to_constln.splice(RfnB->to_constln.end(), RfnB->to_constln,
3067 new_slice);
3068 // 4.7: end for
3069 }
3070 // 4.8: for all bottom states s in RfnB do
3071 bisim_gjkw::permutation_iter_t s_iter = RfnB->unmarked_bottom_begin();
3072 do
3073 {
3074 bisim_gjkw::state_info_ptr const s = *s_iter; mCRL2complexity(s,
3075 add_work(check_complexity::for_all_bottom_states_s_in_RfnB_4_8, 1), );
3076 // 4.9: Set the current constellation pointer of s to the first
3077 // constellation it can reach
3078 s->set_current_constln(s->succ_begin());
3079 // 4.10: end for
3080 }
3081 while (RfnB->unmarked_bottom_end() != ++s_iter);
3082
3083 /*--------------- stabilise w. r. t. found constellations ---------------*/
3084
3085 // 4.11: for all constellations SpC in R (in order) do
3086 while (!R.empty())
3087 { // the work has to be assigned to the transitions from (new) bottom
3088 bisim_gjkw::constln_t* const SpC = *R.begin(); // states to constellation SpC. We do that assignment in the inner
3089 // 4.12: for all blocks B with transitions to SpC that need // loop. Ensure that the inner loop is executed:
3090 /* postprocessing do */ assert(SpC->postprocess_begin != SpC->postprocess_end);
3091 do
3092 {
3093 // add_work is called indirectly: after refining, work is assigned
3094 // to every (new) bottom state in the refined block.
3095 bisim_gjkw::B_to_C_iter_t const B_iter = SpC->postprocess_begin; assert(part_tr.B_to_C_end() > B_iter);
3096 bisim_gjkw::block_t* const B = B_iter->pred->source->block; assert(B_iter->pred->succ->B_to_C == B_iter);
3097 bisim_gjkw::B_to_C_desc_iter_t FromRed = B_iter->B_to_C_slice; assert(FromRed->begin == B_iter);
3098 #ifndef NDEBUG
3099 bool postproc_a_posteriori = !FromRed->
3100 add_work_to_bottom_transns(check_complexity::
3101 for_all_transitions_that_need_postproc_a_priori_4_12, 1);
3102 #endif
3103 // 4.13: Delete the transitions from B to SpC from those that need
3104 // postprocessing
3105 SpC->postprocess_begin = FromRed->end; assert(SpC->postprocess_begin <= SpC->postprocess_end);
3106 assert(!B->to_constln.empty());
3107 if (B->to_constln.begin() != FromRed)
3108 { assert(FromRed->from_block() == B);
3109 B->to_constln.splice(B->to_constln.begin(), B->to_constln,
3110 FromRed);
3111 }
3112 /* do not refine a trivial block */ assert(0 == B->marked_size());
3113 if (1 == B->size())
3114 { assert(!postproc_a_posteriori);
3115 #ifndef NDEBUG
3116 if (0 != FromRed->work_counter.get_work_counter_4_4())
3117 {
3118 assert(FromRed->add_work_to_bottom_transns(check_complexity::
3119 for_all_transitions_from_bottom_states_a_posteriori_4_4, 1));
3120 FromRed->work_counter.reset_work_counter_4_4();
3121 }
3122 #endif
3123 continue;
3124 }
3125 // refine() may destroy FromRed: if the red subblock is smaller,
3126 // the transitions in FromRed are moved to a new B_to_C slice.
3127 // Therefore we select some transition from it, to restore the
3128 // slice afterwards. Any transition should do.
3129 #ifndef NDEBUG
3130 bisim_gjkw::pred_iter_t FromRed_save = FromRed->begin->pred;
3131 #endif
3132 // 4.14: <RedB, BlueB> := Refine(B, SpC, {}, {transitions to SpC})
3133 RedB = refine(B, SpC, &*FromRed, true);
3134 #ifndef NDEBUG
3135 FromRed = FromRed_save->succ->B_to_C->B_to_C_slice;
3136 if (postproc_a_posteriori && !FromRed->add_work_to_bottom_transns(
3137 check_complexity::
3138 for_all_transitions_that_need_postproc_a_posteriori_4_12, 1))
3139 {
3140 assert(0 && "no new bottom states to assign work to");
3141 }
3142 // try to move the work that was not yet moved to the
3143 // transitions from (new) bottom states now.
3144 if (0 != FromRed->work_counter.get_work_counter_4_4())
3145 {
3146 if (!FromRed->add_work_to_bottom_transns(check_complexity::
3147 for_all_transitions_from_bottom_states_a_posteriori_4_4, 1))
3148 {
3149 assert(0 && "no new bottom states to assign work to");
3150 }
3151 FromRed->work_counter.reset_work_counter_4_4();
3152 }
3153 #endif
3154 // 4.15: for all old bottom states s in RedB do
3155 for (bisim_gjkw::permutation_iter_t
3156 s_iter = RedB->marked_bottom_begin();
3157 RedB->marked_bottom_end() != s_iter; ++s_iter)
3158 {
3159 bisim_gjkw::state_info_ptr const s = *s_iter;
3160 // 4.16: Advance the current constellation pointer of s to the
3161 // next constellation it can reach
3162 if (s->current_constln() < s->succ_end() &&
3163 s->current_constln()->target->constln() == SpC)
3164 {
3165 #ifndef NDEBUG
3166 bisim_gjkw::succ_entry::slice_add_work_to_transns(s->current_constln(),
3167 check_complexity::for_all_old_bottom_states_s_in_RedB_4_15,1);
3168 #endif
3169 s->set_current_constln(bisim_gjkw::succ_entry::slice_end(
3170 s->current_constln()));
3171 } else
3172 { mCRL2complexity(s, add_work(check_complexity::
3173 for_all_old_bottom_states_s_in_RedB_selfloop_4_15, 1), );
3174 assert(B == RedB /* we should test: BlueB is empty */);
3175 assert(B->constln() == SpC);
3176 }
3177 assert(s->succ_end() == s->current_constln() ||
3178 /* 4.17: end for */ *SpC < *s->current_constln()->target->constln());
3179 }
3180 /* 4.18: if RedB contains new bottom states then */ assert(RedB->marked_nonbottom_begin() == RedB->marked_nonbottom_end());
3181 if (0 != RedB->unmarked_bottom_size())
3182 {
3183 // 4.19: <_, RfnB> := Refine(RedB, cosplit(RedB, BlueB), {old
3184 // bottom states in RedB}, {})
3185 #ifndef NDEBUG
3186 blue_begin = RedB->begin();
3187 #endif
3188 if (0 != RedB->marked_bottom_size())
3189 {
3190 RedB = refine(RedB, nullptr, nullptr, true); assert(nullptr != RedB); assert(0 == RedB->unmarked_bottom_size());
3191 // 4.26: Destroy all temporary data
3192 // As part of this line, we unmark all states.
3193 RedB->set_marked_bottom_begin(RedB->bottom_end()); assert(RedB->begin() > blue_begin);
3194 RfnB = RedB->begin()[-1]->block;
3195 }
3196 else
3197 {
3198 RfnB = RedB;
3199 #ifndef NDEBUG
3200 RedB = nullptr;
3201 #endif
3202 } assert(RedB != RfnB);
3203 assert(RfnB->begin() == blue_begin);
3204 // do not refine a trivial block
3205 if (1 == RfnB->size())
3206 { assert(0 == RfnB->marked_size());
3207 continue;
3208 }
3209 // 4.20: Register that the transitions from RfnB to SpC need
3210 // postprocessing
3211 bisim_gjkw::B_to_C_desc_iter_t new_slice =
3212 SpC->postprocess_begin[-1].B_to_C_slice; assert(new_slice->from_block() == RfnB);
3213 assert(new_slice->to_constln() == SpC);
3214 SpC->postprocess_begin = new_slice->begin; assert(new_slice->end <= SpC->postprocess_end);
3215 // move the set of transitions to the end of the list
3216 RfnB->to_constln.splice(RfnB->to_constln.end(),
3217 RfnB->to_constln, new_slice);
3218 // 4.21: Restart the procedure (but keep R),
3219 // i. e. go to Line 4.4
3220 goto Line_4_4;
3221 // 4.22: end if
3222 }
3223 // 4.26: Destroy all temporary data
3224 // As part of this line, we unmark all states.
3225 RedB->set_marked_bottom_begin(RedB->bottom_end());
3226 // 4.23: end for
3227 }
3228 while (SpC->postprocess_begin != SpC->postprocess_end);
3229 // 4.24: Delete SpC from R
3230 R.erase(R.begin());
3231 // 4.25: end for
3232 }
3233 /* 4.26: Destroy all temporary data */ assert(R.empty());
3234
3235 return ResultB;
3236}
3237
3238
3239
3240/*=============================================================================
3241= explicit instantiation requests =
3242=============================================================================*/
3243
3244
3245
3246namespace bisim_gjkw
3247{
3248
3249template class bisim_partitioner_gjkw_initialise_helper<lts_lts_t>;
3250template class bisim_partitioner_gjkw_initialise_helper<lts_aut_t>;
3251template class bisim_partitioner_gjkw_initialise_helper<lts_fsm_t>;
3252
3253} // end namespace bisim_gjkw
3254
3255template class bisim_partitioner_gjkw<lts_lts_t>;
3256template class bisim_partitioner_gjkw<lts_aut_t>;
3257template class bisim_partitioner_gjkw<lts_fsm_t>;
3258
3259} // end namespace detail
3260} // end namespace lts
3261} // end namespace mcrl2
STATE_TYPE_MAX
#define STATE_TYPE_MAX
Definition check_complexity.h:99
mCRL2complexity
#define mCRL2complexity(unit, call, info_for_debug)
Assigns work to a counter and checks for errors.
Definition check_complexity.h:1634
mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor
Definition liblts_bisim_gjkw.h:1334
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::KeyHasher
Definition liblts_bisim_gjkw.h:1683
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::Key
Definition liblts_bisim_gjkw.h:1666
mcrl2::lts::detail::bisim_gjkw::block_t
stores information about a block
Definition liblts_bisim_gjkw.h:404
mcrl2::lts::detail::bisim_gjkw::constln_t
stores information about a constellation
Definition liblts_bisim_gjkw.h:812
mcrl2::lts::detail::bisim_gjkw::fixed_vector
Definition fixed_vector.h:41
mcrl2::lts::detail::bisim_gjkw::part_state_t
refinable partition data structure
Definition liblts_bisim_gjkw.h:1016
mcrl2::lts::detail::bisim_gjkw::part_trans_t
Definition liblts_bisim_gjkw.h:1438
mcrl2::lts::detail::bisim_gjkw::state_info_entry
stores information about a single state
Definition liblts_bisim_gjkw.h:164
mcrl2::lts::detail::bisim_partitioner_gjkw
implements the main algorithm for the stutter equivalence quotient
Definition liblts_bisim_gjkw.h:1742
mcrl2::lts::detail::check_complexity
class for time complexity checks
Definition check_complexity.h:123
mcrl2::lts::detail::check_complexity::ilog2
static int ilog2(state_type size)
calculate the base-2 logarithm, rounded down
Definition check_complexity.h:446
mcrl2::lts::detail::check_complexity::log_n
static unsigned char log_n
value of floor(log2(n)) for easy access
Definition check_complexity.h:441
mcrl2::lts::detail::check_complexity::refine_incoming_transition_3_18
@ refine_incoming_transition_3_18
Definition check_complexity.h:230
mcrl2::lts::detail::check_complexity::refine_outgoing_transition_to_marked_state_3_6l
@ refine_outgoing_transition_to_marked_state_3_6l
Definition check_complexity.h:218
mcrl2::lts::detail::check_complexity::refine_visited_state_3_15
@ refine_visited_state_3_15
Definition check_complexity.h:164
mcrl2::lts::detail::check_complexity::if___s_prime_has_transition_to_SpC_3_23l
@ if___s_prime_has_transition_to_SpC_3_23l
Definition check_complexity.h:251
mcrl2::lts::detail::check_complexity::refine_outgoing_transition_postprocess_new_bottom_3_6l
@ refine_outgoing_transition_postprocess_new_bottom_3_6l
Definition check_complexity.h:261
mcrl2::lts::detail::check_complexity::refine_outgoing_transition_3_6_or_23l
@ refine_outgoing_transition_3_6_or_23l
Definition check_complexity.h:223
mcrl2::lts::detail::check_complexity::refine_bottom_state_3_6l
@ refine_bottom_state_3_6l
Definition check_complexity.h:163
mcrl2::lts::detail::check_complexity::while_FromRed_is_not_empty_3_6r
@ while_FromRed_is_not_empty_3_6r
Definition check_complexity.h:254
mcrl2::lts::detail::check_complexity::check_temporary_work
static void check_temporary_work()
check that not too much superfluous work has been done
Definition check_complexity.h:492
mcrl2::lts::detail::check_complexity::init
static void init(state_type n)
starts counting for a new refinement run
Definition check_complexity.h:1610
mcrl2::lts::detail::constln_ptr_less
function object to compare two constln_t pointers based on their contents
Definition liblts_bisim_gjkw.cpp:2974
mcrl2::lts::detail::constln_ptr_less::operator()
bool operator()(const bisim_gjkw::constln_t *a, const bisim_gjkw::constln_t *b) const
Definition liblts_bisim_gjkw.cpp:2976
mcrl2::lts::transition
A class containing triples, source label and target representing transitions.
Definition transition.h:47
coroutine.h
helper macros for coroutines
ABORT_THIS_COROUTINE
#define ABORT_THIS_COROUTINE()
indicates that this coroutine gives up control to the other one
Definition coroutine.h:363
END_COROUTINE
#define END_COROUTINE
Ends the definition of code for a coroutine.
Definition coroutine.h:200
ABORT_OTHER_COROUTINE
#define ABORT_OTHER_COROUTINE()
indicates that the other coroutine should give up control
Definition coroutine.h:378
COROUTINE_FOR
#define COROUTINE_FOR(location, init, condition, update)
a for loop where every iteration incurs one unit of work
Definition coroutine.h:271
COROUTINE_WHILE
#define COROUTINE_WHILE(location, condition)
a while loop where every iteration incurs one unit of work
Definition coroutine.h:227
COROUTINES_SECTION
#define COROUTINES_SECTION
begin a section with two coroutines
Definition coroutine.h:142
COROUTINE_DO_WHILE
#define COROUTINE_DO_WHILE(location, condition)
a do { } while loop where every iteration incurs one unit of work
Definition coroutine.h:314
END_COROUTINES_SECTION
#define END_COROUTINES_SECTION
Close a section containing coroutines.
Definition coroutine.h:208
COROUTINE
#define COROUTINE
Define the code for a coroutine.
Definition coroutine.h:192
END_COROUTINE_WHILE
#define END_COROUTINE_WHILE
ends a loop started with COROUTINE_WHILE
Definition coroutine.h:252
END_COROUTINE_FOR
#define END_COROUTINE_FOR
ends a loop started with COROUTINE_FOR
Definition coroutine.h:297
COROUTINE_LABELS
#define COROUTINE_LABELS(locations)
Declare the interrupt locations for the coroutines.
Definition coroutine.h:161
END_COROUTINE_DO_WHILE
#define END_COROUTINE_DO_WHILE
ends a loop started with COROUTINE_DO_WHILE
Definition coroutine.h:336
TERMINATE_COROUTINE_SUCCESSFULLY
#define TERMINATE_COROUTINE_SUCCESSFULLY()
terminate the pair of coroutines successfully
Definition coroutine.h:348
mcrl2::lts::detail::bisim_gjkw::part_trans_t::B_to_C
fixed_vector< B_to_C_entry > B_to_C
Definition liblts_bisim_gjkw.h:1442
mcrl2::lts::detail::bisim_gjkw::part_state_t::permutation
permutation_t permutation
permutation array
Definition liblts_bisim_gjkw.h:1023
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::nr_of_states
state_type nr_of_states
Definition liblts_bisim_gjkw.h:1659
mcrl2::lts::detail::bisim_gjkw::part_trans_t::change_to_C
succ_iter_t change_to_C(pred_iter_t pred_iter, ONLY_IF_DEBUG(constln_t *SpC, constln_t *NewC,) bool first_transition_of_state, bool first_transition_of_block)
transition target is moved to a new constellation
Definition liblts_bisim_gjkw.cpp:474
mcrl2::lts::detail::bisim_gjkw::block_t::end
permutation_const_iter_t end() const
iterator past the last state in the block
Definition liblts_bisim_gjkw.h:600
mcrl2::lts::detail::bisim_gjkw::block_t::set_inert_begin
void set_inert_begin(B_to_C_iter_t new_inert_begin)
Definition liblts_bisim_gjkw.h:717
mcrl2::lts::detail::bisim_gjkw::part_trans_t::assert_stability
void assert_stability(const part_state_t &part_st) const
assert that the data structure is consistent and stable
Definition liblts_bisim_gjkw.cpp:1019
mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::to_constln
const constln_t * to_constln() const
compute the goal constellation of the transitions in this slice
Definition liblts_bisim_gjkw.h:1354
mcrl2::lts::detail::bisim_gjkw::block_t::nr_of_blocks
static state_type nr_of_blocks
total number of blocks with unique sequence number allocated
Definition liblts_bisim_gjkw.h:464
mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_bottom_size
state_type unmarked_bottom_size() const
provides the number of unmarked bottom states in the block
Definition liblts_bisim_gjkw.h:558
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::replace_transition_system
void replace_transition_system(const part_state_t &part_st, ONLY_IF_DEBUG(bool branching,) bool preserve_divergence)
Replaces the transition relation of the current LTS by the transitions of the bisimulation-reduced tr...
Definition liblts_bisim_gjkw.cpp:1714
mcrl2::lts::detail::bisim_gjkw::part_trans_t::split_s_inert_out
bool split_s_inert_out(state_info_ptr s ONLY_IF_DEBUG(, constln_t *OldC))
Split outgoing transitions of a state in the splitter.
Definition liblts_bisim_gjkw.cpp:555
mcrl2::lts::detail::bisim_gjkw::block_t::set_marked_bottom_begin
void set_marked_bottom_begin(permutation_iter_t new_marked_bottom_begin)
Definition liblts_bisim_gjkw.h:703
mcrl2::lts::detail::bisim_gjkw::block_t::SetFromRed
void SetFromRed(B_to_C_desc_iter_t new_fromred)
set FromRed to an existing element in to_constln
Definition liblts_bisim_gjkw.h:2001
mcrl2::lts::detail::bisim_gjkw::constln_t::make_nontrivial
void make_nontrivial()
makes a constellation non-trivial (i. e. inserts it into the respective list)
Definition liblts_bisim_gjkw.h:897
mcrl2::lts::detail::bisim_gjkw::block_t::nonbottom_begin
permutation_const_iter_t nonbottom_begin() const
iterator to the first non-bottom state in the block
Definition liblts_bisim_gjkw.h:608
mcrl2::lts::detail::bisim_gjkw::part_trans_t::B_to_C_begin
B_to_C_const_iter_t B_to_C_begin() const
Definition liblts_bisim_gjkw.h:1606
mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_pred_end
pred_const_iter_t inert_pred_end() const
iterator one past the last inert incoming transition
Definition liblts_bisim_gjkw.h:264
mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::from_block
const block_t * from_block() const
compute the source block of the transitions in this slice
Definition liblts_bisim_gjkw.h:1344
mcrl2::lts::detail::bisim_gjkw::constln_t::split_off_small_block
block_t * split_off_small_block()
split off a single block from the constellation
Definition liblts_bisim_gjkw.h:958
mcrl2::lts::detail::bisim_gjkw::constln_t::postprocess_begin
B_to_C_iter_t postprocess_begin
iterator to the first transition into this constellation that needs postprocessing
Definition liblts_bisim_gjkw.h:841
mcrl2::lts::detail::bisim_gjkw::part_trans_t::B_to_C_end
B_to_C_iter_t B_to_C_end()
Definition liblts_bisim_gjkw.h:1607
mcrl2::lts::detail::bisim_gjkw::state_info_entry::constln
const constln_t * constln() const
get constellation where the state belongs
Definition liblts_bisim_gjkw.h:1968
mcrl2::lts::detail::bisim_gjkw::block_t::begin
permutation_const_iter_t begin() const
iterator to the first state in the block
Definition liblts_bisim_gjkw.h:592
mcrl2::lts::detail::bisim_gjkw::part_trans_t::swap_B_to_C
void swap_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2)
Definition liblts_bisim_gjkw.h:1482
mcrl2::lts::detail::bisim_gjkw::state_info_entry::surely_has_no_transition_to
bool surely_has_no_transition_to(const constln_t *SpC) const
mcrl2::lts::detail::bisim_gjkw::block_t::set_begin
void set_begin(permutation_iter_t new_begin)
Definition liblts_bisim_gjkw.h:594
mcrl2::lts::detail::bisim_gjkw::block_t::marked_nonbottom_begin
permutation_const_iter_t marked_nonbottom_begin() const
iterator to the first marked non-bottom state in the block
Definition liblts_bisim_gjkw.h:656
mcrl2::lts::detail::bisim_gjkw::state_info_entry::pos
permutation_iter_t pos
position of the state in the permutation array
Definition liblts_bisim_gjkw.h:189
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::aut
LTS_TYPE & aut
Definition liblts_bisim_gjkw.h:1658
mcrl2::lts::detail::bisim_gjkw::constln_t::nontrivial_first
static constln_t * nontrivial_first
first constellation in the list of non-trivial constellations
Definition liblts_bisim_gjkw.h:828
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::action_block_map
std::unordered_map< label_type, state_type > action_block_map
Definition liblts_bisim_gjkw.h:1697
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::nr_of_transitions
trans_type nr_of_transitions
Definition liblts_bisim_gjkw.h:1661
mcrl2::lts::detail::bisim_gjkw::constln_t::end
permutation_const_iter_t end() const
constant iterator past the last state in the constellation
Definition liblts_bisim_gjkw.h:927
mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_bottom_begin
permutation_const_iter_t unmarked_bottom_begin() const
iterator to the first unmarked bottom state in the block
Definition liblts_bisim_gjkw.h:679
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::inert_out_per_state
std::vector< state_type > inert_out_per_state
Definition liblts_bisim_gjkw.h:1699
mcrl2::lts::detail::bisim_gjkw::part_trans_t::pred
fixed_vector< pred_entry > pred
Definition liblts_bisim_gjkw.h:1440
mcrl2::lts::detail::bisim_gjkw::block_t::set_inert_begin_and_end
void set_inert_begin_and_end(B_to_C_iter_t new_inert_begin, B_to_C_iter_t new_inert_end)
Definition liblts_bisim_gjkw.h:729
mcrl2::lts::detail::bisim_gjkw::block_t::inert_begin
B_to_C_const_iter_t inert_begin() const
iterator to the first inert transition of the block
Definition liblts_bisim_gjkw.h:715
mcrl2::lts::detail::bisim_gjkw::block_t::make_nonrefinable
void make_nonrefinable()
makes a block non-refinable (i. e. removes it from the respective list)
Definition liblts_bisim_gjkw.h:532
mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_begin
permutation_const_iter_t marked_bottom_begin() const
iterator to the first marked bottom state in the block
Definition liblts_bisim_gjkw.h:698
mcrl2::lts::detail::bisim_gjkw::state_info_entry::noninert_pred_begin
pred_const_iter_t noninert_pred_begin() const
iterator to first non-inert incoming transition
Definition liblts_bisim_gjkw.h:247
mcrl2::lts::detail::bisim_gjkw::block_t::mark_nonbottom
bool mark_nonbottom(state_info_ptr s)
mark a non-bottom state
Definition liblts_bisim_gjkw.h:741
mcrl2::lts::detail::bisim_gjkw::block_t::bottom_begin
permutation_const_iter_t bottom_begin() const
iterator to the first bottom state in the block
Definition liblts_bisim_gjkw.h:622
mcrl2::lts::detail::bisim_gjkw::part_trans_t::swap_out
void swap_out(pred_iter_t const pos1, pred_iter_t const pos2)
Definition liblts_bisim_gjkw.h:1461
mcrl2::lts::detail::bisim_gjkw::block_t::size
state_type size() const
provides the number of states in the block
Definition liblts_bisim_gjkw.h:539
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::init_transitions
void init_transitions(part_state_t &part_st, part_trans_t &part_tr, bool branching, bool preserve_divergence)
initialise the state in part_st and the transitions in part_tr
Definition liblts_bisim_gjkw.cpp:1502
mcrl2::lts::detail::bisim_gjkw::block_t::split_off_blue
block_t * split_off_blue(permutation_iter_t blue_nonbottom_end)
refine the block (the blue subblock is smaller)
Definition liblts_bisim_gjkw.cpp:70
mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::end
B_to_C_iter_t end
Definition liblts_bisim_gjkw.h:1336
mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_end
permutation_const_iter_t marked_bottom_end() const
iterator past the last marked bottom state in the block
Definition liblts_bisim_gjkw.h:711
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::inert_out_per_block
std::vector< state_type > inert_out_per_block
Definition liblts_bisim_gjkw.h:1701
mcrl2::lts::detail::bisim_gjkw::state_info_entry::notblue
state_type notblue
number of inert transitions to non-blue states
Definition liblts_bisim_gjkw.h:192
mcrl2::lts::detail::bisim_gjkw::block_t::marked_nonbottom_end
permutation_const_iter_t marked_nonbottom_end() const
iterator one past the last marked non-bottom state in the block
Definition liblts_bisim_gjkw.h:672
mcrl2::lts::detail::bisim_gjkw::constln_t::sort_key
const state_type sort_key
sort key to order constellation-related information
Definition liblts_bisim_gjkw.h:853
mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_size
state_type marked_bottom_size() const
provides the number of marked bottom states in the block
Definition liblts_bisim_gjkw.h:543
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::states_per_block
std::vector< state_type > states_per_block
Definition liblts_bisim_gjkw.h:1702
mcrl2::lts::detail::bisim_gjkw::block_t::seqnr
state_type seqnr() const
Definition liblts_bisim_gjkw.h:505
mcrl2::lts::detail::bisim_gjkw::constln_t::is_trivial
bool is_trivial() const
returns true iff the constellation is trivial
Definition liblts_bisim_gjkw.h:911
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::nr_of_nonbottom_states
state_type nr_of_nonbottom_states
Definition liblts_bisim_gjkw.h:1703
mcrl2::lts::detail::bisim_gjkw::block_t::to_constln
B_to_C_desc_list to_constln
list of B_to_C with transitions from this block
Definition liblts_bisim_gjkw.h:437
mcrl2::lts::detail::bisim_gjkw::succ_entry::slice_end
static succ_iter_t slice_end(succ_iter_t this_)
Definition liblts_bisim_gjkw.h:1245
mcrl2::lts::detail::bisim_gjkw::state_info_entry::block
block_t * block
block where the state belongs
Definition liblts_bisim_gjkw.h:186
mcrl2::lts::detail::bisim_gjkw::constln_t::get_nontrivial_next
const constln_t * get_nontrivial_next() const
provides the next non-trivial constellation
Definition liblts_bisim_gjkw.h:883
mcrl2::lts::detail::bisim_gjkw::block_t::set_marked_nonbottom_begin
void set_marked_nonbottom_begin(permutation_iter_t new_marked_nonbottom_begin)
Definition liblts_bisim_gjkw.h:664
BLOCK_NO_SEQNR
#define BLOCK_NO_SEQNR
Definition liblts_bisim_gjkw.h:458
mcrl2::lts::detail::bisim_gjkw::block_t::perm_begin
static permutation_const_iter_t perm_begin
Definition liblts_bisim_gjkw.h:799
mcrl2::lts::detail::bisim_gjkw::block_t::make_refinable
bool make_refinable()
makes a block refinable (i. e. inserts it into the respective list)
Definition liblts_bisim_gjkw.h:517
mcrl2::lts::detail::bisim_gjkw::part_state_t::state_info
fixed_vector< state_info_entry > state_info
array with all other information about states
Definition liblts_bisim_gjkw.h:1030
mcrl2::lts::detail::bisim_gjkw::part_state_t::state_size
state_type state_size() const
provide size of state space
Definition liblts_bisim_gjkw.h:1099
mcrl2::lts::detail::bisim_gjkw::constln_t::size
state_type size() const
returns number of states in the constellation
Definition liblts_bisim_gjkw.h:937
mcrl2::lts::detail::bisim_gjkw::block_t::inert_end
B_to_C_const_iter_t inert_end() const
iterator past the last inert transition of the block
Definition liblts_bisim_gjkw.h:723
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::Key::second
state_type second
Definition liblts_bisim_gjkw.h:1669
mcrl2::lts::detail::bisim_gjkw::block_t::constln
const constln_t * constln() const
constellation where the block belongs to
Definition liblts_bisim_gjkw.h:575
mcrl2::lts::detail::bisim_gjkw::block_t::bottom_end
permutation_const_iter_t bottom_end() const
iterator past the last bottom state in the block
Definition liblts_bisim_gjkw.h:632
mcrl2::lts::detail::bisim_gjkw::block_t::refinable_first
static block_t * refinable_first
first block in the list of refinable blocks
Definition liblts_bisim_gjkw.h:449
mcrl2::lts::detail::bisim_gjkw::state_info_entry::succ_begin
succ_const_iter_t succ_begin() const
iterator to first outgoing transition
Definition liblts_bisim_gjkw.h:268
mcrl2::lts::detail::bisim_gjkw::state_info_entry::current_constln
succ_const_iter_t current_constln() const
Definition liblts_bisim_gjkw.h:201
mcrl2::lts::detail::bisim_gjkw::part_trans_t::new_red_block_created
void new_red_block_created(block_t *OldB, block_t *NewB, bool postprocessing)
handle B_to_C slices after a new red block has been created
Definition liblts_bisim_gjkw.cpp:837
mcrl2::lts::detail::bisim_gjkw::block_t::set_end
void set_end(permutation_iter_t new_end)
Definition liblts_bisim_gjkw.h:602
mcrl2::lts::detail::bisim_gjkw::part_state_t::print_trans
void print_trans() const
print all transitions
Definition liblts_bisim_gjkw.cpp:309
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::inert_in_per_state
std::vector< state_type > inert_in_per_state
Definition liblts_bisim_gjkw.h:1700
mcrl2::lts::detail::bisim_gjkw::block_t::is_refinable
bool is_refinable() const
checks whether the block is refinable
Definition liblts_bisim_gjkw.h:512
mcrl2::lts::detail::bisim_gjkw::block_t::split_off_red
block_t * split_off_red(permutation_iter_t red_nonbottom_begin)
refine the block (the red subblock is smaller)
Definition liblts_bisim_gjkw.cpp:149
mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_succ_begin
succ_const_iter_t inert_succ_begin() const
iterator to first inert outgoing transition
Definition liblts_bisim_gjkw.h:290
mcrl2::lts::detail::bisim_gjkw::constln_t::begin
permutation_const_iter_t begin() const
constant iterator to the first state in the constellation
Definition liblts_bisim_gjkw.h:917
mcrl2::lts::detail::bisim_gjkw::block_t::assign_seqnr
void assign_seqnr()
assigns a unique sequence number
Definition liblts_bisim_gjkw.h:500
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::extra_kripke_states
std::unordered_map< Key, state_type, KeyHasher > extra_kripke_states
Definition liblts_bisim_gjkw.h:1693
mcrl2::lts::detail::bisim_gjkw::part_trans_t::new_blue_block_created
void new_blue_block_created(block_t *OldB, block_t *NewB)
handle B_to_C slices after a new blue block has been created
Definition liblts_bisim_gjkw.cpp:666
mcrl2::lts::detail::bisim_gjkw::state_info_entry::s_i_begin
static state_info_const_ptr s_i_begin
pointer at the first entry in the state_info array
Definition liblts_bisim_gjkw.h:352
mcrl2::lts::detail::bisim_gjkw::constln_t::get_some_nontrivial
static constln_t * get_some_nontrivial()
provides an arbitrary non-trivial constellation
Definition liblts_bisim_gjkw.h:875
mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_bottom_end
permutation_const_iter_t unmarked_bottom_end() const
iterator past the last unmarked bottom state in the block
Definition liblts_bisim_gjkw.h:686
mcrl2::lts::detail::bisim_gjkw::block_t::set_bottom_begin
void set_bottom_begin(permutation_iter_t new_bottom_begin)
Definition liblts_bisim_gjkw.h:624
mcrl2::lts::detail::bisim_gjkw::state_info_entry::set_inert_succ_begin_and_end
void set_inert_succ_begin_and_end(succ_iter_t new_inert_out_begin, succ_iter_t new_inert_out_end)
Definition liblts_bisim_gjkw.h:312
mcrl2::lts::detail::bisim_gjkw::part_trans_t::swap3_B_to_C
void swap3_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2, succ_iter_t const pos3)
Definition liblts_bisim_gjkw.h:1497
mcrl2::lts::detail::bisim_gjkw::part_state_t::block
const block_t * block(state_type s) const
find block of a state
Definition liblts_bisim_gjkw.h:1104
mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_succ_end
succ_const_iter_t inert_succ_end() const
iterator past the last inert outgoing transition
Definition liblts_bisim_gjkw.h:309
mcrl2::lts::detail::bisim_gjkw::block_t::work_counter
check_complexity::block_counter_t work_counter
Definition liblts_bisim_gjkw.h:797
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::noninert_in_per_state
std::vector< state_type > noninert_in_per_state
Definition liblts_bisim_gjkw.h:1700
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::bisim_partitioner_gjkw_initialise_helper
bisim_partitioner_gjkw_initialise_helper(LTS_TYPE &l, bool branching, bool preserve_divergence)
constructor of the helper class
Definition liblts_bisim_gjkw.cpp:1416
mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_pred_begin
pred_const_iter_t inert_pred_begin() const
iterator to first inert incoming transition
Definition liblts_bisim_gjkw.h:255
mcrl2::lts::detail::bisim_gjkw::state_info_entry::noninert_pred_end
pred_const_iter_t noninert_pred_end() const
iterator past the last non-inert incoming transition
Definition liblts_bisim_gjkw.h:251
mcrl2::lts::detail::bisim_gjkw::block_t::set_inert_end
void set_inert_end(B_to_C_iter_t new_inert_end)
Definition liblts_bisim_gjkw.h:725
mcrl2::lts::detail::bisim_gjkw::state_info_entry::pred_end
pred_const_iter_t pred_end() const
iterator past the last incoming transition
Definition liblts_bisim_gjkw.h:233
mcrl2::lts::detail::bisim_gjkw::part_trans_t::succ
fixed_vector< succ_entry > succ
Definition liblts_bisim_gjkw.h:1441
mcrl2::lts::detail::bisim_gjkw::state_info_entry::s_i_end
static state_info_const_ptr s_i_end
pointer past the last actual entry in the state_info array
Definition liblts_bisim_gjkw.h:359
mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_nonbottom_begin
permutation_const_iter_t unmarked_nonbottom_begin() const
iterator to the first unmarked non-bottom state in the block
Definition liblts_bisim_gjkw.h:636
mcrl2::lts::detail::bisim_gjkw::block_t::nonbottom_end
permutation_const_iter_t nonbottom_end() const
iterator past the last non-bottom state in the block
Definition liblts_bisim_gjkw.h:612
mcrl2::lts::detail::bisim_gjkw::state_info_entry::succ_end
succ_const_iter_t succ_end() const
iterator past the last outgoing transition
Definition liblts_bisim_gjkw.h:276
mcrl2::lts::detail::bisim_gjkw::block_t::FromRed
B_to_C_descriptor * FromRed(const constln_t *SpC)
read FromRed
Definition liblts_bisim_gjkw.h:1979
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::noninert_out_per_block
std::vector< state_type > noninert_out_per_block
Definition liblts_bisim_gjkw.h:1701
mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_nonbottom_end
permutation_const_iter_t unmarked_nonbottom_end() const
iterator past the last unmarked non-bottom state in the block
Definition liblts_bisim_gjkw.h:640
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::Key::first
label_type first
Definition liblts_bisim_gjkw.h:1668
mcrl2::lts::detail::bisim_gjkw::part_state_t::print_block
void print_block(const char *message, const block_t *B, permutation_const_iter_t begin, permutation_const_iter_t end) const
print a slice of the partition (typically a block)
Definition liblts_bisim_gjkw.cpp:221
mcrl2::lts::detail::bisim_gjkw::block_t::marked_size
state_type marked_size() const
provides the number of marked states in the block
Definition liblts_bisim_gjkw.h:551
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper::noninert_out_per_state
std::vector< state_type > noninert_out_per_state
Definition liblts_bisim_gjkw.h:1699
mcrl2::lts::detail::bisim_gjkw::part_trans_t::trans_size
trans_type trans_size() const
Definition liblts_bisim_gjkw.h:1536
mcrl2::lts::detail::bisim_gjkw::constln_t::postprocess_end
B_to_C_iter_t postprocess_end
iterator past the last transition into this constellation that needs postprocessing
Definition liblts_bisim_gjkw.h:845
mcrl2::lts::detail::bisim_gjkw::part_state_t::print_part
void print_part(const part_trans_t &part_tr) const
print the partition as a tree (per constellation and block)
Definition liblts_bisim_gjkw.cpp:255
mcrl2::lts::detail::bisim_gjkw::state_info_entry::set_current_constln
void set_current_constln(succ_iter_t const new_current_constln)
Definition liblts_bisim_gjkw.h:203
mcrl2::lts::detail::bisim_gjkw::block_t::mark
bool mark(state_info_ptr s)
mark a state
Definition liblts_bisim_gjkw.h:755
mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::begin
B_to_C_iter_t begin
Definition liblts_bisim_gjkw.h:1336
mcrl2::lts::detail::bisim_gjkw::state_info_entry::pred_begin
pred_const_iter_t pred_begin() const
iterator to first incoming transition
Definition liblts_bisim_gjkw.h:225
mcrl2::lts::detail::bisim_gjkw::state_info_entry::surely_has_transition_to
bool surely_has_transition_to(const constln_t *SpC) const
ONLY_IF_DEBUG
#define ONLY_IF_DEBUG(...)
include something in Debug mode
Definition liblts_bisim_dnj.h:134
liblts_bisim_gjkw.h
O(m log n)-time stuttering equivalence algorithm.
mCRL2log
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
lts_aut.h
This file contains a class that contains labelled transition systems in aut format.
lts_fsm.h
This file contains a class that contains labelled transition systems in fsm format.
lts_utilities.h
This file contains some utility functions to manipulate lts's.
mcrl2::log::verbose
@ verbose
Definition logger.h:37
mcrl2::lts::detail::bisim_gjkw::state_info_const_ptr
const state_info_entry * state_info_const_ptr
Definition liblts_bisim_gjkw.h:119
mcrl2::lts::detail::bisim_gjkw::pred_iter_t
fixed_vector< pred_entry >::iterator pred_iter_t
Definition liblts_bisim_gjkw.h:141
mcrl2::lts::detail::bisim_gjkw::succ_const_iter_t
fixed_vector< succ_entry >::const_iterator succ_const_iter_t
Definition liblts_bisim_gjkw.h:146
mcrl2::lts::detail::bisim_gjkw::red_is_smaller
static void red_is_smaller(block_t *BlueB, block_t *RedB)
moves temporary counters to normal ones if the red block is smaller
Definition liblts_bisim_gjkw.cpp:2229
mcrl2::lts::detail::bisim_gjkw::permutation_iter_t
permutation_t::iterator permutation_iter_t
Definition liblts_bisim_gjkw.h:131
mcrl2::lts::detail::bisim_gjkw::pred_const_iter_t
fixed_vector< pred_entry >::const_iterator pred_const_iter_t
Definition liblts_bisim_gjkw.h:145
mcrl2::lts::detail::bisim_gjkw::permutation_const_iter_t
permutation_t::const_iterator permutation_const_iter_t
Definition liblts_bisim_gjkw.h:132
mcrl2::lts::detail::bisim_gjkw::B_to_C_desc_const_iter_t
B_to_C_desc_list::const_iterator B_to_C_desc_const_iter_t
Definition liblts_bisim_gjkw.h:150
mcrl2::lts::detail::bisim_gjkw::B_to_C_desc_iter_t
B_to_C_desc_list::iterator B_to_C_desc_iter_t
Definition liblts_bisim_gjkw.h:149
mcrl2::lts::detail::bisim_gjkw::B_to_C_iter_t
fixed_vector< B_to_C_entry >::iterator B_to_C_iter_t
Definition liblts_bisim_gjkw.h:140
mcrl2::lts::detail::bisim_gjkw::blue_is_smaller
static void blue_is_smaller(block_t *BlueB, block_t *RedB, const constln_t *NewC)
moves temporary counters to normal ones if the blue block is smaller
Definition liblts_bisim_gjkw.cpp:2135
mcrl2::lts::detail::bisim_gjkw::succ_iter_t
fixed_vector< succ_entry >::iterator succ_iter_t
Definition liblts_bisim_gjkw.h:142
mcrl2::lts::detail::state_type
std::size_t state_type
type used to store state (numbers and) counts
Definition check_complexity.h:97
mcrl2::lts::detail::R_map_t
std::set< bisim_gjkw::constln_t *, constln_ptr_less > R_map_t
Definition liblts_bisim_gjkw.cpp:2984
mcrl2::lts::detail::label_type
std::size_t label_type
type used to store label numbers and counts
Definition liblts_bisim_dnj.h:141
mcrl2::lts::detail::trans_type
std::size_t trans_type
type used to store transition (numbers and) counts
Definition check_complexity.h:107
mcrl2::utilities::split
std::vector< std::string > split(const std::string &line, const std::string &separators)
Split the text.
Definition text_utility.cpp:55
mcrl2
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72