PBESCONSTELM(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

NAME 💖

okay bestie, this is the pbesconstelm page — manual name PBESCONSTELM(1), chillin' under User Commands — and its whole thing is:

remove constant parameters from a PBES ✨

SYNOPSIS 🫶

pbesconstelm [OPTION]... [INFILE [OUTFILE]]

that's the vibe, no cap. INFILE and OUTFILE are the optional placeholders, iykyk.

DESCRIPTION 🦋

okay so here's the tea: pbesconstelm reads a file containing a PBES, and applies constant parameter elimination to it. 💅

If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used. That's literally the flow. ✨

OPTIONS 🎀

OPTION can be any of the following:

  • -a, --check-quantifiers — also analyse which quantified parameters are constant. 👀
  • -c, --compute-conditions — compute propagation conditions. 🔥
  • -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. 🌈
  • -pNAME, --pbes-rewriter=NAME — use pbes rewrite strategy NAME: 'simplify' for simplification (default), 'quantifier-all' for eliminating all quantifiers, 'quantifier-finite' for eliminating finite quantifier variables, 'quantifier-inside' for pushing quantifiers inside, 'quantifier-one-point' for one point rule quantifier elimination, 'pfnf' for rewriting into PFNF normal form, 'ppg' for rewriting into Parameterised Parity Game form, 'bqnf-quantifier' for rewriting quantifiers over conjuncts to conjuncts of quantifiers (experimental). 😭
  • -QNUM, --qlimit=NUM — limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited). 💀
  • -e, --remove-equations — remove redundant equations. 🙈
  • -rNAME, --rewriter=NAME — use rewrite strategy NAME: 'jitty' jitty rewriting (default), 'jittyc' compiled jitty rewriting, 'jittyp' jitty rewriting with prover. ⭐
  • --timings[=FILE] — append timing measurements to FILE. Measurements are written to standard error if no FILE is provided. 🍓

Standard options 🧚

  • -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; Simon Janssen and Tim Willemse. 💖

REPORTING BUGS 😭

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

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

SEE ALSO 🌈

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

okay that's the whole page, bestie — source/version pbesconstelm mCRL2 toolset 202..., dated October 2026, manual name PBESCONSTELM(1). slay 💅💖

📦 where this page comes from