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 mcrl2::data::enumerator_list_element::expression_type

typedef for Expression

Protected attributes

Expression mcrl2::data::enumerator_list_element::phi

data::variable_list mcrl2::data::enumerator_list_element::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)

Expression &expression()

const Expression &expression() const

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