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
25#include "mcrl2/lts/lts_aut.h"
26#include "mcrl2/lts/lts_fsm.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;
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.
63 #endif
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
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());
127 // set_marked_bottom_begin(marked_bottom_begin());
129 set_begin(splitpoint);
130
132
133 return NewB;
134}
135
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
184 #endif
185 if (BLOCK_NO_SEQNR != seqnr())
186 {
187 NewB->assign_seqnr();
188 }
189 // NewB->set_end(end());
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
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,
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 {
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 {
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
310 {
312 state_info.end() - 1;
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 {
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,
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,
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
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
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(bisim_gjkw::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
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 -
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
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 -
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
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;
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 -
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());
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 -
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();
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) =
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) =
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(
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::
1280 succ_iter->target->constln()->size()),
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>
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()];
1471 ++noninert_out_per_block[action_block.first->second];
1472 ++states_per_block[action_block.first->second];
1473 ++nr_of_states;
1475 }
1476 ++noninert_in_per_state[extra_state.first->second];
1477 ++noninert_out_per_state[t.from()];
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()
1487 }
1489 }
1490 }
1491 mCRL2log(log::verbose) << "Number of extra states: "
1492 << extra_kripke_states.size() << "\n";
1493 #ifndef NDEBUG
1495 #endif
1496}
1497
1498
1500template<class 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>
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>
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>
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 = bisim_gjkw::check_complexity::log_n -
1873 /*-------------------- find predecessors of SpB ---------------------*/ bisim_gjkw::check_complexity::ilog2(SpB->size());
1874 #endif
1875 /* 2.8: Mark block SpB as refinable */ mCRL2complexity(SpB, add_work(bisim_gjkw::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, add_work(bisim_gjkw::check_complexity::
1886 /* we can mark state s if necessary. Marking will move s to a */ 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(bisim_gjkw::
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;
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).
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:
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(
2045 for_all_refinable_blocks_RfnB_2_20, max_counter), );
2046 #endif
2047 if (1 == RfnB->size())
2048 {
2049 // if the block only contains a single state, the refinement
2050 // would be trivial anyway (and it cannot find new bottom
2051 // states).
2052 RfnB->set_marked_bottom_begin(RfnB->bottom_end());
2053 continue;
2054 }
2055 // 2.22: <RedB, BlueB> := Refine(RfnB, NewC, {marked states in
2056 // RfnB}, {})
2057 bisim_gjkw::block_t* RedB = refine(RfnB, NewC, nullptr, false);
2058 // 2.23: if RedB contains new bottom states then
2059 if (0 != RedB->unmarked_bottom_size())
2060 {
2061 // 2.24: RedB := PostprocessNewBottom(RedB, BlueB)
2062 RedB = postprocess_new_bottom(RedB);
2063 if (nullptr == RedB) continue;
2064 // 2.25: end if
2065 }
2066 // 2.30: Unmark all states of the original RfnB as predecessors
2067 // (first part) This needs to be done to make sure the call to
2068 // Refine in line 2.26 does not regard some states as marked.
2069 else
2070 {
2071 RedB->set_marked_bottom_begin(RedB->bottom_end());
2072 }
2073 assert(0 == RedB->marked_size());
2074 if (1 == RedB->size() || nullptr == RedB->FromRed(SpC))
2075 {
2076 // If the block only contains a single state or has no
2077 // transitions to SpC, the refinement would be trivial anyway
2078 // (and it cannot find new bottom states).
2079 continue;
2080 }
2081
2082 // 2.26: <RedB, BlueB> := Refine(RedB, SpC\SpB, {}, {transitions
2083 // from RedB to SpC\SpB})
2084 RedB = refine(RedB, SpC, RedB->FromRed(SpC), false ONLY_IF_DEBUG( , NewC )
2085 );
2086 // 2.27: if RedB contains new bottom states then
2087 if (0 != RedB->unmarked_bottom_size())
2088 {
2089 // 2.28: PostprocessNewBottom(RedB, BlueB)
2090 postprocess_new_bottom(RedB);
2091 // 2.29: endif
2092 }
2093 // 2.30: Unmark all states of the original RfnB as predecessors
2094 // if postprocess_new_bottom is called, that procedure already
2095 // unmarks the new bottom states.
2096 else
2097 {
2098 RedB->set_marked_bottom_begin(RedB->bottom_end());
2099 } assert(0 == RedB->marked_size());
2100 // 2.31: end for
2101 }
2102 #ifndef NDEBUG
2103 if (mCRL2logEnabled(log::debug))
2104 {
2105 part_st.print_part(part_tr);
2106 part_st.print_trans();
2107 }
2108
2109 /* 2.32: end while */ part_tr.assert_stability(part_st);
2110 #endif
2111 }
2112 // 2.33: return P
2113 // (this happens implicitly, through the bisim_partitioner_gjkw object
2114 // data)
2115 mCRL2log(log::verbose) << "number of blocks in the quotient: "
2116 << bisim_gjkw::block_t::nr_of_blocks << '\n';
2117}
2118 #ifndef NDEBUG
2119 namespace bisim_gjkw
2120 {
2121/*=============================================================================
2122= Refine -- Algorithm 3 in [GJKW 2017] =
2123=============================================================================*/
2136 static void blue_is_smaller(block_t* BlueB, block_t* RedB,
2137 const constln_t* NewC)
2138 {
2139 assert(nullptr != RedB);
2140 if (nullptr != BlueB)
2141 {
2142 assert(BlueB->size() <= RedB->size());
2143 unsigned const max_NewB = nullptr == BlueB ? 0
2145 for (permutation_iter_t i = BlueB->begin(); BlueB->end() != i; ++i)
2146 {
2147 state_info_ptr s = *i;
2148 mCRL2complexity(s, finalise_work(check_complexity::
2149 while_Test_is_not_empty_3_6l_s_is_blue_3_11l,
2151 max_NewB), );
2152 mCRL2complexity(s, finalise_work(check_complexity::
2153 while_Blue_contains_unvisited_states_3_15l,
2155 max_NewB), );
2156 for (succ_iter_t succ = s->succ_begin(); s->succ_end() != succ;
2157 ++succ)
2158 {
2159 mCRL2complexity(succ->B_to_C->pred,finalise_work(
2161 if___s_prime_has_transition_to_SpC_3_23l,
2164 }
2165 for (pred_iter_t pred = s->pred_begin(); s->pred_end() != pred;
2166 ++pred)
2167 {
2168 mCRL2complexity(pred, finalise_work(check_complexity::
2169 for_all_s_prime_in_pred_s_setminus_Red_3_18l,
2171 max_NewB), );
2172 }
2173 }
2174 }
2175 // cancel work counters for the red states, and also measure the work
2176 // done in the blue coroutine on states that turned out to be red.
2177 unsigned const max_NewC = nullptr == NewC ? 0
2179 for (permutation_iter_t i = RedB->begin(); RedB->end() != i; ++i)
2180 {
2181 state_info_ptr s = *i;
2182 mCRL2complexity(s, cancel_work(check_complexity::
2183 while_Red_contains_unvisited_states_3_15r), );
2184 for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
2185 {
2186 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2188 // the following counter should only be set for transitions to
2189 // the splitter constellation. For others transitions, no
2190 // (temporary) work should have been done.
2191 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2193 while_Test_is_not_empty_3_6l_s_is_red_3_9l,
2196 succ->target->constln() == NewC ? max_NewC : 0), );
2197 // the following counter only gets 1 during postprocessing, at
2198 // a time when state s is already stored as bottom state.
2199 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2201 while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing,
2204 1), );
2205 // the following counter only gets 1 before postprocessing, at
2206 // the same time as when it is discovered to be a new bottom
2207 // state
2208 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2211 refine_outgoing_transition_from_new_bottom_3_23l, 1), );
2212 }
2213 for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
2214 {
2215 mCRL2complexity(pred, cancel_work(check_complexity::
2216 for_all_s_prime_in_pred_s_3_18r), );
2217 }
2218 }
2219 // check the balance between useful and cancelled work:
2221 }
2222
2230 static void red_is_smaller(block_t* BlueB, block_t* RedB)
2231 {
2232 assert(nullptr != BlueB);
2233 assert(nullptr != RedB);
2234 assert(BlueB->size() >= RedB->size());
2235 for (permutation_iter_t i = BlueB->begin(); BlueB->end() != i; ++i)
2236 {
2237 state_info_ptr s = *i;
2238 mCRL2complexity(s, cancel_work(check_complexity::
2239 while_Test_is_not_empty_3_6l_s_is_blue_3_11l), );
2240 mCRL2complexity(s, cancel_work(check_complexity::
2241 while_Blue_contains_unvisited_states_3_15l), );
2242 for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
2243 {
2244 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2246 if___s_prime_has_transition_to_SpC_3_23l), );
2247 }
2248 for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
2249 {
2250 mCRL2complexity(pred, cancel_work(check_complexity::
2251 for_all_s_prime_in_pred_s_setminus_Red_3_18l), );
2252 }
2253 }
2254 unsigned const max_NewB = check_complexity::log_n -
2256 for (permutation_iter_t i = RedB->begin(); RedB->end() != i; ++i)
2257 {
2258 state_info_ptr s = *i;
2259 mCRL2complexity(s, finalise_work(check_complexity::
2260 while_Red_contains_unvisited_states_3_15r,
2262 for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
2263 {
2264 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2267 refine_outgoing_transition_3_6_or_23l, max_NewB), );
2268 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2270 while_Test_is_not_empty_3_6l_s_is_red_3_9l), );
2271 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2273 while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing), );
2274 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2276 if___s_prime_has_transition_to_SpC_3_23l), );
2277 }
2278 for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
2279 {
2280 mCRL2complexity(pred, finalise_work(check_complexity::
2281 for_all_s_prime_in_pred_s_3_18r,
2283 max_NewB), );
2284 }
2285 }
2287 }
2288
2289 } // end namespace bisim_gjkw
2290 #endif
2360
2361template <class LTS_TYPE>
2363 bisim_gjkw::block_t* const RfnB, const bisim_gjkw::constln_t* const SpC,
2364 const bisim_gjkw::B_to_C_descriptor* const FromRed,
2365 bool const postprocessing ONLY_IF_DEBUG( , const bisim_gjkw::constln_t* NewC )
2366 )
2367{
2368 #ifndef NDEBUG
2369 if (nullptr != FromRed)
2370 {
2371 assert(FromRed->from_block() == RfnB);
2372 assert(FromRed->to_constln() == SpC);
2373 assert(nullptr != SpC);
2374 assert(0 == RfnB->marked_size());
2375 }
2376 else
2377 {
2378 assert(0 != RfnB->marked_size());
2379 }
2380 assert(1 < RfnB->size());
2381 #endif
2382 // 3.2: if RfnB subseteq SpC then return RfnB
2383 if (RfnB->constln() == SpC)
2384 {
2385 // Mark all bottom states to indicate there are no new bottom states.
2388 return RfnB;
2389 }
2390 // 3.3: Test := {bottom states}\Red, ...
2391 // 3.4: Spend the same amount of work on either coroutine:
2392 // and
2393 // 3.39: RedB := RfnB or RedB := NewB , respectively
2394 #ifndef NDEBUG
2395 bisim_gjkw::permutation_iter_t const red_end = RfnB->end();
2396 #endif
2397 bisim_gjkw::block_t* RedB;
2398
2400 // common variables
2401 bisim_gjkw::permutation_iter_t notblue_initialised_end =
2402 RfnB->nonbottom_begin();
2403 bool FromRed_is_empty = nullptr == FromRed;
2404
2405 // variables for the blue coroutine
2406 bisim_gjkw::permutation_iter_t blue_visited_end;
2408 bisim_gjkw::pred_iter_t blue_pred_iter;
2409 bisim_gjkw::state_info_ptr blue_s_prime;
2410 bisim_gjkw::permutation_iter_t blue_blue_nonbottom_end;
2413
2414 // variables for the red coroutine
2415 bisim_gjkw::B_to_C_iter_t red_fromred_visited_begin;
2416 bisim_gjkw::permutation_iter_t red_visited_begin;
2418 bisim_gjkw::pred_iter_t red_pred_iter;
2419
2420 COROUTINE_LABELS( (REFINE_BLUE_PREDECESSOR_HANDLED)
2421 (REFINE_BLUE_TESTING)
2422 (REFINE_BLUE_STATE_HANDLED)
2423 (REFINE_BLUE_COLLECT_BOTTOM)
2424 (REFINE_RED_COLLECT_FROMRED)
2425 (REFINE_RED_PREDECESSOR_HANDLED)
2426 (REFINE_RED_STATE_HANDLED))
2427
2428/*--------------------------- handle blue states ----------------------------*/
2429
2430
2462
2463 COROUTINE assert(RfnB->nonbottom_begin() == notblue_initialised_end);
2464 // we have to decide which unmarked bottom states are blue. So we
2465 // walk over all of them and check whether they have a transition
2466 // to SpC or not.
2467 // 3.3: ..., Blue := {}
2468 blue_visited_end = RfnB->unmarked_bottom_begin();
2469 // 3.5l: whenever |Blue| > |RfnB|/2 do Abort this coroutine
2470 // nothing needs to be done now, as |Blue| = 0 here.
2471
2472 /* - - - - - - - collect blue bottom states - - - - - - - */
2473
2474 // 3.6l: while Test is not empty and FromRed is not empty do
2475 // We use the variable blue_visited_end in this loop to
2476 // indicate the boundary between blue states (namely those
2477 // in the interval [RfnB->unmarked_bottom_begin(),
2478 // blue_visited_end) ) and Test states (namely those in
2479 // [blue_visited_end, RfnB->unmarked_bottom_end()) ).
2480 COROUTINE_WHILE (REFINE_BLUE_COLLECT_BOTTOM,
2481 RfnB->unmarked_bottom_end() > blue_visited_end)
2482 {
2483 if (FromRed_is_empty)
2484 {
2485 // 3.14l: Blue := Blue union Test
2486 // done implicitly: we now regard all unmarked
2487 // bottom states as blue, i. e. the whole
2488 // interval [RfnB->unmarked_bottom_begin(),
2489 // RfnB->unmarked_bottom_end()).
2490 // 3.5l: whenever |Blue|>|RfnB|/2 do Abort this coroutine
2491 // In this case, Test may not yet be empty, so here we
2492 // have to check the condition of Line 3.5l.
2493 if (RfnB->unmarked_bottom_size() > RfnB->size() / 2)
2494 {
2496 }
2497 break;
2498 }
2499 // 3.7l: Choose s in Test
2500 blue_s = *blue_visited_end;
2501 // 3.8l: if s --> SpC then
2502 if (blue_s->surely_has_transition_to(SpC))
2503 {
2504 // 3.9l: Move s from Test to Red
2505 // The state s is not blue. Move it to the slice of
2506 // non-blue bottom states.
2508 RfnB->marked_bottom_begin() - 1);
2509 bisim_gjkw::swap_permutation(blue_visited_end,
2510 RfnB->marked_bottom_begin());
2511 // 3.5r: whenever |Red|>|RfnB|/2 do Abort the red coroutine
2512 if (RfnB->marked_size() > RfnB->size() / 2)
2513 {
2515 }
2516 #ifndef NDEBUG
2517 // The state is red. Depending on the context of refinement, the work done
2518 // on this state is attributed to one or another element of the Kripke
2519 // structure.
2520 if (postprocessing)
2521 {
2522 // refine() has been called from line 4.14. During postprocessing, the
2523 // work is ascribed to the transitions from s to SpC.
2524 // Using the current_constln pointer of s, find a transition to SpC.
2525 // The work has to be ascribed to the transitions from s to SpC.
2526 bisim_gjkw::succ_iter_t to_SpC = blue_s->current_constln();
2527 if (to_SpC == blue_s->succ_end() || to_SpC->target->constln() != SpC)
2528 {
2529 assert(blue_s->succ_begin() < to_SpC);
2530 --to_SpC;
2531 assert(to_SpC->target->constln() == SpC);
2532 }
2533 bisim_gjkw::succ_entry::slice_add_work_to_transns(to_SpC,
2535 while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing, 1);
2536 }
2537 else
2538 {
2539 // refine() has been called from line 2.26, and RfnB is a block with a
2540 // transition to SpB. The state has been marked because of these
2541 // transitions (which are not transitions to SpC!).
2542 // code similar to the case if (postprocessing).
2543 bisim_gjkw::succ_iter_t to_NewC = blue_s->current_constln();
2544 if (to_NewC == blue_s->succ_end() || to_NewC->target->constln() == SpC)
2545 {
2546 assert(blue_s->succ_begin() < to_NewC);
2547 --to_NewC;
2548 assert(to_NewC->target->constln() != SpC);
2549 }
2550 bisim_gjkw::succ_entry::slice_add_work_to_transns(to_NewC, bisim_gjkw::
2551 check_complexity::while_Test_is_not_empty_3_6l_s_is_red_3_9l, 1);
2552 }
2553 #endif
2554 // 3.10l: else
2555 }
2556 else
2557 { assert(blue_s->surely_has_no_transition_to(SpC));
2558 // 3.11l: Move s from Test to Blue
2559 ++blue_visited_end;
2560 // 3.5l: whenever |Blue|>|RfnB|/2 do Abort this coroutine
2561 if ((state_type) (blue_visited_end -
2562 RfnB->unmarked_bottom_begin()) > RfnB->size() / 2)
2563 {
2566 while_Test_is_not_empty_3_6l_s_is_blue_3_11l, 1), );
2567 // 3.12l: end if
2568 }
2569 // 3.13l: end while
2570 }
2571 END_COROUTINE_WHILE; assert(RfnB->constln() != SpC);
2572
2573 if (0 == RfnB->unmarked_bottom_size())
2574 {
2575 // all bottom states are red, so there cannot be any blue
2576 // states.
2578 // RfnB->set_marked_bottom_begin(RfnB->bottom_begin());
2579 RedB = RfnB; ONLY_IF_DEBUG( blue_is_smaller(nullptr, RedB, NewC); )
2581 }
2582
2583 /* - - - - - - - - visit blue states - - - - - - - - */
2584
2585 // 3.15l: while Blue contains unvisited states do
2586 blue_visited_end = RfnB->unmarked_bottom_begin();
2587 blue_blue_nonbottom_end = RfnB->unmarked_nonbottom_begin();
2588 COROUTINE_DO_WHILE (REFINE_BLUE_STATE_HANDLED,
2589 blue_visited_end != blue_blue_nonbottom_end)
2590 {
2591 // 3.16l: Choose an unvisited s in Blue
2592 blue_s = *blue_visited_end; assert(blue_visited_end < blue_blue_nonbottom_end ||
2593 (RfnB->unmarked_bottom_begin() <= blue_visited_end &&
2594 RfnB->unmarked_bottom_end() > blue_visited_end));
2595 assert(RfnB->unmarked_nonbottom_begin() <= blue_blue_nonbottom_end);
2596 assert(blue_blue_nonbottom_end <= notblue_initialised_end);
2597 /* 3.17l: Mark s as visited */ assert(RfnB->unmarked_nonbottom_end() >= notblue_initialised_end);
2598 ++blue_visited_end;
2599 // 3.18l: for all s_prime in inert_in(s) \ Red do
2600 COROUTINE_FOR (REFINE_BLUE_PREDECESSOR_HANDLED,
2601 blue_pred_iter = blue_s->inert_pred_begin(),
2602 blue_s->inert_pred_end()!=blue_pred_iter, ++blue_pred_iter)
2603 {
2604 blue_s_prime = blue_pred_iter->source;
2605 if (blue_s_prime->pos >= RfnB->marked_nonbottom_begin())
2606 { mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
2607 for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2608 continue;
2609 }
2610 // 3.19l: if notblue(s_prime) undefined then
2611 if (blue_s_prime->pos >= notblue_initialised_end)
2612 {
2613 // 3.20l: notblue(s_prime) := |inert_out(s_prime)|
2614 blue_s_prime->notblue = blue_s_prime->inert_succ_end()-
2615 blue_s_prime->inert_succ_begin();
2616 bisim_gjkw::swap_permutation(blue_s_prime->pos,
2617 notblue_initialised_end);
2618 ++notblue_initialised_end;
2619 // 3.21l: end if
2620 }
2621 // 3.22l: notblue(s_prime) := notblue(s_prime) - 1
2622 --blue_s_prime->notblue;
2623 // 3.23l: if notblue(s_prime) == 0 && ...
2624 if (0 != blue_s_prime->notblue)
2625 { mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
2626 for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2627 continue;
2628 }
2629 // 3.23l: ... && (FromRed == {} ||
2630 // out_noninert(s_prime) intersect SpC == {}) then
2631 if (!FromRed_is_empty)
2632 {
2633 if (blue_s_prime->surely_has_transition_to(SpC))
2634 { mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
2635 for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2636 continue;
2637 }
2638 if (!blue_s_prime->surely_has_no_transition_to(SpC))
2639 {
2640 // It is not yet known whether s_prime has a
2641 // transition to SpC or not. Execute the slow test
2642 // now.
2643 COROUTINE_FOR (REFINE_BLUE_TESTING,
2644 (blue_begin = blue_s_prime->succ_begin(),
2645 blue_end = blue_s_prime->succ_end() ),
2646 blue_begin < blue_end, (void) 0)
2647 {
2648 // binary search for transitions from s_prime
2649 // to constellation SpC.
2651 blue_begin + (blue_end - blue_begin) / 2;
2652 if (*SpC <= *mid->target->constln())
2653 {
2654 blue_end = mid->slice_begin();
2655 }
2656 if (*mid->target->constln() <= *SpC)
2657 {
2658 blue_begin =
2659 bisim_gjkw::succ_entry::slice_end(mid);
2660 }
2661 #ifndef NDEBUG
2662 bisim_gjkw::succ_entry::slice_add_work_to_transns(mid, bisim_gjkw::
2663 check_complexity::if___s_prime_has_transition_to_SpC_3_23l, 1);
2664 #endif
2665 }
2667 if (blue_begin != blue_end)
2668 { mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
2669 for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2670 continue;
2671 }
2672 }
2673 }
2674 // 3.24l: Blue := Blue union {s_prime}
2675 bisim_gjkw::swap_permutation(blue_s_prime->pos,
2676 blue_blue_nonbottom_end);
2677 ++blue_blue_nonbottom_end;
2678 // 3.5l: whenever |Blue|>|RfnB| / 2 do Abort this coroutine
2679 if (blue_blue_nonbottom_end -
2680 RfnB->unmarked_nonbottom_begin() +
2681 RfnB->unmarked_bottom_size() > RfnB->size() / 2)
2682 {
2684 }
2685 // 3.25l: end if
2686 // this is implicit in the `continue` statements above.
2687 /* 3.26l: end for */ mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
2688 for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2689 }
2691 /* 3.27l: end while */ mCRL2complexity(blue_s, add_work(bisim_gjkw::check_complexity::
2692 while_Blue_contains_unvisited_states_3_15l, 1), );
2693 if (RfnB->unmarked_bottom_end() == blue_visited_end)
2694 {
2695 blue_visited_end = RfnB->unmarked_nonbottom_begin();
2696 }
2697 }
2699
2700 /* - - - - - - - - split off blue block - - - - - - - - */
2701
2702 // 3.28l: Abort the other coroutine
2704 // All non-blue states are red.
2705 // 3.29l: Move Blue to a new block NewB
2706 // and
2707 // 3.30l: Destroy all temporary data
2708 bisim_gjkw::block_t* const NewB =
2709 RfnB->split_off_blue(blue_blue_nonbottom_end);
2710 part_tr.new_blue_block_created(RfnB, NewB);
2711 #ifndef NDEBUG
2712 unsigned const max_counter = bisim_gjkw::check_complexity::log_n -
2713 bisim_gjkw::check_complexity::ilog2(NewB->size());
2715 for_all_s_in_NewB_3_31, max_counter), );
2716 #endif
2717 // 3.31l: for all s in NewB do
2718 for (bisim_gjkw::permutation_iter_t s_iter = NewB->begin();
2719 NewB->end() != s_iter; ++s_iter)
2720 {
2721 blue_s = *s_iter; // mCRL2complexity(s, ...) -- optimized to the above call.
2722 // 3.32l: for all s_prime in inert_in(s) \ NewB do
2723 for (blue_pred_iter = blue_s->inert_pred_begin();
2724 blue_s->inert_pred_end()!=blue_pred_iter; ++blue_pred_iter)
2725 { mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
2726 for_all_s_prime_in_pred_s_3_32l, max_counter), );
2727 assert(part_tr.pred_end() > blue_pred_iter);
2728 assert(blue_pred_iter->succ->B_to_C->pred == blue_pred_iter);
2729 blue_s_prime = blue_pred_iter->source;
2730 if (blue_s_prime->block == NewB) { continue; } assert(blue_s_prime->block == RfnB);
2731 // 3.33l: s_prime --> s is no longer inert
2732 part_tr.make_noninert(blue_pred_iter->succ);
2733 // 3.34l: if |inert_out(s_prime)| == 0 then
2734 if (blue_s_prime->inert_succ_begin() ==
2735 blue_s_prime->inert_succ_end())
2736 {
2737 // 3.35l: s_prime is a new bottom state
2739 RfnB->bottom_begin() - 1);
2741 swap_permutation(blue_s_prime->pos,
2742 RfnB->bottom_begin()); // assert("blue_s_prime has a transition to SpC");
2743 // 3.36l: end if
2744 }
2745 // 3.37l: end for
2746 }
2747 // 3.38l: end for
2748 }
2749
2750 RedB = RfnB; ONLY_IF_DEBUG( blue_is_smaller(NewB, RedB, NewC); )
2752
2753/*---------------------------- handle red states ----------------------------*/
2754
2782
2783 COROUTINE
2784 // 3.5r: whenever |Red| > |RfnB|/2 then Abort this coroutine
2785 if (RfnB->marked_size() > RfnB->size()/2) ABORT_THIS_COROUTINE();
2786 // The red block contains at most RfnB->size() -
2787 // RfnB->unmarked_bottom_size() + FromRed->size() states. If that
2788 // is <= RfnB->size() / 2, we could abort the other coroutine
2789 // immediately. We don't do it here because we want to investigate
2790 // the effect of this and similar heuristics more systematically.
2791
2792 /* - - - - - - - collect states from FromRed - - - - - - - */
2793
2794 // 3.6r: while FromRed != {} do
2795 if (nullptr != FromRed)
2796 { assert(FromRed->from_block() == RfnB);
2797 red_fromred_visited_begin = FromRed->end; assert(RfnB->inert_end() <= FromRed->begin ||
2798 (RfnB->inert_begin() >= red_fromred_visited_begin &&
2799 RfnB->inert_end() > red_fromred_visited_begin));
2800 COROUTINE_WHILE (REFINE_RED_COLLECT_FROMRED,
2801 FromRed->begin != red_fromred_visited_begin)
2802 {
2803 // 3.10r (order of lines changed): FromRed := FromRed \ {s --> t}
2804 // We can change the order of lines because the
2805 // coroutine is not interrupted in between.
2806 --red_fromred_visited_begin;
2807 // 3.7r: Choose s --> t in FromRed
2808 bisim_gjkw::state_info_ptr const red_s =
2809 red_fromred_visited_begin->pred->source; assert(RfnB->begin() <= red_s->pos);
2810 /* 3.8r: Test := Test \ {s} */ assert(red_s->pos < RfnB->end());
2811 // and
2812 // 3.9r: Red := Red union {s}
2813 if (red_s->pos < notblue_initialised_end)
2814 {
2815 // The non-bottom state has a transition to a blue
2816 // state, so notblue is initialised; however, now it is
2817 // revealed to be red anyway.
2818 bisim_gjkw::swap_permutation(red_s->pos,
2819 --notblue_initialised_end);
2820 }
2821 if (RfnB->mark(red_s) &&
2822 // 3.5r: whenever |Red| > |RfnB|/2 do Abort this coroutine
2823 RfnB->marked_size() > RfnB->size() / 2)
2824 {
2826 }
2827 /* 3.13r: end while */ mCRL2complexity(red_fromred_visited_begin->pred, add_work(bisim_gjkw::
2828 check_complexity::while_FromRed_is_not_empty_3_6r, 1), );
2829 }
2831
2832 // The shared variable FromRed_is_empty is set to true as soon
2833 // as FromRed should be considered empty. (From that moment
2834 // on, no slow tests are needed any more.)
2835 FromRed_is_empty = true;
2836 } assert(FromRed_is_empty); assert(0 != RfnB->marked_size());
2837
2838 /* - - - - - - - - visit red states - - - - - - - - */
2839
2840 red_visited_begin = RfnB->marked_bottom_end();
2841 if (RfnB->marked_bottom_begin() == red_visited_begin)
2842 {
2843 // It may happen that all found states are non-bottom states.
2844 // (In that case, some of these states will become new bottom
2845 // states.)
2846 red_visited_begin = RfnB->marked_nonbottom_end();
2847 }
2848 // 3.15r: while Red contains unvisited states do
2849 COROUTINE_DO_WHILE(REFINE_RED_STATE_HANDLED,
2850 RfnB->marked_nonbottom_begin() != red_visited_begin)
2851 {
2852 // 3.17r (order of lines changed): Mark s as visited
2853 --red_visited_begin; assert(RfnB->marked_bottom_begin() <= red_visited_begin ||
2854 (RfnB->marked_nonbottom_begin() <= red_visited_begin &&
2855 RfnB->marked_nonbottom_end() > red_visited_begin));
2856 // 3.16r: Choose an unvisited s in Red
2857 red_s = *red_visited_begin;
2858 // 3.18r: for all s_prime in inert_in(s) do
2859 COROUTINE_FOR (REFINE_RED_PREDECESSOR_HANDLED,
2860 red_pred_iter = red_s->inert_pred_begin(),
2861 red_s->inert_pred_end() != red_pred_iter, ++red_pred_iter)
2862 {
2863 bisim_gjkw::state_info_ptr const s_prime =
2864 red_pred_iter->source;
2865 // 3.24r: Red := Red union {s_prime}
2866 if (s_prime->pos < notblue_initialised_end)
2867 {
2868 // The state has a transition to a blue state, so
2869 // notblue is initialised; however, now it is revealed
2870 // to be red anyway.
2871 bisim_gjkw::swap_permutation(s_prime->pos,
2872 --notblue_initialised_end);
2873 }
2874 if (RfnB->mark_nonbottom(s_prime) &&
2875 // 3.5r: whenever |Red| > |RfnB|/2 do Abort this coroutine
2876 RfnB->marked_size() > RfnB->size() / 2)
2877 {
2879 }
2880 /* 3.26r: end for */ mCRL2complexity(red_pred_iter, add_work(bisim_gjkw::check_complexity::
2881 for_all_s_prime_in_pred_s_3_18r, 1), );
2882 }
2884 /* 3.27r: end while */ mCRL2complexity(red_s, add_work(bisim_gjkw::check_complexity::
2885 while_Red_contains_unvisited_states_3_15r, 1), );
2886 if (RfnB->marked_bottom_begin() == red_visited_begin)
2887 {
2888 red_visited_begin = RfnB->marked_nonbottom_end();
2889 }
2890 }
2892
2893 /* - - - - - - - - split off red block - - - - - - - - */
2894
2895 // 3.28r: Abort the other coroutine
2897 // All non-red states are blue.
2898 // 3.29r: Move Red to a new block RedB
2899 // and
2900 // 3.30r: Destroy all temporary data
2901 RedB = RfnB->split_off_red(RfnB->marked_nonbottom_begin());
2902 part_tr.new_red_block_created(RfnB, RedB, postprocessing);
2903 #ifndef NDEBUG
2904 unsigned const max_counter = bisim_gjkw::check_complexity::log_n -
2905 bisim_gjkw::check_complexity::ilog2(RedB->size());
2907 for_all_s_in_NewB_3_31, max_counter), );
2908 #endif
2909 // 3.31r: for all non-bottom s in RedB do
2910 // we have to run through the states backwards because
2911 // otherwise, we might miss out some states.
2912 for (bisim_gjkw::permutation_iter_t s_iter = RedB->nonbottom_end();
2913 RedB->nonbottom_begin() != s_iter; )
2914 {
2915 --s_iter;
2916 red_s = *s_iter; // mCRL2complexity(s, ...) -- optimized to the above call.
2917 // 3.32r: for all s_prime in inert_out(s) \ RedB do
2919 succ_iter = red_s->inert_succ_begin();
2920 red_s->inert_succ_end()!=succ_iter; ++succ_iter)
2921 { mCRL2complexity(succ_iter->B_to_C->pred, add_work(bisim_gjkw::
2922 check_complexity::for_all_s_prime_in_succ_s_3_32r, max_counter), );
2923 assert(part_tr.succ_end() > succ_iter);
2924 assert(succ_iter->B_to_C->pred->succ == succ_iter);
2925 if (bisim_gjkw::state_info_ptr const s_prime =
2926 succ_iter->target;
2927 s_prime->block == RedB)
2928 {
2929 continue;
2930 } else assert(s_prime->block == RfnB);
2931 // 3.33r: s --> s_prime is no longer inert
2932 part_tr.make_noninert(succ_iter);
2933 // 3.34r: end for
2934 }
2935 // 3.35r: if |inert_out(s)| == 0 then
2936 if (red_s->inert_succ_begin() == red_s->inert_succ_end())
2937 {
2938 // 3.36r: s is a new bottom state
2939 RedB->set_marked_nonbottom_begin(RedB->bottom_begin() - 1);
2941 swap_permutation(red_s->pos, RedB->bottom_begin()); // assert("red_s has a transition to SpC");
2942 // 3.37r: end if
2943 }
2944 // 3.38r: end for
2945 } assert(RfnB->end() < red_end);
2946 ONLY_IF_DEBUG( red_is_smaller(RfnB, RedB); )
2949
2950
2951 /* 3.41 P := partition P where NewB is added and the states in NewB are */ assert(RedB->end() == red_end);
2952 // removed from RfnB
2953 // done through adapting the data structures in the coroutines.
2954 // 3.42: return <RedB, BlueB> (with old and new bottom states separated)
2955 // The separation is indicated by marking the old bottom states.
2956 // Only RedB is returned explicitly, as most calls to Refine only use
2957 // RedB.
2958 return RedB;
2959}
2960
2961
2962
2963/*=============================================================================
2964= PostprocessNewBottom -- Algorithm 4 in [GJKW 2017] =
2965=============================================================================*/
2966
2967
2968
2975{
2976 public:
2978 const bisim_gjkw::constln_t* b) const
2979 {
2980 return *a < *b;
2981 }
2982};
2983
2984
2985typedef std::set<bisim_gjkw::constln_t*, constln_ptr_less> R_map_t;
2986
2987
3004template <class LTS_TYPE>
3007 /* , bisim_gjkw::block_t* BlueB */)
3008{ assert(0 != RedB->unmarked_bottom_size());
3009 assert(RedB->marked_nonbottom_begin() == RedB->marked_nonbottom_end());
3010 /*------- collect constellations reachable from new bottom states -------*/
3011
3012 // 4.3: <ResultB, RfnB> := Refine(RedB, cosplit(RedB, BlueB), {old bottom
3013 // states in RedB}, {})
3014 bisim_gjkw::block_t* ResultB;
3015 bisim_gjkw::block_t* RfnB;
3016 #ifndef NDEBUG
3017 bisim_gjkw::permutation_const_iter_t blue_begin = RedB->begin();
3018 #endif
3019 if (0 != RedB->marked_bottom_size())
3020 {
3021 // postprocessing == false is required here because we need to keep
3022 // ResultB->FromRed().
3023 ResultB = refine(RedB, nullptr, nullptr, false); assert(nullptr != ResultB); assert(0 == ResultB->unmarked_bottom_size());
3024 // 4.26: Destroy all temporary data
3025 // As part of this line, we unmark all states.
3026 ResultB->set_marked_bottom_begin(ResultB->bottom_end()); assert(ResultB->begin() > blue_begin);
3027 RfnB = ResultB->begin()[-1]->block;
3028 }
3029 else
3030 {
3031 RfnB = RedB;
3032 ResultB = nullptr;
3033 } assert(ResultB != RfnB); assert(RfnB->begin() == blue_begin);
3034 // do not refine a trivial block
3035 if (1 == RfnB->size())
3036 { assert(0 == RfnB->marked_size());
3037 return ResultB;
3038 }
3039 // 4.2: Create an empty search tree R of constellations
3040 R_map_t R;
3041Line_4_4:
3042 /* 4.4: for all constellations C not in R reachable from RfnB do */ assert(0 == RfnB->marked_bottom_size());
3043 while (!RfnB->to_constln.front().needs_postprocessing())
3044 {
3045 bisim_gjkw::B_to_C_desc_iter_t const new_slice =
3046 RfnB->to_constln.begin(); // try to assign the work to the transitions from bottom states in RfnB to C.
3047 #ifndef NDEBUG
3048 if (!new_slice->add_work_to_bottom_transns(bisim_gjkw::check_complexity::
3049 for_all_transitions_from_bottom_states_a_priori_4_4, 1))
3050 {
3051 // It didn't work out -- now assign it temporarily to the
3052 // B_to_C slice itself.
3053 mCRL2complexity(new_slice, add_work(bisim_gjkw::check_complexity::
3054 for_all_constellations_C_not_in_R_from_RfnB_4_4, 1), );
3055 }
3056 #endif
3057 bisim_gjkw::constln_t* const C = new_slice->to_constln();
3058 // 4.5: Add C to R
3059 if (!R.insert(C).second) //< complexity log(n)
3060 { assert(0 && "The constellation already was in R");
3061 }
3062 // 4.6: Register that the transitions from RfnB to C need
3063 /* postprocessing */ assert(C->postprocess_begin == C->postprocess_end);
3064 C->postprocess_begin = new_slice->begin;
3065 C->postprocess_end = new_slice->end; assert(C->postprocess_begin < C->postprocess_end);
3066 // move the set of transitions to the end of the list
3067 RfnB->to_constln.splice(RfnB->to_constln.end(), RfnB->to_constln,
3068 new_slice);
3069 // 4.7: end for
3070 }
3071 // 4.8: for all bottom states s in RfnB do
3073 do
3074 {
3076 for_all_bottom_states_s_in_RfnB_4_8, 1), );
3077 // 4.9: Set the current constellation pointer of s to the first
3078 // constellation it can reach
3080 // 4.10: end for
3081 }
3082 while (RfnB->unmarked_bottom_end() != ++s_iter);
3083
3084 /*--------------- stabilise w. r. t. found constellations ---------------*/
3085
3086 // 4.11: for all constellations SpC in R (in order) do
3087 while (!R.empty())
3088 { // the work has to be assigned to the transitions from (new) bottom
3089 bisim_gjkw::constln_t* const SpC = *R.begin(); // states to constellation SpC. We do that assignment in the inner
3090 // 4.12: for all blocks B with transitions to SpC that need // loop. Ensure that the inner loop is executed:
3091 /* postprocessing do */ assert(SpC->postprocess_begin != SpC->postprocess_end);
3092 do
3093 {
3094 // add_work is called indirectly: after refining, work is assigned
3095 // to every (new) bottom state in the refined block.
3096 bisim_gjkw::B_to_C_iter_t const B_iter = SpC->postprocess_begin; assert(part_tr.B_to_C_end() > B_iter);
3097 bisim_gjkw::block_t* const B = B_iter->pred->source->block; assert(B_iter->pred->succ->B_to_C == B_iter);
3098 bisim_gjkw::B_to_C_desc_iter_t FromRed = B_iter->B_to_C_slice; assert(FromRed->begin == B_iter);
3099 #ifndef NDEBUG
3100 bool postproc_a_posteriori = !FromRed->
3101 add_work_to_bottom_transns(bisim_gjkw::check_complexity::
3102 for_all_transitions_that_need_postproc_a_priori_4_12, 1);
3103 #endif
3104 // 4.13: Delete the transitions from B to SpC from those that need
3105 // postprocessing
3106 SpC->postprocess_begin = FromRed->end; assert(SpC->postprocess_begin <= SpC->postprocess_end);
3107 assert(!B->to_constln.empty());
3108 if (B->to_constln.begin() != FromRed)
3109 { assert(FromRed->from_block() == B);
3110 B->to_constln.splice(B->to_constln.begin(), B->to_constln,
3111 FromRed);
3112 }
3113 /* do not refine a trivial block */ assert(0 == B->marked_size());
3114 if (1 == B->size())
3115 { assert(!postproc_a_posteriori);
3116 #ifndef NDEBUG
3117 if (0 != FromRed->work_counter.get_work_counter_4_4())
3118 {
3119 assert(FromRed->add_work_to_bottom_transns(
3121 for_all_transitions_from_bottom_states_a_posteriori_4_4, 1));
3122 FromRed->work_counter.reset_work_counter_4_4();
3123 }
3124 #endif
3125 continue;
3126 }
3127 // refine() may destroy FromRed: if the red subblock is smaller,
3128 // the transitions in FromRed are moved to a new B_to_C slice.
3129 // Therefore we select some transition from it, to restore the
3130 // slice afterwards. Any transition should do.
3131 #ifndef NDEBUG
3132 bisim_gjkw::pred_iter_t FromRed_save = FromRed->begin->pred;
3133 #endif
3134 // 4.14: <RedB, BlueB> := Refine(B, SpC, {}, {transitions to SpC})
3135 RedB = refine(B, SpC, &*FromRed, true);
3136 #ifndef NDEBUG
3137 FromRed = FromRed_save->succ->B_to_C->B_to_C_slice;
3138 if (postproc_a_posteriori && !FromRed->add_work_to_bottom_transns(
3140 for_all_transitions_that_need_postproc_a_posteriori_4_12, 1))
3141 {
3142 assert(0 && "no new bottom states to assign work to");
3143 }
3144 // try to move the work that was not yet moved to the
3145 // transitions from (new) bottom states now.
3146 if (0 != FromRed->work_counter.get_work_counter_4_4())
3147 {
3148 if (!FromRed->add_work_to_bottom_transns(bisim_gjkw::check_complexity::
3149 for_all_transitions_from_bottom_states_a_posteriori_4_4, 1))
3150 {
3151 assert(0 && "no new bottom states to assign work to");
3152 }
3153 FromRed->work_counter.reset_work_counter_4_4();
3154 }
3155 #endif
3156 // 4.15: for all old bottom states s in RedB do
3158 s_iter = RedB->marked_bottom_begin();
3159 RedB->marked_bottom_end() != s_iter; ++s_iter)
3160 {
3161 bisim_gjkw::state_info_ptr const s = *s_iter;
3162 // 4.16: Advance the current constellation pointer of s to the
3163 // next constellation it can reach
3164 if (s->current_constln() < s->succ_end() &&
3165 s->current_constln()->target->constln() == SpC)
3166 {
3167 #ifndef NDEBUG
3168 bisim_gjkw::succ_entry::slice_add_work_to_transns(s->current_constln(),
3169 bisim_gjkw::check_complexity::for_all_old_bottom_states_s_in_RedB_4_15,1);
3170 #endif
3171 s->set_current_constln(bisim_gjkw::succ_entry::slice_end(
3172 s->current_constln()));
3173 } else
3175 for_all_old_bottom_states_s_in_RedB_selfloop_4_15, 1), );
3176 assert(B == RedB /* we should test: BlueB is empty */);
3177 assert(B->constln() == SpC);
3178 }
3179 assert(s->succ_end() == s->current_constln() ||
3180 /* 4.17: end for */ *SpC < *s->current_constln()->target->constln());
3181 }
3182 /* 4.18: if RedB contains new bottom states then */ assert(RedB->marked_nonbottom_begin() == RedB->marked_nonbottom_end());
3183 if (0 != RedB->unmarked_bottom_size())
3184 {
3185 // 4.19: <_, RfnB> := Refine(RedB, cosplit(RedB, BlueB), {old
3186 // bottom states in RedB}, {})
3187 #ifndef NDEBUG
3188 blue_begin = RedB->begin();
3189 #endif
3190 if (0 != RedB->marked_bottom_size())
3191 {
3192 RedB = refine(RedB, nullptr, nullptr, true); assert(nullptr != RedB); assert(0 == RedB->unmarked_bottom_size());
3193 // 4.26: Destroy all temporary data
3194 // As part of this line, we unmark all states.
3195 RedB->set_marked_bottom_begin(RedB->bottom_end()); assert(RedB->begin() > blue_begin);
3196 RfnB = RedB->begin()[-1]->block;
3197 }
3198 else
3199 {
3200 RfnB = RedB;
3201 #ifndef NDEBUG
3202 RedB = nullptr;
3203 #endif
3204 } assert(RedB != RfnB);
3205 assert(RfnB->begin() == blue_begin);
3206 // do not refine a trivial block
3207 if (1 == RfnB->size())
3208 { assert(0 == RfnB->marked_size());
3209 continue;
3210 }
3211 // 4.20: Register that the transitions from RfnB to SpC need
3212 // postprocessing
3214 SpC->postprocess_begin[-1].B_to_C_slice; assert(new_slice->from_block() == RfnB);
3215 assert(new_slice->to_constln() == SpC);
3216 SpC->postprocess_begin = new_slice->begin; assert(new_slice->end <= SpC->postprocess_end);
3217 // move the set of transitions to the end of the list
3218 RfnB->to_constln.splice(RfnB->to_constln.end(),
3219 RfnB->to_constln, new_slice);
3220 // 4.21: Restart the procedure (but keep R),
3221 // i. e. go to Line 4.4
3222 goto Line_4_4;
3223 // 4.22: end if
3224 }
3225 // 4.26: Destroy all temporary data
3226 // As part of this line, we unmark all states.
3227 RedB->set_marked_bottom_begin(RedB->bottom_end());
3228 // 4.23: end for
3229 }
3230 while (SpC->postprocess_begin != SpC->postprocess_end);
3231 // 4.24: Delete SpC from R
3232 R.erase(R.begin());
3233 // 4.25: end for
3234 }
3235 /* 4.26: Destroy all temporary data */ assert(R.empty());
3236
3237 return ResultB;
3238}
3239
3240
3241
3242/*=============================================================================
3243= explicit instantiation requests =
3244=============================================================================*/
3245
3246
3247
3248namespace bisim_gjkw
3249{
3250
3251template class bisim_partitioner_gjkw_initialise_helper<lts_lts_t>;
3252template class bisim_partitioner_gjkw_initialise_helper<lts_aut_t>;
3253template class bisim_partitioner_gjkw_initialise_helper<lts_fsm_t>;
3254
3255} // end namespace bisim_gjkw
3256
3257template class bisim_partitioner_gjkw<lts_lts_t>;
3258template class bisim_partitioner_gjkw<lts_aut_t>;
3259template class bisim_partitioner_gjkw<lts_fsm_t>;
3260
3261} // end namespace detail
3262} // end namespace lts
3263} // end namespace mcrl2
#define STATE_TYPE_MAX
#define mCRL2complexity(unit, call,...)
Assigns work to a counter and checks for errors.
stores information about a block
static void init(state_type n)
starts counting for a new refinement run
static int ilog2(state_type size)
calculate the base-2 logarithm, rounded down
static unsigned char log_n
value of floor(log2(n)) for easy access
static void check_temporary_work()
check that not too much superfluous work has been done
stores information about a constellation
stores information about a single state
implements the main algorithm for the stutter equivalence quotient
function object to compare two constln_t pointers based on their contents
bool operator()(const bisim_gjkw::constln_t *a, const bisim_gjkw::constln_t *b) const
A class containing triples, source label and target representing transitions.
Definition transition.h:43
helper macros for coroutines
#define ABORT_THIS_COROUTINE()
indicates that this coroutine gives up control to the other one
Definition coroutine.h:363
#define END_COROUTINE
Ends the definition of code for a coroutine.
Definition coroutine.h:200
#define ABORT_OTHER_COROUTINE()
indicates that the other coroutine should give up control
Definition coroutine.h:378
#define COROUTINE_FOR(location, init, condition, update)
a for loop where every iteration incurs one unit of work
Definition coroutine.h:271
#define COROUTINE_WHILE(location, condition)
a while loop where every iteration incurs one unit of work
Definition coroutine.h:227
#define COROUTINES_SECTION
begin a section with two coroutines
Definition coroutine.h:142
#define COROUTINE_DO_WHILE(location, condition)
a do { } while loop where every iteration incurs one unit of work
Definition coroutine.h:314
#define END_COROUTINES_SECTION
Close a section containing coroutines.
Definition coroutine.h:208
#define COROUTINE
Define the code for a coroutine.
Definition coroutine.h:192
#define END_COROUTINE_WHILE
ends a loop started with COROUTINE_WHILE
Definition coroutine.h:252
#define END_COROUTINE_FOR
ends a loop started with COROUTINE_FOR
Definition coroutine.h:297
#define COROUTINE_LABELS(locations)
Declare the interrupt locations for the coroutines.
Definition coroutine.h:161
#define END_COROUTINE_DO_WHILE
ends a loop started with COROUTINE_DO_WHILE
Definition coroutine.h:336
#define TERMINATE_COROUTINE_SUCCESSFULLY()
terminate the pair of coroutines successfully
Definition coroutine.h:348
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
permutation_const_iter_t end() const
iterator past the last state in the block
void set_inert_begin(B_to_C_iter_t new_inert_begin)
void assert_stability(const part_state_t &part_st) const
assert that the data structure is consistent and stable
const constln_t * to_constln() const
compute the goal constellation of the transitions in this slice
static state_type nr_of_blocks
total number of blocks with unique sequence number allocated
state_type unmarked_bottom_size() const
provides the number of unmarked bottom states in the block
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...
bool split_s_inert_out(state_info_ptr s ONLY_IF_DEBUG(, constln_t *OldC))
Split outgoing transitions of a state in the splitter.
void set_marked_bottom_begin(permutation_iter_t new_marked_bottom_begin)
void SetFromRed(B_to_C_desc_iter_t new_fromred)
set FromRed to an existing element in to_constln
void make_nontrivial()
makes a constellation non-trivial (i. e. inserts it into the respective list)
permutation_const_iter_t nonbottom_begin() const
iterator to the first non-bottom state in the block
pred_const_iter_t inert_pred_end() const
iterator one past the last inert incoming transition
const block_t * from_block() const
compute the source block of the transitions in this slice
block_t * split_off_small_block()
split off a single block from the constellation
B_to_C_iter_t postprocess_begin
iterator to the first transition into this constellation that needs postprocessing
const constln_t * constln() const
get constellation where the state belongs
permutation_const_iter_t begin() const
iterator to the first state in the block
void swap_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2)
bool surely_has_no_transition_to(const constln_t *SpC) const
void set_begin(permutation_iter_t new_begin)
permutation_const_iter_t marked_nonbottom_begin() const
iterator to the first marked non-bottom state in the block
permutation_iter_t pos
position of the state in the permutation array
static constln_t * nontrivial_first
first constellation in the list of non-trivial constellations
permutation_const_iter_t end() const
constant iterator past the last state in the constellation
permutation_const_iter_t unmarked_bottom_begin() const
iterator to the first unmarked bottom state in the block
void set_inert_begin_and_end(B_to_C_iter_t new_inert_begin, B_to_C_iter_t new_inert_end)
B_to_C_const_iter_t inert_begin() const
iterator to the first inert transition of the block
void make_nonrefinable()
makes a block non-refinable (i. e. removes it from the respective list)
permutation_const_iter_t marked_bottom_begin() const
iterator to the first marked bottom state in the block
pred_const_iter_t noninert_pred_begin() const
iterator to first non-inert incoming transition
bool mark_nonbottom(state_info_ptr s)
mark a non-bottom state
permutation_const_iter_t bottom_begin() const
iterator to the first bottom state in the block
void swap_out(pred_iter_t const pos1, pred_iter_t const pos2)
state_type size() const
provides the number of states in the block
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
block_t * split_off_blue(permutation_iter_t blue_nonbottom_end)
refine the block (the blue subblock is smaller)
permutation_const_iter_t marked_bottom_end() const
iterator past the last marked bottom state in the block
state_type notblue
number of inert transitions to non-blue states
permutation_const_iter_t marked_nonbottom_end() const
iterator one past the last marked non-bottom state in the block
const state_type sort_key
sort key to order constellation-related information
state_type marked_bottom_size() const
provides the number of marked bottom states in the block
bool is_trivial() const
returns true iff the constellation is trivial
B_to_C_desc_list to_constln
list of B_to_C with transitions from this block
static succ_iter_t slice_end(succ_iter_t this_)
block_t * block
block where the state belongs
const constln_t * get_nontrivial_next() const
provides the next non-trivial constellation
void set_marked_nonbottom_begin(permutation_iter_t new_marked_nonbottom_begin)
#define BLOCK_NO_SEQNR
static permutation_const_iter_t perm_begin
bool make_refinable()
makes a block refinable (i. e. inserts it into the respective list)
fixed_vector< state_info_entry > state_info
array with all other information about states
state_type state_size() const
provide size of state space
state_type size() const
returns number of states in the constellation
B_to_C_const_iter_t inert_end() const
iterator past the last inert transition of the block
const constln_t * constln() const
constellation where the block belongs to
permutation_const_iter_t bottom_end() const
iterator past the last bottom state in the block
static block_t * refinable_first
first block in the list of refinable blocks
succ_const_iter_t succ_begin() const
iterator to first outgoing transition
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
void set_end(permutation_iter_t new_end)
void print_trans() const
print all transitions
bool is_refinable() const
checks whether the block is refinable
block_t * split_off_red(permutation_iter_t red_nonbottom_begin)
refine the block (the red subblock is smaller)
succ_const_iter_t inert_succ_begin() const
iterator to first inert outgoing transition
permutation_const_iter_t begin() const
constant iterator to the first state in the constellation
void assign_seqnr()
assigns a unique sequence number
std::unordered_map< Key, state_type, KeyHasher > extra_kripke_states
void new_blue_block_created(block_t *OldB, block_t *NewB)
handle B_to_C slices after a new blue block has been created
static state_info_const_ptr s_i_begin
pointer at the first entry in the state_info array
static constln_t * get_some_nontrivial()
provides an arbitrary non-trivial constellation
permutation_const_iter_t unmarked_bottom_end() const
iterator past the last unmarked bottom state in the block
void set_bottom_begin(permutation_iter_t new_bottom_begin)
void set_inert_succ_begin_and_end(succ_iter_t new_inert_out_begin, succ_iter_t new_inert_out_end)
void swap3_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2, succ_iter_t const pos3)
const block_t * block(state_type s) const
find block of a state
succ_const_iter_t inert_succ_end() const
iterator past the last inert outgoing transition
check_complexity::block_counter_t work_counter
bisim_partitioner_gjkw_initialise_helper(LTS_TYPE &l, bool branching, bool preserve_divergence)
constructor of the helper class
pred_const_iter_t inert_pred_begin() const
iterator to first inert incoming transition
pred_const_iter_t noninert_pred_end() const
iterator past the last non-inert incoming transition
void set_inert_end(B_to_C_iter_t new_inert_end)
pred_const_iter_t pred_end() const
iterator past the last incoming transition
static state_info_const_ptr s_i_end
pointer past the last actual entry in the state_info array
permutation_const_iter_t unmarked_nonbottom_begin() const
iterator to the first unmarked non-bottom state in the block
permutation_const_iter_t nonbottom_end() const
iterator past the last non-bottom state in the block
succ_const_iter_t succ_end() const
iterator past the last outgoing transition
B_to_C_descriptor * FromRed(const constln_t *SpC)
read FromRed
permutation_const_iter_t unmarked_nonbottom_end() const
iterator past the last unmarked non-bottom state in the 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)
state_type marked_size() const
provides the number of marked states in the block
B_to_C_iter_t postprocess_end
iterator past the last transition into this constellation that needs postprocessing
void print_part(const part_trans_t &part_tr) const
print the partition as a tree (per constellation and block)
void set_current_constln(succ_iter_t const new_current_constln)
bool mark(state_info_ptr s)
mark a state
pred_const_iter_t pred_begin() const
iterator to first incoming transition
bool surely_has_transition_to(const constln_t *SpC) const
#define ONLY_IF_DEBUG(...)
include something in Debug mode
O(m log n)-time stuttering equivalence algorithm.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
This file contains a class that contains labelled transition systems in aut format.
This file contains a class that contains labelled transition systems in fsm format.
This file contains some utility functions to manipulate lts's.
@ verbose
Definition logger.h:35
const state_info_entry * state_info_const_ptr
fixed_vector< pred_entry >::iterator pred_iter_t
fixed_vector< succ_entry >::const_iterator succ_const_iter_t
static void red_is_smaller(block_t *BlueB, block_t *RedB)
moves temporary counters to normal ones if the red block is smaller
permutation_t::iterator permutation_iter_t
fixed_vector< pred_entry >::const_iterator pred_const_iter_t
permutation_t::const_iterator permutation_const_iter_t
B_to_C_desc_list::const_iterator B_to_C_desc_const_iter_t
B_to_C_desc_list::iterator B_to_C_desc_iter_t
fixed_vector< B_to_C_entry >::iterator B_to_C_iter_t
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
fixed_vector< succ_entry >::iterator succ_iter_t
std::size_t state_type
type used to store state (numbers and) counts
std::set< bisim_gjkw::constln_t *, constln_ptr_less > R_map_t
std::size_t label_type
type used to store label numbers and counts
std::size_t trans_type
type used to store transition (numbers and) counts
std::vector< std::string > split(const std::string &line, const std::string &separators)
Split the text.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72