PBESSOLVE(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💖 NAME 💖

okay so welcome to the PBESSOLVE(1) manual page — yes, the User Commands one — for pbessolve: Generate a BES from a PBES and solve it. That’s the name, that’s the mission, periodt. 🫶

✨ SYNOPSIS ✨

run it like this, bestie:

pbessolve [OPTION]... [INFILE]

🦋 DESCRIPTION 🦋

Solves (P)BES from INFILE. If INFILE is not present, stdin is used. The PBES is first instantiated into a parity game, which is then solved using Zielonka’s algorithm. It supports the generation of a witness or counter example for the property encoded by the PBES.

🎀 OPTIONS 🎀

OPTION can be any of the following:

  • --evidence-file=NAME — the file to which the evidence is written. If not set, a default name will be chosen.
  • -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.
  • -iFORMAT, --in=FORMAT — use input format FORMAT: 'pbes' PBES in internal format (default).
  • --prune-todo-list — prune the todo list periodically.
  • -QNUM, --qlimit=NUM — limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for 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.
  • --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.

🐛 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/pbessolve.html.

okay that’s the whole page, bestie — pbessolve, mCRL2 toolset 202507..., October 2026, PBESSOLVE(1). byeeee 💅🫶✨

📦 where this page comes from