multi_action.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// 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_LPS_MULTI_ACTION_H
#define MCRL2_LPS_MULTI_ACTION_H
 
#include "mcrl2/core/print.h"
#include "mcrl2/process/process_expression.h"
 
namespace mcrl2
{
 
namespace lps
{
 
// prototype declaration
bool is_multi_action(const atermpp::aterm& x);
 
//--- start generated class multi_action ---//
class multi_action: public atermpp::aterm
{
  public:
 
 
    multi_action(const multi_action&) noexcept = default;
    multi_action(multi_action&&) noexcept = default;
    multi_action& operator=(const multi_action&) noexcept = default;
    multi_action& operator=(multi_action&&) noexcept = default;
 
    const process::action_list& actions() const
    {
      return atermpp::down_cast<process::action_list>((*this)[0]);
    }
 
    const data::data_expression& time() const
    {
      return atermpp::down_cast<data::data_expression>((*this)[1]);
    }
//--- start user section multi_action ---//
    explicit multi_action(const process::action_list& actions = process::action_list(), 
                          data::data_expression time = data::undefined_real())
      : atermpp::aterm(core::detail::function_symbol_TimedMultAct(), actions, time)
    {
      assert(data::sort_real::is_real(time.sort()));
    }
 
    explicit multi_action(const atermpp::aterm& term)
      : atermpp::aterm(term)
    {
      assert(core::detail::check_term_TimedMultAct(*this));
    }
 
    explicit multi_action(const process::action& l)
      : multi_action(process::action_list({ l }),data::undefined_real())
    {}
 
    bool has_time() const
    {
      return time() != data::undefined_real();
    }
 
    multi_action operator+(const multi_action& other) const
    {
      assert(time() == other.time());
      return multi_action(actions() + other.actions(), time());
    }
 
    multi_action sort_actions() const
    {
      if (actions().size()<=1)  // There is almost always only one action. 
      {
        return *this;
      }
      return multi_action(atermpp::sort_list(actions()),time());
    }
 
   //--- end user section multi_action ---//
};
 
template <class... ARGUMENTS>
inline void make_multi_action(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_TimedMultAct(), args...);
}
 
typedef atermpp::term_list<multi_action> multi_action_list;
 
typedef std::vector<multi_action>    multi_action_vector;
 
inline
bool is_multi_action(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::TimedMultAct;
}
 
// prototype declaration
std::string pp(const multi_action& x);
 
inline
std::ostream& operator<<(std::ostream& out, const multi_action& x)
{
  return out << lps::pp(x);
}
 
inline void swap(multi_action& t1, multi_action& t2)
{
  t1.swap(t2);
}
//--- end generated class multi_action ---//
 
 
// template function overloads
lps::multi_action normalize_sorts(const multi_action& x, const data::sort_specification& sortspec);
lps::multi_action translate_user_notation(const lps::multi_action& x);
std::set<data::variable> find_all_variables(const lps::multi_action& x);
std::set<data::variable> find_free_variables(const lps::multi_action& x);
 
namespace detail
{
 
template <typename Iter, typename Function>
void forall_permutations(Iter first, Iter last, Function f)
{
  if (first == last)
  {
    f();
    return;
  }
  Iter next = first;
  ++next;
  forall_permutations(next, last, f);
  while (std::next_permutation(first->first, first->second))
  {
    forall_permutations(next, last, f);
  }
}
 
inline bool equal_action_signatures(const std::vector<process::action>& a, const std::vector<process::action>& b)
{
  if (a.size() != b.size())
  {
    return false;
  }
  std::vector<process::action>::const_iterator i, j;
  for (i = a.begin(), j = b.begin(); i != a.end(); ++i, ++j)
  {
    if (i->label() != j->label())
    {
      return false;
    }
  }
  return true;
}
 
struct compare_action_labels
{
  bool operator()(const process::action& a, const process::action& b) const
  {
    return a.label() < b.label();
  }
};
 
struct compare_action_label_arguments
{
  bool operator()(const process::action& a, const process::action& b) const
  {
    if (a.label() != b.label())
    {
      return a.label() < b.label();
    }
    return a < b;
  }
};
 
struct equal_data_parameters_builder
{
  const std::vector<process::action>& a;
  const std::vector<process::action>& b;
  std::set<data::data_expression>& result;
 
  equal_data_parameters_builder(const std::vector<process::action>& a_,
                                const std::vector<process::action>& b_,
                                std::set<data::data_expression>& result_
                               )
    : a(a_),
      b(b_),
      result(result_)
  {}
 
  void operator()()
  {
    std::vector<data::data_expression> v;
    std::vector<process::action>::const_iterator i, j;
    for (i = a.begin(), j = b.begin(); i != a.end(); ++i, ++j)
    {
      data::data_expression_list d1 = i->arguments();
      data::data_expression_list d2 = j->arguments();
      assert(d1.size() == d2.size());
      data::data_expression_list::iterator i1 = d1.begin(), i2 = d2.begin();
      for (     ; i1 != d1.end(); ++i1, ++i2)
      {
        v.push_back(data::lazy::equal_to(*i1, *i2));
      }
    }
    data::data_expression expr = data::lazy::join_and(v.begin(), v.end());
    result.insert(expr);
  }
};
 
struct not_equal_multi_actions_builder
{
  const std::vector<process::action>& a;
  const std::vector<process::action>& b;
  std::vector<data::data_expression>& result;
 
  not_equal_multi_actions_builder(const std::vector<process::action>& a_,
                                  const std::vector<process::action>& b_,
                                  std::vector<data::data_expression>& result_
                                 )
    : a(a_),
      b(b_),
      result(result_)
  {}
 
  void operator()()
  {
    using namespace data::lazy;
 
    std::vector<data::data_expression> v;
    std::vector<process::action>::const_iterator i, j;
    for (i = a.begin(), j = b.begin(); i != a.end(); ++i, ++j)
    {
      data::data_expression_list d1 = i->arguments();
      data::data_expression_list d2 = j->arguments();
      assert(d1.size() == d2.size());
      data::data_expression_list::iterator i1=d1.begin(), i2=d2.begin();
      for (   ; i1 != d1.end(); ++i1, ++i2)
      {
        v.push_back(data::not_equal_to(*i1, *i2));
      }
    }
    result.push_back(data::lazy::join_or(v.begin(), v.end()));
  }
};
 
} // namespace detail
 
inline data::data_expression equal_multi_actions(const multi_action& a, const multi_action& b)
{
#ifdef MCRL2_EQUAL_MULTI_ACTIONS_DEBUG
  mCRL2log(debug) << "\n<equal multi actions>" << std::endl;
  mCRL2log(debug) << "a = " << process::pp(a.actions()) << std::endl;
  mCRL2log(debug) << "b = " << process::pp(b.actions()) << std::endl;
#endif
  using namespace data::lazy;
 
  // make copies of a and b and sort them
  std::vector<process::action> va(a.actions().begin(), a.actions().end()); // protection not needed
  std::vector<process::action> vb(b.actions().begin(), b.actions().end()); // protection not needed
  std::sort(va.begin(), va.end(), detail::compare_action_label_arguments());
  std::sort(vb.begin(), vb.end(), detail::compare_action_label_arguments());
 
  if (!detail::equal_action_signatures(va, vb))
  {
#ifdef MCRL2_EQUAL_MULTI_ACTIONS_DEBUG
    mCRL2log(debug) << "different action signatures detected!" << std::endl;
    mCRL2log(debug) << "a = " << process::action_list(va.begin(), va.end()) << std::endl;
    mCRL2log(debug) << "b = " << process::action_list(vb.begin(), vb.end()) << std::endl;
#endif
    return data::sort_bool::false_();
  }
 
  // compute the intervals of a with equal names
  typedef std::vector<process::action>::iterator action_iterator;
  std::vector<std::pair<action_iterator, action_iterator> > intervals;
  action_iterator first = va.begin();
  while (first != va.end())
  {
    action_iterator next = std::upper_bound(first, va.end(), *first, detail::compare_action_labels());
    intervals.push_back(std::make_pair(first, next));
    first = next;
  }
 
  std::set<data::data_expression> z;
  detail::equal_data_parameters_builder f(va, vb, z);
  detail::forall_permutations(intervals.begin(), intervals.end(), f);
  data::data_expression result = data::lazy::join_or(z.begin(), z.end());
  return result;
}
 
inline data::data_expression not_equal_multi_actions(const multi_action& a, const multi_action& b)
{
  using namespace data::lazy;
 
  // make copies of a and b and sort them
  std::vector<process::action> va(a.actions().begin(), a.actions().end());
  std::vector<process::action> vb(b.actions().begin(), b.actions().end());
  std::sort(va.begin(), va.end(), detail::compare_action_label_arguments());
  std::sort(vb.begin(), vb.end(), detail::compare_action_label_arguments());
 
  if (!detail::equal_action_signatures(va, vb))
  {
    return data::sort_bool::true_();
  }
 
  // compute the intervals of a with equal names
  typedef std::vector<process::action>::iterator action_iterator;
  std::vector<std::pair<action_iterator, action_iterator> > intervals;
  action_iterator first = va.begin();
  while (first != va.end())
  {
    action_iterator next = std::upper_bound(first, va.end(), *first, detail::compare_action_labels());
    intervals.push_back(std::make_pair(first, next));
    first = next;
  }
  std::vector<data::data_expression> z;
  detail::not_equal_multi_actions_builder f(va, vb, z);
  detail::forall_permutations(intervals.begin(), intervals.end(), f);
  data::data_expression result = data::lazy::join_and(z.begin(), z.end());
  return result;
}
 
} // namespace lps
 
} // namespace mcrl2
 
namespace std
{
template<>
struct hash< mcrl2::lps::multi_action >
{
  std::size_t operator()(const mcrl2::lps::multi_action& ma) const
  {
    std::hash<atermpp::aterm> hasher;
    return hasher(ma.actions()) ^ (hasher(ma.time())<<1);
  }
};
 
} // namespace std
 
#endif // MCRL2_LPS_MULTI_ACTION_H