liblts.cpp

Go to the documentation of this file.

// Author(s): Muck van Weerdenburg
// 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)
//
/// \file liblts.cpp
 
#include <array>
 
#include "mcrl2/lts/lts_algorithm.h"
#include "mcrl2/lts/lts_io.h"
 
using namespace mcrl2::core;
using namespace mcrl2::core::detail;
using namespace mcrl2::log;
 
 
 
 
namespace mcrl2::lts::detail
{
 
lts_type guess_format(std::string const& s, const bool be_verbose/*=true*/)
{
  std::string::size_type pos = s.find_last_of('.');
 
  if (pos != std::string::npos)
  {
    std::string ext = s.substr(pos+1);
 
    if (ext == "aut")
    {
      if (be_verbose)
      {
        mCRL2log(log_level_t::verbose) << "Detected .aut extension.\n";
      }
      return lts_type::lts_aut;
    }
    else if (ext == "lts")
    {
      if (be_verbose)
      {
        mCRL2log(log_level_t::verbose) << "Detected .lts extension.\n";
      }
      return lts_type::lts_lts;
    }
    else if (ext == "fsm")
    {
      if (be_verbose)
      {
        mCRL2log(log_level_t::verbose) << "Detected .fsm extension.\n";
      }
      return lts_type::lts_fsm;
    }
    else if (ext == "dot")
    {
      if (be_verbose)
      {
        mCRL2log(log_level_t::verbose) << "Detected .dot extension.\n";
      }
      return lts_type::lts_dot;
    }
  }
 
  return lts_type::lts_none;
}
 
static const std::array<std::string, 5> type_strings = { "unknown", "lts", "aut", "fsm", "dot" };
 
static const std::array<std::string, 5> extension_strings = { "", "lts", "aut", "fsm", "dot" };
 
static const std::array<std::string, 5> type_desc_strings = {
    "unknown LTS format",
    "mCRL2 LTS format",
    "Aldebaran format (CADP)",
    "Finite State Machine format",
    "GraphViz format (no longer supported as input format)"
                                         };
 
 
static const std::array<std::string, 5> mime_type_strings = { "",
    "application/lts",
    "text/aut",
    "text/fsm",
    "text/dot"
                                         };
 
lts_type parse_format(std::string const& s)
{
  if (s == "lts")
  {
    return lts_type::lts_lts;
  }
  else if (s == "aut")
  {
    return lts_type::lts_aut;
  }
  else if (s == "fsm")
  {
    return lts_type::lts_fsm;
  }
  else if (s == "dot")
  {
    return lts_type::lts_dot;
  }
  return lts_type::lts_none;
}
 
std::string string_for_type(const lts_type type)
{
  return (type_strings.at(static_cast<std::size_t>(type)));
}
 
std::string extension_for_type(const lts_type type)
{
  return (extension_strings.at(static_cast<std::size_t>(type)));
}
 
std::string mime_type_for_type(const lts_type type)
{
  return (mime_type_strings.at(static_cast<std::size_t>(type)));
}
 
static const std::set<lts_type>& initialise_supported_lts_formats()
{
  static std::set<lts_type> s;
  for (std::size_t i = static_cast<std::size_t>(lts_type::lts_type_min); i<1+static_cast<std::size_t>(lts_type::lts_type_max); ++i)
  {
    if (lts_type::lts_none != (lts_type) i)
    {
      s.insert((lts_type) i);
    }
  }
  return s;
}
const std::set<lts_type>& supported_lts_formats()
{
  static const std::set<lts_type>& s = initialise_supported_lts_formats();
  return s;
}
 
/* Auxiliary function, used below */
template<std::size_t Size, typename T>
bool lts_named_cmp(const std::array<std::string, Size>& N, T a, T b)
{
  return N[static_cast<std::size_t>(a)] < N[static_cast<std::size_t>(b)];
}
 
std::string supported_lts_formats_text(lts_type default_format, const std::set<lts_type>& supported)
{
  std::vector<lts_type> types(supported.begin(), supported.end());
  std::sort(types.begin(),
            types.end(),
            [](const lts_type& t1, const lts_type& t2){ return lts_named_cmp(type_strings, t1, t2); });
 
  std::string r;
  for (std::vector<lts_type>::iterator i=types.begin(); i!=types.end(); ++i)
  {
    r += "  '" + type_strings.at(static_cast<std::size_t>(*i)) + "' for the " + type_desc_strings.at(static_cast<std::size_t>(*i));
 
    if (*i == default_format)
    {
      r += " (default)";
    }
 
    // Append the separator that fits the position of this entry. The last entry
    // gets none, the penultimate one gets ", or", the rest get a comma.
    const std::size_t remaining = static_cast<std::size_t>(std::distance(i, types.end()));
    if (remaining == 2)
    {
      r += ", or\n";
    }
    else if (remaining > 2)
    {
      r += ",\n";
    }
  }
 
  return r;
}
 
std::string supported_lts_formats_text(const std::set<lts_type>& supported)
{
  return supported_lts_formats_text(lts_type::lts_none,supported);
}
 
std::string lts_extensions_as_string(const std::string& sep, const std::set<lts_type>& supported)
{
  std::vector<lts_type> types(supported.begin(), supported.end());
  std::sort(types.begin(),
            types.end(),
            [](const lts_type& t1, const lts_type& t2){ return lts_named_cmp(extension_strings, t1, t2); });
 
  std::string r;
  std::string prev;
  bool first = true;
  for (auto & type : types)
  {
    if (extension_strings[static_cast<std::size_t>(type)] == prev)   // avoid mentioning extensions more than once
    {
      continue;
    }
    if (first)
    {
      first = false;
    }
    else
    {
      r += sep;
    }
    r += "*." + extension_strings[static_cast<std::size_t>(type)];
    prev = extension_strings[static_cast<std::size_t>(type)];
  }
 
  return r;
}
 
std::string lts_extensions_as_string(const std::set<lts_type>& supported)
{
  return lts_extensions_as_string(",",supported);
}
 
} // namespace mcrl2::lts::detail
//lts
//data