mcrl2/lts/lts_probabilistic_equivalence.h

Include file:

#include "mcrl2/lts/lts_probabilistic_equivalence.h"

Type recording the probabilistic equivalence reductions supported by the LTS library.

Hector Joao Rivera Verduzco

Enumerated types

type mcrl2::lts::lts_probabilistic_equivalence

Values:

  • lts_probabilistic_eq_none Unknown or no equivalence

  • lts_probabilistic_bisim_bem Probabilistic bisimulation equivalence using the O(mn (log n + log m)) algorithm [Bier]

  • lts_probabilistic_bisim_grv Probabilistic bisimulation equivalence using the O(m(log n)) algorithm by Groote, Rivera Verduzco and de Vink

LTS equivalence relations.

This enumerated type defines equivalence relations on LTSs. They can be used to reduce an LTS or decide whether two LTSs are equivalent.

type mcrl2::lts::lts_probabilistic_preorder

Values:

  • lts_probabilistic_pre_none Unknown or no preorder

LTS preorder relations.

This enumerated type defines equivalence relations on LTSs. They can be used to reduce an LTS or decide whether two LTSs are equivalent.

Functions

std::string mcrl2::lts::description(const lts_probabilistic_equivalence &eq)

Gives a description of an equivalence.

Parameters:

  • eq The equivalence type.

Returns: A string describing the equivalence specified by eq.

std::string mcrl2::lts::description(const lts_probabilistic_preorder &pre)

Gives a description of an preorder.

Parameters:

  • pre The preorder type.

Returns: A string describing the preorder specified by pre.

std::ostream &mcrl2::lts::operator<<(std::ostream &os, const lts_probabilistic_equivalence &eq)
std::ostream &mcrl2::lts::operator<<(std::ostream &os, const lts_probabilistic_preorder &pre)
std::istream &mcrl2::lts::operator>>(std::istream &is, lts_probabilistic_equivalence &eq)
std::istream &mcrl2::lts::operator>>(std::istream &is, lts_probabilistic_preorder &eq)
lts_probabilistic_equivalence mcrl2::lts::parse_probabilistic_equivalence(const std::string &s)

Determines the equivalence from a string.

The following strings may be used:

  • “none” for identity equivalence;

  • “pbisim” for Probabilistic bisimulation equivalence using the O(mn (log n + log m)) algorithm [Bier];

Parameters:

  • s The string specifying the equivalence.

Returns: The equivalence type specified by s. If s is none of the above values then lts_probabilistic_eq_none is returned.

lts_probabilistic_preorder mcrl2::lts::parse_probabilistic_preorder(std::string const &s)

Determines the probabilistic preorder from a string.

The following strings may be used:

  • “none” for identity preorder;

Parameters:

  • s The string specifying the equivalence.

Returns: The equivalence type specified by s. If s is none of the above values then lts_probabilistic_pre_none is returned.

std::string mcrl2::lts::print_probabilistic_equivalence(const lts_probabilistic_equivalence &eq)

Gives the short name of an equivalence.

Parameters:

  • eq The equivalence type.

Returns: A short string representing the equivalence specified by eq. The returned value is one of the strings listed for parse_equivalence.

std::string mcrl2::lts::print_probabilistic_preorder(const lts_probabilistic_preorder &pre)

Gives the short name of an preorder.

Parameters:

  • pre The preorder type.

Returns: A short string representing the preorder specified by pre. The returned value is one of the strings listed for parse_preorder.