mCRL2
|
block where the state belongs More...
#include <liblts_bisim_dnj.h>
Public Attributes | |
pred_entry * | ed_noninert_end |
block_t * | ock |
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.
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.
block_t* mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t::ock |
Definition at line 244 of file liblts_bisim_dnj.h.