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
using	state_index = std::size_t
using	transition_index = std::size_t
using	label_index = std::size_t
using	outgoing_transitions_it = fixed_vector< outgoing_transition_type >::iterator
using	outgoing_transitions_const_it = fixed_vector< outgoing_transition_type >::const_iterator
using	BLC_list_iterator = transition_index *
using	BLC_list_iterator_or_null = transition_index *
using	BLC_list_const_iterator = const transition_index *

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

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
constexpr transition_index	marked_range
	the number of counter values that can be used for one subblock
constexpr transition_index	marked_NewBotSt =marked(NewBotSt)
	counter value to indicate that a state is in the NewBotSt subset
constexpr transition_index	marked_HitSmall =marked_NewBotSt+1

Typedef Documentation

BLC_list_const_iterator

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

Definition at line 137 of file liblts_bisim_gj.h.

BLC_list_iterator

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

Definition at line 135 of file liblts_bisim_gj.h.

BLC_list_iterator_or_null

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

Definition at line 136 of file liblts_bisim_gj.h.

label_index

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

Definition at line 65 of file liblts_bisim_gj.h.

outgoing_transitions_const_it

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

Definition at line 67 of file liblts_bisim_gj.h.

outgoing_transitions_it

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

Definition at line 66 of file liblts_bisim_gj.h.

state_index

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

Definition at line 62 of file liblts_bisim_gj.h.

transition_index

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

Definition at line 63 of file liblts_bisim_gj.h.

Enumeration Type Documentation

subblocks

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

Enumerator
ReachAlw
AvoidSml
AvoidLrg
NewBotSt

Definition at line 87 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 128 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 118 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 103 of file liblts_bisim_gj.h.

Variable Documentation

marked_HitSmall

constexpr transition_index mcrl2::lts::detail::bisimulation_gj::marked_HitSmall =marked_NewBotSt+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 115 of file liblts_bisim_gj.h.

marked_NewBotSt

constexpr transition_index mcrl2::lts::detail::bisimulation_gj::marked_NewBotSt =marked(NewBotSt)

constexpr

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

Definition at line 111 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_NewBotSt, and marked_HitSmall), and the other values needs to be distributed over three subblocks (ReachAlw, AvoidLrg, and AvoidSml).

Definition at line 84 of file liblts_bisim_gj.h.

null_action

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

constexpr

Definition at line 72 of file liblts_bisim_gj.h.

null_block

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

constexpr

Definition at line 74 of file liblts_bisim_gj.h.

null_constellation

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

constexpr

Definition at line 70 of file liblts_bisim_gj.h.

null_state

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

constexpr

Definition at line 73 of file liblts_bisim_gj.h.

null_transition

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

constexpr

Definition at line 71 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 78 of file liblts_bisim_gj.h.