mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::probabilistic_data_expression Class Reference

This class contains labels for probabilistic transistions, consisting of a numerator and a denumerator. More...

#include <probabilistic_data_expression.h>

Inheritance diagram for mcrl2::lps::probabilistic_data_expression:
mcrl2::data::data_expression atermpp::term_appl< aterm > atermpp::aterm atermpp::unprotected_aterm

Public Member Functions

 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.
 
- Public Member Functions inherited from mcrl2::data::data_expression
 data_expression ()
 \brief Default constructor.
 
 data_expression (const atermpp::aterm &term)
 
 data_expression (const data_expression &) noexcept=default
 Move semantics.
 
 data_expression (data_expression &&) noexcept=default
 
data_expressionoperator= (const data_expression &) noexcept=default
 
data_expressionoperator= (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 data expression to two data expressions.
 
application operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3) const
 Apply 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 data expression to four data expressions.
 
sort_expression sort () const
 Returns the sort of the data expression.
 
- Public Member Functions inherited from atermpp::term_appl< aterm >
 term_appl ()
 Default constructor.
 
 term_appl (const aterm &t)
 Explicit constructor from an aterm.
 
 term_appl (const term_appl &other) noexcept=default
 This class has user-declared copy constructor so declare default copy and move operators.
 
 term_appl (term_appl &&other) noexcept=default
 
 term_appl (const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
 Constructor that provides an aterm_appl based on a function symbol and forward iterator providing the arguments.
 
 term_appl (const function_symbol &sym, InputIterator begin, InputIterator end)
 Constructor that provides an aterm_appl based on a function symbol and an input iterator providing the arguments.
 
 term_appl (const function_symbol &sym, InputIterator begin, InputIterator end, TermConverter converter)
 
 term_appl (const function_symbol &sym)
 Constructor.
 
 term_appl (const function_symbol &symbol, const Terms &...arguments)
 Constructor for n-arity function application.
 
term_apploperator= (const term_appl &other) noexcept=default
 
term_apploperator= (term_appl &&other) noexcept=default
 
const function_symbolfunction () const
 Returns the function symbol belonging to an aterm_appl.
 
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 atermoperator[] (const size_type i) const
 Returns the i-th argument.
 
- Public Member Functions inherited from atermpp::aterm
 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.
 
atermoperator= (const aterm &other) noexcept
 Assignment operator.
 
atermassign (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>
atermunprotected_assign (const aterm &other) noexcept
 Assignment operator, to be used when the busy flags do not need to be set.
 
atermoperator= (aterm &&other) noexcept
 Move assignment operator.
 
- Public Member Functions inherited from atermpp::unprotected_aterm
 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_symbolfunction () const
 Yields the function symbol in an aterm.
 

Static Public Member Functions

static probabilistic_data_expression zero ()
 Constant zero.
 
static probabilistic_data_expression one ()
 Constant one.
 

Protected Member Functions

void remove_common_factors (std::size_t &enumerator, std::size_t &denominator)
 
- Protected Member Functions inherited from atermpp::term_appl< aterm >
 term_appl (detail::_term_appl *t)
 Constructor.
 

Static Protected Member Functions

static data::data_specification data_specification_with_real ()
 
static const data::rewriterm_rewriter ()
 
static std::size_t to_number_t (const std::string &s)
 
static std::size_t greatest_common_divisor (std::size_t x, std::size_t y)
 

Additional Inherited Members

- Public Types inherited from atermpp::term_appl< aterm >
typedef aterm value_type
 The type of object, T stored in the term_appl.
 
typedef atermpointer
 Pointer to T.
 
typedef atermreference
 Reference to T.
 
typedef const aterm const_reference
 Const reference to T.
 
typedef std::size_t size_type
 An unsigned integral type.
 
typedef ptrdiff_t difference_type
 A signed integral type.
 
typedef term_appl_iterator< atermiterator
 Iterator used to iterate through an term_appl.
 
typedef term_appl_iterator< atermconst_iterator
 Const iterator used to iterate through an term_appl.
 
- Protected Attributes inherited from atermpp::unprotected_aterm
const detail::_atermm_term
 

Detailed Description

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 36 of file probabilistic_data_expression.h.

Constructor & Destructor Documentation

◆ probabilistic_data_expression() [1/4]

mcrl2::lps::probabilistic_data_expression::probabilistic_data_expression ( )
inline

Definition at line 109 of file probabilistic_data_expression.h.

◆ probabilistic_data_expression() [2/4]

mcrl2::lps::probabilistic_data_expression::probabilistic_data_expression ( const data::data_expression d)
inlineexplicit

Construct a probabilistic_data_expression from a data_expression, which must be of sort real.

Definition at line 115 of file probabilistic_data_expression.h.

◆ probabilistic_data_expression() [3/4]

mcrl2::lps::probabilistic_data_expression::probabilistic_data_expression ( std::size_t  enumerator,
std::size_t  denominator 
)
inline

Definition at line 123 of file probabilistic_data_expression.h.

◆ probabilistic_data_expression() [4/4]

mcrl2::lps::probabilistic_data_expression::probabilistic_data_expression ( const std::string &  enumerator,
const std::string &  denominator 
)
inline

Definition at line 133 of file probabilistic_data_expression.h.

Member Function Documentation

◆ data_specification_with_real()

static data::data_specification mcrl2::lps::probabilistic_data_expression::data_specification_with_real ( )
inlinestaticprotected

Definition at line 41 of file probabilistic_data_expression.h.

◆ greatest_common_divisor()

static std::size_t mcrl2::lps::probabilistic_data_expression::greatest_common_divisor ( std::size_t  x,
std::size_t  y 
)
inlinestaticprotected

Definition at line 60 of file probabilistic_data_expression.h.

◆ m_rewriter()

static const data::rewriter & mcrl2::lps::probabilistic_data_expression::m_rewriter ( )
inlinestaticprotected

Definition at line 48 of file probabilistic_data_expression.h.

◆ one()

static probabilistic_data_expression mcrl2::lps::probabilistic_data_expression::one ( )
inlinestatic

Constant one.

Definition at line 100 of file probabilistic_data_expression.h.

◆ operator!=()

bool mcrl2::lps::probabilistic_data_expression::operator!= ( const probabilistic_data_expression other) const
inline

Definition at line 159 of file probabilistic_data_expression.h.

◆ operator+()

probabilistic_data_expression mcrl2::lps::probabilistic_data_expression::operator+ ( const probabilistic_data_expression other) const
inline

Standard addition operator. Note that the expression is not evaluated. For this the rewriter has to be applied on it explicitly.

Definition at line 204 of file probabilistic_data_expression.h.

◆ operator-()

probabilistic_data_expression mcrl2::lps::probabilistic_data_expression::operator- ( const probabilistic_data_expression other) const
inline

Standard subtraction operator.

Definition at line 212 of file probabilistic_data_expression.h.

◆ operator<()

bool mcrl2::lps::probabilistic_data_expression::operator< ( const probabilistic_data_expression other) const
inline

Definition at line 166 of file probabilistic_data_expression.h.

◆ operator<=()

bool mcrl2::lps::probabilistic_data_expression::operator<= ( const probabilistic_data_expression other) const
inline

Definition at line 182 of file probabilistic_data_expression.h.

◆ operator==()

bool mcrl2::lps::probabilistic_data_expression::operator== ( const probabilistic_data_expression other) const
inline

Definition at line 143 of file probabilistic_data_expression.h.

◆ operator>()

bool mcrl2::lps::probabilistic_data_expression::operator> ( const probabilistic_data_expression other) const
inline

Definition at line 189 of file probabilistic_data_expression.h.

◆ operator>=()

bool mcrl2::lps::probabilistic_data_expression::operator>= ( const probabilistic_data_expression other) const
inline

Definition at line 196 of file probabilistic_data_expression.h.

◆ remove_common_factors()

void mcrl2::lps::probabilistic_data_expression::remove_common_factors ( std::size_t &  enumerator,
std::size_t &  denominator 
)
inlineprotected

Definition at line 79 of file probabilistic_data_expression.h.

◆ to_number_t()

static std::size_t mcrl2::lps::probabilistic_data_expression::to_number_t ( const std::string &  s)
inlinestaticprotected

Definition at line 54 of file probabilistic_data_expression.h.

◆ zero()

static probabilistic_data_expression mcrl2::lps::probabilistic_data_expression::zero ( )
inlinestatic

Constant zero.

Definition at line 92 of file probabilistic_data_expression.h.


The documentation for this class was generated from the following file: