#include <check_complexity.h>
Public Member Functions | |
| bool | no_temporary_work (unsigned const max_sourceB, unsigned const max_targetC, unsigned const max_targetB, bool const source_bottom) |
| ensures there is no orphaned temporary work counter | |
| bool | add_work_notemporary (enum counter_type const ctr, unsigned const max_value) |
| register work with some temporary counter without changing the balance between sensible and superfluous work | |
 Public Member Functions inherited from mcrl2::lts::detail::check_complexity::counter_t< TRANS_gj_MIN, TRANS_gj_MAX, TRANS_gj_MIN_TEMP,(enum counter_type)(TRANS_gj_MAX_TEMP+1)> | |
| 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< TRANS_gj_MIN, TRANS_gj_MAX, TRANS_gj_MIN_TEMP,(enum counter_type)(TRANS_gj_MAX_TEMP+1)> | |
| unsigned char | counters [LastCounter - FirstCounter+1] |
| actual space to store the counters | |
Detailed Description
Definition at line 1473 of file check_complexity.h.
Member Function Documentation
◆ add_work_notemporary()
|
inline |
register work with some temporary counter without changing the balance between sensible and superfluous work
The function increases a temporary work counter. It is also checked that the counter does not get too large. This variant of add_work() should be used if one wants to assign a single step of work to multiple temporary counters of transitions: for one of them, the normal add_work() is called, and for the others add_work_notemporary().
- Parameters
-
ctr counter with which work is registered max_value maximal allowed value of the counter. The old value of the counter should be strictly smaller. (Because it is a temporary counter, only 1is sensible.)
- Returns
- false iff the counter was too large. 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 1602 of file check_complexity.h.
◆ 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. Further, there should not be any work ascribed to bottom-state counters in transitions from non-bottom states, but only to transitions from (new) bottom states. This function verifies these properties. It also sets all counters for bottom states to 1 so that later no more work can be assigned to them. The function additionally ensures that no work counter exceeds its maximal allowed value, based on the size of the source block, target block or target constellation. (The constellation size is the relevant unit for counters that are related to transitions into the splitter, which is the constellation NewC. The block size is the unit for counters that are related to refinements. Because some parts of a refinement look at incoming transitions of the refined block and others at outgoing transitions, we need two block sizes.)
- Parameters
-
max_sourceB the maximum allowed value for work counters based on the source state of the transition max_targetC the maximum allowed value for work counters based on the target constellation max_targetB the maximum allowed value for work counters based on the target block source_bottom trueiff the transition to which these counters belong starts in a bottom state
- Returns
- false iff some temporary counter or some bottom-state counter of a transition with non-bottom source 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 1509 of file check_complexity.h.
The documentation for this class was generated from the following file:
- lts/include/mcrl2/lts/detail/check_complexity.h
