- 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. | |
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).
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(). These functions are not normally called directly, but through red_is_smaller() or blue_is_smaller(): If the red subblock is smaller, call red_is_smaller(temporary counter, normal counter, new counter value) for each state and each transition of the block that was refined; if the blue subblock is smaller, call blue_is_smaller(...). 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, 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.cpp.
1.9.7