mcrl2/lts/lts_equivalence.h

Include file:

#include "mcrl2/lts/lts_equivalence.h"

Type recording the equivalence reductions supported by the LTS library.

Jan Friso Groote, Bas Ploeger, Muck van Weerdenburg, Jeroen Keiren

Enumerated types

type lts_equivalence

Values:

  • lts_eq_none Unknown or no equivalence
  • lts_eq_bisim Strong bisimulation equivalence using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017]
  • lts_eq_bisim_gv Strong bisimulation equivalence using the O(mn) algorithm [Groote/Vaandrager 1990]
  • lts_eq_bisim_dnj Strong bisimulation equivalence using the O(m log n) algorithm directly on an LTS; experimental.
  • lts_eq_bisim_sigref Strong bisimulation equivalence using the signature refinement algorithm [Blom/Orzan 2003]
  • lts_eq_branching_bisim Branching bisimulation equivalence using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017]
  • lts_eq_branching_bisim_gv Branching bisimulation equivalence using the O(mn) algorithm [Groote/Vaandrager 1990]
  • lts_eq_branching_bisim_dnj Branching bisimulation equivalence using the O(m log n) algorithm directly on an LTS; experimental
  • lts_eq_branching_bisim_sigref Branching bisimulation equivalence using the signature refinement algorithm [Blom/Orzan 2003]
  • lts_eq_divergence_preserving_branching_bisim Divergence-preserving branching bisimulation equivalence using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017]
  • lts_eq_divergence_preserving_branching_bisim_gv Divergence-preserving branching bisimulation equivalence using the O(mn) algorithm [Groote/Vaandrager 1990]
  • lts_eq_divergence_preserving_branching_bisim_dnj Divergence-preserving branching bisimulation equivalence using the O(m log n) algorithm directly on an LTS; experimental
  • lts_eq_divergence_preserving_branching_bisim_sigref
  • lts_eq_weak_bisim Divergence-preserving branching bisimulation equivalence using the signature refinement algorithm [Blom/Orzan 2003] Weak bisimulation equivalence
  • lts_eq_divergence_preserving_weak_bisim Divergence-preserving weak bisimulation equivalence
  • lts_eq_sim Strong simulation equivalence
  • lts_eq_ready_sim Strong ready-simulation equivalence
  • lts_eq_trace Strong trace equivalence
  • lts_eq_weak_trace Weak trace equivalence
  • lts_red_tau_star Tau star reduction
  • lts_red_determinisation Used for a determinisation reduction

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.

Functions

std::string mcrl2::lts::description(const lts_equivalence eq)

Gives a description of an equivalence.

Parameters:

  • eq The equivalence type.

Returns: A string describing the equivalence specified by eq.

std::ostream &mcrl2::lts::operator<<(std::ostream &os, const lts_equivalence eq)
std::istream &mcrl2::lts::operator>>(std::istream &is, lts_equivalence &eq)
lts_equivalence mcrl2::lts::parse_equivalence(std::string const &s)

Determines the equivalence from a string.

The following strings may be used:

  • “none” for identity equivalence;
  • “bisim” for strong bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017];
  • “bisim-gv” for strong bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990];
  • “bisim-sig” for strong bisimilarity using the signature refinement algorithm [Blom/Orzan 2003];
  • “branching-bisim” for branching bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017];
  • “branching-bisim-gv” for branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990];
  • “branching-bisim-sig” for branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003];
  • “dpbranching-bisim” for divergence-preserving branching bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017];
  • “dpbranching-bisim-gv” for divergence-preserving branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990];
  • “dpbranching-bisim-sig” for divergence-preserving branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003];
  • “weak-bisim” for weak bisimilarity;
  • “dpweak-bisim” for divergence-preserving weak bisimilarity;
  • “sim” for strong simulation equivalence;
  • “trace” for strong trace equivalence;
  • “weak-trace” for weak trace equivalence;
  • “determinisation” for a determinisation reduction.

Parameters:

  • s The string specifying the equivalence.

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

std::string mcrl2::lts::print_equivalence(const lts_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.