mCRL2
Loading...
Searching...
No Matches
check_complexity.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
71
72
74
75namespace mcrl2
76{
77namespace lts
78{
79namespace detail
80{
81namespace bisim_gjkw
82{
83
84#ifndef NDEBUG
85
87unsigned char check_complexity::log_n = '\0';
88
91
99const char *check_complexity::work_names[TRANS_dnj_MAX - BLOCK_MIN + 1] =
100{
101 // block counters
102 "2.4: while C contains a nontrivial constellation",
103 "2.10: for all s in SpB",
104 "3.29: Move Blue/Red to a new block NewB (set pointers to new block)",
105 "3.29: Move Blue/Red to a new block NewB (for all states s in NewB)",
106 "3.31: for all s in NewB",
107
108 // state counters
109 "3.29: Move Blue/Red to a new block NewB (swap states)",
110
111 "3.6l: refine bottom state",
112 "3.15: refine visited state",
113
114 // temporary state counters (blue):
115 "3.6l: while Test is not empty (3.11l: s is blue)",
116 "3.15l: while Blue contains unvisited states",
117
118 // temporary state counters (red):
119 "3.15r: while Red contains unvisited states",
120
121 // new bottom state counters: every state is visited once
122 "4.8: for all bottom states s in RfnB",
123 "4.15: for all old bottom states s in RedB (self-loop)",
124
125 // B_to_C_descriptor counters
126 "2.20: for all refinable blocks RfnB",
127 "2.17: Register that inert transitions from s go to NewC (B_to_C)",
128 "4.4: for all constellations C not in R reachable from RfnB",
129
130 // transition counters: every transition is visited O(log n) times
131 "2.11: for all s_prime in in(s)",
132 "2.17: Register that inert transitions from s go to NewC (out)",
133 "2.17: Register that inert transitions from s go to NewC (swap "
134 "transitions)",
135 "3.6l: refine outgoing transition to marked state",
136
137 "3.6/3.23l: refine outgoing transition",
138 "3.29: Move Blue/Red to a new block NewB (for all transitions in out(s))",
139 "3.32r: for all s_prime in out(s)",
140
141 "3.18: refine incoming transition",
142 "3.32l: for all s_prime in in(s)",
143
144 // temporary transition counters (blue):
145 "3.6l: while Test is not empty (3.9l: s is red)",
146 "3.6l: while Test is not empty (3.9l: s is red) during postprocessing",
147 "3.18l: for all s_prime in in(s) \\ Red",
148 "3.23l: if ... s_prime has no transition to SpC",
149
150 // temporary transition counters (red):
151 "3.6r: while FromRed is not empty",
152 "3.18r: for all s_prime in in(s)",
153
154 // new bottom transition counters: every transition is visited once
155 "3.6l: refine outgoing transition (called from PostprocessNewBottom)",
156 "3.23l: refine outgoing transition (state is new bottom state)",
157 "4.4: for all transitions from new bottom states (a priori)",
158 "4.4: for all transitions from new bottom states (a posteriori)",
159 "4.12: for all blocks B with transitions to SpC that need postprocessing "
160 "(a priori)",
161 "4.12: for all blocks B with transitions to SpC that need postprocessing "
162 "(a posteriori)",
163 "4.15: for all old bottom states s in RedB",
164
165 /*---------------- counters for the bisim_jgkw algorithm ----------------*/
166
167 // block counters
168 "split_off_block()",
169 "adapt_transitions_for_new_block()",
170 "create_initial_partition()",
171
172 // state counters
173 "split(), find predecessors of a state in the smaller subblock",
174 "split(), while U-coroutine runs, find predecessors of a U-state",
175 "split(), while R-coroutine runs, find predecessors of a R-state",
176 "handle_new_noninert_transns()",
177
178 // bunch counters (only for small bunches, i. e. bunches that have been
179 // split off from a large bunch)
180 "refine_partition_until_it_becomes_stable(), find predecessors",
181
182 // block_bunch-slice counters (only for block_bunch-slices that are
183 // part of a small bunch)
184 "refine_partition_until_it_becomes_stable(), stabilize",
185 "refine_partition_until_it_becomes_stable(), stabilize for large splitter",
186 "handle_new_noninert_transns(), make block_bunch-slice without bottom "
187 "states unstable (temporary counter)",
188
189 // transition counters
190 "move_out_slice_to_new_block()",
191 "split(), handle a transition from a state in the smaller subblock",
192 "split(), handle a transition to a state in the smaller subblock",
193 "split(), while U-coroutine runs, handle a transition to a U-state",
194 "split(), while U-coroutine runs, test noninert outgoing transitions",
195 "split(), while R-coroutine runs, handle a transition from a R-state",
196 "split(), while R-coroutine runs, handle a transition to a R-state",
197 "split(), the test for noninert transitions found a new bottom state",
198 "handle_new_noninert_transns(), make block_bunch-slice with bottom states "
199 "unstable",
200 "handle_new_noninert_transns(), make block_bunch-slice without bottom "
201 "states unstable (final counter)",
202 "refine_partition_until_it_becomes_stable(), stabilize block with bottom "
203 "states for new non-inert transitions",
204 "refine_partition_until_it_becomes_stable(), stabilize block without "
205 "bottom states for new non-inert transitions"
206};
207
208
209#if 0
211#define test_work_name(var, ctr) \
212 do \
213 { \
214 assert((var) == ctr); \
215 mCRL2log(log::debug, "bisim_gjkw") << "work_names[" #ctr "] = \"" \
216 << work_names[ctr] << "\".\n";\
217 (var) = (enum counter_type) ((var) + 1); \
218 } \
219 while (0)
220
221
232void check_complexity::test_work_names()
233{
235 // block counters
236 assert(check_complexity::BLOCK_MIN == i);
238 test_work_name(i, for_all_s_in_SpB_2_10);
241 test_work_name(i, for_all_s_in_NewB_3_31);
242 assert(check_complexity::BLOCK_MAX + 1 == i);
243
244 // state counters
245 assert(check_complexity::STATE_MIN == i);
247 test_work_name(i, refine_bottom_state_3_6l);
248 test_work_name(i, refine_visited_state_3_15);
249
250 // temporary state counters (blue):
253
254 // temporary state counters (red):
256
257 // new bottom state counters
258 test_work_name(i, for_all_bottom_states_s_in_RfnB_4_8);
260 assert(check_complexity::STATE_MAX + 1 == i);
261
262 // B_to_C_descriptor counters
263 assert(check_complexity::B_TO_C_MIN == i);
264 test_work_name(i, for_all_refinable_blocks_RfnB_2_20);
265 test_work_name(i,
267 // temporary B_to_C_descriptor counters
269 assert(check_complexity::B_TO_C_MAX + 1 == i);
270
271 // transition counters
272 assert(check_complexity::TRANS_MIN == i);
273 test_work_name(i, for_all_s_prime_in_pred_s_2_11);
274 test_work_name(i,
276 test_work_name(i,
279
280 test_work_name(i, refine_outgoing_transition_3_6_or_23l);
282 test_work_name(i, for_all_s_prime_in_succ_s_3_32r);
283
284 test_work_name(i, refine_incoming_transition_3_18);
285 test_work_name(i, for_all_s_prime_in_pred_s_3_32l);
286
287 // temporary transition counters (blue):
290 test_work_name(i,
294
295 // temporary transition counters (red):
296 test_work_name(i, while_FromRed_is_not_empty_3_6r);
297 test_work_name(i, for_all_s_prime_in_pred_s_3_18r);
298 assert(check_complexity::TRANS_MAX_TEMP + 1 == i);
299
300 // new bottom transition counters
308 assert(check_complexity::TRANS_MAX + 1 == i);
309
310 /*---------------- counters for the bisim_jgkw algorithm ----------------*/
311
312 // block counters
314 test_work_name(i, split_off_block);
315 test_work_name(i, adapt_transitions_for_new_block);
316 test_work_name(i, create_initial_partition);
317 assert(check_complexity::BLOCK_dnj_MAX + 1 == i);
318
319 // state counters
323 test_work_name(i, split_U__find_predecessors_of_U_state);
324 test_work_name(i, split_R__find_predecessors_of_R_state);
326 test_work_name(i, handle_new_noninert_transns);
327 assert(check_complexity::STATE_dnj_MAX + 1 == i);
328
329 // bunch counters (only for small bunches, i. e. bunches that have been
330 // split off from a large bunch)
333 assert(check_complexity::BUNCH_dnj_MAX + 1 == i);
334
335 // block_bunch-slice counters (only for block_bunch-slices that are
336 // part of a small bunch)
339 test_work_name(i,
345
346 // transition counters
348 test_work_name(i, move_out_slice_to_new_block);
352 test_work_name(i, split_U__handle_transition_to_U_state);
353 test_work_name(i, split_U__test_noninert_transitions);
355 test_work_name(i, split_R__handle_transition_to_R_state);
360 test_work_name(i,
362 test_work_name(i,
364 assert(check_complexity::TRANS_dnj_MAX + 1 == i);
365
366 exit(EXIT_SUCCESS);
367}
368#endif // #if 0
369
370#endif // #ifndef NDEBUG
371
372} // end namespace bisim_gjkw
373} // end namespace detail
374} // end namespace lts
375} // end namespace mcrl2
helper class for time complexity checks during test runs
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)
std::ptrdiff_t signed_trans_type
type used to store differences between transition counters
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72