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
pred_entry *	ed_noninert_end
block_t *	ock

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 242 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 243 of file liblts_bisim_dnj.h.

ock

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

Definition at line 244 of file liblts_bisim_dnj.h.

---

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

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