PBES2BES(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 pbes2bes(1) 💅

okay bestie, you found the page for pbes2bes — that's a User Commands manual entry, and she is literally the glow-up machine of the mCRL2 toolset. she takes a PBES and hands you back a BES. no cap, it's giving "transformation era." 🦋

✨ SYNOPSIS ✨

pbes2bes [OPTION]... [INFILE [OUTFILE]]

🌸 DESCRIPTION 🌸

so here's the vibe: she reads the PBES from INFILE and writes an equivalent BES to OUTFILE. that's the whole main character arc. 👑

and if you're like "bestie what if I don't give her a file" — no worries:

  • no INFILE? she reads from stdin. casual. 💅
  • no OUTFILE? she writes to stdout. iconic.

🎀 OPTIONS 🎀

OPTION can be any of the following, and yes we're going through ALL of them because we don't skip parts in this house:

  • -eLEVEL, --erase=LEVEL — use remove level LEVEL to remove bes variables. the levels, queen by queen:
    • 'none' — never remove a generated bes variable and its equation. sounds chill but lowkey this can lead to excessive memory usage 😭 (this is the default)
    • 'some' — remove generated bes variables that do not occur anymore in the generated BES, except if the right hand side of its equation is true or false. the rhss of removed variables must have to be recalculated when this bes variable is encountered again.
    • 'all' — remove the equation for bes variables that do not occur anymore in the generated boolean equation system. this is quite memory efficient, but fr fr it can be very time consuming as the rhss of removed bes variables may have to be recalculated quite often. 💀
  • -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
  • -QNUM, --qlimit=NUM — limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, and NUM=0 means unlimited ✨)
  • -rNAME, --rewriter=NAME — use rewrite strategy NAME:
    • 'jitty' — jitty rewriting (default)
    • 'jittyc' — compiled jitty rewriting
    • 'jittyp' — jitty rewriting with prover
  • -zSEARCH, --search=SEARCH — use search strategy SEARCH:
    • 'breadth-first' — compute the right hand side of the boolean variables in a first come first served basis. this is comparable with a breadth-first search. this is good for generating counter examples. (default) 🫶
    • 'depth-first' — compute the right hand side of a boolean variables where the last generated variable is investigated first. this corresponds to a depth-first search. this can substantially outperform breadth-first search when the validity of a formula is determined at a larger depth. 🔥
    • 'b' — shorthand for breadth-first.
    • 'd' — shorthand for depth-first.
  • -sSTRAT, --strategy=STRAT — use substitution strategy STRAT, and bestie there are four of them so buckle up:
    • '0' — compute all boolean equations which can be reached from the initial state, without optimization. this is is the most data efficient option per generated equation. (default)
    • '1' — optimize by immediately substituting the right hand sides for already investigated variables that are true or false when generating an expression. this is as memory efficient as 0.
    • '2' — in addition to 1, also substitute variables that are true or false into an already generated right hand side. this can mean that certain variables become unreachable (e.g. X0 in X0 and X1, when X1 becomes false, assuming X0 does not occur elsewhere — and yes it will be maintained which variables have become unreachable as these do not have to be investigated). depending on the PBES, this can reduce the size of the generated BES substantially but requires a larger memory footprint. 🧠
    • '3' — in addition to 2, investigate for generated variables whether they occur on a loop, such that they can be set to true or false, depending on the fixed point symbol. this can increase the time needed to generate an equation substantially. ⏳
  • --timings[=FILE] — append timing measurements to FILE. measurements are written to standard error if no FILE is provided.
  • -u, --unused_data — do not remove unused parts of the data specification.

⭐ Standard options ⭐

the classics, the essentials, the little icons of the toolset:

  • -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, iykyk)

👑 AUTHOR 👑

Written by Jan Friso Groote. we stan. 🫶

🙈 REPORTING BUGS 🙈

Report bugs at <http://www.mcrl2.org/issuetracker>. please do, she wants to grow 🌱

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. (yes, all caps, they mean it fr fr 💀)

🌈 SEE ALSO 🌈

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

and that's the whole page babes — this was pbes2bes from the mCRL2 toolset 202507...., dated October 2026. go forth, transform your PBES into a BES, and slay 💅✨🎀

📦 where this page comes from