LCOV - code coverage report
Current view: top level - bes/include/mcrl2/bes/detail - boolean_expression2pbes_expression_traverser.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 28 40 70.0 %
Date: 2020-02-28 00:44:21 Functions: 9 12 75.0 %
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/bes/detail/boolean_expression2pbes_expression_traverser.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_BES_DETAIL_BOOLEAN_EXPRESSION2PBES_EXPRESSION_TRAVERSER_H
      13             : #define MCRL2_BES_DETAIL_BOOLEAN_EXPRESSION2PBES_EXPRESSION_TRAVERSER_H
      14             : 
      15             : #include "mcrl2/bes/traverser.h"
      16             : #include "mcrl2/pbes/pbes_expression.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace bes
      22             : {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27           8 : struct boolean_expression2pbes_expression_traverser: public bes::boolean_expression_traverser<boolean_expression2pbes_expression_traverser>
      28             : {
      29             :   typedef bes::boolean_expression_traverser<boolean_expression2pbes_expression_traverser> super;
      30             :   typedef core::term_traits<pbes_system::pbes_expression> tr;
      31             : 
      32             :   using super::apply;
      33             :   using super::enter;
      34             :   using super::leave;
      35             : 
      36             :   /// \brief A stack containing PBES expressions.
      37             :   std::vector<pbes_system::pbes_expression> expression_stack;
      38             : 
      39           8 :   void push(const pbes_system::pbes_expression& x)
      40             :   {
      41           8 :     expression_stack.push_back(x);
      42           8 :   }
      43             : 
      44           4 :   pbes_system::pbes_expression pop()
      45             :   {
      46           4 :     assert(!expression_stack.empty());
      47           4 :     pbes_system::pbes_expression result = expression_stack.back();
      48           4 :     expression_stack.pop_back();
      49           4 :     return result;
      50             :   }
      51             : 
      52             :   /// \brief Returns the top element of the expression stack, which is the result of the conversion.
      53           4 :   pbes_system::pbes_expression result() const
      54             :   {
      55           4 :     assert(!expression_stack.empty());
      56           4 :     return expression_stack.back();
      57             :   }
      58             : 
      59             :   /// \brief Enter true node
      60           0 :   void enter(const true_& /* x */)
      61             :   {
      62           0 :     push(tr::true_());
      63           0 :   }
      64             : 
      65             :   /// \brief Enter false node
      66           1 :   void enter(const false_& /* x */)
      67             :   {
      68           1 :     push(tr::false_());
      69           1 :   }
      70             : 
      71             :   /// \brief Leave not node
      72           0 :   void leave(const not_& /* x */)
      73             :   {
      74           0 :     pbes_system::pbes_expression b = pop();
      75           0 :     push(tr::not_(b));
      76           0 :   }
      77             : 
      78             :   /// \brief Leave and node
      79           0 :   void leave(const and_& /* x */)
      80             :   {
      81             :     // join the two expressions on top of the stack
      82           0 :     pbes_system::pbes_expression right = pop();
      83           0 :     pbes_system::pbes_expression left  = pop();
      84           0 :     push(tr::and_(left, right));
      85           0 :   }
      86             : 
      87             :   /// \brief Leave or node
      88           1 :   void leave(const or_& /* x */)
      89             :   {
      90             :     // join the two expressions on top of the stack
      91           2 :     pbes_system::pbes_expression right = pop();
      92           2 :     pbes_system::pbes_expression left  = pop();
      93           1 :     push(tr::or_(left, right));
      94           1 :   }
      95             : 
      96             :   /// \brief Enter imp node
      97             :   /// \param e A term
      98           1 :   void leave(const imp& /* x */)
      99             :   {
     100             :     // join the two expressions on top of the stack
     101           2 :     pbes_system::pbes_expression right = pop();
     102           2 :     pbes_system::pbes_expression left  = pop();
     103           1 :     push(tr::imp(left, right));
     104           1 :   }
     105             : 
     106             :   /// \brief Enter propositional_variable node
     107             :   /// \param e A term
     108             :   /// \param X A propositional variable
     109           5 :   void enter(const boolean_variable& x)
     110             :   {
     111           5 :     push(pbes_system::propositional_variable_instantiation(x.name(), data::data_expression_list()));
     112           5 :   }
     113             : };
     114             : 
     115             : } // namespace detail
     116             : 
     117             : } // namespace bes
     118             : 
     119             : } // namespace mcrl2
     120             : 
     121             : #endif // MCRL2_BES_DETAIL_BOOLEAN_EXPRESSION2PBES_EXPRESSION_TRAVERSER_H

Generated by: LCOV version 1.13