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

# lps2pbes(1)

generate a PBES from an LPS and a state formula

## NAME

lps2pbes - generate a PBES from an LPS and a state formula

## SYNOPSIS

**lps2pbes** \[*OPTION*\]... --formula=FILE \[*INFILE* \[*OUTFILE*\]\]

## DESCRIPTION

Convert the state formula in FILE and the LPS in INFILE to a parameterised  boolean equation system (PBES) and save it to OUTFILE. If OUTFILE is not  present, stdout is used. If INFILE is not present, stdin is used.

## OPTIONS

- *OPTION* can be any of the following:

  - **-f***FILE*, **--formula**=*FILE*

  use the state formula from FILE

- **-o***FORMAT*, **--out**=*FORMAT*

  use output format FORMAT: 'pbes' PBES in internal format 'pbes\_text' PBES in internal textual format 'text' PBES in textual (mCRL2) format

- **-s**, **--structured**

  generate equations such that no mixed conjunctions and disjunctions occur

- **-t**, **--timed**

  use the timed version of the algorithm, even for untimed LPS's

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

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

- **-u**, **--unoptimized**

  do not simplify boolean expressions

- 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 Wieger Wesselink; Tim Willemse.

## 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/lps2pbes.html\>.