process_specification.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_SPECIFICATION_H
#define MCRL2_PROCESS_PROCESS_SPECIFICATION_H
 
#include "mcrl2/core/load_aterm.h"
#include "mcrl2/core/print.h"
#include "mcrl2/data/data_io.h"
#include "mcrl2/data/detail/io.h"
#include "mcrl2/process/process_equation.h"
 
namespace mcrl2
{
 
namespace process
{
 
class process_specification;
atermpp::aterm process_specification_to_aterm(const process_specification& spec);
void complete_data_specification(process_specification&);
 
// template function overloads
std::string pp(const process_specification& x);
void normalize_sorts(process_specification& x, const data::sort_specification& sortspec);
void translate_user_notation(process::process_specification& x);
std::set<data::sort_expression> find_sort_expressions(const process::process_specification& x);
std::set<core::identifier_string> find_identifiers(const process::process_specification& x);
std::set<data::variable> find_free_variables(const process::process_specification& x);
 
inline
bool is_process_specification(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::ProcSpec;
}
 
//<ProcSpec>     ::= ProcSpec(<DataSpec>, <ActSpec>, <GlobVarSpec>, <ProcEqnSpec>, <ProcInit>)
class process_specification
{
  protected:
    data::data_specification m_data;
 
    process::action_label_list m_action_labels;
 
    std::set<data::variable> m_global_variables;
 
    std::vector<process_equation> m_equations;
 
    process_expression m_initial_process;
 
    void construct_from_aterm(const atermpp::aterm& t)
    {
      atermpp::aterm::iterator i = t.begin();
      m_data            = data::data_specification(*i++);
      m_action_labels   = atermpp::down_cast<process::action_label_list>((*i++)[0]);
      data::variable_list global_variables = atermpp::down_cast<data::variable_list>((*i++)[0]);
      m_global_variables = std::set<data::variable>(global_variables.begin(),global_variables.end());
      process_equation_list l = atermpp::down_cast<process_equation_list>((*i++)[0]);
      atermpp::aterm init = (*i);
      m_initial_process = process_expression(init[0]);
      m_equations       = std::vector<process_equation>(l.begin(), l.end());
    }
 
  public:
    process_specification()
    {}
 
    process_specification(atermpp::aterm t)
    {
      assert(core::detail::check_term_ProcSpec(t));
      construct_from_aterm(t);
      complete_data_specification(*this);
    }
 
    process_specification(data::data_specification data, process::action_label_list action_labels, process_equation_list equations, process_expression init)
      : m_data(data),
        m_action_labels(action_labels),
        m_equations(equations.begin(), equations.end()),
        m_initial_process(init)
    {}
 
    process_specification(
      data::data_specification data,
      process::action_label_list action_labels,
      data::variable_list global_variables,
      process_equation_list equations,
      process_expression init)
      : m_data(data),
        m_action_labels(action_labels),
        m_global_variables(global_variables.begin(),global_variables.end()),
        m_equations(equations.begin(), equations.end()),
        m_initial_process(init)
    {}
 
    const data::data_specification& data() const
    {
      return m_data;
    }
 
    data::data_specification& data()
    {
      return m_data;
    }
 
    const process::action_label_list& action_labels() const
    {
      return m_action_labels;
    }
 
    process::action_label_list& action_labels()
    {
      return m_action_labels;
    }
 
    const std::set<data::variable>& global_variables() const
    {
      return m_global_variables;
    }
 
    std::set<data::variable>& global_variables()
    {
      return m_global_variables;
    }
 
    const std::vector<process_equation>& equations() const
    {
      return m_equations;
    }
 
    std::vector<process_equation>& equations()
    {
      return m_equations;
    }
 
    const process_expression& init() const
    {
      return m_initial_process;
    }
 
    process_expression& init()
    {
      return m_initial_process;
    }
};
 
//--- start generated class process_specification ---//
// prototype declaration
std::string pp(const process_specification& x);
 
inline
std::ostream& operator<<(std::ostream& out, const process_specification& x)
{
  return out << process::pp(x);
}
//--- end generated class process_specification ---//
 
inline
void complete_data_specification(process_specification& spec)
{
  std::set<data::sort_expression> s = process::find_sort_expressions(spec);
  spec.data().add_context_sorts(s);
}
 
inline
atermpp::aterm process_specification_to_aterm(const process_specification& spec)
{
  return atermpp::aterm(core::detail::function_symbol_ProcSpec(),
           data::detail::data_specification_to_aterm(spec.data()),
           atermpp::aterm(core::detail::function_symbol_ActSpec(), spec.action_labels()),
           atermpp::aterm(core::detail::function_symbol_GlobVarSpec(), data::variable_list(spec.global_variables().begin(),spec.global_variables().end())),
           atermpp::aterm(core::detail::function_symbol_ProcEqnSpec(), process_equation_list(spec.equations().begin(), spec.equations().end())),
           atermpp::aterm(core::detail::function_symbol_ProcessInit(), spec.init())
         );
}
 
inline
bool operator==(const process_specification& spec1, const process_specification& spec2)
{
  return process_specification_to_aterm(spec1) == process_specification_to_aterm(spec2);
}
 
inline
bool operator!=(const process_specification& spec1, const process_specification& spec2)
{
  return !(spec1 == spec2);
}
 
} // namespace process
 
} // namespace mcrl2
 
#endif // MCRL2_PROCESS_PROCESS_SPECIFICATION_H