mCRL2
|
#include <check_complexity.h>
Public Member Functions | |
bool | no_temporary_work (unsigned const max_block) |
ensures there is no orphaned temporary work counter | |
Public Member Functions inherited from mcrl2::lts::detail::check_complexity::counter_t< BLOCK_dnj_MIN, BLOCK_dnj_MAX, create_initial_partition > | |
bool | cancel_work (enum counter_type const ctr) |
cancel temporary work | |
bool | finalise_work (enum counter_type const from, enum counter_type const to, unsigned const max_value) |
move temporary work to its final counter | |
counter_t () | |
constructor, initializes all counters to 0 | |
bool | add_work (enum counter_type const ctr, unsigned const max_value) |
register work with some counter | |
bool | move_work (enum counter_type const from, enum counter_type const to, unsigned const max_value) |
move temporary work to another counter | |
Additional Inherited Members | |
Public Attributes inherited from mcrl2::lts::detail::check_complexity::counter_t< BLOCK_dnj_MIN, BLOCK_dnj_MAX, create_initial_partition > | |
unsigned char | counters [LastCounter - FirstCounter+1] |
actual space to store the counters | |
Definition at line 1025 of file check_complexity.h.
|
inline |
ensures there is no orphaned temporary work counter
When a refinement has finished, all work registered with temporary counters should have been moved to normal counters. This function verifies this property. The function additionally ensures that no work counter exceeds its maximal allowed value, based on the size of the block or its constellation. (The size of the constellation is the unit used for counters related to [blocks in the] splitter constellation; the size of the block is used for other counters.)
max_block | ilog2(n^2) - ilog2(size of block) |
mCRL2complexity()
, because that macro will print the remainder of the error message as needed. Definition at line 1044 of file check_complexity.h.