PBESSOLVESYMBOLIC(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 pbessolvesymbolic(1) 💅

okay so bestie, welcome to pbessolvesymbolic, a genuine mCRL2 toolset icon from the User Commands section of the manual, and she is here to solve a PBES for you. no cap.

🌸 NAME 🌸

pbessolvesymbolic — solves a PBES using symbolic data structures. yes queen, that's literally her whole job.

✨ SYNOPSIS ✨

pbessolvesymbolic [OPTION]... [INFILE [OUTFILE]]

🦋 DESCRIPTION 🦋

So. She solves the PBES from INFILE. and like, if INFILE isn't there? she just reads from stdin, nbd, she's flexible like that 🫶

The way it works is: the PBES gets first instantiated into a parity game, and then that parity game is solved using Zielonka's algorithm. that's the pipeline, that's the lore, that's the whole vibe. 💖

🎀 OPTIONS 🎀

OPTION can be literally any of the following, and yes there are a lot of them, we're getting through all of them:

  • --cached — use transition group caching to speed up state space exploration. she's caching, she's thriving ✨
  • --chaining — reduces the amount of breadth-first iterations by applying the transition groups consecutively.
  • --evidence-file=NAME — the file that the evidence gets written to. if you don't set it, a default name will be chosen for you. she's got you 💅
  • -fNAME, --file=NAME — the file containing the LPS or LTS that was used to generate the PBES using lps2pbes -c. if this option is set, a counter example or witness for the encoded property will be generated. the extension of the file should be .lps in case of an LPS file — in all other cases it is assumed to be an LTS. iykyk 🐚
  • --groups[=GROUPS] — summand grouping, and there are options, so many options:
    • 'none' (default) — no summand groups
    • 'used' — summands with the same variables are joined
    • 'simple' — summands with the same read/write variables are joined
    • a user defined list of summand groups separated by semicolons, e.g. '0; 1 3 4; 2 5'
  • --info — print read/write information of the summands. the tea ☕
  • --lace-dqsize[=NUM] — set length of Lace task queue (default 1024*1024*4).
  • --lace-stacksize[=NUM] — set size of program stack in kilobytes (0=default stack size).
  • --max-iterations[=NUM] — limit number of breadth-first iterations to NUM. boundaries, bestie 🚧
  • -m[NUM], --memory-limit[=NUM] — Sylvan memory limit in gigabytes (default 3).
  • --print-exact — prints the sizes of LDDs exactly when within the representable range, and in scientific notation otherwise.
  • --print-nodesize — print the number of LDD nodes in addition to the number of elements, represented as 'elements[nodes]'.
  • -QNUM, --qlimit=NUM — limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, and NUM=0 for unlimited).
  • --reorder[=ORDER] — variable reordering, take your pick:
    • 'none' (default) — no variable reordering
    • 'random' — variables are put in a random order
    • 'weighted' — variables are put in an order defined by their connectivity weight
    • a user defined permutation e.g. '1 3 2 0 4'
  • --reset — set constant values when introducing parameters.
  • -rNAME, --rewriter=NAME — use rewrite strategy NAME:
    • 'jitty' — jitty rewriting (default)
    • 'jittyc' — compiled jitty rewriting
    • 'jittyp' — jitty rewriting with prover
  • --saturation — reduces the amount of breadth-first iterations by applying the transition groups until fixed point. she's saturating, she's not stopping 🔥
  • -sNUM, --solve-strategy=NUM — use solve strategy NUM. heads up: all strategies except 0 periodically apply on-the-fly solving, which may lead to early termination.
    • '0' — no on-the-fly solving is applied (default)
    • '1' — detect solitair winning cycles.
    • '2' — detect solitair winning cycles with safe attractors.
    • '3' — detect forced winning cycles.
    • '4' — detect forced winning cycles with safe attractors.
    • '5' — detect fatal attractors.
    • '6' — detect fatal attractors with safe attractors.
    • '7' — solve subgames using a Zielonka solver.
  • -c, --split-conditions — split disjunctive conditions to obtain more summands with potentially less dependencies.
  • --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. 💀 mac girlies beware.
  • --timings[=FILE] — append timing measurements to FILE. measurements are written to standard error if no FILE is provided.
  • -t, --total — make the SRF PBES total.

🌈 Standard options 🌈

the everyday essentials, the little black dress of flags:

  • -q, --quiet — do not display warning messages. blissful silence 🙈
  • -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 👑🫶

⭐ AUTHOR ⭐

Written by Wieger Wesselink. ty king 🫡

💜 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. fr fr, none, zero, nada 😭

🍓 SEE ALSO 🍓

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

okay that's the whole page bestie, and for the cute sign-off: this is pbessolvesymbolic from the mCRL2 toolset (the version string got a lil truncated in the footer, we love a mysterious queen), dated October 2026, page PBESSOLVESYMBOLIC(1). slay, go solve some PBES 💅✨💖

📦 where this page comes from