ltsmin-convert [OPTIONS]… input output


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.



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


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


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


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 any LTS as a single edge label LTS during a load/store copy.


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


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


Number of blocks in a cluster. Defaults to 32.

General Options


Increase the level of verbosity


Be quiet; do not print anything to the terminal.


Enable debugging output for file.


Print version string of this tool.

-h, --help

Print help text


Print short usage summary.


Enable statistics gathering/printing.


Terminate after the given amount of seconds.


Include file and line number in debug messages.


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






















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