LCOV - code coverage report
Current view: top level - modal_formula/include/mcrl2/modal_formula - print.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 228 375 60.8 %
Date: 2024-03-08 02:52:28 Functions: 46 201 22.9 %
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/modal_formula/print.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_PRINT_H
      13             : #define MCRL2_MODAL_FORMULA_PRINT_H
      14             : 
      15             : #include "mcrl2/lps/print.h"
      16             : #include "mcrl2/modal_formula/traverser.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace action_formulas {
      21             : 
      22           0 : constexpr inline int precedence(const forall&) { return 21; }
      23           0 : constexpr inline int precedence(const exists&) { return 21; }
      24           0 : constexpr inline int precedence(const imp&)    { return 22; }
      25           0 : constexpr inline int precedence(const or_&)    { return 23; }
      26           1 : constexpr inline int precedence(const and_&)   { return 24; }
      27           0 : constexpr inline int precedence(const at&)     { return 25; }
      28           7 : constexpr inline int precedence(const not_&)   { return 26; }
      29           7 : inline int precedence(const action_formula& x)
      30             : {
      31           7 :   if (is_forall(x))      { return precedence(atermpp::down_cast<forall>(x)); }
      32           7 :   else if (is_exists(x)) { return precedence(atermpp::down_cast<exists>(x)); }
      33           7 :   else if (is_imp(x))    { return precedence(atermpp::down_cast<imp>(x)); }
      34           7 :   else if (is_or(x))     { return precedence(atermpp::down_cast<or_>(x)); }
      35           7 :   else if (is_and(x))    { return precedence(atermpp::down_cast<and_>(x)); }
      36           7 :   else if (is_at(x))     { return precedence(atermpp::down_cast<at>(x)); }
      37           7 :   else if (is_not(x))    { return precedence(atermpp::down_cast<not_>(x)); }
      38           5 :   return core::detail::max_precedence;
      39             : }
      40             : 
      41             : // only defined for binary operators
      42           0 : inline bool is_left_associative(const imp&)  { return false; }
      43           0 : inline bool is_left_associative(const or_&)  { return true; }
      44           0 : inline bool is_left_associative(const and_&) { return true; }
      45             : inline bool is_left_associative(const action_formula& x)
      46             : {
      47             :   if (is_imp(x))      { return is_left_associative(atermpp::down_cast<imp>(x)); }
      48             :   else if (is_or(x))  { return is_left_associative(atermpp::down_cast<or_>(x)); }
      49             :   else if (is_and(x)) { return is_left_associative(atermpp::down_cast<and_>(x)); }
      50             :   return false;
      51             : }
      52             : 
      53           0 : inline bool is_right_associative(const imp&)  { return true; }
      54           0 : inline bool is_right_associative(const or_&)  { return true; }
      55           0 : inline bool is_right_associative(const and_&) { return true; }
      56             : inline bool is_right_associative(const action_formula& x)
      57             : {
      58             :   if (is_imp(x))      { return is_right_associative(atermpp::down_cast<imp>(x)); }
      59             :   else if (is_or(x))  { return is_right_associative(atermpp::down_cast<or_>(x)); }
      60             :   else if (is_and(x)) { return is_right_associative(atermpp::down_cast<and_>(x)); }
      61             :   return false;
      62             : }
      63             : 
      64             : namespace detail
      65             : {
      66             : 
      67             : template <typename Derived>
      68             : struct printer: public action_formulas::add_traverser_sort_expressions<lps::detail::printer, Derived>
      69             : {
      70             :   typedef action_formulas::add_traverser_sort_expressions<lps::detail::printer, Derived> super;
      71             : 
      72             :   using super::enter;
      73             :   using super::leave;
      74             :   using super::apply;
      75             :   using super::derived;
      76             :   using super::print_abstraction;
      77             :   using super::print_list;
      78             :   using super::print_action_declarations;
      79             :   using super::print_expression;
      80             :   using super::print_unary_left_operation;
      81             :   using super::print_binary_operation;
      82             : 
      83          14 :   void apply(const action_formulas::true_& x)
      84             :   {
      85          14 :     derived().enter(x);
      86          14 :     derived().print("true");
      87          14 :     derived().leave(x);
      88          14 :   }
      89             : 
      90           0 :   void apply(const action_formulas::false_& x)
      91             :   {
      92           0 :     derived().enter(x);
      93           0 :     derived().print("false");
      94           0 :     derived().leave(x);
      95           0 :   }
      96             : 
      97           5 :   void apply(const action_formulas::not_& x)
      98             :   {
      99           5 :     derived().enter(x);
     100           5 :     print_unary_left_operation(x, "!");
     101           5 :     derived().leave(x);
     102           5 :   }
     103             : 
     104           1 :   void apply(const action_formulas::and_& x)
     105             :   {
     106           1 :     derived().enter(x);
     107           1 :     print_binary_operation(x, " && ");
     108           1 :     derived().leave(x);
     109           1 :   }
     110             : 
     111           0 :   void apply(const action_formulas::or_& x)
     112             :   {
     113           0 :     derived().enter(x);
     114           0 :     print_binary_operation(x, " || ");
     115           0 :     derived().leave(x);
     116           0 :   }
     117             : 
     118           0 :   void apply(const action_formulas::imp& x)
     119             :   {
     120           0 :     derived().enter(x);
     121           0 :     print_binary_operation(x, " => ");
     122           0 :     derived().leave(x);
     123           0 :   }
     124             : 
     125           0 :   void apply(const action_formulas::forall& x)
     126             :   {
     127           0 :     derived().enter(x);
     128           0 :     print_abstraction(x, "forall");
     129           0 :     derived().leave(x);
     130           0 :   }
     131             : 
     132           0 :   void apply(const action_formulas::exists& x)
     133             :   {
     134           0 :     derived().enter(x);
     135           0 :     print_abstraction(x, "exists");
     136           0 :     derived().leave(x);
     137           0 :   }
     138             : 
     139           0 :   void apply(const action_formulas::at& x)
     140             :   {
     141           0 :     derived().enter(x);
     142           0 :     derived().apply(x.operand());
     143           0 :     derived().print(" @ ");
     144           0 :     print_expression(x.time_stamp(), precedence(x.time_stamp()) < core::detail::max_precedence);
     145           0 :     derived().leave(x);
     146           0 :   }
     147             : 
     148          52 :   void apply(const action_formulas::multi_action& x)
     149             :   {
     150          52 :     derived().enter(x);
     151          52 :     if (x.actions().empty())
     152             :     {
     153           0 :       derived().print("tau");
     154             :     }
     155             :     else
     156             :     {
     157          52 :       print_list(x.actions(), "", "", "|");
     158             :     }
     159          52 :     derived().leave(x);
     160          52 :   }
     161             : };
     162             : 
     163             : } // namespace detail
     164             : 
     165             : /// \brief Prints the object t to a stream.
     166             : template <typename T>
     167           0 : void pp(const T& t, std::ostream& out)
     168             : {
     169           0 :   core::detail::apply_printer<action_formulas::detail::printer> printer(out);
     170           0 :   printer.apply(t);
     171           0 : }
     172             : 
     173             : /// \brief Returns a string representation of the object t.
     174             : template <typename T>
     175           0 : std::string pp(const T& t)
     176             : {
     177           0 :   std::ostringstream out;
     178           0 :   action_formulas::pp(t, out);
     179           0 :   return out.str();
     180           0 : }
     181             : 
     182             : } // namespace action_formulas
     183             : 
     184             : namespace regular_formulas {
     185             : 
     186           0 : constexpr inline int precedence(const seq&)          { return 31; }
     187           0 : constexpr inline int precedence(const alt&)          { return 32; }
     188           0 : constexpr inline int precedence(const trans&)        { return 33; }
     189           3 : constexpr inline int precedence(const trans_or_nil&) { return 33; }
     190           3 : inline int precedence(const regular_formula& x)
     191             : {
     192           3 :   if (is_seq(x))               { return precedence(atermpp::down_cast<seq>(x)); }
     193           3 :   else if (is_alt(x))          { return precedence(atermpp::down_cast<alt>(x)); }
     194           3 :   else if (is_trans(x))        { return precedence(atermpp::down_cast<trans>(x)); }
     195           3 :   else if (is_trans_or_nil(x)) { return precedence(atermpp::down_cast<trans_or_nil>(x)); }
     196           3 :   return core::detail::max_precedence;
     197             : }
     198             : 
     199             : // only defined for binary operators
     200           0 : inline bool is_left_associative(const seq&)  { return false; }
     201           0 : inline bool is_left_associative(const alt&)  { return true; }
     202             : inline bool is_left_associative(const regular_formula& x)
     203             : {
     204             :   if (is_seq(x))      { return is_left_associative(atermpp::down_cast<seq>(x)); }
     205             :   else if (is_alt(x)) { return is_left_associative(atermpp::down_cast<alt>(x)); }
     206             :   return false;
     207             : }
     208             : 
     209           0 : inline bool is_right_associative(const seq&)  { return true; }
     210           0 : inline bool is_right_associative(const alt&)  { return true; }
     211             : inline bool is_right_associative(const regular_formula& x)
     212             : {
     213             :   if (is_seq(x))      { return is_right_associative(atermpp::down_cast<seq>(x)); }
     214             :   else if (is_alt(x)) { return is_right_associative(atermpp::down_cast<alt>(x)); }
     215             :   return false;
     216             : }
     217             : 
     218             : namespace detail
     219             : {
     220             : 
     221             : template <typename Derived>
     222             : struct printer: public regular_formulas::add_traverser_sort_expressions<action_formulas::detail::printer, Derived>
     223             : {
     224             :   typedef regular_formulas::add_traverser_sort_expressions<action_formulas::detail::printer, Derived> super;
     225             : 
     226             :   using super::enter;
     227             :   using super::leave;
     228             :   using super::apply;
     229             :   using super::derived;
     230             :   using super::print_action_declarations;
     231             : 
     232             :   using super::print_expression;
     233             :   using super::print_unary_left_operation;
     234             :   using super::print_unary_right_operation;
     235             :   using super::print_binary_operation;
     236             : 
     237           0 :   void apply(const regular_formulas::seq& x)
     238             :   {
     239           0 :     derived().enter(x);
     240           0 :     print_binary_operation(x, " . ");
     241           0 :     derived().leave(x);
     242           0 :   }
     243             : 
     244           0 :   void apply(const regular_formulas::alt& x)
     245             :   {
     246           0 :     derived().enter(x);
     247           0 :     print_binary_operation(x, " + ");
     248           0 :     derived().leave(x);
     249           0 :   }
     250             : 
     251           0 :   void apply(const regular_formulas::trans& x)
     252             :   {
     253           0 :     derived().enter(x);
     254           0 :     print_unary_right_operation(x, "+");
     255           0 :     derived().leave(x);
     256           0 :   }
     257             : 
     258           3 :   void apply(const regular_formulas::trans_or_nil& x)
     259             :   {
     260           3 :     derived().enter(x);
     261           3 :     print_unary_right_operation(x, "*");
     262           3 :     derived().leave(x);
     263           3 :   }
     264             : 
     265           0 :   void apply(const regular_formulas::untyped_regular_formula& x)
     266             :   {
     267           0 :     derived().enter(x);
     268           0 :     print_expression(x.left(), false);
     269           0 :     derived().print(" " + std::string(x.name()) + " ");
     270           0 :     print_expression(x.right(), false);
     271           0 :     derived().leave(x);
     272           0 :   }
     273             : };
     274             : 
     275             : } // namespace detail
     276             : 
     277             : /// \brief Prints the object t to a stream.
     278             : template <typename T>
     279           0 : void pp(const T& t, std::ostream& out)
     280             : {
     281           0 :   core::detail::apply_printer<regular_formulas::detail::printer> printer(out);
     282           0 :   printer.apply(t);
     283           0 : }
     284             : 
     285             : /// \brief Returns a string representation of the object t.
     286             : template <typename T>
     287           0 : std::string pp(const T& t)
     288             : {
     289           0 :   std::ostringstream out;
     290           0 :   regular_formulas::pp(t, out);
     291           0 :   return out.str();
     292           0 : }
     293             : 
     294             : } // namespace regular_formulas
     295             : 
     296             : namespace state_formulas {
     297             : 
     298          47 : constexpr inline int precedence(const mu&)                 { return 41; }
     299           2 : constexpr inline int precedence(const nu&)                 { return 41; }
     300           3 : constexpr inline int precedence(const forall&)             { return 42; }
     301           0 : constexpr inline int precedence(const exists&)             { return 42; }
     302           0 : constexpr inline int precedence(const infimum&)            { return 42; }
     303           0 : constexpr inline int precedence(const supremum&)           { return 42; }
     304          10 : constexpr inline int precedence(const imp&)                { return 45; }
     305          28 : constexpr inline int precedence(const or_&)                { return 46; }
     306          45 : constexpr inline int precedence(const and_&)               { return 47; }
     307           0 : constexpr inline int precedence(const plus&)               { return 43; }
     308           0 : constexpr inline int precedence(const const_multiply&)     { return 44; }
     309           0 : constexpr inline int precedence(const const_multiply_alt&) { return 44; }
     310          58 : constexpr inline int precedence(const must&)               { return 48; }
     311          40 : constexpr inline int precedence(const may&)                { return 48; }
     312          20 : constexpr inline int precedence(const not_&)               { return 50; }
     313         228 : inline int precedence(const state_formula& x)
     314             : {
     315         228 :   if      (is_mu(x))                 { return precedence(atermpp::down_cast<mu>(x)); }
     316         181 :   else if (is_nu(x))                 { return precedence(atermpp::down_cast<nu>(x)); }
     317         179 :   else if (is_forall(x))             { return precedence(atermpp::down_cast<forall>(x)); }
     318         176 :   else if (is_exists(x))             { return precedence(atermpp::down_cast<exists>(x)); }
     319         176 :   else if (is_infimum(x))            { return precedence(atermpp::down_cast<infimum>(x)); }
     320         176 :   else if (is_supremum(x))           { return precedence(atermpp::down_cast<supremum>(x)); }
     321         176 :   else if (is_imp(x))                { return precedence(atermpp::down_cast<imp>(x)); }
     322         176 :   else if (is_or(x))                 { return precedence(atermpp::down_cast<or_>(x)); }
     323         171 :   else if (is_and(x))                { return precedence(atermpp::down_cast<and_>(x)); }
     324         165 :   else if (is_plus(x))               { return precedence(atermpp::down_cast<plus>(x)); }
     325         165 :   else if (is_const_multiply(x))     { return precedence(atermpp::down_cast<const_multiply>(x)); }
     326         165 :   else if (is_const_multiply_alt(x)) { return precedence(atermpp::down_cast<const_multiply_alt>(x)); }
     327         165 :   else if (is_must(x))               { return precedence(atermpp::down_cast<must>(x)); }
     328         151 :   else if (is_may(x))                { return precedence(atermpp::down_cast<may>(x)); }
     329         135 :   else if (is_not(x))                { return precedence(atermpp::down_cast<not_>(x)); }
     330         131 :   return core::detail::max_precedence;
     331             : }
     332             : 
     333             : // only defined for binary operators
     334           0 : inline bool is_left_associative(const imp&)  { return false; }
     335           0 : inline bool is_left_associative(const or_&)  { return true; }
     336           0 : inline bool is_left_associative(const and_&) { return true; }
     337           0 : inline bool is_left_associative(const plus&) { return true; }
     338           0 : inline bool is_left_associative(const const_multiply&) { return true; }
     339             : inline bool is_left_associative(const const_multiply_alt&) { return true; }
     340             : inline bool is_left_associative(const state_formula& x)
     341             : {
     342             :   if (is_imp(x))      { return is_left_associative(atermpp::down_cast<imp>(x)); }
     343             :   else if (is_or(x))  { return is_left_associative(atermpp::down_cast<or_>(x)); }
     344             :   else if (is_and(x)) { return is_left_associative(atermpp::down_cast<and_>(x)); }
     345             :   else if (is_plus(x)) { return is_left_associative(atermpp::down_cast<plus>(x)); }
     346             :   else if (is_const_multiply(x)) { return is_left_associative(atermpp::down_cast<const_multiply>(x)); }
     347             :   else if (is_const_multiply_alt(x)) { return is_left_associative(atermpp::down_cast<const_multiply_alt>(x)); }
     348             :   return false;
     349             : }
     350             : 
     351           0 : inline bool is_right_associative(const imp&)  { return true; }
     352           0 : inline bool is_right_associative(const or_&)  { return true; }
     353           5 : inline bool is_right_associative(const and_&) { return true; }
     354           0 : inline bool is_right_associative(const plus&) { return true; }
     355           0 : inline bool is_right_associative(const const_multiply&) { return true; }
     356             : inline bool is_right_associative(const const_multiply_alt&) { return true; }
     357             : inline bool is_right_associative(const state_formula& x)
     358             : {
     359             :   if (is_imp(x))      { return is_right_associative(atermpp::down_cast<imp>(x)); }
     360             :   else if (is_or(x))  { return is_right_associative(atermpp::down_cast<or_>(x)); }
     361             :   else if (is_and(x)) { return is_right_associative(atermpp::down_cast<and_>(x)); }
     362             :   else if (is_plus(x)) { return is_right_associative(atermpp::down_cast<plus>(x)); }
     363             :   else if (is_const_multiply(x)) { return is_right_associative(atermpp::down_cast<const_multiply>(x)); }
     364             :   else if (is_const_multiply_alt(x)) { return is_right_associative(atermpp::down_cast<const_multiply_alt>(x)); }
     365             :   return false;
     366             : }
     367             : 
     368             : namespace detail
     369             : {
     370             : 
     371             : template <typename Derived>
     372             : struct printer: public state_formulas::add_traverser_sort_expressions<regular_formulas::detail::printer, Derived>
     373             : {
     374             :   typedef state_formulas::add_traverser_sort_expressions<regular_formulas::detail::printer, Derived> super;
     375             : 
     376             :   using super::enter;
     377             :   using super::leave;
     378             :   using super::apply;
     379             :   using super::derived;
     380             :   using super::print_abstraction;
     381             :   using super::print_variables;
     382             :   using super::print_list;
     383             :   using super::print_action_declarations;
     384             : 
     385             :   using super::print_expression;
     386             :   using super::print_unary_left_operation;
     387             :   using super::print_binary_operation;
     388             :   using super::print_unary_operand;
     389             : 
     390             :   // Determines whether or not data expressions should be wrapped inside 'val'.
     391             :   std::vector<bool> val;
     392             : 
     393         190 :   void disable_val()
     394             :   {
     395         190 :     val.push_back(false);
     396         190 :   }
     397             : 
     398         190 :   void enable_val()
     399             :   {
     400         190 :     assert(!val.empty());
     401         190 :     val.pop_back();
     402         190 :   }
     403             : 
     404         103 :   void apply(const data::data_expression& x)
     405             :   {
     406         103 :     bool print_val = val.empty();
     407         103 :     derived().enter(x);
     408         103 :     if (print_val)
     409             :     {
     410          24 :       disable_val();
     411          24 :       derived().print("val(");
     412             :     }
     413         103 :     super::apply(x);
     414         103 :     if (print_val)
     415             :     {
     416          24 :       derived().print(")");
     417          24 :       enable_val();
     418             :     }
     419         103 :     derived().leave(x);
     420         103 :   }
     421             : 
     422          78 :   void apply(const state_formulas::true_& x)
     423             :   {
     424          78 :     derived().enter(x);
     425          78 :     derived().print("true");
     426          78 :     derived().leave(x);
     427          78 :   }
     428             : 
     429          23 :   void apply(const state_formulas::false_& x)
     430             :   {
     431          23 :     derived().enter(x);
     432          23 :     derived().print("false");
     433          23 :     derived().leave(x);
     434          23 :   }
     435             : 
     436          16 :   void apply(const state_formulas::not_& x)
     437             :   {
     438          16 :     derived().enter(x);
     439          16 :     print_unary_left_operation(x, "!");
     440          16 :     derived().leave(x);
     441          16 :   }
     442             : 
     443           0 :   void apply(const state_formulas::minus& x)
     444             :   {
     445           0 :     derived().enter(x);
     446           0 :     print_unary_left_operation(x, "-");
     447           0 :     derived().leave(x);
     448           0 :   }
     449             : 
     450          39 :   void apply(const state_formulas::and_& x)
     451             :   {
     452          39 :     derived().enter(x);
     453          39 :     print_binary_operation(x, " && ");
     454          39 :     derived().leave(x);
     455          39 :   }
     456             : 
     457          23 :   void apply(const state_formulas::or_& x)
     458             :   {
     459          23 :     derived().enter(x);
     460          23 :     print_binary_operation(x, " || ");
     461          23 :     derived().leave(x);
     462          23 :   }
     463             : 
     464          10 :   void apply(const state_formulas::imp& x)
     465             :   {
     466          10 :     derived().enter(x);
     467          10 :     print_binary_operation(x, " => ");
     468          10 :     derived().leave(x);
     469          10 :   }
     470             : 
     471           0 :   void apply(const state_formulas::plus& x)
     472             :   {
     473           0 :     derived().enter(x);
     474           0 :     print_binary_operation(x, " + ");
     475           0 :     derived().leave(x);
     476           0 :   }
     477             : 
     478           0 :   void apply(const state_formulas::const_multiply& x)
     479             :   {
     480           0 :     derived().enter(x);
     481           0 :     print_binary_operation(x, " * ");
     482           0 :     derived().leave(x);
     483           0 :   }
     484             : 
     485           0 :   void apply(const state_formulas::const_multiply_alt& x)
     486             :   {
     487           0 :     derived().enter(x);
     488           0 :     derived().apply(x.left());
     489           0 :     derived().print("*"); 
     490           0 :     derived().apply(x.right());
     491             :     // print_expression(x.right(), false);
     492           0 :     derived().leave(x);
     493           0 :   }
     494             : 
     495          11 :   void apply(const state_formulas::forall& x)
     496             :   {
     497          11 :     derived().enter(x);
     498          11 :     print_abstraction(x, "forall");
     499          11 :     derived().leave(x);
     500          11 :   }
     501             : 
     502           5 :   void apply(const state_formulas::exists& x)
     503             :   {
     504           5 :     derived().enter(x);
     505           5 :     print_abstraction(x, "exists");
     506           5 :     derived().leave(x);
     507           5 :   }
     508             : 
     509           3 :   void apply(const state_formulas::infimum& x)
     510             :   {
     511           3 :     derived().enter(x);
     512           3 :     print_abstraction(x, "inf");
     513           3 :     derived().leave(x);
     514           3 :   }
     515             : 
     516           3 :   void apply(const state_formulas::supremum& x)
     517             :   {
     518           3 :     derived().enter(x);
     519           3 :     print_abstraction(x, "sup");
     520           3 :     derived().leave(x);
     521           3 :   }
     522             : 
     523          44 :   void apply(const state_formulas::must& x)
     524             :   {
     525          44 :     derived().enter(x);
     526          44 :     derived().print("[");
     527          44 :     disable_val();
     528          44 :     derived().apply(x.formula());
     529          44 :     enable_val();
     530          44 :     derived().print("]");
     531          44 :     print_unary_operand(x, x.operand());
     532          44 :     derived().leave(x);
     533          44 :   }
     534             : 
     535          24 :   void apply(const state_formulas::may& x)
     536             :   {
     537          24 :     derived().enter(x);
     538          24 :     derived().print("<");
     539          24 :     disable_val();
     540          24 :     derived().apply(x.formula());
     541          24 :     enable_val();
     542          24 :     derived().print(">");
     543          24 :     print_unary_operand(x, x.operand());
     544          24 :     derived().leave(x);
     545          24 :   }
     546             : 
     547           0 :   void apply(const state_formulas::yaled& x)
     548             :   {
     549           0 :     derived().enter(x);
     550           0 :     derived().print("yaled");
     551           0 :     derived().leave(x);
     552           0 :   }
     553             : 
     554           0 :   void apply(const state_formulas::yaled_timed& x)
     555             :   {
     556           0 :     disable_val();
     557           0 :     derived().enter(x);
     558           0 :     derived().print("yaled");
     559           0 :     derived().print(" @ ");
     560           0 :     print_expression(x.time_stamp(), precedence(x.time_stamp()) < core::detail::max_precedence);
     561           0 :     derived().leave(x);
     562           0 :     enable_val();
     563           0 :   }
     564             : 
     565           0 :   void apply(const state_formulas::delay& x)
     566             :   {
     567           0 :     derived().enter(x);
     568           0 :     derived().print("delay");
     569           0 :     derived().leave(x);
     570           0 :   }
     571             : 
     572           2 :   void apply(const state_formulas::delay_timed& x)
     573             :   {
     574           2 :     disable_val();
     575           2 :     derived().enter(x);
     576           2 :     derived().print("delay");
     577           2 :     derived().print(" @ ");
     578           2 :     print_expression(x.time_stamp(), precedence(x.time_stamp()) < core::detail::max_precedence);
     579           2 :     derived().leave(x);
     580           2 :     enable_val();
     581           2 :   }
     582             : 
     583          83 :   void apply(const state_formulas::variable& x)
     584             :   {
     585          83 :     disable_val();
     586          83 :     derived().enter(x);
     587          83 :     derived().apply(x.name());
     588          83 :     print_list(x.arguments(), "(", ")", ", ", false);
     589          83 :     derived().leave(x);
     590          83 :     enable_val();
     591          83 :   }
     592             : 
     593             :   // TODO: merge this function with the version in data/print.h (?)
     594          96 :   void print_assignments(const data::assignment_list& assignments)
     595             :   {
     596          96 :     if (assignments.empty())
     597             :     {
     598          83 :       return;
     599             :     }
     600          13 :     disable_val();
     601          13 :     derived().print("(");
     602          29 :     for (auto i = assignments.begin(); i != assignments.end(); ++i)
     603             :     {
     604          16 :       if (i != assignments.begin())
     605             :       {
     606           3 :         derived().print(", ");
     607             :       }
     608          16 :       derived().apply(i->lhs());
     609          16 :       derived().print(": ");
     610          16 :       derived().apply(i->lhs().sort());
     611          16 :       derived().print(" = ");
     612          16 :       derived().apply(i->rhs());
     613             :     }
     614          13 :     derived().print(")");
     615          13 :     enable_val();
     616             :   }
     617             : 
     618          20 :   void apply(const state_formulas::nu& x)
     619             :   {
     620          20 :     derived().enter(x);
     621          20 :     derived().print("nu ");
     622          20 :     derived().apply(x.name());
     623          20 :     print_assignments(x.assignments());
     624          20 :     derived().print(". ");
     625          20 :     derived().apply(x.operand());
     626          20 :     derived().leave(x);
     627          20 :   }
     628             : 
     629          76 :   void apply(const state_formulas::mu& x)
     630             :   {
     631          76 :     derived().enter(x);
     632          76 :     derived().print("mu ");
     633          76 :     derived().apply(x.name());
     634          76 :     print_assignments(x.assignments());
     635          76 :     derived().print(". ");
     636          76 :     derived().apply(x.operand());
     637          76 :     derived().leave(x);
     638          76 :   }
     639             : 
     640           3 :   void apply(const state_formulas::state_formula_specification& x)
     641             :   {
     642           3 :     derived().enter(x);
     643           3 :     derived().apply(x.data());
     644           3 :     print_action_declarations(x.action_labels(), "act  ",";\n\n", ";\n     ");
     645           3 :     derived().print("form ");
     646           3 :     derived().apply(x.formula());
     647           3 :     derived().print(";\n");
     648           3 :     derived().leave(x);
     649           3 :   }
     650             : };
     651             : 
     652             : } // namespace detail
     653             : 
     654             : /// \brief Prints the object t to a stream.
     655             : template <typename T>
     656         140 : void pp(const T& t, std::ostream& out)
     657             : {
     658         140 :   core::detail::apply_printer<state_formulas::detail::printer> printer(out);
     659         140 :   printer.apply(t);
     660         140 : }
     661             : 
     662             : /// \brief Returns a string representation of the object t.
     663             : template <typename T>
     664         140 : std::string pp(const T& t)
     665             : {
     666         140 :   std::ostringstream out;
     667         140 :   state_formulas::pp(t, out);
     668         280 :   return out.str();
     669         140 : }
     670             : 
     671             : } // namespace state_formulas
     672             : 
     673             : } // namespace mcrl2
     674             : 
     675             : #endif // MCRL2_MODAL_FORMULA_PRINT_H
     676             : 

Generated by: LCOV version 1.14