PBESPARELM(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 PBESPARELM(1) — the group chat guide

okay bestie, welcome to the pbesparelm page 💖 this one's a User Command straight out of the mCRL2 toolset, and honestly? it's giving "small but mighty". it takes your PBES and does parameter elimination on it. that's the whole vibe. iconic, honestly 🎀

✨ NAME ✨

pbesparelm — remove unused parameters from a PBES 🧹✨

like, it literally goes in and yeets the parameters nobody's using. self-care for your PBES, fr fr 💅

🌸 SYNOPSIS 🌸

pbesparelm [OPTION]... [INFILE [OUTFILE]]

🦋 DESCRIPTION 🦋

so here's the tea ☕: pbesparelm reads a file containing a PBES, and applies parameter elimination to it.

where does it read from and write to? adorable of you to ask:

  • if OUTFILE is not present, standard output is used 🖨️
  • if INFILE is not present, standard input is used ⌨️

that's it. that's the whole thing. no cap. it's literally that simple and honestly we love a low-drama tool 🫶

💜 OPTIONS 💜

OPTION can be any of the following:

  • -iFORMAT, --in=FORMAT — use input format FORMAT:
    • 'pbes' — PBES in internal format (default ✨)
    • 'pgsolver' — BES in PGSolver format
    • 'text' — PBES in textual (mCRL2) format
  • -oFORMAT, --out=FORMAT — use output format FORMAT:
    • 'bes' — BES in internal format
    • 'pbes' — PBES in internal format (default ✨)
    • 'pgsolver' — BES in PGSolver format
    • 'text' — PBES in textual (mCRL2) format
  • --timings[=FILE] — append timing measurements to FILE. Measurements are written to standard error if no FILE is provided ⏱️
ngl bestie, don't sleep on that 'bes' output option — it's right there and it's not the default, so pick it on purpose, okay? iykyk 💀

🌈 Standard options 🌈

the classics. the main characters of every mCRL2 tool 💅

  • -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 Wieger Wesselink; Simon Janssen and Tim Willemse. absolute legends, no notes 🔥

💀 REPORTING BUGS 💀

Report bugs at <http://www.mcrl2.org/issuetracker>.

like, please actually report them instead of just screaming into the void? the maintainers 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.

bestie i'm serious about the all-caps there — NO WARRANTY. don't come crying to the Eindhoven girlies if it eats your PBES 😭

🌟 SEE ALSO 🌟

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

alright that's the whole page, you ate that 🍓✨ this was pbesparelm from the mCRL2 toolset, version 20250..., dated October 2026 — mwah, go eliminate some parameters, icon 💋👑

📦 where this page comes from