Manual page for lps2jani


lps2jani   [OPTION]... [INFILE [OUTFILE]]


Reads the LPS in INFILE and writes a corresponding file in Jani format to OUTFILE. The LPS must only contain simple data types (Numbers, Booleans) that the Jani format supports. See http://jani-spec.org for more information about the Jani format. If OUTFILE is not present, stdout is used. If INFILE is not present, stdin is used.

Command line options

-QNUM , --qlimit=NUM

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

-rNAME , --rewriter=NAME

use rewrite strategy NAME:


jitty rewriting


compiled jitty rewriting


jitty rewriting with prover


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 intermediate messages

-d , --debug

display detailed intermediate messages


display intermediate messages up to and including level

-h , --help

display help information


display version information


Jan Friso Groote