LCOV - code coverage report
Current view: top level - bes/include/mcrl2/bes/detail - pbes_expression2boolean_expression_traverser.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 34 51 66.7 %
Date: 2020-02-29 00:53:40 Functions: 10 14 71.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/detail/pbes_expression2boolean_expression_traverser.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_BES_DETAIL_PBES_EXPRESSION2BOOLEAN_EXPRESSION_TRAVERSER_H
      13             : #define MCRL2_BES_DETAIL_PBES_EXPRESSION2BOOLEAN_EXPRESSION_TRAVERSER_H
      14             : 
      15             : #include "mcrl2/bes/boolean_expression.h"
      16             : #include "mcrl2/pbes/traverser.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace bes
      22             : {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27         102 : struct pbes_expression2boolean_expression_traverser: public pbes_system::pbes_expression_traverser<pbes_expression2boolean_expression_traverser>
      28             : {
      29             :   typedef pbes_system::pbes_expression_traverser<pbes_expression2boolean_expression_traverser> super;
      30             :   typedef core::term_traits<pbes_system::pbes_expression> tr;
      31             :   typedef core::term_traits<bes::boolean_expression> br;
      32             : 
      33             :   using super::apply;
      34             :   using super::enter;
      35             :   using super::leave;
      36             : 
      37             :   /// \brief A stack containing boolean expressions.
      38             :   std::vector<bes::boolean_expression> expression_stack;
      39             : 
      40         117 :   void push(const bes::boolean_expression& x)
      41             :   {
      42         117 :     expression_stack.push_back(x);
      43         117 :   }
      44             : 
      45          66 :   bes::boolean_expression pop()
      46             :   {
      47          66 :     assert(!expression_stack.empty());
      48          66 :     auto result = expression_stack.back();
      49          66 :     expression_stack.pop_back();
      50          66 :     return result;
      51             :   }
      52             : 
      53             :   /// \brief Returns the top element of the expression stack, which is the result of the conversion.
      54          51 :   bes::boolean_expression result() const
      55             :   {
      56          51 :     assert(!expression_stack.empty());
      57          51 :     return expression_stack.back();
      58             :   }
      59             : 
      60           2 :   void leave(const data::data_expression& x)
      61             :   {
      62           2 :     if (tr::is_true(x))
      63             :     {
      64           2 :       push(br::true_());
      65             :     }
      66           0 :     else if (tr::is_false(x))
      67             :     {
      68           0 :       push(br::false_());
      69             :     }
      70             :     else
      71             :     {
      72           0 :       throw mcrl2::runtime_error("data_expression encountered in pbes_expression2boolean_expression_traverser");
      73             :     }
      74           2 :   }
      75             : 
      76           0 :   void leave(const pbes_system::not_&)
      77             :   {
      78           0 :     bes::boolean_expression b = pop();
      79           0 :     push(br::not_(b));
      80           0 :   }
      81             : 
      82          17 :   void leave(const pbes_system::and_&)
      83             :   {
      84             :     // join the two expressions on top of the stack
      85          34 :     bes::boolean_expression right = pop();
      86          34 :     bes::boolean_expression left  = pop();
      87          17 :     push(br::and_(left, right));
      88          17 :   }
      89             : 
      90          16 :   void leave(const pbes_system::or_&)
      91             :   {
      92             :     // join the two expressions on top of the stack
      93          32 :     bes::boolean_expression right = pop();
      94          32 :     bes::boolean_expression left  = pop();
      95          16 :     push(br::or_(left, right));
      96          16 :   }
      97             : 
      98           0 :   void leave(const pbes_system::imp&)
      99             :   {
     100             :     // join the two expressions on top of the stack
     101           0 :     bes::boolean_expression right = pop();
     102           0 :     bes::boolean_expression left  = pop();
     103           0 :     push(br::imp(left, right));
     104           0 :   }
     105             : 
     106           0 :   void enter(const pbes_system::forall&)
     107             :   {
     108           0 :     throw mcrl2::runtime_error("forall encountered in pbes_expression2boolean_expression_traverser");
     109             :   }
     110             : 
     111           0 :   void enter(const pbes_system::exists&)
     112             :   {
     113           0 :     throw mcrl2::runtime_error("exists encountered in pbes_expression2boolean_expression_traverser");
     114             :   }
     115             : 
     116          82 :   void leave(const pbes_system::propositional_variable_instantiation& x)
     117             :   {
     118          82 :     if (x.parameters().size() > 0)
     119             :     {
     120           0 :       throw mcrl2::runtime_error("propositional variable with parameters encountered in pbes_expression2boolean_expression_traverser");
     121             :     }
     122          82 :     push(bes::boolean_variable(x.name()));
     123          82 :   }
     124             : };
     125             : 
     126             : } // namespace detail
     127             : 
     128             : inline
     129          51 : boolean_expression pbes_expression2boolean_expression(const pbes_system::pbes_expression& x)
     130             : {
     131         102 :   detail::pbes_expression2boolean_expression_traverser f;
     132          51 :   f.apply(x);
     133         102 :   return f.result();
     134             : }
     135             : 
     136             : } // namespace bes
     137             : 
     138             : } // namespace mcrl2
     139             : 
     140             : #endif // MCRL2_BES_DETAIL_PBES_EXPRESSION2BOOLEAN_EXPRESSION_TRAVERSER_H

Generated by: LCOV version 1.13