PBES2BOOL(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 PBES2BOOL 💅

ok so this is the pbes2bool page from the User Commands manual, and honestly? it's a little icon. quick vibe check before we dive in: it takes a (P)BES and solves it. that's the whole thing. let's get into it 🫶

✨ NAME ✨

pbes2bool — bestie, it generates a BES from a PBES and solves it. that's the job. that's the assignment. periodt 💅

🌸 SYNOPSIS 🌸

pbes2bool [OPTION]... [INFILE]

🦋 DESCRIPTION 🦋

okay so here's what's actually happening: pbes2bool solves a (P)BES from INFILE. and if INFILE isn't there? no stress, it just reads from stdin instead 🫶

the PBES first gets instantiated into a parity game, and then that parity game gets solved using Zielonka's algorithm. iconic algorithm, no notes.

and the best part — it supports generating a witness or a counter example for the property that's encoded by the PBES. so you don't just get a yes/no, you can get the receipts 🔥

🎀 OPTIONS 🎀

OPTION can be any of the following, bestie:

  • --evidence-file=NAME — the file where the evidence gets written. if you don't set it, a default name is chosen for you. lowkey convenient ✨
  • -fNAME, --file=NAME — the file containing the LPS or LTS that was used to generate the PBES using lps2pbes -c. if you set this, a counter example or witness for the encoded property will be generated. heads up on the extension: it should be .lps in case of an LPS file, and in all other cases it's assumed to be an LTS.
  • -iFORMAT, --in=FORMAT — use input format FORMAT: 'pbes' means PBES in internal format (and that's the default btw).
  • --prune-todo-list — prune the todo list periodically. she's tidy 💅
  • -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
  • -zNAME, --search-strategy=NAME — use search strategy NAME:
    • 'breadth-first' — leads to smaller counter examples (default)
    • 'depth-first'
  • -sNAME, --solve-strategy=NAME — use solve strategy NAME. strategies 1–4 periodically apply on-the-fly solving, which may lead to early termination. 👀
    • '0' — no on-the-fly solving is applied (default)
    • '1' — propagate solved equations using an attractor
    • '2' — detect winning loops
    • '3' — solve subgames using a fatal attractor
    • '4' — solve subgames using the solver
  • --threads=NUM — run with NUM threads (default=1). ⚠️ with multiple threads the stack size on a Mac is limited, which can lead to bus errors. so like... be careful out there 🫶
  • --timings[=FILE] — append timing measurements to FILE. measurements are written to standard error if no FILE is provided.

⭐ Standard options ⭐

the everyday essentials, fr fr:

  • -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. thank you legend 🫶

💀 REPORTING BUGS 💀

found a bug? don't suffer in silence bestie, report it at <http://www.mcrl2.org/issuetracker>. the maintainers wanna know, fr fr 🙈

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>.

⚠️ and just so we're clear: there is NO WARRANTY, to the extent permitted by law. none. zero. don't come for them if it goes sideways 💀

🧚 SEE ALSO 🧚

see also the manual at <http://www.mcrl2.org/web/user_manual/tools/release/pbes2bool.html>. iykyk 💖

and that's the whole page, bestie ✨ this one's from the mCRL2 toolset, version 202507..., dated October 2026 — and the page itself is PBES2BOOL(1). go solve some PBESes, you absolute main character 👑💅

📦 where this page comes from