lts_io.h

Go to the documentation of this file.

// Author(s): Muck van Weerdenburg, Jan Friso Groote
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_LTS_LTS_IO_H
#define MCRL2_LTS_LTS_IO_H
 
#include "mcrl2/lps/io.h"
#include "mcrl2/lts/detail/lts_convert.h"
 
#include "mcrl2/atermpp/aterm_io.h"
 
namespace mcrl2::lts
{
 
typedef enum { none_e, data_e, lps_e, mcrl2_e } data_file_type_t; 
 
 
namespace detail
{
 
lts_type guess_format(std::string const& s, const bool be_verbose=true);
 
lts_type parse_format(std::string const& s);
 
std::string string_for_type(const lts_type type);
 
std::string extension_for_type(const lts_type type);
 
std::string mime_type_for_type(const lts_type type);
 
const std::set<lts_type>& supported_lts_formats();
 
std::string supported_lts_formats_text(lts_type default_format = lts_none, const std::set<lts_type>& supported = supported_lts_formats());
 
std::string supported_lts_formats_text(const std::set<lts_type>& supported);
 
std::string lts_extensions_as_string(const std::string& sep = ",", const std::set<lts_type>& supported = supported_lts_formats());
 
std::string lts_extensions_as_string(const std::set<lts_type>& supported);
 
 
inline void read_lps_context(const std::string& data_file,
                             data::data_specification& data,
                             process::action_label_list& action_labels,
                             data::variable_list& process_parameters)
{
  lps::stochastic_specification spec;
  load_lps(spec, data_file);
  data = spec.data();
  action_labels = spec.action_labels();
  process_parameters = spec.process().process_parameters();
}
 
inline void read_data_context(const std::string& data_file,
                              data::data_specification& data,
                              process::action_label_list& action_labels)
{
  // Add "init delta;" to the file to make the input a proper data specification.
  // "init delta;" must appear at the front, such that a second init clause will be
  // reported as wrong. 
  const std::string input="init delta; " + utilities::read_text(data_file);
  process::process_specification procspec =
      process::parse_process_specification(input);
  data=procspec.data();
  action_labels=procspec.action_labels();
}
 
inline void read_mcrl2_context(const std::string& data_file,
                               data::data_specification& data,
                               process::action_label_list& action_labels)
{
  process::process_specification procspec =
      process::parse_process_specification(utilities::read_text(data_file));
  data = procspec.data();
  action_labels = procspec.action_labels();
}
 
// converts an arbitrary lts to lts_lts_t
template <class LTS_TYPE_IN, class LTS_TYPE_OUT>
inline void convert_to_lts_lts(LTS_TYPE_IN& src, 
                               LTS_TYPE_OUT& dest, 
                               const data_file_type_t extra_data_file_type,
                               const std::string& extra_data_file_name)
{
  std::string data_file;
  data::data_specification data;
  process::action_label_list action_labels;
  data::variable_list process_parameters;
  bool extra_data_is_defined=true;
  switch (extra_data_file_type)
  {
    case data_e:  
    { 
      read_data_context(extra_data_file_name,data,action_labels); 
      break;
    }
    case lps_e:   
    {
      read_lps_context(extra_data_file_name,data,action_labels,process_parameters); 
      break;
    }
    case mcrl2_e: 
    {
      read_mcrl2_context(extra_data_file_name,data,action_labels); 
      break;
    }
    default:
    {
      extra_data_is_defined = false;
      mCRL2log(log::info) << "No data and action label specification is provided. Only the standard data types and no action labels can be used." << std::endl; break;
    }
  }
  lts_convert(src, dest, data, action_labels, process_parameters, extra_data_is_defined);
}
} //  namespace detail
 
template <class LTS_TYPE>
inline void load_lts(LTS_TYPE& 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="")
{
  switch (type)
  {
    case lts_lts:
    case lts_lts_probabilistic:
    {
      if (extra_data_file_type != none_e)
      {
        mCRL2log(log::warning) << "The lts file comes with a data specification. Ignoring the extra data and action label specification provided." << std::endl;
      }
      result.load(infilename);
      break;
    }
    case lts_none:
      mCRL2log(log::warning) << "Cannot determine type of input. Assuming .aut.\n";
      [[fallthrough]]; // For the default (lts_none) load as aut file.
    case lts_aut:
    case lts_aut_probabilistic:
    {
      probabilistic_lts_aut_t l;
      l.load(infilename);
      convert_to_lts_lts(l, result,extra_data_file_type,extra_data_file_name);
      break;
    }
    case lts_fsm:
    case lts_fsm_probabilistic:
    {
      probabilistic_lts_fsm_t l;
      l.load(infilename);
      convert_to_lts_lts(l, result,extra_data_file_type,extra_data_file_name);
      break;
    }
    case lts_dot:
    {
      throw mcrl2::runtime_error("Reading of .dot files is not supported anymore.");
    }
  }
}
 
 
inline void load_lts_as_fsm_file(const std::string& path, lts_fsm_t& l)
{
  const lts_type intype = mcrl2::lts::detail::guess_format(path);
  switch (intype)
  {
    case lts_lts:
    case lts_lts_probabilistic:
    {
      lts_lts_t l1;
      l1.load(path);
      detail::lts_convert(l1,l);
      return;
    }
    case lts_none:
      mCRL2log(log::warning) << "Cannot determine type of input. Assuming .aut.\n";
      [[fallthrough]]; // For the default (lts_none) load as aut file.
    case lts_aut:
    case lts_aut_probabilistic:
    {
      lts_aut_t l1;
      l1.load(path);
      detail::lts_convert(l1,l);
      return;
    }
    case lts_fsm:
    case lts_fsm_probabilistic:
    {
      l.load(path);
      return;
    }
    case lts_dot:
    {
      throw mcrl2::runtime_error("Reading of dot files is not supported.");
    }
  }
}
 
// Proper interface.
 
atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, lts_lts_t& lts);
atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, probabilistic_lts_lts_t& lts);
 
atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const lts_lts_t& lts);
atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const probabilistic_lts_lts_t& lts);
 
// Streaming an LTS to disk:
//  write_lts_header(data_spec, parameters, action_labels)
//
// In any order:
//  Write transitions (to, label, from), where 'to' and 'from' are indices and 'label' the multi_action, as necessary.
//  Write state labels (state_label_lts) in their order such that writing the i-th state label belongs to state with index i.
//  Write the initial state.
 
void write_lts_header(atermpp::aterm_ostream& stream,
  const data::data_specification& data,
  const data::variable_list& parameters,
  const process::action_label_list& action_labels);
 
void write_transition(atermpp::aterm_ostream& stream, std::size_t from, const lps::multi_action& label, std::size_t to);
void write_transition(atermpp::aterm_ostream& stream, std::size_t from, const lps::multi_action& label, const probabilistic_lts_lts_t::probabilistic_state_t& to);
 
void write_state_label(atermpp::aterm_ostream& stream, const state_label_lts& label);
 
void write_initial_state(atermpp::aterm_ostream& stream, std::size_t index);
 
} // namespace mcrl2::lts
 
#endif // MCRL2_LTS_LTS_IO_H