mcrl2::lts::detail::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::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter >

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

Definition at line 512 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::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter >::counter_t ( )

inline

constructor, initializes all counters to 0

Definition at line 583 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::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

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.

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 602 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::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

ctr	temporary 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 532 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::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

from	temporary counter from where work is moved
to	normal counter to which work is moved
max_value	maximal 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 563 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::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

from	temporary counter from where work is moved
to	(temporary or normal) counter to which work is moved
max_value	maximal 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 640 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::check_complexity::counter_t< FirstCounter, LastCounter, FirstTempCounter, FirstPostprocessCounter >::counters[LastCounter - FirstCounter+1]

actual space to store the counters

Definition at line 520 of file check_complexity.h.

---

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

• lts/include/mcrl2/lts/detail/check_complexity.h