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