mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t Union Reference

pointer to next non-trivial bunch (in the single-linked list) or label More...

#include <liblts_bisim_dnj.h>

Public Member Functions
	next_nontrivial_and_label_t ()
	constructor

Public Attributes
bunch_t *	next_nontrivial
	pointer to the next non-trivial bunch in the single-linked list
label_type	label
	action label of the transition

Detailed Description

pointer to next non-trivial bunch (in the single-linked list) or label

During refinement, this field stores a pointer to the next nontrivial bunch. After refinement, it is set to the label.

Definition at line 970 of file liblts_bisim_dnj.h.

Constructor & Destructor Documentation

next_nontrivial_and_label_t()

mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t::next_nontrivial_and_label_t ( )

inline

constructor

Definition at line 984 of file liblts_bisim_dnj.h.

Member Data Documentation

label

label_type mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t::label

action label of the transition

Definition at line 980 of file liblts_bisim_dnj.h.

next_nontrivial

bunch_t* mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t::next_nontrivial

pointer to the next non-trivial bunch in the single-linked list

This pointer is == nullptr if the bunch is trivial. The last entry in the list points to itself so its pointer is still != nullptr.

Definition at line 977 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