mcrl2::lts::detail::check_complexity::BLC_gj_counter_t Class Reference

#include <check_complexity.h>

Inheritance diagram for mcrl2::lts::detail::check_complexity::BLC_gj_counter_t:

Public Member Functions
bool	no_temporary_work (unsigned max_sourceC, unsigned max_targetC)
	ensures there is no orphaned temporary work counter
Public Member Functions inherited from mcrl2::lts::detail::check_complexity::counter_t< BLC_gj_MIN, BLC_gj_MAX >
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< BLC_gj_MIN, BLC_gj_MAX >
unsigned char	counters [LastCounter - FirstCounter+1]
	actual space to store the counters

Detailed Description

Definition at line 1359 of file check_complexity.h.

Member Function Documentation

no_temporary_work()

bool mcrl2::lts::detail::check_complexity::BLC_gj_counter_t::no_temporary_work ( unsigned  max_sourceC, unsigned  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_sourceC	ilog2(n) - ilog2(size of source constellation) Note that it should be the size of the source constellation, even though the transitions all start in the same block.
max_targetC	ilog2(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 1379 of file check_complexity.h.

---

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

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