LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - print.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 133 135 98.5 %
Date: 2020-02-19 00:44:21 Functions: 55 91 60.4 %
Legend: Lines: hit not hit

          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         320 : constexpr inline int precedence(const forall&) { return 21; }
      23         157 : constexpr inline int precedence(const exists&) { return 21; }
      24           5 : constexpr inline int precedence(const imp&)    { return 22; }
      25        4445 : constexpr inline int precedence(const or_&)    { return 23; }
      26        2423 : constexpr inline int precedence(const and_&)   { return 24; }
      27          38 : constexpr inline int precedence(const not_&)   { return 25; }
      28       16104 : inline int precedence(const pbes_expression& x)
      29             : {
      30       16104 :   if      (is_forall(x)) { return precedence(atermpp::down_cast<forall>(x)); }
      31       15784 :   else if (is_exists(x)) { return precedence(atermpp::down_cast<exists>(x)); }
      32       15627 :   else if (is_imp(x))    { return precedence(atermpp::down_cast<imp>(x)); }
      33       15622 :   else if (is_or(x))     { return precedence(atermpp::down_cast<or_>(x)); }
      34       11177 :   else if (is_and(x))    { return precedence(atermpp::down_cast<and_>(x)); }
      35        8754 :   else if (is_not(x))    { return precedence(atermpp::down_cast<not_>(x)); }
      36        8716 :   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         953 : 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         840 : inline bool is_right_associative(const or_&)  { return true; }
      53        1252 : 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       15974 :   void print_pbes_expression(const T& x, bool needs_parentheses = false)
      81             :   {
      82       15974 :     bool is_data_expr = is_data(x);
      83       15974 :     if (is_data_expr)
      84             :     {
      85        4789 :       derived().print("val");
      86             :     }
      87       15974 :     if (needs_parentheses || is_data_expr)
      88             :     {
      89        8357 :       derived().print("(");
      90             :     }
      91       15974 :     derived().apply(x);
      92       15974 :     if (needs_parentheses || is_data_expr)
      93             :     {
      94        8357 :       derived().print(")");
      95             :     }
      96       15974 :   }
      97             : 
      98         321 :   void print_pbes_unary_operand(const pbes_expression& x, const pbes_expression& operand)
      99             :   {
     100         321 :     print_pbes_expression(operand, precedence(operand) < precedence(x));
     101         321 :   }
     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        7731 :   void print_pbes_binary_operation(const T& x, const std::string& op)
     116             :   {
     117        7731 :     const auto& x1 = x.left();
     118        7731 :     const auto& x2 = x.right();
     119        7731 :     auto p = precedence(x);
     120        7731 :     auto p1 = precedence(x1);
     121        7731 :     auto p2 = precedence(x2);
     122        7731 :     print_pbes_expression(x1, (p1 < p) || (p1 == p && !is_left_associative(x)));
     123        7731 :     derived().print(op);
     124        7731 :     print_pbes_expression(x2, (p2 < p) || (p2 == p && !is_right_associative(x)));
     125        7731 :   }
     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         299 :   void print_pbes_abstraction(const Abstraction& x, const std::string& op)
     131             :   {
     132         299 :     derived().enter(x);
     133         299 :     derived().print(op + " ");
     134         299 :     print_variables(x.variables(), true, true, false, "", "", ", ");
     135         299 :     derived().print(". ");
     136         299 :     print_pbes_unary_operand(x, x.body());
     137         299 :     derived().leave(x);
     138         299 :   }
     139             : 
     140         438 :   void apply(const pbes_system::propositional_variable& x)
     141             :   {
     142         438 :     derived().enter(x);
     143         438 :     derived().apply(x.name());
     144         438 :     print_variables(x.parameters());
     145         438 :     derived().leave(x);
     146         438 :   }
     147             : 
     148         449 :   void apply(const pbes_system::fixpoint_symbol& x)
     149             :   {
     150         449 :     derived().enter(x);
     151         449 :     derived().print(x.is_mu() ? "mu" : "nu");
     152         449 :     derived().leave(x);
     153         449 :   }
     154             : 
     155         361 :   void apply(const pbes_system::pbes_equation& x)
     156             :   {
     157         361 :     derived().enter(x);
     158         361 :     derived().apply(x.symbol());
     159         361 :     derived().print(" ");
     160         361 :     derived().apply(x.variable());
     161             :     // TODO: change the weird convention of putting the rhs of an equation on a new line
     162         361 :     derived().print(" =\n       ");
     163         361 :     bool print_val = data::is_data_expression(x.formula());
     164         361 :     if (print_val)
     165             :     {
     166          76 :       derived().print("val(");
     167             :     }
     168         361 :     derived().apply(x.formula());
     169         361 :     if (print_val)
     170             :     {
     171          76 :       derived().print(")");
     172             :     }
     173         361 :     derived().print(";");
     174         361 :     derived().leave(x);
     175         361 :   }
     176             : 
     177         191 :   void apply(const pbes_system::pbes& x)
     178             :   {
     179         191 :     derived().enter(x);
     180         191 :     derived().apply(x.data());
     181         191 :     print_variables(x.global_variables(), true, true, true, "glob ", ";\n\n", ";\n     ");
     182         191 :     print_list(x.equations(), "pbes ", "\n\n", "\n     ");
     183         191 :     derived().print("init ");
     184         191 :     print_pbes_expression(x.initial_state());
     185         191 :     derived().print(";\n");
     186         191 :     derived().leave(x);
     187         191 :   }
     188             : 
     189        9818 :   void apply(const pbes_system::propositional_variable_instantiation& x)
     190             :   {
     191        9818 :     derived().enter(x);
     192        9818 :     derived().apply(x.name());
     193        9818 :     print_list(x.parameters(), "(", ")", ", ", false);
     194        9818 :     derived().leave(x);
     195        9818 :   }
     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        3198 :   void apply(const pbes_system::and_& x)
     205             :   {
     206        3198 :     derived().enter(x);
     207        3198 :     print_pbes_binary_operation(x, " && ");
     208        3198 :     derived().leave(x);
     209        3198 :   }
     210             : 
     211        4514 :   void apply(const pbes_system::or_& x)
     212             :   {
     213        4514 :     derived().enter(x);
     214        4514 :     print_pbes_binary_operation(x, " || ");
     215        4514 :     derived().leave(x);
     216        4514 :   }
     217             : 
     218          19 :   void apply(const pbes_system::imp& x)
     219             :   {
     220          19 :     derived().enter(x);
     221          19 :     print_pbes_binary_operation(x, " => ");
     222          19 :     derived().leave(x);
     223          19 :   }
     224             : 
     225         206 :   void apply(const pbes_system::forall& x)
     226             :   {
     227         206 :     derived().enter(x);
     228         206 :     print_pbes_abstraction(x, "forall");
     229         206 :     derived().leave(x);
     230         206 :   }
     231             : 
     232          93 :   void apply(const pbes_system::exists& x)
     233             :   {
     234          93 :     derived().enter(x);
     235          93 :     print_pbes_abstraction(x, "exists");
     236          93 :     derived().leave(x);
     237          93 :   }
     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        6962 :   void operator()(const T& x, std::ostream& out)
     247             :   {
     248        6962 :     core::detail::apply_printer<pbes_system::detail::printer> printer(out);
     249        6962 :     printer.apply(x);
     250        6962 :   }
     251             : };
     252             : 
     253             : /// \brief Returns a string representation of the object x.
     254             : template <typename T>
     255        6962 : std::string pp(const T& x)
     256             : {
     257       13924 :   std::ostringstream out;
     258        6962 :   stream_printer()(x, out);
     259       13924 :   return out.str();
     260             : }
     261             : 
     262             : } // namespace pbes_system
     263             : 
     264             : } // namespace mcrl2
     265             : 
     266             : #endif // MCRL2_PBES_PRINT_H

Generated by: LCOV version 1.13