text: // Author(s): Wieger Wesselink
  // Copyright: see the accompanying file COPYING or copy at
  // https://svn.win.tue.nl/trac/MCRL2/browser/trunk/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 mcrl2/modal_formula/action_formula.h
  /// \brief Add your file description here.
  
  #ifndef MCRL2_MODAL_ACTION_FORMULA_H
  #define MCRL2_MODAL_ACTION_FORMULA_H
  
  #include <iostream> // for debugging
  #include <stdexcept>
  #include <string>
  #include <cassert>
  #include "mcrl2/atermpp/aterm_appl.h"
  #include "mcrl2/core/detail/precedence.h"
  #include "mcrl2/data/data_specification.h"
  #include "mcrl2/lps/multi_action.h"
  #include "mcrl2/process/process_expression.h"
  #include "mcrl2/process/untyped_multi_action.h"
  
  namespace mcrl2
  {
  
  namespace action_formulas
  {
  
  //--- start generated classes ---//
  /// \brief An action formula
  class action_formula: public atermpp::aterm_appl
  {
    public:
      /// \brief Default constructor.
      action_formula()
        : atermpp::aterm_appl(core::detail::default_values::ActFrm)
      {}
  
      /// \brief Constructor.
      /// \param term A term
      explicit action_formula(const atermpp::aterm& term)
        : atermpp::aterm_appl(term)
      {
        assert(core::detail::check_rule_ActFrm(*this));
      }
  
      /// \brief Constructor.
      action_formula(const data::data_expression& x)
        : atermpp::aterm_appl(x)
      {}
  
      /// \brief Constructor.
      action_formula(const data::untyped_data_parameter& x)
        : atermpp::aterm_appl(x)
      {}
  
      /// \brief Constructor.
      action_formula(const process::untyped_multi_action& x)
        : atermpp::aterm_appl(x)
      {}
  };
  
  /// \brief list of action_formulas
  typedef atermpp::term_list<action_formula> action_formula_list;
  
  /// \brief vector of action_formulas
  typedef std::vector<action_formula>    action_formula_vector;
  
  // prototypes
  inline bool is_true(const atermpp::aterm_appl& x);
  inline bool is_false(const atermpp::aterm_appl& x);
  inline bool is_not(const atermpp::aterm_appl& x);
  inline bool is_and(const atermpp::aterm_appl& x);
  inline bool is_or(const atermpp::aterm_appl& x);
  inline bool is_imp(const atermpp::aterm_appl& x);
  inline bool is_forall(const atermpp::aterm_appl& x);
  inline bool is_exists(const atermpp::aterm_appl& x);
  inline bool is_at(const atermpp::aterm_appl& x);
  inline bool is_multi_action(const atermpp::aterm_appl& x);
  
  /// \brief Test for a action_formula expression
  /// \param x A term
  /// \return True if \a x is a action_formula expression
  inline
  bool is_action_formula(const atermpp::aterm_appl& x)
  {
    return data::is_data_expression(x) ||
           action_formulas::is_true(x) ||
           action_formulas::is_false(x) ||
           action_formulas::is_not(x) ||
           action_formulas::is_and(x) ||
           action_formulas::is_or(x) ||
           action_formulas::is_imp(x) ||
           action_formulas::is_forall(x) ||
           action_formulas::is_exists(x) ||
           action_formulas::is_at(x) ||
           action_formulas::is_multi_action(x) ||
           process::is_untyped_multi_action(x) ||
           data::is_untyped_data_parameter(x);
  }
  
  // prototype declaration
  std::string pp(const action_formula& x);
  
  /// \brief Outputs the object to a stream
  /// \param out An output stream
  /// \param x Object x
  /// \return The output stream
  inline
  std::ostream& operator<<(std::ostream& out, const action_formula& x)
  {
    return out << action_formulas::pp(x);
  }
  
  /// \brief swap overload
  inline void swap(action_formula& t1, action_formula& t2)
  {
    t1.swap(t2);
  }
  
  
  /// \brief The value true for action formulas
  class true_: public action_formula
  {
    public:
      /// \brief Default constructor.
      true_()
        : action_formula(core::detail::default_values::ActTrue)
      {}
  
      /// \brief Constructor.
      /// \param term A term
      explicit true_(const atermpp::aterm& term)
        : action_formula(term)
      {
        assert(core::detail::check_term_ActTrue(*this));
      }
  };
  
  /// \brief Test for a true expression
  /// \param x A term
  /// \return True if \a x is a true expression
  inline
  bool is_true(const atermpp::aterm_appl& x)
  {
    return x.function() == core::detail::function_symbols::ActTrue;
  }
  
  // prototype declaration
  std::string pp(const true_& x);
  
  /// \brief Outputs the object to a stream
  /// \param out An output stream
  /// \param x Object x
  /// \return The output stream
  inline
  std::ostream& operator<<(std::ostream& out, const true_& x)
  {
    return out << action_formulas::pp(x);
  }
  
  /// \brief swap overload
  inline void swap(true_& t1, true_& t2)
  {
    t1.swap(t2);
  }
  
  
  /// \brief The value false for action formulas
  class false_: public action_formula
  {
    public:
      /// \brief Default constructor.
      false_()
        : action_formula(core::detail::default_values::ActFalse)
      {}
  
      /// \brief Constructor.
      /// \param term A term
      explicit false_(const atermpp::aterm& term)
        : action_formula(term)
      {
        assert(core::detail::check_term_ActFalse(*this));
      }
  };
  
  /// \brief Test for a false expression
  /// \param x A term
  /// \return True if \a x is a false expression
  inline
  bool is_false(const atermpp::aterm_appl& x)
  {
    return x.function() == core::detail::function_symbols::ActFalse;
  }
  
  // prototype declaration
  std::string pp(const false_& x);
  
  /// \brief Outputs the object to a stream
  /// \param out An output stream
  /// \param x Object x
  /// \return The output stream
  inline
  std::ostream& operator<<(std::ostream& out, const false_& x)
  {
    return out << action_formulas::pp(x);
  }
  
  /// \brief swap overload
  inline void swap(false_& t1, false_& t2)
  {
    t1.swap(t2);
  }
  
  
  /// \brief The not operator for action formulas
  class not_: public action_formula
  {
    public:
      /// \brief Default constructor.
      not_()
        : action_formula(core::detail::default_values::ActNot)
      {}
  
      /// \brief Constructor.
      /// \param term A term
      explicit not_(const atermpp::aterm& term)
        : action_formula(term)
      {
        assert(core::detail::check_term_ActNot(*this));
      }
  
      /// \brief Constructor.
      not_(const action_formula& operand)
        : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActNot(), operand))
      {}
  
      const action_formula& operand() const
      {
        return atermpp::down_cast<action_formula>((*this)[0]);
      }
  };
  
  /// \brief Test for a not expression
  /// \param x A term
  /// \return True if \a x is a not expression
  inline
  bool is_not(const atermpp::aterm_appl& x)
  {
    return x.function() == core::detail::function_symbols::ActNot;
  }
  
  // prototype declaration
  std::string pp(const not_& x);
  
  /// \brief Outputs the object to a stream
  /// \param out An output stream
  /// \param x Object x
  /// \return The output stream
  inline
  std::ostream& operator<<(std::ostream& out, const not_& x)
  {
    return out << action_formulas::pp(x);
  }
  
  /// \brief swap overload
  inline void swap(not_& t1, not_& t2)
  {
    t1.swap(t2);
  }
  
  
  /// \brief The and operator for action formulas
  class and_: public action_formula
  {
    public:
      /// \brief Default constructor.
      and_()
        : action_formula(core::detail::default_values::ActAnd)
      {}
  
      /// \brief Constructor.
      /// \param term A term
      explicit and_(const atermpp::aterm& term)
        : action_formula(term)
      {
        assert(core::detail::check_term_ActAnd(*this));
      }
  
      /// \brief Constructor.
      and_(const action_formula& left, const action_formula& right)
        : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActAnd(), left, right))
      {}
  
      const action_formula& left() const
      {
        return atermpp::down_cast<action_formula>((*this)[0]);
      }
  
      const action_formula& right() const
      {
        return atermpp::down_cast<action_formula>((*this)[1]);
      }
  };
  
  /// \brief Test for a and expression
  /// \param x A term
  /// \return True if \a x is a and expression
  inline
  bool is_and(const atermpp::aterm_appl& x)
  {
    return x.function() == core::detail::function_symbols::ActAnd;
  }
  
  // prototype declaration
  std::string pp(const and_& x);
  
  /// \brief Outputs the object to a stream
  /// \param out An output stream
  /// \param x Object x
  /// \return The output stream
  inline
  std::ostream& operator<<(std::ostream& out, const and_& x)
  {
    return out << action_formulas::pp(x);
  }
  
  /// \brief swap overload
  inline void swap(and_& t1, and_& t2)
  {
    t1.swap(t2);
  }
  
  
  /// \brief The or operator for action formulas
  class or_: public action_formula
  {
    public:
      /// \brief Default constructor.
      or_()
        : action_formula(core::detail::default_values::ActOr)
      {}
  
      /// \brief Constructor.
      /// \param term A term
      explicit or_(const atermpp::aterm& term)
        : action_formula(term)
      {
        assert(core::detail::check_term_ActOr(*this));
      }
  
      /// \brief Constructor.
      or_(const action_formula& left, const action_formula& right)
        : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActOr(), left, right))
      {}
  
      const action_formula& left() const
      {
        return atermpp::down_cast<action_formula>((*this)[0]);
      }
  
      const action_formula& right() const
      {
        return atermpp::down_cast<action_formula>((*this)[1]);
      }
  };
  
  /// \brief Test for a or expression
  /// \param x A term
  /// \return True if \a x is a or expression
  inline
  bool is_or(const atermpp::aterm_appl& x)
  {
    return x.function() == core::detail::function_symbols::ActOr;
  }
  
  // prototype declaration
  std::string pp(const or_& x);
  
  /// \brief Outputs the object to a stream
  /// \param out An output stream
  /// \param x Object x
  /// \return The output stream
  inline
  std::ostream& operator<<(std::ostream& out, const or_& x)
  {
    return out << action_formulas::pp(x);
  }
  
  /// \brief swap overload
  inline void swap(or_& t1, or_& t2)
  {
    t1.swap(t2);
  }
  
  
  /// \brief The implication operator for action formulas
  class imp: public action_formula
  {
    public:
      /// \brief Default constructor.
      imp()
        : action_formula(core::detail::default_values::ActImp)
      {}
  
      /// \brief Constructor.
      /// \param term A term
      explicit imp(const atermpp::aterm& term)
        : action_formula(term)
      {
        assert(core::detail::check_term_ActImp(*this));
      }
  
      /// \brief Constructor.
      imp(const action_formula& left, const action_formula& right)
        : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActImp(), left, right))
      {}
  
      const action_formula& left() const
      {
        return atermpp::down_cast<action_formula>((*this)[0]);
      }
  
      const action_formula& right() const
      {
        return atermpp::down_cast<action_formula>((*this)[1]);
      }
  };
  
  /// \brief Test for a imp expression
  /// \param x A term
  /// \return True if \a x is a imp expression
  inline
  bool is_imp(const atermpp::aterm_appl& x)
  {
    return x.function() == core::detail::function_symbols::ActImp;
  }
  
  // prototype declaration
  std::string pp(const imp& x);
  
  /// \brief Outputs the object to a stream
  /// \param out An output stream
  /// \param x Object x
  /// \return The output stream
  inline
  std::ostream& operator<<(std::ostream& out, const imp& x)
  {
    return out << action_formulas::pp(x);
  }
  
  /// \brief swap overload
  inline void swap(imp& t1, imp& t2)
  {
    t1.swap(t2);
  }
  
  
  /// \brief The universal quantification operator for action formulas
  class forall: public action_formula
  {
    public:
      /// \brief Default constructor.
      forall()
        : action_formula(core::detail::default_values::ActForall)
      {}
  
      /// \brief Constructor.
      /// \param term A term
      explicit forall(const atermpp::aterm& term)
        : action_formula(term)
      {
        assert(core::detail::check_term_ActForall(*this));
      }
  
      /// \brief Constructor.
      forall(const data::variable_list& variables, const action_formula& body)
        : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActForall(), variables, body))
      {}
  
      const data::variable_list& variables() const
      {
        return atermpp::down_cast<data::variable_list>((*this)[0]);
      }
  
      const action_formula& body() const
      {
        return atermpp::down_cast<action_formula>((*this)[1]);
      }
  };
  
  /// \brief Test for a forall expression
  /// \param x A term
  /// \return True if \a x is a forall expression
  inline
  bool is_forall(const atermpp::aterm_appl& x)
  {
    return x.function() == core::detail::function_symbols::ActForall;
  }
  
  // prototype declaration
  std::string pp(const forall& x);
  
  /// \brief Outputs the object to a stream
  /// \param out An output stream
  /// \param x Object x
  /// \return The output stream
  inline
  std::ostream& operator<<(std::ostream& out, const forall& x)
  {
    return out << action_formulas::pp(x);
  }
  
  /// \brief swap overload
  inline void swap(forall& t1, forall& t2)
  {
    t1.swap(t2);
  }
  
  
  /// \brief The existential quantification operator for action formulas
  class exists: public action_formula
  {
    public:
      /// \brief Default constructor.
      exists()
        : action_formula(core::detail::default_values::ActExists)
      {}
  
      /// \brief Constructor.
      /// \param term A term
      explicit exists(const atermpp::aterm& term)
        : action_formula(term)
      {
        assert(core::detail::check_term_ActExists(*this));
      }
  
      /// \brief Constructor.
      exists(const data::variable_list& variables, const action_formula& body)
        : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActExists(), variables, body))
      {}
  
      const data::variable_list& variables() const
      {
        return atermpp::down_cast<data::variable_list>((*this)[0]);
      }
  
      const action_formula& body() const
      {
        return atermpp::down_cast<action_formula>((*this)[1]);
      }
  };
  
  /// \brief Test for a exists expression
  /// \param x A term
  /// \return True if \a x is a exists expression
  inline
  bool is_exists(const atermpp::aterm_appl& x)
  {
    return x.function() == core::detail::function_symbols::ActExists;
  }
  
  // prototype declaration
  std::string pp(const exists& x);
  
  /// \brief Outputs the object to a stream
  /// \param out An output stream
  /// \param x Object x
  /// \return The output stream
  inline
  std::ostream& operator<<(std::ostream& out, const exists& x)
  {
    return out << action_formulas::pp(x);
  }
  
  /// \brief swap overload
  inline void swap(exists& t1, exists& t2)
  {
    t1.swap(t2);
  }
  
  
  /// \brief The at operator for action formulas
  class at: public action_formula
  {
    public:
      /// \brief Default constructor.
      at()
        : action_formula(core::detail::default_values::ActAt)
      {}
  
      /// \brief Constructor.
      /// \param term A term
      explicit at(const atermpp::aterm& term)
        : action_formula(term)
      {
        assert(core::detail::check_term_ActAt(*this));
      }
  
      /// \brief Constructor.
      at(const action_formula& operand, const data::data_expression& time_stamp)
        : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActAt(), operand, time_stamp))
      {}
  
      const action_formula& operand() const
      {
        return atermpp::down_cast<action_formula>((*this)[0]);
      }
  
      const data::data_expression& time_stamp() const
      {
        return atermpp::down_cast<data::data_expression>((*this)[1]);
      }
  };
  
  /// \brief Test for a at expression
  /// \param x A term
  /// \return True if \a x is a at expression
  inline
  bool is_at(const atermpp::aterm_appl& x)
  {
    return x.function() == core::detail::function_symbols::ActAt;
  }
  
  // prototype declaration
  std::string pp(const at& x);
  
  /// \brief Outputs the object to a stream
  /// \param out An output stream
  /// \param x Object x
  /// \return The output stream
  inline
  std::ostream& operator<<(std::ostream& out, const at& x)
  {
    return out << action_formulas::pp(x);
  }
  
  /// \brief swap overload
  inline void swap(at& t1, at& t2)
  {
    t1.swap(t2);
  }
  
  
  /// \brief The multi action for action formulas
  class multi_action: public action_formula
  {
    public:
      /// \brief Default constructor.
      multi_action()
        : action_formula(core::detail::default_values::ActMultAct)
      {}
  
      /// \brief Constructor.
      /// \param term A term
      explicit multi_action(const atermpp::aterm& term)
        : action_formula(term)
      {
        assert(core::detail::check_term_ActMultAct(*this));
      }
  
      /// \brief Constructor.
      multi_action(const process::action_list& actions)
        : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActMultAct(), actions))
      {}
  
      const process::action_list& actions() const
      {
        return atermpp::down_cast<process::action_list>((*this)[0]);
      }
  };
  
  /// \brief Test for a multi_action expression
  /// \param x A term
  /// \return True if \a x is a multi_action expression
  inline
  bool is_multi_action(const atermpp::aterm_appl& x)
  {
    return x.function() == core::detail::function_symbols::ActMultAct;
  }
  
  // prototype declaration
  std::string pp(const multi_action& x);
  
  /// \brief Outputs the object to a stream
  /// \param out An output stream
  /// \param x Object x
  /// \return The output stream
  inline
  std::ostream& operator<<(std::ostream& out, const multi_action& x)
  {
    return out << action_formulas::pp(x);
  }
  
  /// \brief swap overload
  inline void swap(multi_action& t1, multi_action& t2)
  {
    t1.swap(t2);
  }
  //--- end generated classes ---//
  
  //template <typename T>
  //int left_precedence(const T&)
  //{
  //  return core::detail::precedences::max_precedence;
  //}
  inline int left_precedence(const forall&) { return 21; }
  inline int left_precedence(const exists&) { return 21; }
  inline int left_precedence(const imp&)    { return 22; }
  inline int left_precedence(const or_&)    { return 23; }
  inline int left_precedence(const and_&)   { return 24; }
  inline int left_precedence(const at&)     { return 25; }
  inline int left_precedence(const not_&)   { return 26; }
  inline int left_precedence(const action_formula& x)
  {
    if      (is_forall(x)) { return left_precedence(static_cast<const forall&>(x)); }
    else if (is_exists(x)) { return left_precedence(static_cast<const exists&>(x)); }
    else if (is_imp(x))    { return left_precedence(static_cast<const imp&>(x)); }
    else if (is_or(x))     { return left_precedence(static_cast<const or_&>(x)); }
    else if (is_and(x))    { return left_precedence(static_cast<const and_&>(x)); }
    else if (is_at(x))     { return left_precedence(static_cast<const at&>(x)); }
    else if (is_not(x))    { return left_precedence(static_cast<const not_&>(x)); }
    return core::detail::precedences::max_precedence;
  }
  
  inline int right_precedence(const forall& x) { return (std::max)(left_precedence(x), left_precedence(static_cast<const forall&>(x).body())); }
  inline int right_precedence(const exists& x) { return (std::max)(left_precedence(x), left_precedence(static_cast<const exists&>(x).body())); }
  inline int right_precedence(const action_formula& x)
  {
    if      (is_forall(x)) { return right_precedence(static_cast<const forall&>(x)); }
    else if (is_exists(x)) { return right_precedence(static_cast<const exists&>(x)); }
    return left_precedence(x);
  }
  
  inline const action_formula& unary_operand(const not_& x) { return x.operand(); }
  inline const action_formula& unary_operand(const at& x)   { return x.operand(); }
  inline const action_formula& binary_left(const and_& x)   { return x.left(); }
  inline const action_formula& binary_right(const and_& x)  { return x.right(); }
  inline const action_formula& binary_left(const or_& x)    { return x.left(); }
  inline const action_formula& binary_right(const or_& x)   { return x.right(); }
  inline const action_formula& binary_left(const imp& x)    { return x.left(); }
  inline const action_formula& binary_right(const imp& x)   { return x.right(); }
  
  // template function overloads
  std::set<data::variable> find_all_variables(const action_formulas::action_formula& x);
  
  } // namespace action_formulas
  
  } // namespace mcrl2
  
  #endif // MCRL2_MODAL_ACTION_FORMULA_H
  