SYNOPSIS

ltsmin-convert [OPTIONS]… input output

DESCRIPTION

This tool copies input to output and changes the archive format on-the-fly. Both input and output format are detected by pattern matching. See the File Formats section for details.

OPTIONS

--copy

Perform a streaming copy from <input> to <output>.

--rdwr

Perform a load/store copy from <input> to <output>.

--index

Transform the vector based <input> to indexed <output>.

--segments=N

Set the number of segments in the output file. If the output format does not support segmentation (BCG) then the default is 1 and specifying any number other than 1 is an error. Otherwise, the default is the same number of segments as the input. Please note that the algorithm used for changing the number of segments is simple. It guarantees that the number of states in the output is balanced, but not much more. E.g., if the input is in BFS order and just one segment then then the output will still be in BFS order. However, if the input has more than one segment then BFS order is lost.

--encode

Encode any LTS as a single edge label LTS during a load/store copy.

--bfs

Change the indexing of the LTS to match BFS exploration order during a load/store copy. Note that the current version cannot reorder the LTS if it has state vectors.

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.

File Formats

The following file formats are supported:

  • Directory format (*.dir, *.dz and *.gcf)

  • Vector format (*.dir, *.gcd, *.gcf)

  • Binary Coded Graphs (*.bcg)

  • Aldebaran Format (*.aut)

  • FSM Format (*.fsm)

  • MRMC/Prism (*.tra+*.lab)

  • PGSolver format (*.pg)

If a tool operates in streaming mode then support for file formats is limited, as can be seen in the following table:

Format Streaming mode Load/Store mode

DIR

R/W

R/W

VEC

R/W

R/W

BCG

W

R/W

AUT

W

R/W

FSM

W

W

TRA

-

R/W

PG

-

W

The directory format uses multiple files to store an LTS. The various extension explain how these files are stored in the underlying file system. The *.dir format uses multiple files in a directory without compression. If the LTS has one edge label, no state labels and does not store state vectors then these files are backwards compatible. Neither the *.dz nor the *.gcf formats are backwards compatible. Both formats use compression. The first uses a directory for the files, second interleaves files into a single file.

If you try to open a *.dir with the old mCRL tools and you get the error message:

wrong file version: 0

then the directory is probably compressed. If that happens then you may convert the directory by typing the command:

ltsmin-convert bad.dir good.dir

EXIT STATUS

0

Successful termination.

255

Some error occurred. == SEE ALSO ltsmin(7), ltsmin-compare(1), ltsmin-reduce(1), ltsmin-reduce-dist(1), lpo2lts-dist(1), lpo2lts-mc(1), lpo2lts-seq(1), lpo2lts-sym(1), CADP, BCG