LTSCOMPARE(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 ltscompare(1) — User Commands, bestie

okay so like, welcome to ltscompare, the tool that answers the one question every LTS girlie needs answered: are these two things literally the same, or nah? This is the LTSCOMPARE(1) situation and honestly it's giving main character energy. 🦋

✨ NAME ✨

ltscompare — compare two LTSs

🌸 SYNOPSIS 🌸

ltscompare [OPTION]... [INFILE1] INFILE2

💖 DESCRIPTION 💖

So here's the vibe check: ltscompare determines whether or not the labelled transition systems (LTSs) in INFILE1 and INFILE2 are related by some equivalence or preorder. That's it, that's the whole job, and it ate. 💅

  • If INFILE1 is not supplied, stdin is used.
  • If INFILE1 and/or INFILE2 is -, stdin is used.
  • Reading two LTSs via stdin is only supported for the 'aut' format, and those LTSs must be separated by an EOT character (4). no cap, that's a hard requirement bestie 🫶

The input formats are determined by the contents of INFILE1 and INFILE2. If you don't trust the vibes, options --in1 and --in2 can be used to force the input format of INFILE1 and INFILE2, respectively. The supported formats are:

  • 'aut' for the Aldebaran format (CADP)
  • 'dot' for the GraphViz format (no longer supported as input format) 💀
  • 'fsm' for the Finite State Machine format
  • 'lts' for the mCRL2 LTS format

🔥 OPTIONS 🔥

OPTION can be any of the following:

  • -c, --counter-example — generate a counter example if the input lts's are not equivalent. iconic behavior tbh 😭
  • --counter-example-file=NAME — the file to which the counterexample should be written
  • -eNAME), --equivalence=NAME) — use equivalence NAME (not allowed in combination with -p/--preorder). here's the whole menu, bestie, and yes you're gonna read all of it 🙈
    • 'none' — identity equivalence (default)
    • 'bisim' — strong bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
    • 'bisim-gv' — strong bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]
    • 'bisim-gjkw' — strong bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]
    • 'bisim-gj' — strong bisimilarity using the O(m log n) experimental algorithm [Groote/Jansen 2024]
    • 'branching-bisim' — branching bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
    • 'branching-bisim-gv' — branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]
    • 'branching-bisim-gjkw' — branching bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]
    • 'branching-bisim-gj' — branching bisimilarity using the O(m log n) experimental algorithm [Groote/Jansen 2024]
    • 'dpbranching-bisim' — divergence-preserving branching bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
    • 'dpbranching-bisim-gv' — divergence-preserving branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]
    • 'dpbranching-bisim-gjkw' — divergence-preserving branching bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]
    • 'dpbranching-bisim-gj' — divergence-preserving branching bisimilarity using the O(m log n) experimental algorithm [Groote/Jansen 2024]
    • 'weak-bisim' — weak bisimilarity
    • 'dpweak-bisim' — divergence-preserving weak bisimilarity
    • 'sim' — strong simulation equivalence
    • 'ready-sim' — strong ready simulation equivalence
    • 'trace' — strong trace equivalence
    • 'weak-trace' — weak trace equivalence
    • 'coupled-sim' — coupled simulation equivalence
  • -iFORMAT, --in1=FORMAT — use FORMAT as the format for INFILE1 (or stdin)
  • -jFORMAT, --in2=FORMAT — use FORMAT as the format for INFILE2
  • -pNAME, --preorder=NAME — use preorder NAME (not allowed in combination with -e/--equivalence). the preorder lineup, get into it ✨
    • 'unknown' — default void preorder (default)
    • 'sim' — strong simulation preorder
    • 'ready-sim' — strong ready simulation preorder
    • 'trace' — strong trace preorder
    • 'weak-trace' — weak trace preorder
    • 'trace-ac' — trace preorder based on an anti chain algorithm
    • 'weak-trace-ac' — weak trace preorder based on an anti chain algorithm
    • 'failures' — failures refinement
    • 'weak-failures' — weak failures refinement
    • 'failures-divergence' — failures divergence refinement (automatically weak)
    • 'impossible-futures' — impossible futures
  • -sNAME, --strategy=NAME — explore the state space using strategy NAME (only for antichain based algorithms; includes all failures refinements):
    • 'b', 'breadth' — breadth-first search (default)
    • 'd', 'depth' — depth-first search
  • --tau=ACTNAMES — consider actions with a name in the comma separated list ACTNAMES to be internal (tau) actions in addition to those defined as such by the input
  • --timings[=FILE] — append timing measurements to FILE. Measurements are written to standard error if no FILE is provided

⭐ Standard options ⭐

  • -q, --quiet — do not display warning messages 🤫
  • -v, --verbose — display short log messages
  • -d, --debug — display detailed log messages
  • --log-level=LEVEL — display log messages up to and including level; either warn, verbose, debug or trace
  • -h, --help — display help information
  • --version — display version information
  • --help-all — display help information, including hidden and experimental options 👀

🎀 AUTHOR 🎀

Written by Muck van Weerdenburg. we stan 🫶

🦋 REPORTING BUGS 🦋

Report bugs at <http://www.mcrl2.org/issuetracker>. please do it, the maintainers wanna know fr fr 😭

Copyright © 2025 Technische Universiteit Eindhoven.

This is free software. You may redistribute copies of it under the terms of the Boost Software License <http://www.boost.org/LICENSE_1_0.txt>. There is NO WARRANTY, to the extent permitted by law. (that's the dramatic part, bestie — no warranty at all 💀)

💜 SEE ALSO 💜

See also the manual at <http://www.mcrl2.org/web/user_manual/tools/release/ltscompare.html>. iykyk 🔥

and that's the whole page, no skips, no cap. go compare some LTSs, you're gonna slay. 👑

ltscompare — mCRL2 toolset 20250... — October 2026 — that's the version and date, mwah 💋

📦 where this page comes from