---
name: "pbespgsolve"
section: "1"
platform: "linux"
package: "mcrl2"
version: "201409.0-1+b2"
release: "Debian 10 (Buster)"
platforms: ["linux"]
url: "https://new.carta.tech/pbespgsolve"
---

# pbespgsolve(1)

Solve a (P)BES or parity game using a parity game solver

## NAME

pbespgsolve - Solve a (P)BES or parity game using a parity game solver

## SYNOPSIS

**pbespgsolve** \[*OPTION*\]... \[*INFILE*\]

## DESCRIPTION

Reads a file containing a (P)BES or a max parity game in PGSolver  format,instantiates it into a BES, and applies a parity game solver to it. If INFILE is not present, standard input is used.

## OPTIONS

- *OPTION* can be any of the following:

  - **-C**, **--cycle**

  Eliminate cycles

- **-i***FORMAT*, **--in**=*FORMAT*

  use input format FORMAT: 'pbes' PBES in internal format 'pbes\_text' PBES in internal textual format 'text' PBES in textual (mCRL2) format 'bes' BES in internal format 'bes\_text' BES in internal textual format 'cwi' BES in CWI format 'pgsolver' BES in PGSolver format

- **-L**, **--loop**

  Eliminate self-loops

- **-g**, **--onlygenerate**

  Only generate the BES without solving

- **-Q***NUM*, **--qlimit**=*NUM*

  limit enumeration of quantifiers to NUM variables. (Default NUM=1000, NUM=0 for  unlimited).

- **-r***NAME*, **--rewriter**=*NAME*

  use rewrite strategy NAME: 'jitty' jitty rewriting (default) 'jittyc' compiled jitty rewriting 'jittyp' jitty rewriting with prover

- **-c**, **--scc**

  Use scc decomposition

- **-s***NAME*, **--solver-type**=*NAME*

  Use the solver type NAME: 'spm' Small progress measures (default) 'altspm' Alternative implementation of small progress measures 'recursive' Recursive algorithm

- **--timings**\[=*FILE*\]

  append timing measurements to FILE. Measurements are written to standard error  if no FILE is provided

- **-e**, **--verify**

  Verify the solution

- Standard options:

  - **-q**, **--quiet**

  do not display warning messages

- **-v**, **--verbose**

  display short intermediate messages

- **-d**, **--debug**

  display detailed intermediate messages

- **--log-level**=*LEVEL*

  display intermediate messages up to and including level

- **-h**, **--help**

  display help information

- **--version**

  display version information

## AUTHOR

Written by Maks Verver and Wieger Wesselink; Michael Weber.

## REPORTING BUGS

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

## COPYRIGHT

Copyright © 2014 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/release/user\_manual/tools/pbespgsolve.html\>.