mCRL2
Loading...
Searching...
No Matches
check_complexity.h File Reference

helper class for time complexity checks during test runs More...

Go to the source code of this file.

Classes

class  mcrl2::lts::detail::bisim_gjkw::check_complexity
 class for time complexity checks More...
 
class  mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter >
 subset of counters (to be associated with a state or transition) More...
 
class  mcrl2::lts::detail::bisim_gjkw::check_complexity::block_counter_t
 counters for a block More...
 
class  mcrl2::lts::detail::bisim_gjkw::check_complexity::B_to_C_counter_t
 counters for a B_to_C slice More...
 
class  mcrl2::lts::detail::bisim_gjkw::check_complexity::state_counter_t
 
class  mcrl2::lts::detail::bisim_gjkw::check_complexity::trans_counter_t
 
class  mcrl2::lts::detail::bisim_gjkw::check_complexity::block_dnj_counter_t
 
class  mcrl2::lts::detail::bisim_gjkw::check_complexity::state_dnj_counter_t
 
class  mcrl2::lts::detail::bisim_gjkw::check_complexity::bunch_dnj_counter_t
 
class  mcrl2::lts::detail::bisim_gjkw::check_complexity::block_bunch_dnj_counter_t
 
class  mcrl2::lts::detail::bisim_gjkw::check_complexity::trans_dnj_counter_t
 

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.
 
namespace  mcrl2::lts::detail::bisim_gjkw
 

Macros

#define STATE_TYPE_MIN   ((state_type) 0)
 
#define STATE_TYPE_MAX   SIZE_MAX
 
#define TRANS_TYPE_MIN   ((trans_type) 0)
 
#define TRANS_TYPE_MAX   SIZE_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, ...)
 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::ptrdiff_t mcrl2::lts::detail::signed_trans_type
 type used to store differences between transition counters
 

Detailed Description

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(). (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.

Author
David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands

Definition in file check_complexity.h.

Macro Definition Documentation

◆ DONT_COUNT_TEMPORARY

#define DONT_COUNT_TEMPORARY   (std::numeric_limits<unsigned char>::max()-1)

special value for temporary work without changing the balance

Definition at line 346 of file check_complexity.h.

◆ mCRL2complexity

#define mCRL2complexity (   unit,
  call,
  ... 
)
Value:
do \
{ \
if (!((unit)->work_counter. call )) \
{ \
mCRL2log(log::error)<<(unit)->debug_id(__VA_ARGS__)<<'\n';\
exit(EXIT_FAILURE); \
} \
/* else \
{ \
mCRL2log(log::debug, "bisim_dnj") << "mCRL2complexity(" \
<< (unit)->debug_id(__VA_ARGS__) << ", " #call ")\n";\
} */ \
} \
while (0)

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.

Parameters
unitthe unit to which work is assigned
calla function call that assigns work to a counter of unit

Definition at line 1248 of file check_complexity.h.

◆ STATE_TYPE_MAX

#define STATE_TYPE_MAX   SIZE_MAX

Definition at line 93 of file check_complexity.h.

◆ STATE_TYPE_MIN

#define STATE_TYPE_MIN   ((state_type) 0)

Definition at line 92 of file check_complexity.h.

◆ TRANS_TYPE_MAX

#define TRANS_TYPE_MAX   SIZE_MAX

Definition at line 100 of file check_complexity.h.

◆ TRANS_TYPE_MIN

#define TRANS_TYPE_MIN   ((trans_type) 0)

Definition at line 99 of file check_complexity.h.