mcrl2/lts/lts2lps.h

Include file:

#include "mcrl2/lts/lts2lps.h"

This file contains functions to translate lts’s into` LPS format.

Functions

lps::specification mcrl2::lts::transform_lts2lps(const lts_aut_t &l1, const data_specification &data, const process::action_label_list &action_labels, const variable_list &process_parameters)

transform an lts in aut format into a linear process.

Parameters:

  • l1 A labelled transition system in aut format.
  • data A separate data specification.
  • action_labels A list containing the action labels used in the lts.
  • process_parameters The process parameters of the current process.

Returns: The function returns a linear process with the same behaviour as the lts.

lps::specification mcrl2::lts::transform_lts2lps(const lts_fsm_t &l1, const data_specification &data, const process::action_label_list &action_labels, const variable_list &process_parameters)

transform an lts in fsm format into a linear process.

Parameters:

  • l1 A labelled transition system in fsm format.
  • data A separate data specification.
  • action_labels A list containing the action labels used in the lts.
  • process_parameters The process parameters of the current process. XXXXX Is this needed????

Returns: The function returns a linear process with the same behaviour as the lts.

lps::specification mcrl2::lts::transform_lts2lps(const lts_lts_t &l)

transform an lts in lts format into a linear process.

Parameters:

  • l A labelled transition system in lts format.

Returns: The function returns a linear process with the same behaviour as the lts.