LTSPCOMPARE(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 NAME

ltspcompare — literally just compare two LTSs, bestie ✨

okay so this is the tool that looks at two labelled transition systems and is like "are these two things related or not" — and honestly? it ate. 🫶

🌸 SYNOPSIS

ltspcompare [OPTION]... [INFILE1] INFILE2

🦋 DESCRIPTION

So what it actually does: it determines whether the labelled transition systems sitting in INFILE1 and INFILE2 are related by some probabilistic equivalence or preorder. That's the whole vibe check. If INFILE1 isn't supplied, no stress — stdin gets used instead. 💖

The input formats are figured out from the contents of INFILE1 and INFILE2, which is honestly so smart of it. But if you wanna force it, the options --in1 and --in2 let you set the input format of INFILE1 and INFILE2 respectively. Iconic. The supported formats are:

  • 'aut' for the Aldebaran format (CADP)
  • 'dot' for the GraphViz format (no longer supported as input format — rip, it's giving retired 💀)
  • 'fsm' for the Finite State Machine format
  • 'lts' for the mCRL2 LTS format

✨ OPTIONS ✨

OPTION can be literally any of these:

  • -eNAME, --equivalence=NAME — use equivalence NAME. Not allowed in combination with -p/--preorder, so pick a lane bestie. Your choices: 'none' identity equivalence (default), 'pbisim' probabilistic bisimulation equivalence using the O(m(log n)) algorithm by Groote, Rivera-Verduzco and de Vink, 2017, or 'pbisim-bem' probabilistic bisimulation equivalence using the O(mn (log n + log m)) algorithm by Baier, Engelen and Majster-Cederbaum, 2000 👑
  • -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, fr fr pick one. Choices: 'none' identity preorder (default)
  • --tau=ACTNAMES — treat actions whose names are in the comma separated list ACTNAMES as internal (tau) actions, on top of the ones already defined as such by the input 🙈
  • --timings[=FILE] — append timing measurements to FILE. If you don't give a FILE, the measurements get written to standard error instead. cute.

🌈 Standard options

  • -q, --quiet — do not display warning messages (silence! 🤫)
  • -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 Jan Friso Groote. king behavior honestly 👑

💜 REPORTING BUGS

Report bugs at <http://www.mcrl2.org/issuetracker>. Please do, the devs wanna know 🫶

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. Like, none at all, don't come for them 😭

⭐ SEE ALSO

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

okay bestie that's the whole page 💅 this is ltspcompare from the mCRL2 toolset 2025, dated October 2026, and yeah — that's your LTSPCOMPARE(1) manual page, periodt 🎀✨

📦 where this page comes from