This file contains a class that contains labels for probabilistic transitions as a mCRL2 data expression of type real. More...

Classes
class	mcrl2::lps::probabilistic_data_expression
	This class contains labels for probabilistic transistions, consisting of a numerator and a denumerator. More...

struct	std::hash< mcrl2::lps::probabilistic_data_expression >

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.

namespace	mcrl2::lps
	The main namespace for the LPS library.

namespace	mcrl2::lps::detail

namespace	std
	STL namespace.

Functions
std::size_t	mcrl2::lps::detail::greatest_common_divisor (std::size_t x, std::size_t y)

void	mcrl2::lps::detail::remove_common_divisor (std::size_t &enumerator, std::size_t &denominator)

std::string	mcrl2::lps::pp (const probabilistic_data_expression &l)

std::ostream &	mcrl2::lps::operator<< (std::ostream &out, const probabilistic_data_expression &x)
	Pretty print to an outstream.

Detailed Description

This file contains a class that contains labels for probabilistic transitions as a mCRL2 data expression of type real.

Classes