Line data    Source code

       1             : // Author(s): Wieger Wesselink, Thomas Neele
       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/detail/pbes2data_rewriter.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_REWRITERS_PBES2DATA_REWRITER_H
      13             : #define MCRL2_PBES_REWRITERS_PBES2DATA_REWRITER_H
      14             : 
      15             : #include "mcrl2/data/consistency.h"
      16             : #include "mcrl2/pbes/builder.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : namespace detail {
      23             : 
      24             : // transforms outer level data operators to their pbes equivalents, for the following operators:
      25             : // !x
      26             : // x && y
      27             : // x || y
      28             : // x => y
      29             : // exists d:D. x
      30             : // forall d:D. x
      31             : template <typename Derived>
      32             : struct pbes2data_builder: public pbes_expression_builder<Derived>
      33             : {
      34             :   typedef pbes_expression_builder<Derived> super;
      35             :   using super::apply;
      36             : 
      37           0 :   data::data_expression pbes2data(const pbes_expression& x) const
      38             :   {
      39           0 :     if (is_not(x))
      40             :     {
      41           0 :       return data::not_(pbes2data(accessors::arg(x)));
      42             :     }
      43           0 :     else if (is_and(x))
      44             :     {
      45           0 :       return data::and_(pbes2data(accessors::left(x)), pbes2data(accessors::right(x)));
      46             :     }
      47           0 :     else if (is_or(x))
      48             :     {
      49           0 :       return data::or_(pbes2data(accessors::left(x)), pbes2data(accessors::right(x)));
      50             :     }
      51           0 :     else if (is_imp(x))
      52             :     {
      53           0 :       return data::imp(pbes2data(accessors::left(x)), pbes2data(accessors::right(x)));
      54             :     }
      55           0 :     else if (is_forall(x))
      56             :     {
      57           0 :       forall y(x);
      58           0 :       return data::forall(y.variables(), pbes2data(y.body()));
      59           0 :     }
      60           0 :     else if (is_exists(x))
      61             :     {
      62           0 :       exists y(x);
      63           0 :       return data::exists(y.variables(), pbes2data(y.body()));
      64           0 :     }
      65           0 :     else if(data::is_data_expression(x))
      66             :     {
      67           0 :       return atermpp::down_cast<data::data_expression>(x);
      68             :     }
      69             :     else
      70             :     {
      71           0 :       throw mcrl2::runtime_error("PBES expression " + pp(x) + " cannot be rewritten to a data expression.");
      72             :     }
      73             :   }
      74             : 
      75             :   template <class T>
      76           0 :   void apply(T& result, const pbes_expression& x)
      77             :   {
      78           0 :     result = pbes2data(x);
      79           0 :   }
      80             : };
      81             : 
      82             : template <typename T>
      83           0 : T pbes2data(const T& x,
      84             :             typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
      85             :            )
      86             : {
      87           0 :   T result;
      88           0 :   core::make_apply_builder<pbes2data_builder>().apply(result, x);
      89           0 :   return result;
      90           0 : }
      91             : 
      92             : template <typename T>
      93             : void pbes2data(T& x,
      94             :                typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
      95             :               )
      96             : {
      97             :   core::make_apply_builder<pbes2data_builder>().update(x);
      98             : }
      99             : 
     100             : } // namespace detail
     101             : 
     102             : class pbes2data_rewriter
     103             : {
     104             :   public:
     105             :     /// \brief The term type
     106             :     typedef pbes_expression term_type;
     107             : 
     108             :     /// \brief The variable type
     109             :     typedef data::variable variable_type;
     110             : 
     111             :     /// \brief Rewrites a pbes expression.
     112             :     /// \param x A term
     113             :     /// \return The rewrite result.
     114             :     pbes_expression operator()(const pbes_expression& x) const
     115             :     {
     116             :       return detail::pbes2data(x);
     117             :     }
     118             : };
     119             : 
     120             : } // namespace pbes_system
     121             : 
     122             : } // namespace mcrl2
     123             : 
     124             : #endif // MCRL2_PBES_REWRITERS_PBES2DATA_REWRITER_H