Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/pbes/pbes_equation.h
      10             : /// \brief The class pbes_equation.
      11             : 
      12             : #ifndef MCRL2_PBES_PBES_EQUATION_H
      13             : #define MCRL2_PBES_PBES_EQUATION_H
      14             : 
      15             : #include "mcrl2/data/detail/sequence_algorithm.h"
      16             : #include "mcrl2/pbes/fixpoint_symbol.h"
      17             : #include "mcrl2/pbes/pbes_expression.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace pbes_system
      23             : {
      24             : 
      25             : class pbes_equation;
      26             : atermpp::aterm_appl pbes_equation_to_aterm(const pbes_equation& eqn);
      27             : bool is_well_typed(const pbes_equation& eqn);
      28             : bool has_propositional_variables(const pbes_expression& x);
      29             : 
      30             : /// \brief pbes equation.
      31             : class pbes_equation
      32             : {
      33             :   protected:
      34             :     /// \brief The fixpoint symbol of the equation
      35             :     fixpoint_symbol m_symbol;
      36             : 
      37             :     /// \brief The variable on the left hand side of the equation
      38             :     propositional_variable m_variable;
      39             : 
      40             :     /// \brief The expression on the right hand side of the equation
      41             :     pbes_expression m_formula;
      42             : 
      43             :   public:
      44             :     /// \brief The expression type of the equation.
      45             :     typedef pbes_expression term_type;
      46             : 
      47             :     /// \brief The variable type of the equation.
      48             :     typedef propositional_variable variable_type;
      49             : 
      50             :     /// \brief The symbol type of the equation.
      51             :     typedef fixpoint_symbol symbol_type;
      52             : 
      53             :     /// \brief Constructor.
      54          17 :     pbes_equation() = default;
      55             : 
      56             :     /// \brief Constructor.
      57             :     /// \param symbol A fixpoint symbol
      58             :     /// \param variable A propositional variable declaration
      59             :     /// \param expr A PBES expression
      60        3818 :     pbes_equation(const fixpoint_symbol& symbol, const propositional_variable& variable, const pbes_expression& expr)
      61        3818 :       :
      62        3818 :       m_symbol(symbol),
      63        3818 :       m_variable(variable),
      64        3818 :       m_formula(expr)
      65             :     {
      66        3818 :     }
      67             : 
      68             :     /// \brief Returns the fixpoint symbol of the equation.
      69             :     /// \return The fixpoint symbol of the equation.
      70        6258 :     const fixpoint_symbol& symbol() const
      71             :     {
      72        6258 :       return m_symbol;
      73             :     }
      74             : 
      75             :     /// \brief Returns the fixpoint symbol of the equation.
      76             :     /// \return The fixpoint symbol of the equation.
      77          61 :     fixpoint_symbol& symbol()
      78             :     {
      79          61 :       return m_symbol;
      80             :     }
      81             : 
      82             :     /// \brief Returns the pbes variable of the equation.
      83             :     /// \return The pbes variable of the equation.
      84       25935 :     const propositional_variable& variable() const
      85             :     {
      86       25935 :       return m_variable;
      87             :     }
      88             : 
      89             :     /// \brief Returns the pbes variable of the equation.
      90             :     /// \return The pbes variable of the equation.
      91       12549 :     propositional_variable& variable()
      92             :     {
      93       12549 :       return m_variable;
      94             :     }
      95             : 
      96             :     /// \brief Returns the predicate formula on the right hand side of the equation.
      97             :     /// \return The predicate formula on the right hand side of the equation.
      98       14554 :     const pbes_expression& formula() const
      99             :     {
     100       14554 :       return m_formula;
     101             :     }
     102             : 
     103             :     /// \brief Returns the predicate formula on the right hand side of the equation.
     104             :     /// \return The predicate formula on the right hand side of the equation.
     105       21543 :     pbes_expression& formula()
     106             :     {
     107       21543 :       return m_formula;
     108             :     }
     109             : 
     110             :     /// \brief Returns true if the predicate formula on the right hand side contains no predicate variables.
     111             :     // (Comment Wieger: is_const would be a better name)
     112             :     /// \return True if the predicate formula on the right hand side contains no predicate variables.
     113             :     bool is_solved() const;
     114             : 
     115             :     /// \brief Swaps the contents
     116             :     void swap(pbes_equation& other)
     117             :     {
     118             :       using std::swap;
     119             :       swap(m_symbol, other.m_symbol);
     120             :       swap(m_variable, other.m_variable);
     121             :       swap(m_formula, other.m_formula);
     122             :     }
     123             : 
     124             :     /// \brief A comparison operator on pbes equations.
     125             :     /// \detail The comparison is on the addresses of aterm objects and can therefore differ in every run.
     126             :     /// \parameter other The variable to compare with. 
     127             :     /// \return True if the this argument is smaller than other.
     128         652 :     bool operator<(const pbes_equation& other) const
     129             :     {
     130        1172 :       return (m_formula < other.m_formula) ||
     131         520 :              ((m_formula == other.m_formula &&
     132           0 :                  (m_variable < other.m_variable ||
     133           0 :                  (m_variable == other.m_variable &&
     134         652 :                    m_symbol < other.m_symbol))));
     135             :     }
     136             : };
     137             : 
     138             : //--- start generated class pbes_equation ---//
     139             : /// \\brief list of pbes_equations
     140             : typedef atermpp::term_list<pbes_equation> pbes_equation_list;
     141             : 
     142             : /// \\brief vector of pbes_equations
     143             : typedef std::vector<pbes_equation>    pbes_equation_vector;
     144             : 
     145             : // prototype declaration
     146             : std::string pp(const pbes_equation& x);
     147             : 
     148             : /// \\brief Outputs the object to a stream
     149             : /// \\param out An output stream
     150             : /// \\param x Object x
     151             : /// \\return The output stream
     152             : inline
     153           0 : std::ostream& operator<<(std::ostream& out, const pbes_equation& x)
     154             : {
     155           0 :   return out << pbes_system::pp(x);
     156             : }
     157             : 
     158             : /// \\brief swap overload
     159             : inline void swap(pbes_equation& t1, pbes_equation& t2)
     160             : {
     161             :   t1.swap(t2);
     162             : }
     163             : //--- end generated class pbes_equation ---//
     164             : 
     165             : inline bool
     166             : operator==(const pbes_equation& x, const pbes_equation& y)
     167             : {
     168             :   return x.symbol() == y.symbol() &&
     169             :          x.variable() == y.variable() &&
     170             :          x.formula() == y.formula();
     171             : }
     172             : 
     173             : inline bool
     174             : operator!=(const pbes_equation& x, const pbes_equation& y)
     175             : {
     176             :   return !(x == y);
     177             : }
     178             : 
     179             : /// \brief Conversion to atermaPpl.
     180             : /// \return The specification converted to aterm format.
     181             : inline
     182         707 : atermpp::aterm_appl pbes_equation_to_aterm(const pbes_equation& eqn)
     183             : {
     184         707 :   return atermpp::aterm_appl(core::detail::function_symbol_PBEqn(), eqn.symbol(), eqn.variable(), eqn.formula());
     185             : }
     186             : 
     187             : // template function overloads
     188             : std::string pp(const pbes_equation_vector& x);
     189             : void normalize_sorts(pbes_equation_vector& x, const data::sort_specification& sortspec);
     190             : std::set<data::variable> find_free_variables(const pbes_system::pbes_equation& x);
     191             : 
     192             : } // namespace pbes_system
     193             : 
     194             : } // namespace mcrl2
     195             : 
     196             : #endif // MCRL2_PBES_PBES_EQUATION_H