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/detail/pfnf_print.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_PFNF_PRINT_H
      13             : #define MCRL2_PBES_DETAIL_PFNF_PRINT_H
      14             : 
      15             : #include "mcrl2/pbes/detail/is_pfnf.h"
      16             : #include "mcrl2/pbes/print.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : namespace detail {
      23             : 
      24             : template <typename Derived>
      25             : struct pfnf_printer: public pbes_system::detail::printer<Derived>
      26             : {
      27             :   typedef pbes_system::detail::printer<Derived> super;
      28             : 
      29             :   using super::enter;
      30             :   using super::leave;
      31             :   using super::apply;
      32             :   using super::derived;
      33             :   using super::print_abstraction;
      34             :   using super::print_list;
      35             :   using super::print_variables;
      36             : 
      37          18 :   bool is_abstraction(const pbes_system::pbes_expression& x)
      38             :   {
      39          18 :     return is_forall(x) || is_exists(x);
      40             :   }
      41             : 
      42             :   template <typename Abstraction>
      43           2 :   std::string abstraction_operator(const Abstraction& x) const
      44             :   {
      45           2 :     if (is_forall(x))
      46             :     {
      47           2 :       return "forall";
      48             :     }
      49           0 :     else if (is_exists(x))
      50             :     {
      51           0 :       return "exists";
      52             :     }
      53             :     else
      54             :     {
      55           0 :       throw mcrl2::runtime_error("error: unknown abstraction!");
      56             :     }
      57             :     return "";
      58             :   }
      59             : 
      60             :   template <typename Abstraction>
      61           2 :   pbes_expression abstraction_body(const Abstraction& x) const
      62             :   {
      63           2 :     if (is_forall(x))
      64             :     {
      65           2 :       return forall(x).body();
      66             :     }
      67           0 :     else if (is_exists(x))
      68             :     {
      69           0 :       return exists(x).body();
      70             :     }
      71             :     else
      72             :     {
      73           0 :       throw mcrl2::runtime_error("error: unknown abstraction!");
      74             :     }
      75             :     return pbes_expression();
      76             :   }
      77             : 
      78             :   template <typename Abstraction>
      79           2 :   data::variable_list abstraction_variables(const Abstraction& x) const
      80             :   {
      81           2 :     if (is_forall(x))
      82             :     {
      83           2 :       return forall(x).variables();
      84             :     }
      85           0 :     else if (is_exists(x))
      86             :     {
      87           0 :       return exists(x).variables();
      88             :     }
      89             :     else
      90             :     {
      91           0 :       throw mcrl2::runtime_error("error: unknown abstraction!");
      92             :     }
      93             :     return data::variable_list();
      94             :   }
      95             : 
      96             :   template <typename Abstraction>
      97           2 :   void print_pbes_abstraction(const Abstraction& x)
      98             :   {
      99           2 :     std::string op = abstraction_operator(x);
     100           2 :     derived().enter(x);
     101           2 :     derived().print(op + " ");
     102           2 :     print_variables(abstraction_variables(x), true, true, false, "", "", ", ");
     103           2 :     derived().print(". ");
     104           2 :     pbes_expression body = abstraction_body(x);
     105           2 :     if (is_abstraction(body))
     106             :     {
     107           1 :       print_pbes_abstraction(body);
     108             :     }
     109             :     else
     110             :     {
     111           1 :       std::vector<pbes_expression> implications = pfnf_implications(body);
     112           1 :       print_list(implications, "\n       (\n         ", "\n       )", "\n      && ", false);
     113           1 :     }
     114           2 :     derived().leave(x);
     115           2 :   }
     116             : 
     117          16 :   void apply(const pbes_system::pbes_expression& x)
     118             :   {
     119          16 :     derived().enter(x);
     120          16 :     if (is_abstraction(x))
     121             :     {
     122           1 :       print_pbes_abstraction(x);
     123             :     }
     124             :     else
     125             :     {
     126          15 :       super::apply(x);
     127             :     }
     128          16 :     derived().leave(x);
     129          16 :   }
     130             : };
     131             : 
     132             : } // namespace detail
     133             : 
     134             : /// \brief Prints the object x to a stream.
     135             : struct pfnf_stream_printer
     136             : {
     137             :   template <typename T>
     138           1 :   void operator()(const T& x, std::ostream& out)
     139             :   {
     140           1 :     core::detail::apply_printer<pbes_system::detail::pfnf_printer> printer(out);
     141           1 :     printer.apply(x);
     142           1 :   }
     143             : };
     144             : 
     145             : /// \brief Returns a PFNF string representation of the object x.
     146             : template <typename T>
     147           1 : std::string pfnf_pp(const T& x)
     148             : {
     149           1 :   std::ostringstream out;
     150           1 :   pfnf_stream_printer()(x, out);
     151           2 :   return out.str();
     152           1 : }
     153             : 
     154             : } // namespace pbes_system
     155             : 
     156             : } // namespace mcrl2
     157             : 
     158             : #endif // MCRL2_PBES_DETAIL_PFNF_PRINT_H