SYNOPSIS

ltsmin-compare [OPTIONS] <input 1> <input 2>

OPTIONS

-s, --strong

Compare modulo strong bisimulation using the default implementation.

-b, --branching

Compare modulo branching bisimulation using the default implementation.

-l, --lump

Compare modulo CTMC lumping.

-t, --trace

Compare the two LTSs modulo (optionally stuttering) trace equivalence. This happens in multiple steps. First, the LTSs are compared modulo strong bisimulation (or silent step bisimulation if the stutter option is given). If the resulting LTSs are not equal, the LTSs are made deterministic and compared modulo strong bisimulation.

--stutter

Compare module stuttering during trace equivalence comparison.

LTS I/O Options

--block-size=BYTES

Size of a block in bytes. Defaults to 32,768.

--cluster-size=BLOCKS

Number of blocks in a cluster. Defaults to 32.

General Options

-v

Increase the level of verbosity

-q

Be quiet; do not print anything to the terminal.

--debug=file

Enable debugging output for file.

--version

Print version string of this tool.

-h, --help

Print help text

--usage

Print short usage summary.

--stats

Enable statistics gathering/printing.

--timeout=INT

Terminate after the given amount of seconds.

--where

Include file and line number in debug messages.

--when

Include the wall time since program start in all messages.

EXIT STATUS

0

Successful termination: LTSs are equivalent.

1

LTSs are not equivalent.

255

Some error occurred.

SEE ALSO