mcrl2::lps::probabilistic_data_expression

Include file:

#include "mcrl2/lps/probabilistic_data_expression.h

class mcrl2::lps::probabilistic_data_expression

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.

Protected static member functions

static data::data_specification data_specification_with_real()

static std::size_t greatest_common_divisor(std::size_t x, std::size_t y)

static const data::rewriter &m_rewriter()

static std::size_t to_number_t(const std::string &s)

Protected member functions

void remove_common_factors(std::size_t &enumerator, std::size_t &denominator)

Public static member functions

static probabilistic_data_expression one()

Constant one.

static probabilistic_data_expression zero()

Constant zero.

Public member functions

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.

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()

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(const std::string &enumerator, const std::string &denominator)

probabilistic_data_expression(std::size_t enumerator, std::size_t denominator)