lts_lts.h

Go to the documentation of this file.

// Author(s): 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_MCRL2_H
#define MCRL2_LTS_LTS_MCRL2_H
 
#include "mcrl2/lps/parse.h"
#include "mcrl2/lps/print.h"
#include "mcrl2/lps/state.h"
#include "mcrl2/lps/probabilistic_data_expression.h"
#include "mcrl2/lts/probabilistic_lts.h"
 
namespace mcrl2
{
namespace lts
{
 
class state_label_lts : public atermpp::term_list< lps::state >
{
  public:
    typedef atermpp::term_list< lps::state > super;
 
    state_label_lts()
    {}
 
    state_label_lts(const state_label_lts& )=default;
 
    state_label_lts& operator=(const state_label_lts& )=default;
 
    template < class CONTAINER >
    explicit state_label_lts(const CONTAINER& l)
    {
      static_assert(std::is_same<typename CONTAINER::value_type, data::data_expression>::value,"Value type must be a data_expression");
      this->push_front(lps::state(l.begin(),l.size()));
    }
 
    explicit state_label_lts(const lps::state& l)
    {
      this->push_front(l);
    }
 
    explicit state_label_lts(const super& l)
      : super(l)
    {
    }
 
    state_label_lts operator+(const state_label_lts& l) const
    {
      // The order of the state labels should not matter. For efficiency the elements of l are inserted in front of the aterm_list.
      state_label_lts result(*this);
 
      for (const lps::state& el : l)
      {
        result.push_front(el);
      }
 
      return result;
    }
 
    static state_label_lts number_to_label(const std::size_t n)
    {
      return state_label_lts(lps::state(mcrl2::data::sort_nat::nat(n)));
    }
};
 
inline std::string pp(const state_label_lts& label)
{
  std::string s;
  if (label.size()!=1)
  {
    s += "[";
  }
  bool first=true;
  for(const lps::state& l: label)
  {
    if (!first)
    {
      s += ", ";
    }
    first = false;
    s += "(";
    for (lps::state::iterator i=l.begin(); i!=l.end(); ++i)
    {
      if (i!=l.begin())
      {
        s += ",";
      }
      s += data::pp(*i);
    }
    s += ")";
  }
  if (label.size()!=1)
  {
    s += "]";
  }
  return s;
}
 
class action_label_lts: public mcrl2::lps::multi_action
{
  public:
 
    action_label_lts()
    {}
 
    action_label_lts(const action_label_lts& )=default;
 
    action_label_lts& operator=(const action_label_lts& )=default;
 
    explicit action_label_lts(const mcrl2::lps::multi_action& a)
     : mcrl2::lps::multi_action(sort_multiactions(a))
    {
    }
 
    void hide_actions(const std::vector<std::string>& tau_actions)
    {
      process::action_vector new_multi_action;
      for (const process::action& a: this->actions()) 
      {
        if (std::find(tau_actions.begin(),tau_actions.end(),
                      std::string(a.label().name()))==tau_actions.end())  // this action must not be hidden.
        {
          new_multi_action.push_back(a);
        }
      }
      *this= action_label_lts(lps::multi_action(process::action_list(new_multi_action.begin(), new_multi_action.end()),time()));
    }
 
    /* \brief The action label that represents the internal action.
    */
    static const action_label_lts& tau_action()
    {
      static action_label_lts tau_action=action_label_lts();
      return tau_action;
    }
 
  protected:
    static mcrl2::lps::multi_action sort_multiactions(const mcrl2::lps::multi_action& a)
    {
      if (a.actions().size()<=1)
      {
        return a;
      }
      std::multiset<process::action> sorted_actions(a.actions().begin(), a.actions().end());
      return  mcrl2::lps::multi_action(process::action_list(sorted_actions.begin(),sorted_actions.end()),a.time());
    }
};
 
inline std::string pp(const action_label_lts& l)
{
  return lps::pp(mcrl2::lps::multi_action(l));
}
 
inline action_label_lts parse_lts_action(
  const std::string& multi_action_string,
  const data::data_specification& data_spec,
  lps::multi_action_type_checker& typechecker)
{
  std::string l(multi_action_string);
  lps::multi_action al;
  // Find an @ symbol in the action, in which case it is timed.
  size_t position_of_at=l.find_first_of('@');
  std::string time_expression_string;
  if (position_of_at!=std::string::npos)
  {
    // The at symbol is found. It is a timed action.
    time_expression_string=l.substr(position_of_at+1,l.size());
    l=l.substr(0,position_of_at-1);
  }
  try
  {
    al=lps::parse_multi_action(l, typechecker, data_spec);
  }
  catch (mcrl2::runtime_error& e)
  {
    throw mcrl2::runtime_error("Parse error in action label " + multi_action_string + ".\n" + e.what());
  }
 
  if (time_expression_string.size()>0)
  {
    try
    {
      data::data_expression time=parse_data_expression(time_expression_string,data::variable_list(),data_spec);
      // Translate the sort of time to a real.
      if (time.sort()==data::sort_pos::pos())
      {
#ifdef MCRL2_ENABLE_MACHINENUMBERS
        time = data::sort_nat::pos2nat(time);
#else
        time = data::sort_nat::cnat(time);
#endif
      }
      if (time.sort()==data::sort_nat::nat())
      {
        time = data::sort_int::cint(time);
      }
      if (time.sort()==data::sort_int::int_())
      {
        time = data::sort_real::creal(time, data::sort_pos::c1());
      }
      if (time.sort()!=data::sort_real::real_())
      {
        throw mcrl2::runtime_error("The time is not of sort Pos, Nat, Int or Real\n");
      }
      return action_label_lts(lps::multi_action(al.actions(),time));
    }
    catch (mcrl2::runtime_error& e)
    {
      throw mcrl2::runtime_error("Parse error in the time expression " + multi_action_string + ".\n" + e.what());
    }
  }
  return action_label_lts(al);
}
 
namespace detail
{
 
class lts_lts_base
{
  protected:
    data::data_specification m_data_spec;
    data::variable_list m_parameters;
    process::action_label_list m_action_decls;
 
  public:
    lts_lts_base()
    {}
 
    bool operator==(const lts_lts_base& other) const
    {
      return m_data_spec==other.m_data_spec &&
             m_parameters==other.m_parameters &&
             m_action_decls==other.m_action_decls;
    }
 
    void swap(lts_lts_base& l)
    {
      const data::data_specification auxd=m_data_spec;
      m_data_spec=l.m_data_spec;
      l.m_data_spec=auxd;
      m_parameters.swap(l.m_parameters);
      m_action_decls.swap(l.m_action_decls);
    }
 
    static lts_type type()
    {
      return lts_lts;
    }
 
    const data::data_specification& data() const
    {
      return m_data_spec;
    }
 
    const process::action_label_list& action_label_declarations() const
    {
      return m_action_decls;
    }
 
    void set_action_label_declarations(const process::action_label_list& decls)
    {
      m_action_decls=decls;
    }
 
    void set_data(const data::data_specification& spec)
    {
      m_data_spec=spec;
    }
 
    const data::variable_list& process_parameters() const
    {
      return m_parameters;
    }
 
    const data::variable& process_parameter(std::size_t i) const
    {
      assert(i<m_parameters.size());
      data::variable_list::const_iterator j=m_parameters.begin();
      for(std::size_t c=0; c!=i; ++j, ++c)
      {}
      return *j;
    }
 
 
    void set_process_parameters(const data::variable_list& params)
    {
      m_parameters=params;
    }
 
};
 
} // namespace detail
 
 
class lts_lts_t : public lts< state_label_lts, action_label_lts, detail::lts_lts_base >
{
  public:
    lts_lts_t() {}
 
    void load(const std::string& filename);
 
    void save(const std::string& filename) const;
};
 
class probabilistic_lts_lts_t :
         public probabilistic_lts< state_label_lts,
                                   action_label_lts,
                                   probabilistic_state<std::size_t, lps::probabilistic_data_expression>,
                                   detail::lts_lts_base >
{
  public:
    probabilistic_lts_lts_t() {}
 
    void load(const std::string& filename);
 
    void save(const std::string& filename) const;
};
} // namespace lts
} // namespace mcrl2
 
namespace std
{
 
template<>
struct hash< mcrl2::lts::action_label_lts >
{
  std::size_t operator()(const mcrl2::lts::action_label_lts& as) const
  {
    hash<mcrl2::lps::multi_action> hasher;
    return hasher(as);
  }
};
 
} // namespace std
 
 
#endif