mcrl2/lts/lts_io.h

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 data_file_type_t

Values:

  • 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.

Functions

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.

Parameters:

  • 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.

Parameters:

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

Functions

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)
std::string extension_for_type(const lts_type type)

Gives the filename extension associated with an LTS format.

Parameters:

  • type The LTS format.

Returns: The filename extension of the LTS format specified by type.

lts_type guess_format(std::string const &s, const bool be_verbose = true)

Determines the LTS format from a filename by its extension.

Parameters:

  • s The name of the file of which the format will be determined.
  • be_verbose If true, messages about the detected file format are printed in verbose mode.

Returns: The LTS format based on the extension of s. If no supported format can be determined from the extension then lts_none is returned.

std::string lts_extensions_as_string(const std::string &sep = ",", const std::set<lts_type> &supported = supported_lts_formats())

Gives a list of extensions for supported LTS formats.

Parameters:

  • sep The separator to use between each extension.
  • supported The formats that should be considered supported.

Returns: A string containing a list of extensions of the formats in supported, separated by sep. E.g. “.aut,.lts”

std::string lts_extensions_as_string(const std::set<lts_type> &supported)

Gives a list of extensions for supported LTS formats.

Parameters:

  • supported The formats that should be considered supported.

Returns: A string containing a list of extensions of the formats in supported, separated by ‘,’. E.g. “.aut,.lts”

std::string mime_type_for_type(const lts_type type)

Gives the MIME type associated with an LTS format.

Parameters:

  • type The LTS format.

Returns: The MIME type of the LTS format specified by type.

lts_type parse_format(std::string const &s)

Determines the LTS format from a format specification string.

This can be any of the following strings:

  • “aut” for the Aldbaran format;
  • “fsm” for the FSM format;
  • “dot” for the GraphViz format;

Parameters:

  • s The format specification string.

Returns: The LTS format based on the value of s. If no supported format can be determined then lts_none is returned.

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)
std::string string_for_type(const lts_type type)

Gives a string representation of an LTS format.

This is the “inverse” of parse_format.

Parameters:

  • type The LTS format.

Returns: The name of the LTS format specified by type.

const std::set<lts_type> &supported_lts_formats()

Gives the set of all supported LTS formats.

Returns: The set of all supported LTS formats.

std::string supported_lts_formats_text(lts_type default_format = lts_none, const std::set<lts_type> &supported = supported_lts_formats())

Gives a textual list describing supported LTS formats.

Parameters:

  • default_format The format that should be marked as default (or lts_none for no default).
  • supported The formats that should be considered supported.

Returns: A string containing lines of the form ” ‘name’ for the ... format”. Every line except the last is terminated with ‘n’.

std::string supported_lts_formats_text(const std::set<lts_type> &supported)

Gives a textual list describing supported LTS formats.

Parameters:

  • supported The formats that should be considered supported.

Returns: A string containing lines of the form ” ‘name’ for the ... format”. Every line except the last is terminated with ‘n’.