mcrl2::lts::detail::bisimulation_gj Namespace Reference

Classes
struct	BLC_indicators
struct	block_type
struct	constellation_type
	information about a constellation More...
struct	outgoing_transition_type
	information about a transition stored in m_outgoing_transitions More...
struct	state_in_block_pointer
	a pointer to a state, i.e. a reference to a state More...
struct	state_type_gj
	information about a state More...
class	todo_state_vector
struct	transition_type

Typedefs
typedef std::size_t	state_index
typedef std::size_t	transition_index
typedef std::size_t	label_index
typedef fixed_vector< outgoing_transition_type >::iterator	outgoing_transitions_it
typedef fixed_vector< outgoing_transition_type >::const_iterator	outgoing_transitions_const_it
typedef transition_index *	BLC_list_iterator
typedef transition_index *	BLC_list_iterator_or_null
typedef const transition_index *	BLC_list_const_iterator

Enumerations
enum	subblocks { ReachAlw =0 , AvoidSml , AvoidLrg , MultiSub }

Functions
static constexpr transition_index	marked (enum subblocks subblock)
	base marking value for a subblock
static constexpr bool	is_in_marked_range_of (transition_index counter, enum subblocks subblock)
	checks whether a counter value is a marking for a given subblock
template<class CONTAINER >
static void	clear (CONTAINER &c)

Variables
constexpr constellation_type *	null_constellation =nullptr
constexpr transition_index	null_transition =-1
constexpr label_index	null_action =-1
constexpr state_index	null_state =-1
constexpr block_type *	null_block =nullptr
constexpr transition_index	undefined =0
	default counter value if the counter field of a state is not in use currently
constexpr transition_index	marked_range
	the number of counter values that can be used for one subblock
constexpr transition_index	marked_MultiSub =marked(MultiSub)
	counter value to indicate that a state is in the MultiSub subset
constexpr transition_index	marked_HitSmall =marked_MultiSub+1

Typedef Documentation

BLC_list_const_iterator

typedef const transition_index* mcrl2::lts::detail::bisimulation_gj::BLC_list_const_iterator

Definition at line 131 of file liblts_bisim_gj.h.

BLC_list_iterator

typedef transition_index* mcrl2::lts::detail::bisimulation_gj::BLC_list_iterator

Definition at line 129 of file liblts_bisim_gj.h.

BLC_list_iterator_or_null

typedef transition_index* mcrl2::lts::detail::bisimulation_gj::BLC_list_iterator_or_null

Definition at line 130 of file liblts_bisim_gj.h.

label_index

typedef std::size_t mcrl2::lts::detail::bisimulation_gj::label_index

Definition at line 59 of file liblts_bisim_gj.h.

outgoing_transitions_const_it

typedef fixed_vector<outgoing_transition_type>::const_iterator mcrl2::lts::detail::bisimulation_gj::outgoing_transitions_const_it

Definition at line 63 of file liblts_bisim_gj.h.

outgoing_transitions_it

typedef fixed_vector<outgoing_transition_type>::iterator mcrl2::lts::detail::bisimulation_gj::outgoing_transitions_it

Definition at line 61 of file liblts_bisim_gj.h.

state_index

typedef std::size_t mcrl2::lts::detail::bisimulation_gj::state_index

Definition at line 55 of file liblts_bisim_gj.h.

transition_index

typedef std::size_t mcrl2::lts::detail::bisimulation_gj::transition_index

Definition at line 56 of file liblts_bisim_gj.h.

Enumeration Type Documentation

subblocks

enum mcrl2::lts::detail::bisimulation_gj::subblocks

Enumerator
ReachAlw
AvoidSml
AvoidLrg
MultiSub

Definition at line 81 of file liblts_bisim_gj.h.

Function Documentation

clear()

template<class CONTAINER >

static void mcrl2::lts::detail::bisimulation_gj::clear ( CONTAINER &  c )

inlinestatic

The function clear() takes care that a container frees memory when it is cleared and it is large.

Definition at line 122 of file liblts_bisim_gj.h.

is_in_marked_range_of()

static constexpr bool mcrl2::lts::detail::bisimulation_gj::is_in_marked_range_of ( transition_index  counter, enum subblocks  subblock  )

inlinestaticconstexpr

checks whether a counter value is a marking for a given subblock

Definition at line 112 of file liblts_bisim_gj.h.

marked()

static constexpr transition_index mcrl2::lts::detail::bisimulation_gj::marked ( enum subblocks  subblock )

inlinestaticconstexpr

base marking value for a subblock

If the counter has this value, the state definitely belongs to the respective subblock.

Definition at line 97 of file liblts_bisim_gj.h.

Variable Documentation

marked_HitSmall

constexpr transition_index mcrl2::lts::detail::bisimulation_gj::marked_HitSmall =marked_MultiSub+1

constexpr

counter value to indicate that a state has a transition in the small splitter (so it cannot become part of AvoidSml)

Definition at line 109 of file liblts_bisim_gj.h.

marked_MultiSub

constexpr transition_index mcrl2::lts::detail::bisimulation_gj::marked_MultiSub =marked(MultiSub)

constexpr

counter value to indicate that a state is in the MultiSub subset

Definition at line 105 of file liblts_bisim_gj.h.

marked_range

constexpr transition_index mcrl2::lts::detail::bisimulation_gj::marked_range

constexpr

Initial value:

=
    (std::numeric_limits<transition_index>::max()-2)/3

the number of counter values that can be used for one subblock

There are three singular values (undefined, marked_MultiSub, and marked_HitSmall), and the other values needs to be distributed over three subblocks (ReachAlw, AvoidLrg, and AvoidSml).

Definition at line 78 of file liblts_bisim_gj.h.

null_action

constexpr label_index mcrl2::lts::detail::bisimulation_gj::null_action =-1

constexpr

Definition at line 67 of file liblts_bisim_gj.h.

null_block

constexpr block_type* mcrl2::lts::detail::bisimulation_gj::null_block =nullptr

constexpr

Definition at line 69 of file liblts_bisim_gj.h.

null_constellation

constexpr constellation_type* mcrl2::lts::detail::bisimulation_gj::null_constellation =nullptr

constexpr

Definition at line 65 of file liblts_bisim_gj.h.

null_state

constexpr state_index mcrl2::lts::detail::bisimulation_gj::null_state =-1

constexpr

Definition at line 68 of file liblts_bisim_gj.h.

null_transition

constexpr transition_index mcrl2::lts::detail::bisimulation_gj::null_transition =-1

constexpr

Definition at line 66 of file liblts_bisim_gj.h.

undefined

constexpr transition_index mcrl2::lts::detail::bisimulation_gj::undefined =0

constexpr

default counter value if the counter field of a state is not in use currently

Definition at line 72 of file liblts_bisim_gj.h.