mCRL2
Searching...
No Matches
check_complexity.h
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//
7// (See accompanying file LICENSE_1_0.txt or copy at
9
69
70#ifndef _CHECK_COMPLEXITY_H
71#define _CHECK_COMPLEXITY_H
72
73#include <cstring> // for std::size_t and std::memset()
74#include <cassert>
75#include <cmath> // for std::log2()
76#include <climits> // for CHAR_BIT and SIZE_MAX
77
79
80
81namespace mcrl2
82{
83namespace lts
84{
85namespace detail
86{
87
91typedef std::size_t state_type;
92#define STATE_TYPE_MIN ((state_type) 0)
93#define STATE_TYPE_MAX SIZE_MAX
94
98typedef std::size_t trans_type;
99#define TRANS_TYPE_MIN ((trans_type) 0)
100#define TRANS_TYPE_MAX SIZE_MAX
101
102#ifndef NDEBUG
103
105typedef std::ptrdiff_t signed_trans_type;
106
107namespace bisim_gjkw
108{
109
117{
118 public:
129 {
130 // block counters: every state in the block is regarded as visited. In
131 // this way, every state is ``visited'' O(log n) times.
132 // Invariant: block->constln()->size() << (counter value) <= n
135
136 // If a loop runs over every state of a block exactly once, we simplify
137 // the task of updating the counters by making the corresponding loop
138 // counter a block counter:
140 // Invariant of the following block counters:
141 // block->size() << (counter value) <= n
146
147 // state counters: every state is visited O(log n) times
148 // Invariant: s->block->size() << (counter value) <= n
151
152 // The following counters are used when one refines a block: the first
153 // group is used to store the amount of work that (a posteriori) turns
154 // out to be useful. After that, there are two groups of counters to
155 // store temporary work.
158
159 // temporary state counters (blue):
163
164 // temporary state counters (red):
167
168 // new bottom state counters: every state is visited once
169 // Invariant: if s is a non-bottom state, the counter is 0;
170 // otherwise, the counter is 0 or 1.
172 // the next counter is used to count the work done on a virtual
173 // self-loop in line 4.15 (the new bottom state is regarded as red
174 // because it is in the splitter, but there is no transition to the
175 // splitter).
178
179 // B_to_C_descriptor counters: every transition in the B_to_C-slice is
180 // regarded as visited. In this way, every transition is ``visited''
181 // O(log n) times.
182 // Invariant: to_constln()->size() << (counter value) <= n
185
186 // If a loop runs over every transition in a B_to_C slice exactly once,
187 // we simplify the task of updating the counters by making the
188 // corresponding loop counter a B_to_C counter:
190 // the following counter is also meant for temporary work.
191 // Sometimes, after separating the new bottom states from the old ones,
192 // a constellation is reachable from the block of the new bottom
193 // states, but only from non-bottom states in this block. In that
194 // case, it cannot yet be determined which state will be a new bottom
195 // state. Then, the work is assigned temporarily to the B_to_C slice,
196 // until some new bottom state is found to which to assign it.
201
202 // transition counters: every transition is visited O(log n) times
203 // counters for transitions into the splitter NewC
204 // Invariant: target->constln()->size() << (counter value) <= n
210
211 // counters for outgoing transitions
212 // Invariant: source->block->size() << (counter value) <= n
216
217 // counters for incoming transitions
218 // Invariant: target->block->size() << (counter value) <= n
221
222 // temporary transition counters for refine: similar to the temporary
223 // counters for states, we have a first group to store the work done
224 // for the smaller half, and temporary counters to store the work until
225 // it becomes clear which half wins.
226 // Because we have to sort the transitions into those to NewC, the
227 // outgoing and the incoming transitions, these counters are
228 // distributed above. The counters used to store the work done for
229 // the smaller half are: refine_outgoing_transition_3_6_or_23l,
230 // refine_outgoing_transition_to_marked_state_3_6l and
231 // refine_incoming_transition_3_18.
232
233 // temporary transition counters (blue):
238 // The work in the following counter is assigned to red (new
239 // bottom) states if the blue block is smaller!
241
242 // temporary transition counters (red):
246
247 // new bottom transition counters: every transition is visited once
248 // Invariant: If source is a non-bottom state, the counter is 0;
249 // otherwise, the counter is 0 or 1.
252 // For the following counters, we have an ``a priori'' and an ``a
253 // posteriori'' variant. The reason is, as explained with the
254 // B_to_C slice counters, that sometimes a constellation is
255 // reachable from the block of new bottom states but it is not yet
256 // clear which of the source states will become a new bottom state.
257 // In that case, the ``a posteriori'' counters are used. Later,
258 // the same block and the same constellation may be refined another
259 // time, but now with known new bottom states; then, the ``a
260 // priori'' counters are used.
267
268 /*-------------- counters for the bisim_jgkw algorithm --------------*/
269
270 // block counters
271 // Block counters are used to assign some work to each state in the
272 // block (and possibly, by transitivity, each incoming or outgoing
273 // transition of the block).
279
280 // state counters
281 // If every state of a block is handled by some loop, we
282 // abbreviate the counter to a block counter.
285
286 // temporary state counters (U-coroutine):
289
290 // temporary state counters (R-coroutine):
295
296 // bunch counters (only for small bunches, i. e. bunches that have been
297 // split off from a large bunch)
301
302 // block_bunch-slice counters (only for block_bunch-slices that are
303 // part of a small bunch)
314
315 // transition counters
316 // If every transition of a state is handled by some loop, we
317 // abbreviate the counter to a state counter (and possibly, by
318 // transitivity, to a block counter).
319 move_out_slice_to_new_block, // source block size
323
324 // temporary transition counters (U-coroutine):
328 // U: source block size
329
330 // temporary transition counters (R-coroutine):
334
335 // transition counters for new bottom states:
343 };
344
346 #define DONT_COUNT_TEMPORARY (std::numeric_limits<unsigned char>::max()-1)
347
351 static unsigned char log_n;
352
356 static int ilog2(state_type size)
357 {
358 #ifdef __GNUC__
359 if constexpr (sizeof(unsigned) == sizeof(size))
360 {
361 return sizeof(size) * CHAR_BIT - 1 - __builtin_clz(size);
362 }
363 else if constexpr (sizeof(unsigned long) == sizeof(size))
364 {
365 return sizeof(size) * CHAR_BIT - 1 - __builtin_clzl(size);
366 }
367 else if constexpr(sizeof(unsigned long long) == sizeof(size))
368 {
369 return sizeof(size) * CHAR_BIT - 1 - __builtin_clzll(size);
370 }
371 //#elif defined(_MSC_VER)
372 // if constexpr (sizeof(long) == sizeof(size))
373 // {
374 // long result;
375 // _BitScanReverse(result, size);
376 // return result - 1;
377 // }
378 // else if constexpr(sizeof(__int64) == sizeof(size))
379 // {
380 // long result;
381 // _BitScanReverse64(result, size);
382 // return result - 1;
383 // }
384 #endif
385 return (int) std::log2(size);
386 }
387
388 private:
393
394 public:
396 static const char *work_names[TRANS_dnj_MAX - BLOCK_MIN + 1];
397
403 {
404 assert(-1 <= sensible_work);
405 sensible_work = 0;
406 }
407
409 template <enum counter_type FirstCounter, enum counter_type LastCounter,
410 enum counter_type FirstTempCounter =
411 (enum counter_type) (LastCounter + 1),
412 enum counter_type FirstPostprocessCounter = FirstTempCounter>
414 {
415 static_assert(FirstCounter < FirstTempCounter);
416 static_assert(FirstTempCounter <= FirstPostprocessCounter);
417 static_assert(FirstPostprocessCounter <=
418 (enum counter_type) (LastCounter + 1));
419 public:
421 unsigned char counters[LastCounter - FirstCounter + 1];
422
433 bool cancel_work(enum counter_type const ctr)
434 {
435 assert(FirstTempCounter <= ctr);
436 assert(ctr < FirstPostprocessCounter);
437 if ((FirstTempCounter != TRANS_MIN_TEMP &&
438 FirstTempCounter != TRANS_dnj_MIN_TEMP) ||
439 DONT_COUNT_TEMPORARY != counters[ctr - FirstCounter])
440 {
441 assert(counters[ctr - FirstCounter] <= 1);
442 sensible_work -= counters[ctr - FirstCounter];
443 }
444 counters[ctr - FirstCounter] = 0;
445 return true;
446 }
447
448
464 enum counter_type const to, unsigned const max_value)
465 {
466 // assert(...) -- see move_work().
467 if ((FirstTempCounter != TRANS_MIN_TEMP &&
468 FirstTempCounter != TRANS_dnj_MIN_TEMP) ||
469 DONT_COUNT_TEMPORARY != counters[from - FirstCounter])
470 {
471 sensible_work += counters[from - FirstCounter];
472 }
473 else
474 {
475 counters[from - FirstCounter] = 1;
476 }
477 return move_work(from, to, max_value);
478 }
479
480
483 {
484 std::memset(counters, '\0', sizeof(counters));
485 }
486
487
501 bool add_work(enum counter_type const ctr, unsigned const max_value)
502 {
503 assert(FirstCounter <= ctr);
504 assert(ctr <= LastCounter);
505 assert(max_value <= (ctr < FirstTempCounter ? log_n : 1U));
506 if (counters[ctr - FirstCounter] >= max_value)
507 {
508 mCRL2log(log::error) << "Error 1: counter \""
509 << work_names[ctr - BLOCK_MIN] << "\" exceeded "
510 "maximum value (" << max_value << ") for ";
511 return false;
512 }
513 counters[ctr - FirstCounter] = max_value;
514 return true;
515 }
516
517
535 bool move_work(enum counter_type const from,
536 enum counter_type const to, unsigned const max_value)
537 {
538 assert(FirstTempCounter <= from);
539 assert(from < FirstPostprocessCounter);
540 assert(FirstCounter <= to);
541 assert(to <= LastCounter);
542 assert(max_value <= (to < FirstTempCounter ? log_n : 1U));
543 if (0 == counters[from - FirstCounter]) return true;
544 if (counters[to - FirstCounter] >= max_value)
545 {
546 mCRL2log(log::error) << "Error 2: counter \""
547 << work_names[to - BLOCK_MIN] << "\" exceeded "
548 "maximum value (" << max_value << ") for ";
549 return false;
550 }
551 /*
552 if ((FirstTempCounter == TRANS_MIN_TEMP ||
553 FirstTempCounter == TRANS_dnj_MIN_TEMP) &&
554 FirstTempCounter <= to && to < FirstPostprocessCounter &&
555 DONT_COUNT_TEMPORARY == counters[from - FirstCounter])
556 {
557 assert(1 == max_value);
558 // the next assertion is always satisfied if 1 == max_value.
559 // assert(0 == counters[to - FirstCounter]);
560 counters[to - FirstCounter] = DONT_COUNT_TEMPORARY;
561 }
562 else
563 */
564 {
565 counters[to - FirstCounter] = max_value;
566 assert(1 == counters[from - FirstCounter]);
567 }
568 counters[from - FirstCounter] = 0;
569 return true;
570 }
571 };
572
573
574 // usage of the functions below: as soon as the block is refined, one
575 // has to call state_counter_t::blue_is_smaller() or state_counter_t::
576 // red_is_smaller() for every state in the old and new block. Also, one
577 // needs to call trans_counter_t::blue_is_smaller() or trans_counter_t::
578 // red_is_smaller() for every incoming and outgoing transition in the old
579 // and new block. (Inert transitions need to be handled only once.) After
580 // that, one calls check_temporary_work() to verify that not too much
581 // work was done on the larger block.
582
587 class block_counter_t : public counter_t<BLOCK_MIN, BLOCK_MAX>
588 {
589 public:
606 bool no_temporary_work(unsigned const max_C, unsigned const max_B)
607 {
608 assert(max_C <= max_B);
609 for (enum counter_type ctr = BLOCK_MIN;
611 ctr = (enum counter_type) (ctr + 1))
612 {
613 assert(counters[ctr - BLOCK_MIN] <= max_C);
614 counters[ctr - BLOCK_MIN] = max_C;
615 }
616 assert(max_B <= log_n);
617 for (enum counter_type ctr =
619 ctr <= BLOCK_MAX; ctr = (enum counter_type) (ctr + 1))
620 {
621 assert(counters[ctr - BLOCK_MIN] <= max_B);
622 counters[ctr - BLOCK_MIN] = max_B;
623 }
624 return true;
625 }
626 };
627
632 class B_to_C_counter_t : public counter_t<B_TO_C_MIN, B_TO_C_MAX,
633 B_TO_C_MIN_TEMP, (enum counter_type) (B_TO_C_MAX_TEMP + 1)>
634 {
635 public:
649 bool no_temporary_work(unsigned const max_targetC)
650 {
651 assert(max_targetC <= log_n);
652 for (enum counter_type ctr = B_TO_C_MIN;
653 ctr < B_TO_C_MIN_TEMP; ctr = (enum counter_type) (ctr + 1))
654 {
655 assert(counters[ctr - B_TO_C_MIN] <= max_targetC);
656 counters[ctr - B_TO_C_MIN] = max_targetC;
657 }
658 for (enum counter_type ctr = B_TO_C_MIN_TEMP;
659 ctr <= B_TO_C_MAX_TEMP; ctr = (enum counter_type) (ctr + 1))
660 {
661 if (counters[ctr - B_TO_C_MIN] > 0)
662 {
663 mCRL2log(log::error) << "Error 3: counter \""
664 << work_names[ctr - BLOCK_MIN] << "\" exceeded "
665 "maximum value (" << 0 << ") for ";
666 return false;
667 }
668 }
669 static_assert(B_TO_C_MAX_TEMP == B_TO_C_MAX);
670 return true;
671 }
672
673
690 unsigned char get_work_counter_4_4() const
691 {
693 B_TO_C_MIN];
694 }
695
696
712 {
714 B_TO_C_MIN] = 0;
715 }
716 };
717 class state_counter_t : public counter_t<STATE_MIN, STATE_MAX,
718 STATE_MIN_TEMP, (enum counter_type) (STATE_MAX_TEMP + 1)>
719 {
720 public:
742 bool no_temporary_work(unsigned const max_B, bool const bottom)
743 {
744 assert(max_B <= log_n);
745 for (enum counter_type ctr = STATE_MIN;
746 ctr < STATE_MIN_TEMP; ctr = (enum counter_type) (ctr + 1))
747 {
748 assert(counters[ctr - STATE_MIN] <= max_B);
749 counters[ctr - STATE_MIN] = max_B;
750 }
751
752 // temporary state counters must be zero:
753 for (enum counter_type ctr = STATE_MIN_TEMP;
754 ctr <= STATE_MAX_TEMP; ctr = (enum counter_type) (ctr + 1))
755 {
756 if (counters[ctr - STATE_MIN] > 0)
757 {
758 mCRL2log(log::error) << "Error 4: counter \""
759 << work_names[ctr - BLOCK_MIN] << "\" exceeded "
760 "maximum value (" << 0 << ") for ";
761 return false;
762 }
763 }
764 // bottom state counters must be 0 for non-bottom states and 1 for
765 // bottom states:
766 // assert((unsigned) bottom <= 1);
767 for(enum counter_type ctr = (enum counter_type) (STATE_MAX_TEMP+1);
768 ctr <= STATE_MAX ; ctr = (enum counter_type) (ctr + 1))
769 {
770 if (counters[ctr - STATE_MIN] > (unsigned) bottom)
771 {
772 mCRL2log(log::error) << "Error 5: counter \""
773 << work_names[ctr - BLOCK_MIN] << "\" exceeded "
774 "maximum value (" << (unsigned) bottom << ") for ";
775 return false;
776 }
777 counters[ctr - STATE_MIN] = (unsigned) bottom;
778 }
779 return true;
780 }
781 };
782 class trans_counter_t : public counter_t<TRANS_MIN, TRANS_MAX,
783 TRANS_MIN_TEMP, (enum counter_type) (TRANS_MAX_TEMP + 1)>
784 {
785 public:
818 bool no_temporary_work(unsigned const max_sourceB,
819 unsigned const max_targetC,
820 unsigned const max_targetB, bool const source_bottom)
821 {
822 assert(max_targetC <= max_targetB);
823 for (enum counter_type ctr = TRANS_MIN;
825 ctr = (enum counter_type) (ctr + 1))
826 {
827 assert(counters[ctr - TRANS_MIN] <= max_targetC);
828 counters[ctr - TRANS_MIN] = max_targetC;
829 }
830 assert(max_sourceB <= log_n);
833 ctr = (enum counter_type) (ctr + 1))
834 {
835 assert(counters[ctr - TRANS_MIN] <= max_sourceB);
836 counters[ctr - TRANS_MIN] = max_sourceB;
837 }
838 assert(max_targetB <= log_n);
840 ctr < TRANS_MIN_TEMP; ctr = (enum counter_type) (ctr + 1))
841 {
842 assert(counters[ctr - TRANS_MIN] <= max_targetB);
843 counters[ctr - TRANS_MIN] = max_targetB;
844 }
845 // temporary transition counters must be zero
846 for (enum counter_type ctr = TRANS_MIN_TEMP;
847 ctr <= TRANS_MAX_TEMP; ctr = (enum counter_type)(ctr + 1))
848 {
849 if (counters[ctr - TRANS_MIN] > 0)
850 {
851 mCRL2log(log::error) << "Error 6: counter \""
852 << work_names[ctr - BLOCK_MIN] << "\" exceeded "
853 "maximum value (" << 0 << ") for ";
854 return false;
855 }
856 }
857 // bottom state counters must be 0 for transitions from non-bottom
858 // states and 1 for other transitions
859 assert((unsigned) source_bottom <= 1);
860 for(enum counter_type ctr = (enum counter_type) (TRANS_MAX_TEMP+1);
861 ctr <= TRANS_MAX ; ctr = (enum counter_type) (ctr + 1))
862 {
863 if (counters[ctr - TRANS_MIN] > (unsigned) source_bottom)
864 {
865 mCRL2log(log::error) << "Error 7: counter \""
866 << work_names[ctr - BLOCK_MIN] << "\" exceeded "
867 "maximum value (" << (unsigned) source_bottom << ") for ";
868 return false;
869 }
870 counters[ctr - TRANS_MIN] = (unsigned) source_bottom;
871 }
872 return true;
873 }
874
875
895 unsigned const max_value)
896 {
897 if (TRANS_MIN_TEMP > ctr || ctr > TRANS_MAX_TEMP)
898 {
900 }
901
902 assert(1 == max_value);
903 if (0 == counters[ctr - TRANS_MIN])
904 {
906 return true;
907 }
908
909 mCRL2log(log::error) << "Error 8: counter \""
910 << work_names[ctr - BLOCK_MIN] << "\" exceeded "
911 "maximum value (" << max_value << ") for ";
912 return false;
913 }
914 };
915
916 /*----------------- class specialisations for bisim_dnj -----------------*/
917
918 class block_dnj_counter_t : public counter_t<BLOCK_dnj_MIN, BLOCK_dnj_MAX,
919 create_initial_partition>
920 {
921 public:
937 bool no_temporary_work(unsigned const max_block)
938 {
939 assert((log_n + 1U) / 2U <= max_block);
940 if (max_block > log_n)
941 {
942 mCRL2log(log::error) << "Error 14: max_block == "
943 << max_block << " exceeded log_n == "
944 << (unsigned) log_n << " for ";
945 return false;
946 }
947 assert(max_block <= log_n);
948 for (enum counter_type ctr = BLOCK_dnj_MIN;
950 ctr = (enum counter_type) (ctr + 1))
951 {
952 assert(counters[ctr - BLOCK_dnj_MIN] <= max_block);
953 counters[ctr - BLOCK_dnj_MIN] = max_block;
954 }
956 ctr <= BLOCK_dnj_MAX; ctr = (enum counter_type) (ctr + 1))
957 {
958 assert(counters[ctr - BLOCK_dnj_MIN] <= 1);
959 counters[ctr - BLOCK_dnj_MIN] = 1;
960 }
961 return true;
962 }
963 };
964
965 class state_dnj_counter_t : public counter_t<STATE_dnj_MIN, STATE_dnj_MAX,
966 STATE_dnj_MIN_TEMP, (enum counter_type) (STATE_dnj_MAX_TEMP + 1)>
967 {
968 public:
984 bool no_temporary_work(unsigned const max_block, bool const bottom)
985 {
986 assert((log_n + 1U) / 2U <= max_block);
987 assert(max_block <= log_n);
988 for (enum counter_type ctr = STATE_dnj_MIN;
989 ctr < STATE_dnj_MIN_TEMP; ctr = (enum counter_type) (ctr + 1))
990 {
991 assert(counters[ctr - STATE_dnj_MIN] <= max_block);
992 counters[ctr - STATE_dnj_MIN] = max_block;
993 }
994 for (enum counter_type ctr = STATE_dnj_MIN_TEMP;
995 ctr <= STATE_dnj_MAX_TEMP; ctr = (enum counter_type) (ctr + 1))
996 {
997 assert(counters[ctr - STATE_dnj_MIN] <= 0);
998 }
999 // assert((unsigned) bottom <= 1);
1000 for (enum counter_type ctr =
1001 (enum counter_type) (STATE_dnj_MAX_TEMP + 1);
1002 ctr <= STATE_dnj_MAX; ctr = (enum counter_type) (ctr + 1))
1003 {
1004 assert(counters[ctr - STATE_dnj_MIN] <= (unsigned) bottom);
1005 counters[ctr - STATE_dnj_MIN] = (unsigned) bottom;
1006 }
1007 return true;
1008 }
1009 };
1010
1011 class bunch_dnj_counter_t : public counter_t<BUNCH_dnj_MIN, BUNCH_dnj_MAX>
1012 {
1013 public:
1029 bool no_temporary_work(unsigned const max_bunch)
1030 {
1031 assert(max_bunch <= log_n);
1032 for (enum counter_type ctr = BUNCH_dnj_MIN;
1033 ctr <= BUNCH_dnj_MAX; ctr = (enum counter_type) (ctr + 1))
1034 {
1035 assert(counters[ctr - BUNCH_dnj_MIN] <= max_bunch);
1036 counters[ctr - BUNCH_dnj_MIN] = max_bunch;
1037 }
1038 return true;
1039 }
1040 };
1041
1042 class block_bunch_dnj_counter_t : public counter_t<BLOCK_BUNCH_dnj_MIN,
1043 BLOCK_BUNCH_dnj_MAX, BLOCK_BUNCH_dnj_MIN_TEMP,
1044 (enum counter_type) (BLOCK_BUNCH_dnj_MAX_TEMP + 1)>
1045 {
1046 public:
1062 bool no_temporary_work(unsigned const max_bunch)
1063 {
1064 assert(max_bunch <= log_n);
1065 for (enum counter_type ctr = BLOCK_BUNCH_dnj_MIN;
1067 ctr = (enum counter_type) (ctr + 1))
1068 {
1069 if (counters[ctr - BLOCK_BUNCH_dnj_MIN] > max_bunch)
1070 {
1071 mCRL2log(log::error) << "Error 12: counter \""
1072 << work_names[ctr - BLOCK_MIN] << "\" exceeded "
1073 "maximum value (" << (unsigned) max_bunch << ") for ";
1074 return false;
1075 }
1076 assert(counters[ctr - BLOCK_BUNCH_dnj_MIN] <= max_bunch);
1077 counters[ctr - BLOCK_BUNCH_dnj_MIN] = max_bunch;
1078 }
1079 for (enum counter_type ctr = BLOCK_BUNCH_dnj_MIN_TEMP;
1080 ctr <= BLOCK_BUNCH_dnj_MAX; ctr = (enum counter_type) (ctr + 1))
1081 {
1082 if (counters[ctr - BLOCK_BUNCH_dnj_MIN] > 0)
1083 {
1084 mCRL2log(log::error) << "Error 13: counter \""
1085 << work_names[ctr - BLOCK_MIN] << "\" exceeded "
1086 "maximum value (" << (unsigned) 0 << ") for ";
1087 return false;
1088 }
1089 assert(counters[ctr - BLOCK_BUNCH_dnj_MIN] <= 0);
1090 }
1092 return true;
1093 }
1094
1096 {
1099 }
1101 {
1104 }
1105 };
1106
1107 class trans_dnj_counter_t : public counter_t<TRANS_dnj_MIN, TRANS_dnj_MAX,
1108 TRANS_dnj_MIN_TEMP, (enum counter_type) (TRANS_dnj_MAX_TEMP + 1)>
1109 {
1110 public:
1128 bool no_temporary_work(unsigned const max_source_block,
1129 unsigned const max_target_block, bool const bottom)
1130 {
1131 assert((log_n + 1U) / 2U <= max_source_block);
1132 assert(max_source_block <= log_n);
1133 for (enum counter_type ctr = TRANS_dnj_MIN;
1135 ctr = (enum counter_type) (ctr + 1))
1136 {
1137 assert(counters[ctr - TRANS_dnj_MIN] <= max_source_block);
1138 counters[ctr - TRANS_dnj_MIN] = max_source_block;
1139 }
1140 assert((log_n + 1U) / 2U <= max_target_block);
1141 assert(max_target_block <= log_n);
1143 ctr < TRANS_dnj_MIN_TEMP;
1144 ctr = (enum counter_type) (ctr + 1))
1145 {
1146 assert(counters[ctr - TRANS_dnj_MIN] <= max_target_block);
1147 counters[ctr - TRANS_dnj_MIN] = max_target_block;
1148 }
1149 for (enum counter_type ctr = TRANS_dnj_MIN_TEMP;
1150 ctr <= TRANS_dnj_MAX_TEMP; ctr = (enum counter_type) (ctr + 1))
1151 {
1152 assert(counters[ctr - TRANS_dnj_MIN] <= 0);
1153 }
1154 // assert((unsigned) bottom <= 1);
1155 for (enum counter_type ctr =
1156 (enum counter_type) (TRANS_dnj_MAX_TEMP + 1);
1157 ctr <= TRANS_dnj_MAX; ctr = (enum counter_type) (ctr + 1))
1158 {
1159 if (counters[ctr - TRANS_dnj_MIN] > (unsigned) bottom)
1160 {
1161 mCRL2log(log::error) << "Error 11: counter \""
1162 << work_names[ctr - BLOCK_MIN] << "\" exceeded "
1163 "maximum value (" << (unsigned) bottom << ") for ";
1164 return false;
1165 }
1166 counters[ctr - TRANS_dnj_MIN] = (unsigned) bottom;
1167 }
1168 return true;
1169 }
1170
1190 unsigned const max_value)
1191 {
1192 if (TRANS_dnj_MIN_TEMP > ctr || ctr > TRANS_dnj_MAX_TEMP)
1193 {
1195 }
1196
1197 assert(1 == max_value);
1198 if (0 == counters[ctr - TRANS_dnj_MIN])
1199 {
1201 return true;
1202 }
1203
1204 mCRL2log(log::error) << "Error 9: counter \""
1205 << work_names[ctr - BLOCK_MIN] << "\" exceeded "
1206 "maximum value (" << max_value << ") for ";
1207 return false;
1208 }
1209 };
1210
1211 #if 0
1216 static void test_work_names();
1217 #endif
1218
1219
1224 static void init(state_type n)
1225 {
1226 #if 0
1227 // as debugging measure:
1228 test_work_names();
1229 #endif
1230
1231 log_n = ilog2(n);
1232 assert(0 == sensible_work); sensible_work = 0;
1233 }
1234
1235
1248 #define mCRL2complexity(unit, call, ...) \
1249 do \
1250 { \
1251 if (!((unit)->work_counter. call )) \
1252 { \
1253 mCRL2log(log::error)<<(unit)->debug_id(__VA_ARGS__)<<'\n';\
1254 exit(EXIT_FAILURE); \
1255 } \
1256 /* else \
1257 { \
1258 mCRL2log(log::debug, "bisim_dnj") << "mCRL2complexity(" \
1259 << (unit)->debug_id(__VA_ARGS__) << ", " #call ")\n";\
1260 } */ \
1261 } \
1262 while (0)
1263
1264};
1265
1266} // end namespace bisim_gjkw
1267
1268#else // ifndef NDEBUG
1269
1270 #define mCRL2complexity(unit, call, ...) /* ignore unit and call */
1271
1272#endif // ifndef NDEBUG
1273
1274} // end namespace detail
1275} // end namespace lts
1276} // end namespace mcrl2
1277
1278#endif // ifndef _COUNT_ITERATIONS_H
#define DONT_COUNT_TEMPORARY
special value for temporary work without changing the balance
bool no_temporary_work(unsigned const max_targetC)
ensures there is no orphaned temporary work counter
unsigned char get_work_counter_4_4() const
returns the temporary counter associated with line 4.4
void reset_work_counter_4_4()
sets the temporary counter associated with line 4.4 to zero
bool no_temporary_work(unsigned const max_bunch)
ensures there is no orphaned temporary work counter
bool no_temporary_work(unsigned const max_C, unsigned const max_B)
ensures there is no orphaned temporary work counter
bool no_temporary_work(unsigned const max_block)
ensures there is no orphaned temporary work counter
bool no_temporary_work(unsigned const max_bunch)
ensures there is no orphaned temporary work counter
subset of counters (to be associated with a state or transition)
bool finalise_work(enum counter_type const from, enum counter_type const to, unsigned const max_value)
move temporary work to its final counter
unsigned char counters[LastCounter - FirstCounter+1]
actual space to store the counters
bool add_work(enum counter_type const ctr, unsigned const max_value)
register work with some counter
bool cancel_work(enum counter_type const ctr)
cancel temporary work
bool move_work(enum counter_type const from, enum counter_type const to, unsigned const max_value)
move temporary work to another counter
counter_t()
constructor, initializes all counters to 0
bool no_temporary_work(unsigned const max_B, bool const bottom)
ensures there is no orphaned temporary work counter
bool no_temporary_work(unsigned const max_block, bool const bottom)
ensures there is no orphaned temporary work counter
bool no_temporary_work(unsigned const max_sourceB, unsigned const max_targetC, unsigned const max_targetB, bool const source_bottom)
ensures there is no orphaned temporary work counter
bool add_work_notemporary(enum counter_type const ctr, unsigned const max_value)
register work with some temporary counter without changing the balance between sensible and superfluo...
bool no_temporary_work(unsigned const max_source_block, unsigned const max_target_block, bool const bottom)
ensures there is no orphaned temporary work counter
bool add_work_notemporary(enum counter_type const ctr, unsigned const max_value)
register work with some temporary counter without changing the balance between sensible and superfluo...
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 signed_trans_type sensible_work
counter to register the work balance for coroutines
counter_type
Type for complexity budget counters.
static unsigned char log_n
value of floor(log2(n)) for easy access
static const char * work_names[TRANS_dnj_MAX - BLOCK_MIN+1]
printable names of the counter types (for error messages)
static void check_temporary_work()
check that not too much superfluous work has been done
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
std::size_t state_type
type used to store state (numbers and) counts
std::size_t trans_type
type used to store transition (numbers and) counts
std::ptrdiff_t signed_trans_type
type used to store differences between transition counters
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator &i)
From state of an iterator exploring transitions per outgoing state and action.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72