No Matches
mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t Union Reference

block where the state belongs More...

#include <liblts_bisim_dnj.h>

Public Attributes


Detailed Description

block where the state belongs

During initialisation, this field is used to point at the first unused slot of the (non-inert) bledecessors, ahem, predecessors. Sorry for the mock-chinese `‘typo’'. So we always assume that it starts as a pred_entry*, at some moment is converted to a block_t*, and then stays that way until it is destroyed.

Definition at line 940 of file liblts_bisim_dnj.h.

Member Data Documentation

◆ ed_noninert_end

pred_entry* mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t::ed_noninert_end

Definition at line 941 of file liblts_bisim_dnj.h.

◆ ock

block_t* mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t::ock

Definition at line 942 of file liblts_bisim_dnj.h.

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