- Generated by
1.9.7
|
mCRL2
|
helper class for time complexity checks during test runs More...
Go to the source code of this file.
Namespaces | |
| namespace | mcrl2 |
| A class that takes a linear process specification and checks all tau-summands of that LPS for confluence. | |
| namespace | mcrl2::lts |
| The main LTS namespace. | |
| namespace | mcrl2::lts::detail |
| A base class for the lts_dot labelled transition system. | |
Macros | |
| #define | STATE_TYPE_MIN (std::numeric_limits<state_type>::min()) |
| #define | STATE_TYPE_MAX (std::numeric_limits<state_type>::max()) |
| #define | TRANS_TYPE_MIN (std::numeric_limits<trans_type>::min()) |
| #define | TRANS_TYPE_MAX (std::numeric_limits<trans_type>::max()) |
| #define | DONT_COUNT_TEMPORARY (std::numeric_limits<unsigned char>::max()-1) |
| special value for temporary work without changing the balance | |
| #define | mCRL2complexity(unit, call, info_for_debug) |
| Assigns work to a counter and checks for errors. | |
Typedefs | |
| typedef std::size_t | mcrl2::lts::detail::state_type |
| type used to store state (numbers and) counts | |
| typedef std::size_t | mcrl2::lts::detail::trans_type |
| type used to store transition (numbers and) counts | |
| typedef std::make_signed< trans_type >::type | mcrl2::lts::detail::signed_trans_type |
| type used to store differences between transition counters | |
helper class for time complexity checks during test runs
We use the class in this file to check whether the overall time complexity fits in O(m log n). Although it is difficult to test this in general because of the constant factor in the definition of the O() notation, it is often possible to give a (rather tight) upper bound on the number of iterations of most loops.
The principle of time measurement with this file is: the work done in every loop body is assigned to a state or a transition. Every state and every transition gets a counter for every loop body which is assigned to it. When the loop body is executed, the corresponding counter is increased. When increasing a counter, a new value is assigned, based on the logarithm of the size of the corresponding block (or constellation). If the new value is not actually larger than the old one, an error is raised. The new value never is allowed to become larger than log2(n), so we have: For every counter, its value is increased at most log2(n) times, and therefore no more than log2(n) steps (of a certain kind) can be assigned to any single state or transition.
Note that an `‘increase’' is by at least 1, but it may be more than 1. If one always increases to the maximal allowed value, it is ensured that a very small block found early will only incur work that corresponds to its own size (and not to the size of the block from which it was split off).
To assign work to some unit, write mCRL2complexity(unit, add_work(counter type, new counter value), ...); The unit is a state or transition; the counter type is a value of enum check_complexity::counter_type defined below; the new counter value typically is check_complexity::log_n - check_complexity::ilog2(block size). In the place of ..., write parameters which might occur in unit->debug_id(...).
For coroutines, there is an additional provision: work can temporarily be recorded in some special counters. As soon as it becomes clear which coroutine (the one handling red states or the one handling blue states, in our case) is faster, its counters are transferred to normal counters and the counters of the other coroutine are cancelled. It is checked that not too many counters are cancelled.
To transfer work from a temporary to a normal counter, one uses finalise_work(). To cancel counters, use cancel_work(). (The file liblts_bisim_gjkw.cpp contains wrapper functions blue_is_smaller() and red_is_smaller() that call finalise_work() and cancel_work().) After all temporary work has been handled, call check_temporary_work() to compare the amount of sensible work with the amount of cancelled work.
If the work could be assigned to one of several counters (in particular, to any one transition out of a set of transitions), I recommend to assign it to all of them; otherwise, it may happen that a later excess of the time budget goes unnoticed because too few counters were advanced. This, however, poses some difficulties when using temporary counters: a single unit of work should be assigned to multiple counters, but added to the balance between sensible and superfluous work only once. A variant of add_work(), namely add_work_notemporary(), can be called in that case: it assigns a special value DONT_COUNT_TEMPORARY to a temporary counter meaning that it should be disregarded in the calculation of the balance.
Definition in file check_complexity.h.
| #define DONT_COUNT_TEMPORARY (std::numeric_limits<unsigned char>::max()-1) |
special value for temporary work without changing the balance
Definition at line 445 of file check_complexity.h.
| #define mCRL2complexity | ( | unit, | |
| call, | |||
| info_for_debug | |||
| ) |
Assigns work to a counter and checks for errors.
Many functions that assign work to a counter actually return true if everything is ok and false if the counter was too large. In the latter case, they also print the start of an error message (`‘Counter ... too large’'), but as they do not know to which larger unit (state, transition etc.) the counter belongs, this macro prints the end of the error message and aborts the program with a return code indicating failure.
If debugging is off, the macro is translated to do nothing.
| unit | the unit to which work is assigned |
| call | a function call that assigns work to a counter of unit |
Definition at line 1662 of file check_complexity.h.
| #define STATE_TYPE_MAX (std::numeric_limits<state_type>::max()) |
Definition at line 99 of file check_complexity.h.
| #define STATE_TYPE_MIN (std::numeric_limits<state_type>::min()) |
Definition at line 98 of file check_complexity.h.
| #define TRANS_TYPE_MAX (std::numeric_limits<trans_type>::max()) |
Definition at line 109 of file check_complexity.h.
| #define TRANS_TYPE_MIN (std::numeric_limits<trans_type>::min()) |
Definition at line 108 of file check_complexity.h.
1.9.7