counters for a block More...
#include <check_complexity.h>
Public Member Functions | |
| result_type | no_temporary_work (unsigned const max_C, unsigned const max_B) |
| ensures there is no orphaned temporary work counter | |
 Public Member Functions inherited from mcrl2::lts::detail::check_complexity::counter_t< BLOCK_MIN, BLOCK_MAX > | |
| result_type | cancel_work (enum counter_type const ctr) |
| cancel temporary work | |
| result_type | 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 | |
| result_type | add_work (enum counter_type const ctr, unsigned const max_value) |
| register work with some counter | |
Additional Inherited Members | |
| Public Attributes inherited from mcrl2::lts::detail::check_complexity::counter_t< BLOCK_MIN, BLOCK_MAX > | |
| unsigned char | counters [LastCounter - FirstCounter+1] |
| actual space to store the counters | |
| Protected Member Functions inherited from mcrl2::lts::detail::check_complexity::counter_t< BLOCK_MIN, BLOCK_MAX > | |
| result_type | move_work (enum counter_type const from, enum counter_type const to, unsigned const max_value) |
| move temporary work to another counter | |
Detailed Description
counters for a block
The counters stored with a block are meant to be assigned to each state in the block. This means that the counter values need to be copied when the block is split.
Definition at line 815 of file check_complexity.h.
Member Function Documentation
◆ no_temporary_work()
|
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.)
- Parameters
-
max_C ilog2(n) - ilog2(size of constellation) max_B ilog2(n) - ilog2(size of block)
- Returns
- false iff some temporary counter was nonzero. In that case, also the beginning of an error message is printed. The function should be called through the macro
mCRL2complexity(), because that macro will print the remainder of the error message as needed.
Definition at line 835 of file check_complexity.h.
The documentation for this class was generated from the following file:
- lts/include/mcrl2/lts/detail/check_complexity.h
