This class contains state labels for an labelled transition system in .lts format.
More...
|
| | state_label_lts () |
| | 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, typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr) |
| | Creates a term_list with the elements from first to last.
|
| |
| | term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm, typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=0) |
| | 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, typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=0) |
| | Creates a term_list with the elements from first to last, converting and filtering the list.
|
| |
| | term_list (Iter first, Iter last, typename std::enable_if< !std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr) |
| | Creates a term_list from the elements from first to last.
|
| |
| | term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm, typename std::enable_if< !std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr) |
| | 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, typename std::enable_if< !std::is_base_of< std::random_access_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr) |
| | Creates a term_list from the elements from first to last converting and filtering the elements before inserting.
|
| |
| | 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 () noexcept |
| | Default constructor.
|
| |
| | ~aterm () noexcept |
| | Standard destructor.
|
| |
| | aterm (const detail::_aterm *t) noexcept |
| | Constructor based on an internal term data structure. This is not for public use.
|
| |
| | aterm (const aterm &other) noexcept |
| | Copy constructor.
|
| |
| | aterm (aterm &&other) noexcept |
| | Move constructor.
|
| |
| aterm & | operator= (const aterm &other) noexcept |
| | Assignment operator.
|
| |
| aterm & | assign (const aterm &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 & | unprotected_assign (const aterm &other) noexcept |
| | Assignment operator, to be used when the busy flags do not need to be set.
|
| |
| aterm & | operator= (aterm &&other) noexcept |
| | Move assignment operator.
|
| |
| | unprotected_aterm () noexcept |
| | Default constuctor.
|
| |
| | unprotected_aterm (const detail::_aterm *term) noexcept |
| | Constructor.
|
| |
| bool | type_is_appl () const noexcept |
| | Dynamic check whether the term is an aterm_appl.
|
| |
| 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 &t) const |
| | Comparison operator.
|
| |
| bool | operator!= (const unprotected_aterm &t) const |
| | Inequality operator on two unprotected aterms.
|
| |
| bool | operator< (const unprotected_aterm &t) const |
| | Comparison operator for two unprotected aterms.
|
| |
| bool | operator> (const unprotected_aterm &t) const |
| | Comparison operator for two unprotected aterms.
|
| |
| bool | operator<= (const unprotected_aterm &t) const |
| | Comparison operator for two unprotected aterms.
|
| |
| bool | operator>= (const unprotected_aterm &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, term_appl<T>'s and aterm_int.
|
| |
| void | swap (unprotected_aterm &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 39 of file lts_lts.h.
Public Types inherited from atermpp::term_list< lps::state >