mcrl2::data::enumerator_list_element¶

Include file:

#include "mcrl2/data/enumerator.h

class mcrl2::data::enumerator_list_element¶: The default element for the todo list of the enumerator.

Public types¶

type expression_type¶: typedef for Expression

Protected attributes¶

Expression phi¶

data::variable_list v¶

Public member functions¶

enumerator_list_element() = default¶: Default constructor.

enumerator_list_element(data::variable_list v_, const Expression &phi_)¶: Constructs the element (v, phi)

enumerator_list_element(data::variable_list v_, const Expression &phi_, const enumerator_list_element&)¶: Constructs the element (v, phi)

enumerator_list_element(data::variable_list v_, const Expression &phi_, const enumerator_list_element&, const data::variable&, const data::data_expression&)¶: Constructs the element (v, phi)

const Expression &expression() const¶

Expression &expression()¶

void invalidate()¶: Invalidates the element, by giving phi an undefined value.

bool is_solution() const¶

bool is_valid() const¶: Returns true if the element is valid. If it becomes false, this is used to signal that the enumeration has been aborted.

const data::variable_list &variables() const¶