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/print.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_PRINT_H
      13             : #define MCRL2_PBES_PRINT_H
      14             : 
      15             : #include "mcrl2/data/print.h"
      16             : #include "mcrl2/pbes/traverser.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22         335 : constexpr inline int precedence(const forall&) { return 21; }
      23         164 : constexpr inline int precedence(const exists&) { return 21; }
      24          23 : constexpr inline int precedence(const imp&)    { return 22; }
      25        8976 : constexpr inline int precedence(const or_&)    { return 23; }
      26        5659 : constexpr inline int precedence(const and_&)   { return 24; }
      27          38 : constexpr inline int precedence(const not_&)   { return 25; }
      28       16206 : inline int precedence(const pbes_expression& x)
      29             : {
      30       16206 :   if      (is_forall(x)) { return precedence(atermpp::down_cast<forall>(x)); }
      31       15871 :   else if (is_exists(x)) { return precedence(atermpp::down_cast<exists>(x)); }
      32       15707 :   else if (is_imp(x))    { return precedence(atermpp::down_cast<imp>(x)); }
      33       15702 :   else if (is_or(x))     { return precedence(atermpp::down_cast<or_>(x)); }
      34       11254 :   else if (is_and(x))    { return precedence(atermpp::down_cast<and_>(x)); }
      35        8819 :   else if (is_not(x))    { return precedence(atermpp::down_cast<not_>(x)); }
      36        8781 :   return core::detail::max_precedence;
      37             : }
      38             : 
      39             : // only defined for binary operators
      40           0 : inline bool is_left_associative(const imp&)  { return false; }
      41          81 : inline bool is_left_associative(const or_&)  { return true; }
      42         954 : inline bool is_left_associative(const and_&) { return true; }
      43             : inline bool is_left_associative(const pbes_expression& x)
      44             : {
      45             :   if (is_imp(x))      { return is_left_associative(atermpp::down_cast<imp>(x)); }
      46             :   else if (is_or(x))  { return is_left_associative(atermpp::down_cast<or_>(x)); }
      47             :   else if (is_and(x)) { return is_left_associative(atermpp::down_cast<and_>(x)); }
      48             :   return false;
      49             : }
      50             : 
      51           0 : inline bool is_right_associative(const imp&)  { return true; }
      52         841 : inline bool is_right_associative(const or_&)  { return true; }
      53        1258 : inline bool is_right_associative(const and_&) { return true; }
      54             : inline bool is_right_associative(const pbes_expression& x)
      55             : {
      56             :   if (is_imp(x))      { return is_right_associative(atermpp::down_cast<imp>(x)); }
      57             :   else if (is_or(x))  { return is_right_associative(atermpp::down_cast<or_>(x)); }
      58             :   else if (is_and(x)) { return is_right_associative(atermpp::down_cast<and_>(x)); }
      59             :   return false;
      60             : }
      61             : 
      62             : namespace detail {
      63             : 
      64             : template <typename Derived>
      65             : struct printer: public pbes_system::add_traverser_sort_expressions<data::detail::printer, Derived>
      66             : {
      67             :   typedef pbes_system::add_traverser_sort_expressions<data::detail::printer, Derived> super;
      68             : 
      69             :   using super::enter;
      70             :   using super::leave;
      71             :   using super::apply;
      72             :   using super::derived;
      73             :   using super::print_abstraction;
      74             :   using super::print_list;
      75             :   using super::print_variables;
      76             : 
      77             :   // N.B. We need a special version due to the "val" operator that needs to be
      78             :   // put around data expressions.
      79             :   template <typename T>
      80       16079 :   void print_pbes_expression(const T& x, bool needs_parentheses = false)
      81             :   {
      82       16079 :     bool is_data_expr = is_data(x);
      83       16079 :     if (is_data_expr)
      84             :     {
      85        4807 :       derived().print("val");
      86             :     }
      87       16079 :     if (needs_parentheses || is_data_expr)
      88             :     {
      89        8387 :       derived().print("(");
      90             :     }
      91       16079 :     derived().apply(x);
      92       16079 :     if (needs_parentheses || is_data_expr)
      93             :     {
      94        8387 :       derived().print(")");
      95             :     }
      96       16079 :   }
      97             : 
      98         333 :   void print_pbes_unary_operand(const pbes_expression& x, const pbes_expression& operand)
      99             :   {
     100         333 :     print_pbes_expression(operand, precedence(operand) < precedence(x));
     101         333 :   }
     102             : 
     103             :   // N.B. We need a special version due to the "val" operator that needs to be
     104             :   // put around data expressions.
     105             :   template <typename T>
     106          22 :   void print_pbes_unary_left_operation(const T& x, const std::string& op)
     107             :   {
     108          22 :     derived().print(op);
     109          22 :     print_pbes_unary_operand(x, x.operand());
     110          22 :   }
     111             : 
     112             :   // N.B. We need a special version due to the "val" operator that needs to be
     113             :   // put around data expressions.
     114             :   template <typename T>
     115        7770 :   void print_pbes_binary_operation(const T& x, const std::string& op)
     116             :   {
     117        7770 :     const auto& x1 = x.left();
     118        7770 :     const auto& x2 = x.right();
     119        7770 :     auto p = precedence(x);
     120        7770 :     auto p1 = precedence(x1);
     121        7770 :     auto p2 = precedence(x2);
     122        7770 :     print_pbes_expression(x1, (p1 < p) || (p1 == p && !is_left_associative(x)));
     123        7770 :     derived().print(op);
     124        7770 :     print_pbes_expression(x2, (p2 < p) || (p2 == p && !is_right_associative(x)));
     125        7770 :   }
     126             : 
     127             :   // N.B. We need a special version due to the "val" operator that needs to be
     128             :   // put around data expressions.
     129             :   template <typename Abstraction>
     130         311 :   void print_pbes_abstraction(const Abstraction& x, const std::string& op)
     131             :   {
     132         311 :     derived().enter(x);
     133         311 :     derived().print(op + " ");
     134         311 :     print_variables(x.variables(), true, true, false, "", "", ", ");
     135         311 :     derived().print(". ");
     136         311 :     print_pbes_unary_operand(x, x.body());
     137         311 :     derived().leave(x);
     138         311 :   }
     139             : 
     140         472 :   void apply(const pbes_system::propositional_variable& x)
     141             :   {
     142         472 :     derived().enter(x);
     143         472 :     derived().apply(x.name());
     144         472 :     print_variables(x.parameters());
     145         472 :     derived().leave(x);
     146         472 :   }
     147             : 
     148         483 :   void apply(const pbes_system::fixpoint_symbol& x)
     149             :   {
     150         483 :     derived().enter(x);
     151         483 :     derived().print(x.is_mu() ? "mu" : "nu");
     152         483 :     derived().leave(x);
     153         483 :   }
     154             : 
     155         395 :   void apply(const pbes_system::pbes_equation& x)
     156             :   {
     157         395 :     derived().enter(x);
     158         395 :     derived().apply(x.symbol());
     159         395 :     derived().print(" ");
     160         395 :     derived().apply(x.variable());
     161             :     // TODO: change the weird convention of putting the rhs of an equation on a new line
     162         395 :     derived().print(" =\n       ");
     163         395 :     bool print_val = data::is_data_expression(x.formula());
     164         395 :     if (print_val)
     165             :     {
     166          75 :       derived().print("val(");
     167             :     }
     168         395 :     derived().apply(x.formula());
     169         395 :     if (print_val)
     170             :     {
     171          75 :       derived().print(")");
     172             :     }
     173         395 :     derived().print(";");
     174         395 :     derived().leave(x);
     175         395 :   }
     176             : 
     177         206 :   void apply(const pbes_system::pbes& x)
     178             :   {
     179         206 :     derived().enter(x);
     180         206 :     derived().apply(x.data());
     181         206 :     print_variables(x.global_variables(), true, true, true, "glob ", ";\n\n", ";\n     ");
     182         206 :     print_list(x.equations(), "pbes ", "\n\n", "\n     ");
     183         206 :     derived().print("init ");
     184         206 :     print_pbes_expression(x.initial_state());
     185         206 :     derived().print(";\n");
     186         206 :     derived().leave(x);
     187         206 :   }
     188             : 
     189        9896 :   void apply(const pbes_system::propositional_variable_instantiation& x)
     190             :   {
     191        9896 :     derived().enter(x);
     192        9896 :     derived().apply(x.name());
     193        9896 :     print_list(x.parameters(), "(", ")", ", ", false);
     194        9896 :     derived().leave(x);
     195        9896 :   }
     196             : 
     197          22 :   void apply(const pbes_system::not_& x)
     198             :   {
     199          22 :     derived().enter(x);
     200          22 :     print_pbes_unary_left_operation(x, "!");
     201          22 :     derived().leave(x);
     202          22 :   }
     203             : 
     204        3224 :   void apply(const pbes_system::and_& x)
     205             :   {
     206        3224 :     derived().enter(x);
     207        3224 :     print_pbes_binary_operation(x, " && ");
     208        3224 :     derived().leave(x);
     209        3224 :   }
     210             : 
     211        4528 :   void apply(const pbes_system::or_& x)
     212             :   {
     213        4528 :     derived().enter(x);
     214        4528 :     print_pbes_binary_operation(x, " || ");
     215        4528 :     derived().leave(x);
     216        4528 :   }
     217             : 
     218          18 :   void apply(const pbes_system::imp& x)
     219             :   {
     220          18 :     derived().enter(x);
     221          18 :     print_pbes_binary_operation(x, " => ");
     222          18 :     derived().leave(x);
     223          18 :   }
     224             : 
     225         214 :   void apply(const pbes_system::forall& x)
     226             :   {
     227         214 :     derived().enter(x);
     228         214 :     print_pbes_abstraction(x, "forall");
     229         214 :     derived().leave(x);
     230         214 :   }
     231             : 
     232          97 :   void apply(const pbes_system::exists& x)
     233             :   {
     234          97 :     derived().enter(x);
     235          97 :     print_pbes_abstraction(x, "exists");
     236          97 :     derived().leave(x);
     237          97 :   }
     238             : };
     239             : 
     240             : } // namespace detail
     241             : 
     242             : /// \brief Prints the object x to a stream.
     243             : struct stream_printer
     244             : {
     245             :   template <typename T>
     246        6990 :   void operator()(const T& x, std::ostream& out)
     247             :   {
     248        6990 :     core::detail::apply_printer<pbes_system::detail::printer> printer(out);
     249        6990 :     printer.apply(x);
     250        6990 :   }
     251             : };
     252             : 
     253             : /// \brief Returns a string representation of the object x.
     254             : template <typename T>
     255        6990 : std::string pp(const T& x)
     256             : {
     257        6990 :   std::ostringstream out;
     258        6990 :   stream_printer()(x, out);
     259       13980 :   return out.str();
     260        6990 : }
     261             : 
     262             : } // namespace pbes_system
     263             : 
     264             : } // namespace mcrl2
     265             : 
     266             : #endif // MCRL2_PBES_PRINT_H