This class contains labels for probabilistic transistions, consisting of a numerator and a denumerator.
More...
|
| | probabilistic_data_expression () |
| |
| | probabilistic_data_expression (const data::data_expression &d) |
| | Construct a probabilistic_data_expression from a data_expression, which must be of sort real.
|
| |
| | probabilistic_data_expression (std::size_t enumerator, std::size_t denominator) |
| |
| | probabilistic_data_expression (const std::string &enumerator, const std::string &denominator) |
| |
| bool | operator== (const probabilistic_data_expression &other) const |
| |
| bool | operator!= (const probabilistic_data_expression &other) const |
| |
| bool | operator< (const probabilistic_data_expression &other) const |
| |
| bool | operator<= (const probabilistic_data_expression &other) const |
| |
| bool | operator> (const probabilistic_data_expression &other) const |
| |
| bool | operator>= (const probabilistic_data_expression &other) const |
| |
| probabilistic_data_expression | operator+ (const probabilistic_data_expression &other) const |
| | Standard addition operator. Note that the expression is not evaluated. For this the rewriter has to be applied on it explicitly.
|
| |
| probabilistic_data_expression | operator- (const probabilistic_data_expression &other) const |
| | Standard subtraction operator.
|
| |
| | data_expression () |
| | \brief Default constructor X3.
|
| |
| | data_expression (const atermpp::aterm &term) |
| |
| | data_expression (const data_expression &) noexcept=default |
| | Move semantics.
|
| |
| | data_expression (data_expression &&) noexcept=default |
| |
| data_expression & | operator= (const data_expression &) noexcept=default |
| |
| data_expression & | operator= (data_expression &&) noexcept=default |
| |
| bool | is_default_data_expression () const |
| | A function to efficiently determine whether a data expression is made by the default constructor.
|
| |
| application | operator() (const data_expression &e) const |
| | Apply a data expression to a data expression.
|
| |
| application | operator() (const data_expression &e1, const data_expression &e2) const |
| | Apply a data expression to two data expressions.
|
| |
| application | operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3) const |
| | Apply a data expression to three data expressions.
|
| |
| application | operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4) const |
| | Apply a data expression to four data expressions.
|
| |
| application | operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5) const |
| | Apply a data expression to five data expressions.
|
| |
| application | operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5, const data_expression &e6) const |
| | Apply a data expression to six data expressions.
|
| |
| sort_expression | sort () const |
| | Returns the sort of the data expression.
|
| |
| | 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 , typename std::enable_if< mcrl2::utilities::is_iterator< ForwardIterator >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::output_iterator_tag >::value >::type * = nullptr> |
| | 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 , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr, typename std::enable_if< std::is_same< typename InputIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr> |
| | 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 , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr> |
| | aterm (const function_symbol &sym, InputIterator begin, InputIterator end, TermConverter converter) |
| |
| | aterm (const function_symbol &sym) |
| | 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.
|
| |
| bool | operator!= (const unprotected_aterm_core &t) const |
| | Inequality operator on two unprotected aterms.
|
| |
| bool | operator< (const unprotected_aterm_core &t) const |
| | Comparison operator for two unprotected aterms.
|
| |
| bool | operator> (const unprotected_aterm_core &t) const |
| | Comparison operator for two unprotected aterms.
|
| |
| bool | operator<= (const unprotected_aterm_core &t) const |
| | Comparison operator for two unprotected aterms.
|
| |
| bool | 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 labels for probabilistic transistions, consisting of a numerator and a denumerator.
This class provides a number of operators to calculate with real constants (actually fractions). Comparisons of more complex expressions may not always rewrite properly. There are methods to add and subtract such labels. The numbers are used as 64 bit integers. If the integers do not fit into 64 bit, the numerator and denumerator are adapted to make them fit. This means that this library is not exact, but employs rounding at times.
Definition at line 144 of file probabilistic_data_expression.h.
Public Member Functions inherited from mcrl2::data::data_expression