LTSPBISIM(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 LTSPBISIM(1) — the ltspbisim era

okay so bestie, welcome to the ltspbisim manual page, part of the mCRL2 toolset family 🎀 she's a little command-line icon and she's here to convert your LTS and, if you want, minimise it too. no cap.

✨ NAME ✨

ltspbisim — convert and optionally minimise an LTS 🦋

🌸 SYNOPSIS 🌸

ltspbisim [OPTION]... [INFILE [OUTFILE]]

💖 DESCRIPTION 💖

so here's the vibe: ltspbisim takes the labelled transition system (LTS) from INFILE and converts it to OUTFILE in whatever format you asked for, after applying the minimisation method you picked (and the default is literally none, she's chill like that). no OUTFILE? then stdout gets it. no INFILE? then she reads from stdin, main character energy 💅

the output format is decided by the extension of OUTFILE, whereas the input format is decided by the content of INFILE. and if you wanna be bossy about it, --in and --out force the input and output formats. the formats she speaks are:

  • 'aut' — the Aldebaran format (CADP) 🔥
  • 'dot' — the GraphViz format (no longer supported as input format, rip 💀)
  • 'fsm' — the Finite State Machine format
  • 'lts' — the mCRL2 LTS format (this one's the default, she's the favourite 👑)

🫶 OPTIONS 🫶

OPTION can be literally any of these:

  • -eNAME, --equivalence=NAME — generate an equivalent LTS that preserves equivalence NAME:
    • 'none' — identity equivalence (the default, no thoughts just vibes)
    • 'pbisim' — probabilistic bisimulation equivalence using the O(m(log n)) algorithm by Groote, Rivera-Verduzco and de Vink, 2017 ⚡
    • 'pbisim-bem' — probabilistic bisimulation equivalence using the O(mn (log n + log m)) algorithm by Baier, Engelen and Majster-Cederbaum, 2000 🧚
  • --timings[=FILE] — append timing measurements to FILE. if you don't give a FILE, the measurements go to standard error instead 🕐

⭐ 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 🙈 (yes she has secrets)

🌈 AUTHOR 🌈

Written by Hector Joao Rivera Verduzco. we stan 💜

🍓 REPORTING BUGS 🍓

found a bug? report it at <http://www.mcrl2.org/issuetracker>. do it, she wants to 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. (that's a real all-caps NO WARRANTY bestie, respect it 💀)

🧚 SEE ALSO 🧚

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

okay that's the whole page, go forth and convert 🦋 this was ltspbisim, mCRL2 toolset 202507..., dated October 2026 — catch you in the next manpage, mwah 💅💖

📦 where this page comes from