LCOV - code coverage report
Current view: top level - bes/include/mcrl2/bes - parse.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 12 13 92.3 %
Date: 2020-10-20 00:45:57 Functions: 1 1 100.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/parse.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_BES_PARSE_H
      13             : #define MCRL2_BES_PARSE_H
      14             : 
      15             : #include "mcrl2/bes/boolean_equation_system.h"
      16             : #include "mcrl2/bes/detail/pbes_expression2boolean_expression_traverser.h"
      17             : #include "mcrl2/core/parser_utility.h"
      18             : #include "mcrl2/pbes/is_bes.h"
      19             : #include "mcrl2/pbes/parse.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : 
      24             : namespace bes
      25             : {
      26             : 
      27             : namespace detail {
      28             : 
      29             : struct bes_actions: public core::default_parser_actions
      30             : {
      31             :   bes_actions(const core::parser& parser_)
      32             :     : core::default_parser_actions(parser_)
      33             :   {}
      34             : 
      35             :   bes::boolean_expression parse_BesExpr(const core::parse_node& node) const
      36             :   {
      37             :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "true")) { return bes::true_(); }
      38             :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "false")) { return bes::false_(); }
      39             :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "!") && (symbol_name(node.child(1)) == "BesExpr")) { return bes::not_(parse_BesExpr(node.child(1))); }
      40             :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "BesExpr") && (node.child(1).string() == "=>") && (symbol_name(node.child(2)) == "BesExpr")) { return bes::imp(parse_BesExpr(node.child(0)), parse_BesExpr(node.child(2))); }
      41             :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "BesExpr") && (node.child(1).string() == "&&") && (symbol_name(node.child(2)) == "BesExpr")) { return bes::and_(parse_BesExpr(node.child(0)), parse_BesExpr(node.child(2))); }
      42             :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "BesExpr") && (node.child(1).string() == "||") && (symbol_name(node.child(2)) == "BesExpr")) { return bes::or_(parse_BesExpr(node.child(0)), parse_BesExpr(node.child(2))); }
      43             :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "(") && (symbol_name(node.child(1)) == "BesExpr") && (symbol_name(node.child(2)) == ")")) { return parse_BesExpr(node.child(1)); }
      44             :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "BesVar")) { return parse_BesVar(node.child(0)); }
      45             :     throw core::parse_node_unexpected_exception(m_parser, node);
      46             :   }
      47             : 
      48             :   bes::boolean_variable parse_BesVar(const core::parse_node& node) const
      49             :   {
      50             :     return bes::boolean_variable(parse_Id(node.child(0)));
      51             :   }
      52             : 
      53             :   fixpoint_symbol parse_FixedPointOperator(const core::parse_node& node) const
      54             :   {
      55             :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "mu")) { return fixpoint_symbol::mu(); }
      56             :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "nu")) { return fixpoint_symbol::nu(); }
      57             :     throw core::parse_node_unexpected_exception(m_parser, node);
      58             :   }
      59             : 
      60             :   bes::boolean_equation parse_BesEqnDecl(const core::parse_node& node) const
      61             :   {
      62             :     return bes::boolean_equation(parse_FixedPointOperator(node.child(0)), parse_BesVar(node.child(1)), parse_BesExpr(node.child(3)));
      63             :   }
      64             : 
      65             :   std::vector<boolean_equation> parse_BesEqnSpec(const core::parse_node& node) const
      66             :   {
      67             :     return parse_BesEqnDeclList(node.child(1));
      68             :   }
      69             : 
      70             :   bes::boolean_variable parse_BesInit(const core::parse_node& node) const
      71             :   {
      72             :     return parse_BesVar(node.child(1));
      73             :   }
      74             : 
      75             :   bes::boolean_equation_system parse_BesSpec(const core::parse_node& node) const
      76             :   {
      77             :     return bes::boolean_equation_system(parse_BesEqnSpec(node.child(0)), parse_BesInit(node.child(1)));
      78             :   }
      79             : 
      80             :   std::vector<boolean_equation> parse_BesEqnDeclList(const core::parse_node& node) const
      81             :   {
      82             :     return parse_vector<bes::boolean_equation>(node, "BesEqnDecl", [&](const core::parse_node& node) { return parse_BesEqnDecl(node); });
      83             :   }
      84             : };
      85             : 
      86             : inline
      87             : boolean_expression parse_boolean_expression(const std::string& text)
      88             : {
      89             :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
      90             :   unsigned int start_symbol_index = p.start_symbol_index("BesExpr");
      91             :   bool partial_parses = false;
      92             :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
      93             :   core::warn_and_or(node);
      94             :   boolean_expression result = detail::bes_actions(p).parse_BesExpr(node);
      95             :   return result;
      96             : }
      97             : 
      98             : inline
      99             : boolean_equation_system parse_boolean_equation_system(const std::string& text)
     100             : {
     101             :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     102             :   unsigned int start_symbol_index = p.start_symbol_index("BesSpec");
     103             :   bool partial_parses = false;
     104             :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     105             :   core::warn_and_or(node);
     106             :   boolean_equation_system result = detail::bes_actions(p).parse_BesSpec(node);
     107             :   return result;
     108             : }
     109             : 
     110             : } // namespace detail
     111             : 
     112             : /// \brief Reads a boolean equation system from an input stream.
     113             : /// \param from An input stream
     114             : /// \param b A boolean equation system
     115             : /// \return The input stream
     116             : inline
     117          16 : std::istream& operator>>(std::istream& from, boolean_equation_system& b)
     118             : {
     119          32 :   pbes_system::pbes p;
     120          16 :   from >> p;
     121          16 :   if (!is_bes(p))
     122             :   {
     123           0 :     throw mcrl2::runtime_error("parsing of boolean equation system failed: it is not a BES!");
     124             :   }
     125             : 
     126          32 :   std::vector<boolean_equation> equations;
     127          49 :   for (const pbes_system::pbes_equation& eqn: p.equations())
     128             :   {
     129          66 :     boolean_variable v(eqn.variable().name());
     130          66 :     boolean_expression rhs = bes::pbes_expression2boolean_expression(eqn.formula());
     131          33 :     equations.emplace_back(eqn.symbol(), v, rhs);
     132             :   }
     133             : 
     134          32 :   boolean_expression init = bes::pbes_expression2boolean_expression(p.initial_state());
     135          16 :   b = boolean_equation_system(equations, init);
     136          32 :   return from;
     137             : }
     138             : 
     139             : } // namespace bes
     140             : 
     141             : } // namespace mcrl2
     142             : 
     143             : #endif // MCRL2_BES_PARSE_H

Generated by: LCOV version 1.13