mcrl2::lts::state_label_lts

Include file:

#include "mcrl2/lts/lts_lts.h

class mcrl2::lts::state_label_lts

This class contains state labels for an labelled transition system in .lts format.

A state label in .lts format consists of lists of balanced tree of data expressions. These represent sets of state vectors. The reason for the sets is that states can be merged by operations on state spaces, and if so, the sets of labels can easily be joined.

Public types

type mcrl2::lts::state_label_lts::super

typedef for atermpp::term_list< lps::state >

Public member functions

state_label_lts operator+(const state_label_lts &l) const

An operator to concatenate two state labels.

Is optimal whenever |l| is smaller than the left operand, i.e. |l| < |this|.

state_label_lts &operator=(const state_label_lts&) = default

Copy assignment.

state_label_lts()

Default constructor.

state_label_lts(const CONTAINER &l)

Construct a single state label out of the elements in a container.

state_label_lts(const lps::state &l)

Construct a state label out of a balanced tree of data expressions, representing a state label.

state_label_lts(const state_label_lts&) = default

Copy constructor.

state_label_lts(const super &l)

Construct a state label out of list of balanced trees of data expressions, representing a state label.