mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter > Class Template Reference

subset of counters (to be associated with a state or transition) More...

#include <check_complexity.h>

Public Member Functions

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
 

Public Attributes

unsigned char counters [LastCounter - FirstCounter+1]
 actual space to store the counters
 

Detailed Description

template<enum counter_type FirstCounter, enum counter_type LastCounter, enum counter_type FirstTempCounter = (enum counter_type) (LastCounter + 1), enum counter_type FirstPostprocessCounter = FirstTempCounter>
class mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter >

subset of counters (to be associated with a state or transition)

Definition at line 413 of file check_complexity.h.

Constructor & Destructor Documentation

◆ counter_t()

template<enum counter_type FirstCounter, enum counter_type LastCounter, enum counter_type FirstTempCounter = (enum counter_type) (LastCounter + 1), enum counter_type FirstPostprocessCounter = FirstTempCounter>
mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter >::counter_t ( )
inline

constructor, initializes all counters to 0

Definition at line 482 of file check_complexity.h.

Member Function Documentation

◆ add_work()

template<enum counter_type FirstCounter, enum counter_type LastCounter, enum counter_type FirstTempCounter = (enum counter_type) (LastCounter + 1), enum counter_type FirstPostprocessCounter = FirstTempCounter>
bool mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter >::add_work ( enum counter_type const  ctr,
unsigned const  max_value 
)
inline

register work with some counter

The function increases a work counter to a larger value. It is also checked that the counter does not get too large. The function is normally called through the macro mCRL2complexity().

Parameters
ctrcounter with which work is registered
max_valuemaximal allowed value of the counter. The old value of the counter should be strictly smaller.
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 501 of file check_complexity.h.

◆ cancel_work()

template<enum counter_type FirstCounter, enum counter_type LastCounter, enum counter_type FirstTempCounter = (enum counter_type) (LastCounter + 1), enum counter_type FirstPostprocessCounter = FirstTempCounter>
bool mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter >::cancel_work ( enum counter_type const  ctr)
inline

cancel temporary work

The function registers that all counters from first to last (inclusive) are counting superfluous work. It adds them to the pool of superfluous work.

Parameters
ctrtemporary counter whose work is superfluous
Returns
false iff some 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 433 of file check_complexity.h.

◆ finalise_work()

template<enum counter_type FirstCounter, enum counter_type LastCounter, enum counter_type FirstTempCounter = (enum counter_type) (LastCounter + 1), enum counter_type FirstPostprocessCounter = FirstTempCounter>
bool mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter >::finalise_work ( enum counter_type const  from,
enum counter_type const  to,
unsigned const  max_value 
)
inline

move temporary work to its final counter

The function moves work from a temporary counter to a normal counter. It also checks that the normal counter does not get too large.

Parameters
fromtemporary counter from where work is moved
tonormal counter to which work is moved
max_valuemaximal allowed value to the normal counter. The old value of the counter should be strictly smaller.
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 463 of file check_complexity.h.

◆ move_work()

template<enum counter_type FirstCounter, enum counter_type LastCounter, enum counter_type FirstTempCounter = (enum counter_type) (LastCounter + 1), enum counter_type FirstPostprocessCounter = FirstTempCounter>
bool mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter >::move_work ( enum counter_type const  from,
enum counter_type const  to,
unsigned const  max_value 
)
inline

move temporary work to another counter

The function moves work from a temporary counter to another temporary or a normal counter. It also checks that the new counter does not get too large. The function is normally called through the macro mCRL2complexity().

Parameters
fromtemporary counter from where work is moved
to(temporary or normal) counter to which work is moved
max_valuemaximal allowed value to the normal counter. The old value of the counter should be strictly smaller.
Returns
false iff the new 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 535 of file check_complexity.h.

Member Data Documentation

◆ counters

template<enum counter_type FirstCounter, enum counter_type LastCounter, enum counter_type FirstTempCounter = (enum counter_type) (LastCounter + 1), enum counter_type FirstPostprocessCounter = FirstTempCounter>
unsigned char mcrl2::lts::detail::bisim_gjkw::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter >::counters[LastCounter - FirstCounter+1]

actual space to store the counters

Definition at line 421 of file check_complexity.h.


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