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

counters for a B_to_C slice More...

#include <check_complexity.h>

Inheritance diagram for mcrl2::lts::detail::bisim_gjkw::check_complexity::B_to_C_counter_t:
mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< B_TO_C_MIN, B_TO_C_MAX, B_TO_C_MIN_TEMP,(enum counter_type)(B_TO_C_MAX_TEMP+1)>

Public Member Functions

bool no_temporary_work (unsigned const max_targetC)
 ensures there is no orphaned temporary work counter
 
unsigned char get_work_counter_4_4 () const
 returns the temporary counter associated with line 4.4
 
void reset_work_counter_4_4 ()
 sets the temporary counter associated with line 4.4 to zero
 
- Public Member Functions inherited from mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< B_TO_C_MIN, B_TO_C_MAX, B_TO_C_MIN_TEMP,(enum counter_type)(B_TO_C_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< B_TO_C_MIN, B_TO_C_MAX, B_TO_C_MIN_TEMP,(enum counter_type)(B_TO_C_MAX_TEMP+1)>
unsigned char counters [LastCounter - FirstCounter+1]
 actual space to store the counters
 

Detailed Description

counters for a B_to_C slice

The counters stored with a B_to_C slice are meant to be assigned to each transition in the slice. This means that the counter values need to be copied when the slice is split.

Definition at line 632 of file check_complexity.h.

Member Function Documentation

◆ get_work_counter_4_4()

unsigned char mcrl2::lts::detail::bisim_gjkw::check_complexity::B_to_C_counter_t::get_work_counter_4_4 ( ) const
inline

returns the temporary counter associated with line 4.4

The counter associated with line 4.4 is used when some constellation is reachable from a block containing new bottom states but it is not yet clear which states are the new bottom states that can reach the constellation. Then, the work is temporarily assigned to the B_to_C slice until it has become clear to which new bottom states it can be assigned.

We cannot use the normal mechanism of move_work() here because the normal counters are transition counters, not B_to_C slice counters.

This function helps to decide whether the work still needs to be moved from the temporary counter to a normal counter.

Returns
the value of the temporary counter associated with line 4.4

Definition at line 690 of file check_complexity.h.

◆ no_temporary_work()

bool mcrl2::lts::detail::bisim_gjkw::check_complexity::B_to_C_counter_t::no_temporary_work ( unsigned const  max_targetC)
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 target constellation.

Parameters
max_targetCilog2(n) - ilog2(size of target constellation)
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 649 of file check_complexity.h.

◆ reset_work_counter_4_4()

void mcrl2::lts::detail::bisim_gjkw::check_complexity::B_to_C_counter_t::reset_work_counter_4_4 ( )
inline

sets the temporary counter associated with line 4.4 to zero

The counter associated with line 4.4 is needed when some constellation is reachable from a block containing new bottom states but it is not yet clear which states are the new bottom states that can reach the constellation. Then, the work is temporarily assigned to the B_to_C slice until it has become clear to which new bottom states it has to be assigned.

We cannot use the normal mechanism of move_work() here because the normal counters are transition counters, not B_to_C slice counters.

This function resets the temporary work counter and is meant to be called as soon as the work can be assigned to normal counters.

Definition at line 711 of file check_complexity.h.


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