mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisim_gjkw::check_complexity::trans_dnj_counter_t Class Reference

#include <check_complexity.h>

Inheritance diagram for mcrl2::lts::detail::bisim_gjkw::check_complexity::trans_dnj_counter_t:
mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< TRANS_dnj_MIN, TRANS_dnj_MAX, TRANS_dnj_MIN_TEMP,(enum counter_type)(TRANS_dnj_MAX_TEMP+1)>

Public Member Functions

bool no_temporary_work (unsigned const max_source_block, unsigned const max_target_block, bool const 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::bisim_gjkw::check_complexity::counter_t< TRANS_dnj_MIN, TRANS_dnj_MAX, TRANS_dnj_MIN_TEMP,(enum counter_type)(TRANS_dnj_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::bisim_gjkw::check_complexity::counter_t< TRANS_dnj_MIN, TRANS_dnj_MAX, TRANS_dnj_MIN_TEMP,(enum counter_type)(TRANS_dnj_MAX_TEMP+1)>
unsigned char counters [LastCounter - FirstCounter+1]
 actual space to store the counters
 

Detailed Description

Definition at line 1107 of file check_complexity.h.

Member Function Documentation

◆ add_work_notemporary()

bool mcrl2::lts::detail::bisim_gjkw::check_complexity::trans_dnj_counter_t::add_work_notemporary ( enum counter_type const  ctr,
unsigned const  max_value 
)
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
ctrcounter with which work is registered
max_valuemaximal allowed value of the counter. The old value of the counter should be strictly smaller. (Because it is a temporary counter, only 1 is 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 1189 of file check_complexity.h.

◆ no_temporary_work()

bool mcrl2::lts::detail::bisim_gjkw::check_complexity::trans_dnj_counter_t::no_temporary_work ( unsigned const  max_source_block,
unsigned const  max_target_block,
bool const  bottom 
)
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_source_blockilog2(n) - ilog2(size of source block)
max_target_blockilog2(n) - ilog2(size of target block)
bottomtrue iff the transition source is a bottom state
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 1128 of file check_complexity.h.


The documentation for this class was generated from the following file: