LPS2PBES(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💖 LPS2PBES(1) — like, the mCRL2 user-commands glow-up 💖

okay bestie, gather round, because this one is a whole converter and it's lowkey iconic 🎀

✨ NAME ✨

lps2pbes — generates a PBES from an LPS and a state formula. that's it, that's the vibe 💅

🌸 SYNOPSIS 🌸

lps2pbes [OPTION]... --formula=FILE [INFILE [OUTFILE]]

🦋 DESCRIPTION 🦋

so here's the tea 🍓: this tool takes the state formula sitting in FILE plus the LPS in INFILE, converts them into a parameterised boolean equation system (a PBES, iykyk) and saves the whole thing to OUTFILE.

no OUTFILE? it just yeets everything to stdout. no INFILE? it reads from stdin instead. main character energy, honestly 👑

💜 OPTIONS 💜

OPTION can be literally any of these, no cap:

  • -e, --check-only — check the syntax and semantics of the state formula and then dip — no PBES gets generated 🙈
  • -c, --counter-example — adds counter example equations to the generated PBES, so you can catch it in 4K 🔥
  • -fFILE, --formula=FILE — use the state formula from FILE
  • -oFORMAT, --out=FORMAT — use output format FORMAT, and the choices are:
    • 'bes' — BES in internal format
    • 'pbes' — PBES in internal format (this is the default, periodt)
    • 'pgsolver' — BES in PGSolver format
    • 'text' — PBES in textual (mCRL2) format
  • -m, --preprocess-modal-operators — insert dummy fixpoints in modal operators, which may lead to smaller PBESs ✨ (yes please)
  • -s, --structured — generate equations such that no mixed conjunctions and disjunctions occur 🧚 tidy queen behaviour
  • -t, --timed — use the timed version of the algorithm, even for untimed LPS's ⏰
  • --timings[=FILE] — append timing measurements to FILE. Measurements are written to standard error if no FILE is provided 📊
  • -u, --unoptimized — do not simplify boolean expressions 😭 (chaos, but okay)

⭐ 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 👀 (the secret menu, fr fr)

👑 AUTHOR 👑

Written by Wieger Wesselink; Tim Willemse. legends, both of them 💖

🔥 REPORTING BUGS 🔥

Report bugs at <http://www.mcrl2.org/issuetracker>. please do, bestie, they 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. zero. nada. 💀)

🎀 SEE ALSO 🎀

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

ok that's the whole page, go forth and generate those PBESs 🦋💅

and for the cute sign-off: this lil beauty is part of the mCRL2 toolset, version 202507, dated October 2026 — slay, see you in the next manpage 🌸✨💖

📦 where this page comes from