PBESINST(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 PBESINST(1) 💅

okay bestie, sit down, we're doing the pbesinst page from the User Commands manual and honestly? it's giving main character energy for a tool that just... converts one file into another file. but it's SO good at it. let's go 🫶

✨ NAME ✨

pbesinst — compute a BES out of a PBES

like, it takes your parameterised thing and gives you a non-parameterised thing. the way that it just does that. 🔥

🌸 SYNOPSIS 🌸

pbesinst [OPTION]... [INFILE [OUTFILE]]

🦋 DESCRIPTION 🦋

So here's the vibe: it transforms the PBES from INFILE into an equivalent BES and writes it to OUTFILE. That's the whole job. And it ate. 💅

  • If INFILE isn't there → standard input is used.
  • If OUTFILE isn't there → standard output is used.

ngl the format of OUTFILE is determined by its extension (unless you specify it with an option, obviously). the supported formats are:

  • 'pbes' for the mCRL2 PBES format
  • 'bes' for the mCRL2 BES format

🎀 OPTIONS 🎀

OPTION can be any of the following, and yes, we're listing every single one, because leaving stuff out is not the vibe:

  • -iFORMAT, --in=FORMAT — use input format FORMAT:
    • 'pbes' — PBES in internal format (this is the default, bestie)
    • '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 energy ✨)
    • 'pgsolver' — BES in PGSolver format
    • 'text' — PBES in textual (mCRL2) format
  • -QNUM, --qlimit=NUM — limit the enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, and NUM=0 means unlimited, so go off king 👑).
  • -e, --remove-equations — remove redundant equations. decluttering era 🧹
  • -rNAME, --rewriter=NAME — use rewrite strategy NAME:
    • 'jitty' — jitty rewriting (default)
    • 'jittyc' — compiled jitty rewriting
    • 'jittyp' — jitty rewriting with prover
  • -zNAME, --search=NAME — search the state space using strategy NAME:
    • '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.
  • -f[PARAMS], --select[=PARAMS] — select finite parameters that need to be expanded. Examples: --select=X1(b:Bool,c:Bool);X2(b:Bool) or --select=*(*:Bool).
ngl this option only has effect when used together with --strategy=finite. like, it literally will not do anything otherwise. iykyk 🙈
  • -sNAME, --strategy=NAME — compute the BES using strategy NAME:
    • 'lazy' — for computing only boolean equations which can be reached from the initial state
    • 'alternative-lazy' — an alternative version of the lazy strategy that supports more options (default)
    • 'finite' — for computing all possible boolean equations
  • --timings[=FILE] — append timing measurements to FILE. Measurements are written to standard error if no FILE is provided. clock it ⏱️
  • -ONAME, --transformation=NAME — optimize the BES using strategy NAME:
    • '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). 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.

⭐ Standard options ⭐

the classics, the icons, the ones you actually use every day:

  • -q, --quiet — do not display warning messages. silence is golden 💀
  • -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, lowkey 👀

💜 AUTHOR 💜

Written by Wieger Wesselink; Alexander van Dam and Tim Willemse. legends, fr fr 🌈

🍓 REPORTING BUGS 🍓

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

bestie if it's broken, TELL THEM. do not suffer in silence 😭

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/pbesinst.html>.

and that's the page!! mwah 💋 this was pbesinst from the mCRL2 toolset version 202507...., dated October 2026 — yeah the version string really does end in four dots, we don't make the rules, we just think it's iconic 🎀✨👑

📦 where this page comes from