Include file:

#include "mcrl2/lts/lts_io.h"

This include file contains routines to read and write labelled transitions from and to files and from streams.

This is the LTS library’s main header file. It declares all publicly accessible data structures that form the interface of the library. Muck van Weerdenburg

Enumerated types

type mcrl2::lts::data_file_type_t


  • none_e
  • data_e
  • lps_e
  • mcrl2_e

Type for data files that contain extra information for an lts in .aut or .fsm format. Typically this is a data_specification (data_e), a linear process (lps_e) or an .mcrl2 file. The value none_e indicates that no information is available.


void mcrl2::lts::load_lts(lts_lts_t &result, const std::string &infilename, lts_type type, const data_file_type_t extra_data_file_type = none_e, const std::string &extra_data_file_name = "")

Loads an lts of the indicated type, transforms it to an lts of the form lts_lts_t using the additional data parameters.

The file can refer to any file in lts, aut, fsm, or dot format. After reading it is is translated into .lts format. For this a file is read with the name extra_data_file, which is interpreted as a data specification if extra_data_file_type has type data_e, a linear process specification if it has value lps_e, and an mcrl2 file if it has value mcrl2_e.


  • result The lts in which the transition system is put.
  • infilename The name of the file containing the lts.
  • type The type of the lts file, i.e. .lts, .fsm, .dot or .aut.
  • extra_data_file_type The type of the file containing extra information, such as a data specification.
  • extra_data_file_name The name of the file containing extra information.
void mcrl2::lts::load_lts_as_fsm_file(const std::string &path, lts_fsm_t &l)

Read a labelled transition system and return it in fsm format.

The file can refer to any file in lts, aut, fsm, or dot format. After reading it is is attempted to translate it into fsm format.


  • path A string with the name of the file.
  • l The lts in which the transition system is put.


void mcrl2::lts::detail::convert_to_lts_lts(LTS_TYPE &src, mcrl2::lts::lts_lts_t &dest, const data_file_type_t extra_data_file_type, const std::string &extra_data_file_name)
void mcrl2::lts::detail::read_data_context(const std::string &data_file, data::data_specification &data, process::action_label_list &action_labels)
void mcrl2::lts::detail::read_lps_context(const std::string &data_file, data::data_specification &data, process::action_label_list &action_labels, data::variable_list &process_parameters)
void mcrl2::lts::detail::read_mcrl2_context(const std::string &data_file, data::data_specification &data, process::action_label_list &action_labels)