Include file:

#include "mcrl2/lts/lts_preorder.h"

Supperted preorders for LTSes.

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

Enumerated types

type mcrl2::lts::lts_preorder


  • lts_pre_none Unknown or no preorder
  • lts_pre_sim Strong simulation preorder
  • lts_pre_ready_sim Strong ready simulation preorder
  • lts_pre_trace Strong trace preorder
  • lts_pre_weak_trace Weak trace preorder
  • lts_pre_trace_anti_chain Trace preorder based on anti chains
  • lts_pre_weak_trace_anti_chain Weak trace preorder based on anti chains
  • lts_pre_failures_refinement Failures refinement based on anti chains
  • lts_pre_weak_failures_refinement Weak failures refinement based on anti chains
  • lts_pre_failures_divergence_refinement Failures divergence refinement based on anti chains, which is automatically weak
  • lts_preorder_min
  • lts_preorder_max

LTS preorder relations.

This enumerated type defines preorder relations on LTSs. They can be used to decide whether one LTS is behaviourally contained in another LTS.


std::string mcrl2::lts::description(const lts_preorder pre)

Gives a description of a preorder.


  • pre The preorder type.

Returns: A string describing the preorder specified by eq.

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

Determines the preorder from a string.

The following strings may be used:

  • “sim” for strong simulation preorder;
  • “trace” for strong trace preorder;
  • “weak-trace” for weak trace preorder.


  • s The string specifying the preorder.

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

std::string mcrl2::lts::print_preorder(const lts_preorder pre)

Gives the short name of a preorder.


  • 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.