LTSCONVERT(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 ltsconvert(1) — the ltsconvert glow-up page ✨

okay so this is the manual page for ltsconvert, a User Commands situation in the mCRL2 toolset, and bestie, it's about to convert your whole LTS life. buckle up 🎀

🌸 NAME 🌸

ltsconvert — convert and optionally minimise an LTS. that's it, that's the vibe. 💖

✨ SYNOPSIS ✨

ltsconvert [OPTION]... [INFILE [OUTFILE]]

🦋 DESCRIPTION 🦋

so here's the tea: ltsconvert 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 (default is none, like, no minimisation, just vibes).

  • no OUTFILE? stdout gets it. 🫶
  • no INFILE? stdin is the source. slay.

the output format is decided by the extension of OUTFILE, and the input format is decided by the content of INFILE. plot twist! but you can force both with --in and --out if you're a control freak (respectfully). 💅

the supported formats, iconic lineup:

  • 'aut' — for the Aldebaran format (CADP)
  • 'dot' — for the GraphViz format (no longer supported as input format — she's output-only now, okurrr)
  • 'fsm' — for the Finite State Machine format
  • 'lts' — for the mCRL2 LTS format (default)

🔥 OPTIONS 🔥

OPTION can be literally any of the following, no cap:

  • -D, --determinise — determinise LTS. make it deterministic, periodt. ⭐
  • -eNAME, --equivalence=NAME — generate an equivalent LTS that preserves the equivalence NAME. the full menu, and yes, you're getting 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]
    • 'bisim-sig' — strong bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]
    • '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]
    • 'branching-bisim-sig' — branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]
    • '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]
    • 'dpbranching-bisim-sig' — divergence-preserving branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]
    • '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
    • 'tau-star' — tau star reduction

ngl that's a lot of bisim and we're obsessed with all of them 💜

  • -iFORMAT, --in=FORMAT — use FORMAT as the input format. force it, bestie.
  • -lFILE, --lps=FILE — use FILE as the LPS from which the input LTS was generated. this might be needed to store the correct parameter names of states when saving in fsm format, and to convert non-mCRL2 LTSs to a mCRL2 LTS. iykyk 🧚
  • --no-reach — do not perform a reachability check on the input LTS. skipping the vibe check, bold move.
  • -n, --no-state — remove the state information. this can be useful when state labels are huge (we're talking huge huge 😭).
  • -oFORMAT, --out=FORMAT — use FORMAT as the output format.
  • --tau=ACTNAMES — consider actions with a name in the comma separated list ACTNAMES to be internal (tau) actions, in addition to those already defined as such by the input. adding to the tau squad 🫶
  • --timings[=FILE] — append timing measurements to FILE. measurements are written to standard error if no FILE is provided.

🌈 Standard options 🌈

the classics, the main characters:

  • -q, --quiet — do not display warning messages. ignorance is bliss 💅
  • -v, --verbose — display short log messages.
  • -d, --debug — display detailed log messages. give me all the lore.
  • --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. the secret menu 👀

🎀 AUTHOR 🎀

written by Muck van Weerdenburg, Jan Friso Groote. kings. 👑

🐛 REPORTING BUGS 🐛

report bugs at <http://www.mcrl2.org/issuetracker>. pls do, it's giving community support 💖

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. read that again: NO WARRANTY. don't come for her if things go sideways 💀

🌸 SEE ALSO 🌸

see also the manual at <http://www.mcrl2.org/web/user_manual/tools/release/ltsconvert.html>. go read it, it's iconic.

and that's the page, bestie 🫶 this whole thing is ltsconvert from the mCRL2 toolset, version 20250..., dated October 2026 — catch you on the next man page 💜✨

📦 where this page comes from