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/parse_impl.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_PARSE_IMPL_H
      13             : #define MCRL2_MODAL_FORMULA_PARSE_IMPL_H
      14             : 
      15             : #include "mcrl2/lps/parse.h"
      16             : #include "mcrl2/lps/parse_impl.h"
      17             : #include "mcrl2/modal_formula/typecheck.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace action_formulas
      23             : {
      24             : 
      25             : namespace detail
      26             : {
      27             : 
      28             : struct action_formula_actions: public lps::detail::multi_action_actions
      29             : {
      30         179 :   explicit action_formula_actions(const core::parser& parser_)
      31         179 :     : lps::detail::multi_action_actions(parser_)
      32         179 :   {}
      33             : 
      34         297 :   action_formulas::action_formula parse_ActFrm(const core::parse_node& node) const
      35             :   {
      36         297 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "MultAct")) { return process::untyped_multi_action(parse_ActionList(node.child(0))); }
      37         118 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "DataValExpr")) { return parse_DataValExpr(node.child(0)); }
      38         118 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "DataExpr")) { return parse_DataExpr(node.child(0)); }
      39         118 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "true")) { return action_formulas::true_(); }
      40          57 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "false")) { return action_formulas::false_(); }
      41          55 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "!") && (symbol_name(node.child(1)) == "ActFrm")) { return action_formulas::not_(parse_ActFrm(node.child(1))); }
      42          18 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "ActFrm") && (node.child(1).string() == "=>") && (symbol_name(node.child(2)) == "ActFrm")) { return action_formulas::imp(parse_ActFrm(node.child(0)), parse_ActFrm(node.child(2))); }
      43          18 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "ActFrm") && (node.child(1).string() == "&&") && (symbol_name(node.child(2)) == "ActFrm")) { return action_formulas::and_(parse_ActFrm(node.child(0)), parse_ActFrm(node.child(2))); }
      44           9 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "ActFrm") && (node.child(1).string() == "||") && (symbol_name(node.child(2)) == "ActFrm")) { return action_formulas::or_(parse_ActFrm(node.child(0)), parse_ActFrm(node.child(2))); }
      45           6 :     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)) == "ActFrm")) { return action_formulas::forall(parse_VarsDeclList(node.child(1)), parse_ActFrm(node.child(3))); }
      46           3 :     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)) == "ActFrm")) { return action_formulas::exists(parse_VarsDeclList(node.child(1)), parse_ActFrm(node.child(3))); }
      47           1 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "ActFrm") && (node.child(1).string() == "@") && (symbol_name(node.child(2)) == "DataExpr")) { return action_formulas::at(parse_ActFrm(node.child(0)), parse_DataExpr(node.child(2))); }
      48           2 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "(") && (symbol_name(node.child(1)) == "ActFrm") && (symbol_name(node.child(2)) == ")")) { return parse_ActFrm(node.child(1)); }
      49           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
      50             :   }
      51             : };
      52             : 
      53             : } // namespace detail
      54             : 
      55             : } // namespace action_formulas
      56             : 
      57             : namespace regular_formulas
      58             : {
      59             : 
      60             : namespace detail
      61             : {
      62             : 
      63             : struct regular_formula_actions: public action_formulas::detail::action_formula_actions
      64             : {
      65         179 :   explicit regular_formula_actions(const core::parser& parser_)
      66         179 :     : action_formulas::detail::action_formula_actions(parser_)
      67         179 :   {}
      68             : 
      69         268 :   regular_formulas::regular_formula parse_RegFrm(const core::parse_node& node) const
      70             :   {
      71         268 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "ActFrm")) { return parse_ActFrm(node.child(0)); }
      72          38 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "(") && (symbol_name(node.child(1)) == "RegFrm") && (symbol_name(node.child(2)) == ")")) { return parse_RegFrm(node.child(1)); }
      73          38 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "RegFrm") && (symbol_name(node.child(1)) == "*")) { return trans_or_nil(parse_RegFrm(node.child(0))); }
      74           5 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "RegFrm") && (symbol_name(node.child(1)) == "+")) { return trans(parse_RegFrm(node.child(0))); }
      75           5 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "RegFrm") && (node.child(1).string() == ".") && (symbol_name(node.child(2)) == "RegFrm")) { return untyped_regular_formula(core::identifier_string("."), parse_RegFrm(node.child(0)), parse_RegFrm(node.child(2))); }
      76           2 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "RegFrm") && (node.child(1).string() == "+") && (symbol_name(node.child(2)) == "RegFrm")) { return untyped_regular_formula(core::identifier_string("+"), parse_RegFrm(node.child(0)), parse_RegFrm(node.child(2))); }
      77           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
      78             :   }
      79             : };
      80             : 
      81             : } // namespace detail
      82             : 
      83             : } // namespace regular_formulas
      84             : 
      85             : namespace state_formulas
      86             : {
      87             : 
      88             : namespace detail
      89             : {
      90             : 
      91             : struct untyped_state_formula_specification: public data::untyped_data_specification
      92             : {
      93             :   process::action_label_list action_labels;
      94             :   state_formula formula;
      95             : 
      96           5 :   state_formula_specification construct_state_formula_specification()
      97             :   {
      98           5 :     state_formula_specification result;
      99           5 :     result.data() = construct_data_specification();
     100           5 :     result.action_labels() = action_labels;
     101           5 :     result.formula() = formula;
     102           5 :     return result;
     103           0 :   }
     104             : };
     105             : 
     106             : struct state_formula_actions: public regular_formulas::detail::regular_formula_actions
     107             : {
     108         179 :   explicit state_formula_actions(const core::parser& parser_)
     109         179 :     : regular_formulas::detail::regular_formula_actions(parser_)
     110         179 :   {}
     111             : 
     112           3 :   state_formula make_delay(const core::parse_node& node) const
     113             :   {
     114           3 :     if (node.child(0))
     115             :     {
     116           3 :       return delay_timed(parse_DataExpr(node.child(0).child(1)));
     117             :     }
     118             :     else
     119             :     {
     120           0 :       return delay();
     121             :     }
     122             :   }
     123             : 
     124           1 :   state_formula make_yaled(const core::parse_node& node) const
     125             :   {
     126           1 :     if (node.child(0))
     127             :     {
     128           1 :       return yaled_timed(parse_DataExpr(node.child(0).child(1)));
     129             :     }
     130             :     else
     131             :     {
     132           0 :       return yaled();
     133             :     }
     134             :   }
     135             : 
     136          15 :   data::assignment parse_StateVarAssignment(const core::parse_node& node) const
     137             :   {
     138          30 :     return data::assignment(data::variable(parse_Id(node.child(0)), parse_SortExpr(node.child(2))), parse_DataExpr(node.child(4)));
     139             :   }
     140             : 
     141         168 :   data::assignment_list parse_StateVarAssignmentList(const core::parse_node& node) const
     142             :   {
     143         183 :     return parse_list<data::assignment>(node, "StateVarAssignment", [&](const core::parse_node& node) { return parse_StateVarAssignment(node); });
     144             :   }
     145             : 
     146        1033 :   state_formulas::state_formula parse_StateFrm(const core::parse_node& node) const
     147             :   {
     148        1033 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "DataValExpr")) { return parse_DataValExpr(node.child(0)); }
     149        1007 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "DataExpr")) { return parse_DataExpr(node.child(0)); }
     150        1007 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "true")) { return state_formulas::true_(); }
     151         913 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "false")) { return state_formulas::false_(); }
     152         875 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "!") && (symbol_name(node.child(1)) == "StateFrm")) { return state_formulas::not_(parse_StateFrm(node.child(1))); }
     153         839 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "-") && (symbol_name(node.child(1)) == "StateFrm")) { return state_formulas::minus(parse_StateFrm(node.child(1))); }
     154         839 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "StateFrm") && (node.child(1).string() == "=>") && (symbol_name(node.child(2)) == "StateFrm")) { return state_formulas::imp(parse_StateFrm(node.child(0)), parse_StateFrm(node.child(2))); }
     155         815 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "StateFrm") && (node.child(1).string() == "&&") && (symbol_name(node.child(2)) == "StateFrm")) { return state_formulas::and_(parse_StateFrm(node.child(0)), parse_StateFrm(node.child(2))); }
     156         739 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "StateFrm") && (node.child(1).string() == "||") && (symbol_name(node.child(2)) == "StateFrm")) { return state_formulas::or_(parse_StateFrm(node.child(0)), parse_StateFrm(node.child(2))); }
     157         713 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "StateFrm") && (node.child(1).string() == "+") && (symbol_name(node.child(2)) == "StateFrm")) { return state_formulas::plus(parse_StateFrm(node.child(0)), parse_StateFrm(node.child(2))); } 
     158         713 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataValExpr") && (node.child(1).string() == "*") && (symbol_name(node.child(2)) == "StateFrm")) { return state_formulas::const_multiply(parse_DataValExpr(node.child(0)), parse_StateFrm(node.child(2))); }
     159         712 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "StateFrm") && (node.child(1).string() == "*") && (symbol_name(node.child(2)) == "DataValExpr")) { return state_formulas::const_multiply_alt(parse_StateFrm(node.child(0)), parse_DataValExpr(node.child(2))); }
     160         711 :     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)) == "StateFrm")) { return state_formulas::forall(parse_VarsDeclList(node.child(1)), parse_StateFrm(node.child(3))); }
     161         692 :     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)) == "StateFrm")) { return state_formulas::exists(parse_VarsDeclList(node.child(1)), parse_StateFrm(node.child(3))); }
     162         684 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "inf") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "StateFrm")) { return state_formulas::infimum(parse_VarsDeclList(node.child(1)), parse_StateFrm(node.child(3))); }
     163         682 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "sup") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "StateFrm")) { return state_formulas::supremum(parse_VarsDeclList(node.child(1)), parse_StateFrm(node.child(3))); }
     164         681 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "sum") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "StateFrm")) { return state_formulas::sum(parse_VarsDeclList(node.child(1)), parse_StateFrm(node.child(3))); }
     165         680 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "[") && (symbol_name(node.child(1)) == "RegFrm") && (symbol_name(node.child(2)) == "]") && (symbol_name(node.child(3)) == "StateFrm")) { return state_formulas::must(parse_RegFrm(node.child(1)), parse_StateFrm(node.child(3))); }
     166         543 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "<") && (symbol_name(node.child(1)) == "RegFrm") && (symbol_name(node.child(2)) == ">") && (symbol_name(node.child(3)) == "StateFrm")) { return state_formulas::may(parse_RegFrm(node.child(1)), parse_StateFrm(node.child(3))); }
     167         455 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "mu") && (symbol_name(node.child(1)) == "StateVarDecl") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "StateFrm")) { return state_formulas::mu(parse_Id(node.child(1).child(0)), parse_StateVarAssignmentList(node.child(1).child(1)), parse_StateFrm(node.child(3))); }
     168         355 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "nu") && (symbol_name(node.child(1)) == "StateVarDecl") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "StateFrm")) { return state_formulas::nu(parse_Id(node.child(1).child(0)), parse_StateVarAssignmentList(node.child(1).child(1)), parse_StateFrm(node.child(3))); }
     169         287 :     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))); }
     170         147 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "delay")) { return make_delay(node.child(1)); }
     171         142 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "yaled")) { return make_yaled(node.child(1)); }
     172         280 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "(") && (symbol_name(node.child(1)) == "StateFrm") && (symbol_name(node.child(2)) == ")")) { return parse_StateFrm(node.child(1)); }
     173           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
     174             :   }
     175             : 
     176           5 :   state_formula parse_FormSpec(const core::parse_node& node) const
     177             :   {
     178          10 :     return parse_StateFrm(node.child(1));
     179             :   }
     180             : 
     181          44 :   bool callback_StateFrmSpec(const core::parse_node& node, untyped_state_formula_specification& result) const
     182             :   {
     183          44 :     if (symbol_name(node) == "SortSpec")
     184             :     {
     185           4 :       return callback_DataSpecElement(node, result);
     186             :     }
     187          40 :     else if (symbol_name(node) == "ConsSpec")
     188             :     {
     189           4 :       return callback_DataSpecElement(node, result);
     190             :     }
     191          36 :     else if (symbol_name(node) == "MapSpec")
     192             :     {
     193           0 :       return callback_DataSpecElement(node, result);
     194             :     }
     195          36 :     else if (symbol_name(node) == "EqnSpec")
     196             :     {
     197           0 :       return callback_DataSpecElement(node, result);
     198             :     }
     199          36 :     else if (symbol_name(node) == "ActSpec")
     200             :     {
     201           4 :       result.action_labels = result.action_labels + parse_ActSpec(node);
     202           4 :       return true;
     203             :     }
     204          32 :     else if (symbol_name(node) == "FormSpec")
     205             :     {
     206           5 :       result.formula = parse_FormSpec(node);
     207           5 :       return true;
     208             :     }
     209          27 :     else if (symbol_name(node) == "StateFrm")
     210             :     {
     211           0 :       result.formula = parse_StateFrm(node);
     212           0 :       return true;
     213             :     }
     214          27 :     return false;
     215             :   }
     216             : 
     217           5 :   untyped_state_formula_specification parse_StateFrmSpec(const core::parse_node& node) const
     218             :   {
     219           5 :     untyped_state_formula_specification result;
     220          49 :     traverse(node, [&](const core::parse_node& node) { return callback_StateFrmSpec(node, result); });
     221           5 :     return result;
     222           0 :   }
     223             : };
     224             : 
     225             : } // namespace detail
     226             : 
     227             : } // namespace state_formulas
     228             : 
     229             : } // namespace mcrl2
     230             : 
     231             : #endif // MCRL2_MODAL_FORMULA_PARSE_IMPL_H