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/parse_impl.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_PARSE_IMPL_H
      13             : #define MCRL2_PBES_PARSE_IMPL_H
      14             : 
      15             : #include "mcrl2/data/detail/parse_substitution.h"
      16             : #include "mcrl2/data/parse_impl.h"
      17             : #include "mcrl2/pbes/typecheck.h"
      18             : #include "mcrl2/pbes/untyped_pbes.h"
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace pbes_system {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27             : struct pbes_actions: public data::detail::data_specification_actions
      28             : {
      29         470 :   explicit pbes_actions(const core::parser& parser_)
      30         470 :     : data::detail::data_specification_actions(parser_)
      31         470 :   {}
      32             : 
      33        6258 :   pbes_system::pbes_expression parse_PbesExpr(const core::parse_node& node) const
      34             :   {
      35        6258 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "DataValExpr")) { return parse_DataValExpr(node.child(0)); }
      36        5574 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "DataExpr")) { return parse_DataExpr(node.child(0)); }
      37        5574 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "true")) { return pbes_system::true_(); }
      38        3268 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "false")) { return pbes_system::false_(); }
      39        3204 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "forall") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "PbesExpr")) { return pbes_system::forall(parse_VarsDeclList(node.child(1)), parse_PbesExpr(node.child(3))); }
      40        2985 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "exists") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "PbesExpr")) { return pbes_system::exists(parse_VarsDeclList(node.child(1)), parse_PbesExpr(node.child(3))); }
      41        2866 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "!") && (symbol_name(node.child(1)) == "PbesExpr")) { return pbes_system::not_(parse_PbesExpr(node.child(1))); }
      42        2723 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "PbesExpr") && (node.child(1).string() == "=>") && (symbol_name(node.child(2)) == "PbesExpr")) { return pbes_system::imp(parse_PbesExpr(node.child(0)), parse_PbesExpr(node.child(2))); }
      43        2547 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "PbesExpr") && (node.child(1).string() == "&&") && (symbol_name(node.child(2)) == "PbesExpr")) { return pbes_system::and_(parse_PbesExpr(node.child(0)), parse_PbesExpr(node.child(2))); }
      44        2126 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "PbesExpr") && (node.child(1).string() == "||") && (symbol_name(node.child(2)) == "PbesExpr")) { return pbes_system::or_(parse_PbesExpr(node.child(0)), parse_PbesExpr(node.child(2))); }
      45        2705 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "(") && (symbol_name(node.child(1)) == "PbesExpr") && (symbol_name(node.child(2)) == ")")) { return parse_PbesExpr(node.child(1)); }
      46         787 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "PropVarInst")) { return parse_PropVarInst(node.child(0)); }
      47         787 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "Id")) { return data::untyped_data_parameter(parse_Id(node.child(0)), parse_DataExprList(node.child(1))); }
      48           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
      49             :   }
      50             : 
      51        2865 :   pbes_system::propositional_variable parse_PropVarDecl(const core::parse_node& node) const
      52             :   {
      53        5730 :     return pbes_system::propositional_variable(parse_Id(node.child(0)), parse_VarsDeclList(node.child(1)));
      54             :   }
      55             : 
      56         467 :   pbes_system::propositional_variable_instantiation parse_PropVarInst(const core::parse_node& node) const
      57             :   {
      58         934 :     return pbes_system::propositional_variable_instantiation(parse_Id(node.child(0)), parse_DataExprList(node.child(1)));
      59             :   }
      60             : 
      61         467 :   pbes_system::propositional_variable_instantiation parse_PbesInit(const core::parse_node& node) const
      62             :   {
      63         934 :     return parse_PropVarInst(node.child(1));
      64             :   }
      65             : 
      66        2863 :   pbes_system::fixpoint_symbol parse_FixedPointOperator(const core::parse_node& node) const
      67             :   {
      68        2863 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "mu")) { return fixpoint_symbol::mu(); }
      69         285 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "nu")) { return fixpoint_symbol::nu(); }
      70           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
      71             :   }
      72             : 
      73        2863 :   pbes_equation parse_PbesEqnDecl(const core::parse_node& node) const
      74             :   {
      75        2863 :     return pbes_equation(parse_FixedPointOperator(node.child(0)), parse_PropVarDecl(node.child(1)), parse_PbesExpr(node.child(3)));
      76             :   }
      77             : 
      78         467 :   std::vector<pbes_equation> parse_PbesEqnDeclList(const core::parse_node& node) const
      79             :   {
      80        3330 :     return parse_vector<pbes_equation>(node, "PbesEqnDecl", [&](const core::parse_node& node) { return parse_PbesEqnDecl(node); });
      81             :   }
      82             : 
      83         467 :   std::vector<pbes_equation> parse_PbesEqnSpec(const core::parse_node& node) const
      84             :   {
      85         934 :     return parse_PbesEqnDeclList(node.child(1));
      86             :   }
      87             : 
      88         467 :   untyped_pbes parse_PbesSpec(const core::parse_node& node) const
      89             :   {
      90         467 :     untyped_pbes result;
      91         467 :     result.dataspec = parse_DataSpec(node.child(0));
      92         467 :     result.global_variables = parse_GlobVarSpec(node.child(1));
      93         467 :     result.equations = parse_PbesEqnSpec(node.child(2));
      94         467 :     result.initial_state = parse_PbesInit(node.child(3));
      95         467 :     return result;
      96           0 :   }
      97             : };
      98             : 
      99             : } // namespace detail
     100             : 
     101             : } // namespace pbes_system
     102             : 
     103             : } // namespace mcrl2
     104             : 
     105             : #endif // MCRL2_PBES_PARSE_IMPL_H