This class contains state labels for an labelled transition system in .lts format.
More...
|
| | state_label_lts ()=default |
| | Default constructor.
|
| |
| | state_label_lts (const state_label_lts &)=default |
| | Copy constructor.
|
| |
| state_label_lts & | operator= (const state_label_lts &)=default |
| | Copy assignment.
|
| |
| template<class CONTAINER > |
| | 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 super &l) |
| | Construct a state label out of list of balanced trees of data expressions, representing a state label.
|
| |
| state_label_lts | operator+ (const state_label_lts &l) const |
| | An operator to concatenate two state labels.
|
| |
| | term_list () noexcept |
| | Default constructor. Creates an empty list.
|
| |
| | term_list (const aterm &t) noexcept |
| | Constructor from an aterm.
|
| |
| | term_list (const term_list< lps::state > &t) noexcept |
| | Copy constructor.
|
| |
| | term_list (term_list< lps::state > &&t) noexcept |
| | Move constructor.
|
| |
| | term_list (Iter first, Iter last) |
| | Creates a term_list with the elements from first to last.
|
| |
| | term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm) |
| | Creates a term_list with the elements from first to last converting the elements before inserting.
|
| |
| | term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm, const ATermFilter &aterm_filter) |
| | Creates a term_list with the elements from first to last, converting and filtering the list.
|
| |
| | term_list (Iter first, Iter last) |
| | Creates a term_list from the elements from first to last.
|
| |
| | term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm) |
| | Creates a term_list from the elements from first to last converting the elements before inserting.
|
| |
| | term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm, const ATermFilter &aterm_filter) |
| | Creates a term_list from the elements from first to last converting and filtering the elements before inserting.
|
| |
| | term_list (R &&r) |
| | Creates a term_list from the elements in the range.
|
| |
| | term_list (std::initializer_list< lps::state > init) |
| | A constructor based on an initializer list.
|
| |
| term_list & | operator= (const term_list &other) noexcept=default |
| | This class has user-declared copy constructor so declare copy and move assignment.
|
| |
| term_list & | operator= (term_list &&other) noexcept=default |
| |
| const term_list< lps::state > & | tail () const |
| | Returns the tail of the list.
|
| |
| void | pop_front () |
| | Removes the first element of the list.
|
| |
| const lps::state & | front () const |
| | Returns the first element of the list.
|
| |
| void | push_front (const lps::state &el) |
| | Inserts a new element at the beginning of the current list.
|
| |
| void | emplace_front (Args &&... arguments) |
| | Construct and insert a new element at the beginning of the current list.
|
| |
| size_type | size () const |
| | Returns the size of the term_list.
|
| |
| bool | empty () const |
| | Returns true if the list's size is 0.
|
| |
| const_iterator | begin () const |
| | Returns a const_iterator pointing to the beginning of the term_list.
|
| |
| const_iterator | end () const |
| | Returns a const_iterator pointing to the end of the term_list.
|
| |
| const_reverse_iterator | rbegin () const |
| | Returns a const_reverse_iterator pointing to the end of the term_list.
|
| |
| const_reverse_iterator | rend () const |
| | Returns a const_iterator pointing to the end of the term_list.
|
| |
| size_type | max_size () const |
| | Returns the largest possible size of the term_list.
|
| |
| | aterm () |
| | Default constructor.
|
| |
| | aterm (const aterm &other) noexcept=default |
| | This class has user-declared copy constructor so declare default copy and move operators.
|
| |
| aterm & | operator= (const aterm &other) noexcept=default |
| |
| | aterm (aterm &&other) noexcept=default |
| |
| aterm & | operator= (aterm &&other) noexcept=default |
| |
template<class ForwardIterator >
requires (mcrl2::utilities::is_iterator<ForwardIterator>::value && !std::is_same_v<typename ForwardIterator::iterator_category, std::input_iterator_tag> && !std::is_same_v<typename ForwardIterator::iterator_category, std::output_iterator_tag>) |
| | aterm (const function_symbol &sym, ForwardIterator begin, ForwardIterator end) |
| | Constructor that provides an aterm based on a function symbol and forward iterator providing the arguments.
|
| |
template<class InputIterator >
requires mcrl2::utilities::is_iterator<InputIterator> |
| | aterm (const function_symbol &sym, InputIterator begin, InputIterator end) |
| | Constructor that provides an aterm based on a function symbol and an input iterator providing the arguments.
|
| |
template<class InputIterator , class TermConverter >
requires mcrl2::utilities::is_iterator<InputIterator> |
| | aterm (const function_symbol &sym, InputIterator begin, InputIterator end, TermConverter converter) |
| | Constructor.
|
| |
| template<typename... Terms> |
| | aterm (const function_symbol &symbol, const Terms &... arguments) |
| | Constructor for n-arity function application.
|
| |
| const function_symbol & | function () const |
| | Returns the function symbol belonging to an aterm.
|
| |
| size_type | size () const |
| | Returns the number of arguments of this term.
|
| |
| bool | empty () const |
| | Returns true if the term has no arguments.
|
| |
| const_iterator | begin () const |
| | Returns an iterator pointing to the first argument.
|
| |
| const_iterator | end () const |
| | Returns a const_iterator pointing past the last argument.
|
| |
| constexpr size_type | max_size () const |
| | Returns the largest possible number of arguments.
|
| |
| const aterm & | operator[] (const size_type i) const |
| | Returns the i-th argument.
|
| |
| | aterm_core () noexcept |
| | Default constructor.
|
| |
| | ~aterm_core () noexcept |
| | Standard destructor.
|
| |
| | aterm_core (const detail::_aterm *t) noexcept |
| | Constructor based on an internal term data structure. This is not for public use.
|
| |
| | aterm_core (const aterm_core &other) noexcept |
| | Copy constructor.
|
| |
| | aterm_core (aterm_core &&other) noexcept |
| | Move constructor.
|
| |
| aterm_core & | operator= (const aterm_core &other) noexcept |
| | Assignment operator.
|
| |
| aterm_core & | assign (const aterm_core &other, detail::thread_aterm_pool &pool) noexcept |
| | Assignment operator, to be used if busy and forbidden flags are explicitly available.
|
| |
| template<bool CHECK_BUSY_FLAG = true> |
| aterm_core & | unprotected_assign (const aterm_core &other) noexcept |
| | Assignment operator, to be used when the busy flags do not need to be set.
|
| |
| aterm_core & | operator= (aterm_core &&other) noexcept |
| | Move assignment operator.
|
| |
| | unprotected_aterm_core () noexcept |
| | Default constuctor.
|
| |
| | unprotected_aterm_core (const detail::_aterm *term) noexcept |
| | Constructor.
|
| |
| bool | type_is_appl () const noexcept |
| | Dynamic check whether the term is an aterm.
|
| |
| bool | type_is_int () const noexcept |
| | Dynamic check whether the term is an aterm_int.
|
| |
| bool | type_is_list () const noexcept |
| | Dynamic check whether the term is an aterm_list.
|
| |
| bool | operator== (const unprotected_aterm_core &t) const |
| | Comparison operator.
|
| |
| std::weak_ordering | operator<=> (const unprotected_aterm_core &t) const |
| | Comparison operator for two unprotected aterms.
|
| |
| bool | defined () const |
| | Returns true if this term is not equal to the term assigned by the default constructor of aterms, aterm_appls and aterm_int.
|
| |
| void | swap (unprotected_aterm_core &t) noexcept |
| | Swaps this term with its argument.
|
| |
| const function_symbol & | function () const |
| | Yields the function symbol in an aterm.
|
| |
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.
Definition at line 37 of file lts_lts.h.
Public Types inherited from atermpp::term_list< lps::state >