PBESSTATEGRAPH(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 pbesstategraph(1) — the girlies' guide to reducing a PBES

okay so bestie, welcome to pbesstategraph from the mCRL2 toolset ✨ this is the pbesstategraph manual page, and we are gonna get you so comfy with it. grab a lil drink 🍓

🌸 SYNOPSIS 🌸

pbesstategraph [OPTION]... [INFILE [OUTFILE]]

🦋 DESCRIPTION 🦋

So what does it do? It reads a file containing a PBES, and reduces it based on an analysis of control flow parameters. that's the whole vibe, no cap 💅

If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used. simple as that, king 👑

✨ OPTIONS ✨

OPTION can be any of the following, and yes we're listing every single one because we don't skip 🫶

  • -iFORMAT, --in=FORMAT — use input format FORMAT. your choices are: 'pbes' for PBES in internal format (this is the default, main character energy), 'pgsolver' for BES in PGSolver format, and 'text' for PBES in textual (mCRL2) format 🌈
  • -m[NAME], --marking-algorithm[=NAME] — specifies the algorithm that is used for the marking computation: 0 (default), 1 or 2. In certain cases this choice can have a significant impact on the performance 👀 so like, pick wisely bestie
  • -oFORMAT, --out=FORMAT — use output format FORMAT. options are: 'bes' for BES in internal format, 'pbes' for PBES in internal format (default, she's the blueprint 💖), 'pgsolver' for BES in PGSolver format, and 'text' for PBES in textual (mCRL2) format ⭐
  • -QNUM, --qlimit=NUM — limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited). okay so 0 means go off, no limits, feral behaviour 🙈
  • -rNAME, --rewriter=NAME — use rewrite strategy NAME: 'jitty' for jitty rewriting (default 💅), 'jittyc' for compiled jitty rewriting, 'jittyp' for jitty rewriting with prover. three jitties, choose your fighter 🧚
  • --timings[=FILE] — append timing measurements to FILE. Measurements are written to standard error if no FILE is provided. clock it ⏱️
  • -g, --use-global-variant — use the global variant of the algorithm. global girly 🌍

🎀 Standard options 🎀

  • -q, --quiet — do not display warning messages. silence is golden 🤫
  • -v, --verbose — display short log messages. a lil chit-chat 💬
  • -d, --debug — display detailed log messages. she's telling you everything 😭
  • --log-level=LEVEL — display log messages up to and including LEVEL; either warn, verbose, debug or trace. pick your level of yapping 🔥
  • -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; Jeroen Keiren. legends, honestly 💅

😭 REPORTING BUGS 😭

Report bugs at <http://www.mcrl2.org/issuetracker>. pls do, we want her thriving 🐛

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. bestie you are on your own 😭

🍓 SEE ALSO 🍓

See also the manual at <http://www.mcrl2.org/web/user_manual/tools/release/pbesstategraph.html>. go read it, iykyk 💖

okay that's the whole page!! and for the cute lil sign-off: this is pbesstategraph from the mCRL2 toolset, version 2..., dated October 2026 — so mark your calendar bestie, she's timeless ⌚✨ byeee 🦋🎀

📦 where this page comes from