process_expression.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_PROCESS_PROCESS_EXPRESSION_H
#define MCRL2_PROCESS_PROCESS_EXPRESSION_H
 
#include "mcrl2/data/assignment.h"
#include "mcrl2/data/untyped_data_parameter.h"
#include "mcrl2/process/action_label.h"
#include "mcrl2/process/communication_expression.h"
#include "mcrl2/process/process_identifier.h"
#include "mcrl2/process/rename_expression.h"
 
namespace mcrl2
{
 
namespace process
{
 
//--- start generated classes ---//
class process_expression: public atermpp::aterm
{
  public:
    process_expression()
      : atermpp::aterm(core::detail::default_values::ProcExpr)
    {}
 
    explicit process_expression(const atermpp::aterm& term)
      : atermpp::aterm(term)
    {
      assert(core::detail::check_rule_ProcExpr(*this));
    }
 
    process_expression(const data::untyped_data_parameter& x)
      : atermpp::aterm(x)
    {}
 
    process_expression(const process_expression&) noexcept = default;
    process_expression(process_expression&&) noexcept = default;
    process_expression& operator=(const process_expression&) noexcept = default;
    process_expression& operator=(process_expression&&) noexcept = default;
};
 
typedef atermpp::term_list<process_expression> process_expression_list;
 
typedef std::vector<process_expression>    process_expression_vector;
 
// prototypes
inline bool is_action(const atermpp::aterm& x);
inline bool is_process_instance(const atermpp::aterm& x);
inline bool is_process_instance_assignment(const atermpp::aterm& x);
inline bool is_delta(const atermpp::aterm& x);
inline bool is_tau(const atermpp::aterm& x);
inline bool is_sum(const atermpp::aterm& x);
inline bool is_block(const atermpp::aterm& x);
inline bool is_hide(const atermpp::aterm& x);
inline bool is_rename(const atermpp::aterm& x);
inline bool is_comm(const atermpp::aterm& x);
inline bool is_allow(const atermpp::aterm& x);
inline bool is_sync(const atermpp::aterm& x);
inline bool is_at(const atermpp::aterm& x);
inline bool is_seq(const atermpp::aterm& x);
inline bool is_if_then(const atermpp::aterm& x);
inline bool is_if_then_else(const atermpp::aterm& x);
inline bool is_bounded_init(const atermpp::aterm& x);
inline bool is_merge(const atermpp::aterm& x);
inline bool is_left_merge(const atermpp::aterm& x);
inline bool is_choice(const atermpp::aterm& x);
inline bool is_stochastic_operator(const atermpp::aterm& x);
inline bool is_untyped_process_assignment(const atermpp::aterm& x);
 
inline
bool is_process_expression(const atermpp::aterm& x)
{
  return data::is_untyped_data_parameter(x) ||
         process::is_action(x) ||
         process::is_process_instance(x) ||
         process::is_process_instance_assignment(x) ||
         process::is_delta(x) ||
         process::is_tau(x) ||
         process::is_sum(x) ||
         process::is_block(x) ||
         process::is_hide(x) ||
         process::is_rename(x) ||
         process::is_comm(x) ||
         process::is_allow(x) ||
         process::is_sync(x) ||
         process::is_at(x) ||
         process::is_seq(x) ||
         process::is_if_then(x) ||
         process::is_if_then_else(x) ||
         process::is_bounded_init(x) ||
         process::is_merge(x) ||
         process::is_left_merge(x) ||
         process::is_choice(x) ||
         process::is_stochastic_operator(x) ||
         process::is_untyped_process_assignment(x);
}
 
// prototype declaration
std::string pp(const process_expression& x);
 
inline
std::ostream& operator<<(std::ostream& out, const process_expression& x)
{
  return out << process::pp(x);
}
 
inline void swap(process_expression& t1, process_expression& t2)
{
  t1.swap(t2);
}
 
 
class action: public process_expression
{
  public:
    action()
      : process_expression(core::detail::default_values::Action)
    {}
 
    explicit action(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Action(*this));
    }
 
    action(const action_label& label, const data::data_expression_list& arguments)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Action(), label, arguments))
    {}
 
    action(const action&) noexcept = default;
    action(action&&) noexcept = default;
    action& operator=(const action&) noexcept = default;
    action& operator=(action&&) noexcept = default;
 
    const action_label& label() const
    {
      return atermpp::down_cast<action_label>((*this)[0]);
    }
 
    const data::data_expression_list& arguments() const
    {
      return atermpp::down_cast<data::data_expression_list>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_action(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Action(), args...);
}
 
typedef atermpp::term_list<action> action_list;
 
typedef std::vector<action>    action_vector;
 
inline
bool is_action(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Action;
}
 
// prototype declaration
std::string pp(const action& x);
 
inline
std::ostream& operator<<(std::ostream& out, const action& x)
{
  return out << process::pp(x);
}
 
inline void swap(action& t1, action& t2)
{
  t1.swap(t2);
}
 
 
class process_instance: public process_expression
{
  public:
    process_instance()
      : process_expression(core::detail::default_values::Process)
    {}
 
    explicit process_instance(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Process(*this));
    }
 
    process_instance(const process_identifier& identifier, const data::data_expression_list& actual_parameters)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Process(), identifier, actual_parameters))
    {}
 
    process_instance(const process_instance&) noexcept = default;
    process_instance(process_instance&&) noexcept = default;
    process_instance& operator=(const process_instance&) noexcept = default;
    process_instance& operator=(process_instance&&) noexcept = default;
 
    const process_identifier& identifier() const
    {
      return atermpp::down_cast<process_identifier>((*this)[0]);
    }
 
    const data::data_expression_list& actual_parameters() const
    {
      return atermpp::down_cast<data::data_expression_list>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_process_instance(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Process(), args...);
}
 
inline
bool is_process_instance(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Process;
}
 
// prototype declaration
std::string pp(const process_instance& x);
 
inline
std::ostream& operator<<(std::ostream& out, const process_instance& x)
{
  return out << process::pp(x);
}
 
inline void swap(process_instance& t1, process_instance& t2)
{
  t1.swap(t2);
}
 
 
class process_instance_assignment: public process_expression
{
  public:
    process_instance_assignment()
      : process_expression(core::detail::default_values::ProcessAssignment)
    {}
 
    explicit process_instance_assignment(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_ProcessAssignment(*this));
    }
 
    process_instance_assignment(const process_identifier& identifier, const data::assignment_list& assignments)
      : process_expression(atermpp::aterm(core::detail::function_symbol_ProcessAssignment(), identifier, assignments))
    {}
 
    process_instance_assignment(const process_instance_assignment&) noexcept = default;
    process_instance_assignment(process_instance_assignment&&) noexcept = default;
    process_instance_assignment& operator=(const process_instance_assignment&) noexcept = default;
    process_instance_assignment& operator=(process_instance_assignment&&) noexcept = default;
 
    const process_identifier& identifier() const
    {
      return atermpp::down_cast<process_identifier>((*this)[0]);
    }
 
    const data::assignment_list& assignments() const
    {
      return atermpp::down_cast<data::assignment_list>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_process_instance_assignment(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_ProcessAssignment(), args...);
}
 
inline
bool is_process_instance_assignment(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::ProcessAssignment;
}
 
// prototype declaration
std::string pp(const process_instance_assignment& x);
 
inline
std::ostream& operator<<(std::ostream& out, const process_instance_assignment& x)
{
  return out << process::pp(x);
}
 
inline void swap(process_instance_assignment& t1, process_instance_assignment& t2)
{
  t1.swap(t2);
}
 
 
class delta: public process_expression
{
  public:
    delta()
      : process_expression(core::detail::default_values::Delta)
    {}
 
    explicit delta(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Delta(*this));
    }
 
    delta(const delta&) noexcept = default;
    delta(delta&&) noexcept = default;
    delta& operator=(const delta&) noexcept = default;
    delta& operator=(delta&&) noexcept = default;
};
 
inline
bool is_delta(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Delta;
}
 
// prototype declaration
std::string pp(const delta& x);
 
inline
std::ostream& operator<<(std::ostream& out, const delta& x)
{
  return out << process::pp(x);
}
 
inline void swap(delta& t1, delta& t2)
{
  t1.swap(t2);
}
 
 
class tau: public process_expression
{
  public:
    tau()
      : process_expression(core::detail::default_values::Tau)
    {}
 
    explicit tau(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Tau(*this));
    }
 
    tau(const tau&) noexcept = default;
    tau(tau&&) noexcept = default;
    tau& operator=(const tau&) noexcept = default;
    tau& operator=(tau&&) noexcept = default;
};
 
inline
bool is_tau(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Tau;
}
 
// prototype declaration
std::string pp(const tau& x);
 
inline
std::ostream& operator<<(std::ostream& out, const tau& x)
{
  return out << process::pp(x);
}
 
inline void swap(tau& t1, tau& t2)
{
  t1.swap(t2);
}
 
 
class sum: public process_expression
{
  public:
    sum()
      : process_expression(core::detail::default_values::Sum)
    {}
 
    explicit sum(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Sum(*this));
    }
 
    sum(const data::variable_list& variables, const process_expression& operand)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Sum(), variables, operand))
    {}
 
    sum(const sum&) noexcept = default;
    sum(sum&&) noexcept = default;
    sum& operator=(const sum&) noexcept = default;
    sum& operator=(sum&&) noexcept = default;
 
    const data::variable_list& variables() const
    {
      return atermpp::down_cast<data::variable_list>((*this)[0]);
    }
 
    const process_expression& operand() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_sum(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Sum(), args...);
}
 
inline
bool is_sum(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Sum;
}
 
// prototype declaration
std::string pp(const sum& x);
 
inline
std::ostream& operator<<(std::ostream& out, const sum& x)
{
  return out << process::pp(x);
}
 
inline void swap(sum& t1, sum& t2)
{
  t1.swap(t2);
}
 
 
class block: public process_expression
{
  public:
    block()
      : process_expression(core::detail::default_values::Block)
    {}
 
    explicit block(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Block(*this));
    }
 
    block(const core::identifier_string_list& block_set, const process_expression& operand)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Block(), block_set, operand))
    {}
 
    block(const block&) noexcept = default;
    block(block&&) noexcept = default;
    block& operator=(const block&) noexcept = default;
    block& operator=(block&&) noexcept = default;
 
    const core::identifier_string_list& block_set() const
    {
      return atermpp::down_cast<core::identifier_string_list>((*this)[0]);
    }
 
    const process_expression& operand() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_block(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Block(), args...);
}
 
inline
bool is_block(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Block;
}
 
// prototype declaration
std::string pp(const block& x);
 
inline
std::ostream& operator<<(std::ostream& out, const block& x)
{
  return out << process::pp(x);
}
 
inline void swap(block& t1, block& t2)
{
  t1.swap(t2);
}
 
 
class hide: public process_expression
{
  public:
    hide()
      : process_expression(core::detail::default_values::Hide)
    {}
 
    explicit hide(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Hide(*this));
    }
 
    hide(const core::identifier_string_list& hide_set, const process_expression& operand)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Hide(), hide_set, operand))
    {}
 
    hide(const hide&) noexcept = default;
    hide(hide&&) noexcept = default;
    hide& operator=(const hide&) noexcept = default;
    hide& operator=(hide&&) noexcept = default;
 
    const core::identifier_string_list& hide_set() const
    {
      return atermpp::down_cast<core::identifier_string_list>((*this)[0]);
    }
 
    const process_expression& operand() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_hide(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Hide(), args...);
}
 
inline
bool is_hide(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Hide;
}
 
// prototype declaration
std::string pp(const hide& x);
 
inline
std::ostream& operator<<(std::ostream& out, const hide& x)
{
  return out << process::pp(x);
}
 
inline void swap(hide& t1, hide& t2)
{
  t1.swap(t2);
}
 
 
class rename: public process_expression
{
  public:
    rename()
      : process_expression(core::detail::default_values::Rename)
    {}
 
    explicit rename(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Rename(*this));
    }
 
    rename(const rename_expression_list& rename_set, const process_expression& operand)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Rename(), rename_set, operand))
    {}
 
    rename(const rename&) noexcept = default;
    rename(rename&&) noexcept = default;
    rename& operator=(const rename&) noexcept = default;
    rename& operator=(rename&&) noexcept = default;
 
    const rename_expression_list& rename_set() const
    {
      return atermpp::down_cast<rename_expression_list>((*this)[0]);
    }
 
    const process_expression& operand() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_rename(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Rename(), args...);
}
 
inline
bool is_rename(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Rename;
}
 
// prototype declaration
std::string pp(const rename& x);
 
inline
std::ostream& operator<<(std::ostream& out, const rename& x)
{
  return out << process::pp(x);
}
 
inline void swap(rename& t1, rename& t2)
{
  t1.swap(t2);
}
 
 
class comm: public process_expression
{
  public:
    comm()
      : process_expression(core::detail::default_values::Comm)
    {}
 
    explicit comm(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Comm(*this));
    }
 
    comm(const communication_expression_list& comm_set, const process_expression& operand)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Comm(), comm_set, operand))
    {}
 
    comm(const comm&) noexcept = default;
    comm(comm&&) noexcept = default;
    comm& operator=(const comm&) noexcept = default;
    comm& operator=(comm&&) noexcept = default;
 
    const communication_expression_list& comm_set() const
    {
      return atermpp::down_cast<communication_expression_list>((*this)[0]);
    }
 
    const process_expression& operand() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_comm(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Comm(), args...);
}
 
inline
bool is_comm(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Comm;
}
 
// prototype declaration
std::string pp(const comm& x);
 
inline
std::ostream& operator<<(std::ostream& out, const comm& x)
{
  return out << process::pp(x);
}
 
inline void swap(comm& t1, comm& t2)
{
  t1.swap(t2);
}
 
 
class allow: public process_expression
{
  public:
    allow()
      : process_expression(core::detail::default_values::Allow)
    {}
 
    explicit allow(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Allow(*this));
    }
 
    allow(const action_name_multiset_list& allow_set, const process_expression& operand)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Allow(), allow_set, operand))
    {}
 
    allow(const allow&) noexcept = default;
    allow(allow&&) noexcept = default;
    allow& operator=(const allow&) noexcept = default;
    allow& operator=(allow&&) noexcept = default;
 
    const action_name_multiset_list& allow_set() const
    {
      return atermpp::down_cast<action_name_multiset_list>((*this)[0]);
    }
 
    const process_expression& operand() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_allow(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Allow(), args...);
}
 
inline
bool is_allow(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Allow;
}
 
// prototype declaration
std::string pp(const allow& x);
 
inline
std::ostream& operator<<(std::ostream& out, const allow& x)
{
  return out << process::pp(x);
}
 
inline void swap(allow& t1, allow& t2)
{
  t1.swap(t2);
}
 
 
class sync: public process_expression
{
  public:
    sync()
      : process_expression(core::detail::default_values::Sync)
    {}
 
    explicit sync(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Sync(*this));
    }
 
    sync(const process_expression& left, const process_expression& right)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Sync(), left, right))
    {}
 
    sync(const sync&) noexcept = default;
    sync(sync&&) noexcept = default;
    sync& operator=(const sync&) noexcept = default;
    sync& operator=(sync&&) noexcept = default;
 
    const process_expression& left() const
    {
      return atermpp::down_cast<process_expression>((*this)[0]);
    }
 
    const process_expression& right() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_sync(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Sync(), args...);
}
 
inline
bool is_sync(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Sync;
}
 
// prototype declaration
std::string pp(const sync& x);
 
inline
std::ostream& operator<<(std::ostream& out, const sync& x)
{
  return out << process::pp(x);
}
 
inline void swap(sync& t1, sync& t2)
{
  t1.swap(t2);
}
 
 
class at: public process_expression
{
  public:
    at()
      : process_expression(core::detail::default_values::AtTime)
    {}
 
    explicit at(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_AtTime(*this));
    }
 
    at(const process_expression& operand, const data::data_expression& time_stamp)
      : process_expression(atermpp::aterm(core::detail::function_symbol_AtTime(), operand, time_stamp))
    {}
 
    at(const at&) noexcept = default;
    at(at&&) noexcept = default;
    at& operator=(const at&) noexcept = default;
    at& operator=(at&&) noexcept = default;
 
    const process_expression& operand() const
    {
      return atermpp::down_cast<process_expression>((*this)[0]);
    }
 
    const data::data_expression& time_stamp() const
    {
      return atermpp::down_cast<data::data_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_at(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_AtTime(), args...);
}
 
inline
bool is_at(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::AtTime;
}
 
// prototype declaration
std::string pp(const at& x);
 
inline
std::ostream& operator<<(std::ostream& out, const at& x)
{
  return out << process::pp(x);
}
 
inline void swap(at& t1, at& t2)
{
  t1.swap(t2);
}
 
 
class seq: public process_expression
{
  public:
    seq()
      : process_expression(core::detail::default_values::Seq)
    {}
 
    explicit seq(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Seq(*this));
    }
 
    seq(const process_expression& left, const process_expression& right)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Seq(), left, right))
    {}
 
    seq(const seq&) noexcept = default;
    seq(seq&&) noexcept = default;
    seq& operator=(const seq&) noexcept = default;
    seq& operator=(seq&&) noexcept = default;
 
    const process_expression& left() const
    {
      return atermpp::down_cast<process_expression>((*this)[0]);
    }
 
    const process_expression& right() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_seq(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Seq(), args...);
}
 
inline
bool is_seq(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Seq;
}
 
// prototype declaration
std::string pp(const seq& x);
 
inline
std::ostream& operator<<(std::ostream& out, const seq& x)
{
  return out << process::pp(x);
}
 
inline void swap(seq& t1, seq& t2)
{
  t1.swap(t2);
}
 
 
class if_then: public process_expression
{
  public:
    if_then()
      : process_expression(core::detail::default_values::IfThen)
    {}
 
    explicit if_then(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_IfThen(*this));
    }
 
    if_then(const data::data_expression& condition, const process_expression& then_case)
      : process_expression(atermpp::aterm(core::detail::function_symbol_IfThen(), condition, then_case))
    {}
 
    if_then(const if_then&) noexcept = default;
    if_then(if_then&&) noexcept = default;
    if_then& operator=(const if_then&) noexcept = default;
    if_then& operator=(if_then&&) noexcept = default;
 
    const data::data_expression& condition() const
    {
      return atermpp::down_cast<data::data_expression>((*this)[0]);
    }
 
    const process_expression& then_case() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_if_then(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_IfThen(), args...);
}
 
inline
bool is_if_then(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::IfThen;
}
 
// prototype declaration
std::string pp(const if_then& x);
 
inline
std::ostream& operator<<(std::ostream& out, const if_then& x)
{
  return out << process::pp(x);
}
 
inline void swap(if_then& t1, if_then& t2)
{
  t1.swap(t2);
}
 
 
class if_then_else: public process_expression
{
  public:
    if_then_else()
      : process_expression(core::detail::default_values::IfThenElse)
    {}
 
    explicit if_then_else(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_IfThenElse(*this));
    }
 
    if_then_else(const data::data_expression& condition, const process_expression& then_case, const process_expression& else_case)
      : process_expression(atermpp::aterm(core::detail::function_symbol_IfThenElse(), condition, then_case, else_case))
    {}
 
    if_then_else(const if_then_else&) noexcept = default;
    if_then_else(if_then_else&&) noexcept = default;
    if_then_else& operator=(const if_then_else&) noexcept = default;
    if_then_else& operator=(if_then_else&&) noexcept = default;
 
    const data::data_expression& condition() const
    {
      return atermpp::down_cast<data::data_expression>((*this)[0]);
    }
 
    const process_expression& then_case() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
 
    const process_expression& else_case() const
    {
      return atermpp::down_cast<process_expression>((*this)[2]);
    }
};
 
template <class... ARGUMENTS>
inline void make_if_then_else(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_IfThenElse(), args...);
}
 
inline
bool is_if_then_else(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::IfThenElse;
}
 
// prototype declaration
std::string pp(const if_then_else& x);
 
inline
std::ostream& operator<<(std::ostream& out, const if_then_else& x)
{
  return out << process::pp(x);
}
 
inline void swap(if_then_else& t1, if_then_else& t2)
{
  t1.swap(t2);
}
 
 
class bounded_init: public process_expression
{
  public:
    bounded_init()
      : process_expression(core::detail::default_values::BInit)
    {}
 
    explicit bounded_init(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_BInit(*this));
    }
 
    bounded_init(const process_expression& left, const process_expression& right)
      : process_expression(atermpp::aterm(core::detail::function_symbol_BInit(), left, right))
    {}
 
    bounded_init(const bounded_init&) noexcept = default;
    bounded_init(bounded_init&&) noexcept = default;
    bounded_init& operator=(const bounded_init&) noexcept = default;
    bounded_init& operator=(bounded_init&&) noexcept = default;
 
    const process_expression& left() const
    {
      return atermpp::down_cast<process_expression>((*this)[0]);
    }
 
    const process_expression& right() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_bounded_init(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_BInit(), args...);
}
 
inline
bool is_bounded_init(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::BInit;
}
 
// prototype declaration
std::string pp(const bounded_init& x);
 
inline
std::ostream& operator<<(std::ostream& out, const bounded_init& x)
{
  return out << process::pp(x);
}
 
inline void swap(bounded_init& t1, bounded_init& t2)
{
  t1.swap(t2);
}
 
 
class merge: public process_expression
{
  public:
    merge()
      : process_expression(core::detail::default_values::Merge)
    {}
 
    explicit merge(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Merge(*this));
    }
 
    merge(const process_expression& left, const process_expression& right)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Merge(), left, right))
    {}
 
    merge(const merge&) noexcept = default;
    merge(merge&&) noexcept = default;
    merge& operator=(const merge&) noexcept = default;
    merge& operator=(merge&&) noexcept = default;
 
    const process_expression& left() const
    {
      return atermpp::down_cast<process_expression>((*this)[0]);
    }
 
    const process_expression& right() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_merge(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Merge(), args...);
}
 
inline
bool is_merge(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Merge;
}
 
// prototype declaration
std::string pp(const merge& x);
 
inline
std::ostream& operator<<(std::ostream& out, const merge& x)
{
  return out << process::pp(x);
}
 
inline void swap(merge& t1, merge& t2)
{
  t1.swap(t2);
}
 
 
class left_merge: public process_expression
{
  public:
    left_merge()
      : process_expression(core::detail::default_values::LMerge)
    {}
 
    explicit left_merge(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_LMerge(*this));
    }
 
    left_merge(const process_expression& left, const process_expression& right)
      : process_expression(atermpp::aterm(core::detail::function_symbol_LMerge(), left, right))
    {}
 
    left_merge(const left_merge&) noexcept = default;
    left_merge(left_merge&&) noexcept = default;
    left_merge& operator=(const left_merge&) noexcept = default;
    left_merge& operator=(left_merge&&) noexcept = default;
 
    const process_expression& left() const
    {
      return atermpp::down_cast<process_expression>((*this)[0]);
    }
 
    const process_expression& right() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_left_merge(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_LMerge(), args...);
}
 
inline
bool is_left_merge(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::LMerge;
}
 
// prototype declaration
std::string pp(const left_merge& x);
 
inline
std::ostream& operator<<(std::ostream& out, const left_merge& x)
{
  return out << process::pp(x);
}
 
inline void swap(left_merge& t1, left_merge& t2)
{
  t1.swap(t2);
}
 
 
class choice: public process_expression
{
  public:
    choice()
      : process_expression(core::detail::default_values::Choice)
    {}
 
    explicit choice(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_Choice(*this));
    }
 
    choice(const process_expression& left, const process_expression& right)
      : process_expression(atermpp::aterm(core::detail::function_symbol_Choice(), left, right))
    {}
 
    choice(const choice&) noexcept = default;
    choice(choice&&) noexcept = default;
    choice& operator=(const choice&) noexcept = default;
    choice& operator=(choice&&) noexcept = default;
 
    const process_expression& left() const
    {
      return atermpp::down_cast<process_expression>((*this)[0]);
    }
 
    const process_expression& right() const
    {
      return atermpp::down_cast<process_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_choice(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_Choice(), args...);
}
 
inline
bool is_choice(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Choice;
}
 
// prototype declaration
std::string pp(const choice& x);
 
inline
std::ostream& operator<<(std::ostream& out, const choice& x)
{
  return out << process::pp(x);
}
 
inline void swap(choice& t1, choice& t2)
{
  t1.swap(t2);
}
 
 
class stochastic_operator: public process_expression
{
  public:
    stochastic_operator()
      : process_expression(core::detail::default_values::StochasticOperator)
    {}
 
    explicit stochastic_operator(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_StochasticOperator(*this));
    }
 
    stochastic_operator(const data::variable_list& variables, const data::data_expression& distribution, const process_expression& operand)
      : process_expression(atermpp::aterm(core::detail::function_symbol_StochasticOperator(), variables, distribution, operand))
    {}
 
    stochastic_operator(const stochastic_operator&) noexcept = default;
    stochastic_operator(stochastic_operator&&) noexcept = default;
    stochastic_operator& operator=(const stochastic_operator&) noexcept = default;
    stochastic_operator& operator=(stochastic_operator&&) noexcept = default;
 
    const data::variable_list& variables() const
    {
      return atermpp::down_cast<data::variable_list>((*this)[0]);
    }
 
    const data::data_expression& distribution() const
    {
      return atermpp::down_cast<data::data_expression>((*this)[1]);
    }
 
    const process_expression& operand() const
    {
      return atermpp::down_cast<process_expression>((*this)[2]);
    }
};
 
template <class... ARGUMENTS>
inline void make_stochastic_operator(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_StochasticOperator(), args...);
}
 
inline
bool is_stochastic_operator(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::StochasticOperator;
}
 
// prototype declaration
std::string pp(const stochastic_operator& x);
 
inline
std::ostream& operator<<(std::ostream& out, const stochastic_operator& x)
{
  return out << process::pp(x);
}
 
inline void swap(stochastic_operator& t1, stochastic_operator& t2)
{
  t1.swap(t2);
}
 
 
class untyped_process_assignment: public process_expression
{
  public:
    untyped_process_assignment()
      : process_expression(core::detail::default_values::UntypedProcessAssignment)
    {}
 
    explicit untyped_process_assignment(const atermpp::aterm& term)
      : process_expression(term)
    {
      assert(core::detail::check_term_UntypedProcessAssignment(*this));
    }
 
    untyped_process_assignment(const core::identifier_string& name, const data::untyped_identifier_assignment_list& assignments)
      : process_expression(atermpp::aterm(core::detail::function_symbol_UntypedProcessAssignment(), name, assignments))
    {}
 
    untyped_process_assignment(const std::string& name, const data::untyped_identifier_assignment_list& assignments)
      : process_expression(atermpp::aterm(core::detail::function_symbol_UntypedProcessAssignment(), core::identifier_string(name), assignments))
    {}
 
    untyped_process_assignment(const untyped_process_assignment&) noexcept = default;
    untyped_process_assignment(untyped_process_assignment&&) noexcept = default;
    untyped_process_assignment& operator=(const untyped_process_assignment&) noexcept = default;
    untyped_process_assignment& operator=(untyped_process_assignment&&) noexcept = default;
 
    const core::identifier_string& name() const
    {
      return atermpp::down_cast<core::identifier_string>((*this)[0]);
    }
 
    const data::untyped_identifier_assignment_list& assignments() const
    {
      return atermpp::down_cast<data::untyped_identifier_assignment_list>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_untyped_process_assignment(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_UntypedProcessAssignment(), args...);
}
 
inline
bool is_untyped_process_assignment(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::UntypedProcessAssignment;
}
 
// prototype declaration
std::string pp(const untyped_process_assignment& x);
 
inline
std::ostream& operator<<(std::ostream& out, const untyped_process_assignment& x)
{
  return out << process::pp(x);
}
 
inline void swap(untyped_process_assignment& t1, untyped_process_assignment& t2)
{
  t1.swap(t2);
}
//--- end generated classes ---//
 
// template function overloads
std::string pp(const process_expression_list& x);
std::string pp(const process_expression_vector& x);
std::set<data::sort_expression> find_sort_expressions(const process::process_expression& x);
std::string pp(const action_list& x);
std::string pp(const action_vector& x);
action normalize_sorts(const action& x, const data::sort_specification& sortspec);
action translate_user_notation(const action& x);
process::process_expression translate_user_notation(const process::process_expression& x);
std::set<data::variable> find_all_variables(const action& x);
std::set<data::variable> find_free_variables(const action& x);
 
inline
bool equal_signatures(const action& a, const action& b)
{
  if (a.label() != b.label())
  {
    return false;
  }
 
  const data::data_expression_list& a_args = a.arguments();
  const data::data_expression_list& b_args = b.arguments();
 
  if (a_args.size() != b_args.size())
  {
    return false;
  }
 
  return std::equal(a_args.begin(), a_args.end(), b_args.begin(), [](const data::data_expression& x, const data::data_expression& y) { return x.sort() == y.sort(); });
}
 
} // namespace process
 
} // namespace mcrl2
 
namespace std
{
 
template <>
struct hash<mcrl2::process::action>
{
  std::size_t operator()(const mcrl2::process::action& t) const
  {
    return std::hash<atermpp::aterm>()(t);
  }
 
};
 
 
} // namespace std
 
#endif // MCRL2_PROCESS_PROCESS_EXPRESSION_H