SYNOPSIS

mpirun <nodespec> ltsmin-mpi [OPTION] <input> <output>

DESCRIPTION

This tool reduces a labeled transition system modulo bisimulation. The default bisimulation is strong bisimulation. Both input and output can be a GCF archive or a set of files. To use a set of files the argument needs an occurrence of %s. If no %s is present then a GCF archive is assumed.

The tool uses MPI for distributed computation, thus it has to be started via mpirun. nodespec determines which processors the tool is run on.

The workers send messages to themselves. So if you use Open MPI, you have to use mpirun -mca btl CONNECT,self NODESPEC where CONNECT can be tcp, mx, ib, etc..

OPTIONS

Reductions

-s, --strong

Apply strong bisimulation reduction. This is the default.

-b, --branching

Apply branching bisimulation reduction.

General Options

-v

Increase the level of verbosity

-q

Be quiet; do not print anything to the terminal.

--debug

Enable debugging output.

--version

Print version string of this tool.

-h, --help

Print help text

--usage

Print short usage summary.

EXIT STATUS

0

Successful termination.

1

Some error occurred.

SEE ALSO

ltsmin(7), lpo2lts-mpi(1), lps2lts-mpi(1), nips2lts-mpi(1), ltsmin-convert(1)