LPS2LTS(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 LPS2LTS(1) — the lps2lts girlie's guide

okay so real talk, this is the manual page for lps2lts, a User Commands icon in the mCRL2 toolset. she takes your LPS and gives you an LTS. that's it, that's the vibe. let's get into it ✨

🌸 SYNOPSIS 🌸

lps2lts [OPTION]... [INFILE [OUTFILE]]

🦋 DESCRIPTION 🦋

so what does she do? she transforms the LPS in INFILE and writes a corresponding LTS to OUTFILE. literally that's the whole job, and she does it flawlessly 💅

  • if OUTFILE isn't there, or it's -, and an output format is specified → stdout gets the glow-up.
  • if INFILE isn't there, or it's - → stdin is the main character.

✨ OPTIONS ✨

OPTION can be any of the following, bestie. strap in, there's a lot and they're all iconic:

  • -aNAMES, --action=NAMES — reports actions in the transition system that occur in the comma-separated list of action names NAMES. and ooh, the flag --trace can be used to generate traces to these actions 🫶
  • --cached — uses enumeration caching techniques to speed up state space generation. speed. slay.
  • -c[NAME], --confluence[=NAME] — applies prioritization of transitions with the action label NAME (default 'ctau'). to give priority to tau, use the flag -ctau. important caveat, no cap: only if the linear process is tau-confluent is the generated state space branching bisimilar to the state space of the lps. the generation algorithm that's used does not require the linear process to be tau convergent 💜
  • -D, --deadlock — reports deadlocks, i.e. states with no outgoing transitions. the flag --trace can be used to generate traces to these deadlocks 💀
  • -F, --divergence — reports divergences, i.e. states with a tau loop. heads up: the algorithm to detect divergences is linear for every state, so state space exploration becomes quadratic with this option enabled 😭. the flag --trace can be used to generate traces to these divergences.
  • -lNUM, --max=NUM — explores at most NUM states. boundaries, we love them.
  • -mNAMES, --multiaction=NAMES — reports occurrences of multi-actions in the transition system that occur in the comma-separated list of actions NAMES. works like --action, except that multi-actions are matched exactly, including data parameters. the flag --trace can be used to generate traces to these multi-actions ✨
  • --no-info — does not add state label information to OUTFILE. this option only applies to .lts files.
  • --no-probability-checking — does not check if probabilities in stochastic specifications have sensible values. living dangerously, honestly.
  • -n, --nondeterminism — reports nondeterministic states, i.e. states with outgoing transitions with the same label to different states. the flag --trace can be used to generate traces to these nondeterministic states 🙈
  • -oFORMAT, --out=FORMAT — saves the output in the specified FORMAT.
  • -QNUM, --qlimit=NUM — limits enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited) 🔥
  • -rNAME, --rewriter=NAME — uses rewrite strategy NAME:
    • 'jitty' — jitty rewriting (default) 👑
    • 'jittyc' — compiled jitty rewriting
    • 'jittyp' — jitty rewriting with prover
  • --save-at-end — delays saving of the generated LTS until the end. this option only applies to .aut and .lts files, which are by default saved on the fly. dramatic finale energy 🎀
  • -sNAME, --strategy=NAME — explores the state space using strategy NAME:
    • 'b', 'breadth' — breadth-first search (default)
    • 'd', 'depth' — depth-first search
    • 'h', 'highway' — highway search. only part of the state space is explored, by restricting the size of the todo list. N.B. the implementation deviates slightly from the published version 👀
  • --suppress — in verbose mode, does not print progress messages indicating the number of visited states and transitions. quiet luxury.
  • --tau=NAMES — considers actions that occur in the comma-separated list of action names NAMES to be internal. this setting only affects the option --divergence.
  • --threads=NUM — runs with NUM threads (default 1). with multiple threads the stack size on a Mac is limited, which can lead to bus errors 😭 careful bestie.
  • --timings[=FILE] — appends timing measurements to FILE. measurements are written to standard error if no FILE is provided.
  • --todo-max=NUM — keeps at most NUM states in the todo list; this option is only relevant for highway search, where NUM is the maximum number of states per level per thread.
  • -t[NUM], --trace[=NUM] — writes a trace to states that are reported using one of the flags --action, --deadlock, --divergence, --multiaction or --nondeterminism. after NUM traces have been written, state space generation stops. if NUM is not supplied, the number of traces is not limited. for each trace a unique file with extension .trc (trace) will be created, containing a shortest trace starting from the initial state. the traces can be pretty printed and converted to other formats using tracepp. if the maximum amount of traces has been reached, state space generation is aborted. and fr fr: there is no guarantee that the traces are fully contained in the partial state space 🫶

⭐ Standard options ⭐

the classics. the essentials. we stan:

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

👑 AUTHOR 👑

Written by Wieger Wesselink. (thank you king 🫡)

💀 REPORTING BUGS 💀

Report bugs at <http://www.mcrl2.org/issuetracker>. don't suffer in silence bestie, tell them.

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.

🌈 SEE ALSO 🌈

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

💖 that's the whole page, bestie. go forth and generate those state spaces.

so yeah — that's lps2lts from the mCRL2 toolset, version 202507.0..., dated October 2026. mwah, catch you in the next manpage 💅✨🌸

📦 where this page comes from