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.h 10 : /// \brief Parser for pbes expressions. 11 : 12 : #ifndef MCRL2_PBES_PARSE_H 13 : #define MCRL2_PBES_PARSE_H 14 : 15 : #include "mcrl2/data/detail/parse_substitution.h" 16 : #include "mcrl2/pbes/typecheck.h" 17 : #include "mcrl2/pbes/untyped_pbes.h" 18 : #include <boost/algorithm/string.hpp> 19 : #include <boost/algorithm/string/join.hpp> 20 : 21 : namespace mcrl2 22 : { 23 : 24 : namespace pbes_system 25 : { 26 : 27 : namespace detail 28 : { 29 : 30 : pbes_expression parse_pbes_expression_new(const std::string& text); 31 : untyped_pbes parse_pbes_new(const std::string& text); 32 : void complete_pbes(pbes& x); 33 : propositional_variable parse_propositional_variable(const std::string& text); 34 : pbes_expression parse_pbes_expression(const std::string& text); 35 : 36 : } // namespace detail 37 : 38 : inline 39 465 : pbes parse_pbes(std::istream& in) 40 : { 41 465 : std::string text = utilities::read_text(in); 42 465 : pbes result = detail::parse_pbes_new(text).construct_pbes(); 43 465 : detail::complete_pbes(result); 44 930 : return result; 45 465 : } 46 : 47 : /// \brief Reads a PBES from an input stream. 48 : /// \param from An input stream 49 : /// \param result A PBES 50 : /// \return The input stream 51 : inline 52 465 : std::istream& operator>>(std::istream& from, pbes& result) 53 : { 54 465 : result = parse_pbes(from); 55 465 : return from; 56 : } 57 : 58 : inline 59 : pbes parse_pbes(const std::string& text) 60 : { 61 : std::istringstream in(text); 62 : return parse_pbes(in); 63 : } 64 : 65 : template <typename VariableContainer> 66 2 : propositional_variable parse_propositional_variable(const std::string& text, 67 : const VariableContainer& variables, 68 : const data::data_specification& dataspec = data::data_specification() 69 : ) 70 : { 71 2 : propositional_variable result = detail::parse_propositional_variable(text); 72 4 : return typecheck_propositional_variable(result, variables, dataspec); 73 2 : } 74 : 75 : /** \brief Parse a pbes expression. 76 : * Throws an exception if something went wrong. 77 : * \param[in] text A string containing a pbes expression. 78 : * \param[in] variables A sequence of data variables that may appear in x. 79 : * \param[in] propositional_variables A sequence of propositional variables that may appear in x. 80 : * \param[in] dataspec A data specification. 81 : * \param[in] type_check If true the parsed input is also typechecked. 82 : * \return The parsed PBES expression. 83 : **/ 84 : template <typename VariableContainer, typename PropositionalVariableContainer> 85 1 : pbes_expression parse_pbes_expression(const std::string& text, 86 : const data::data_specification& dataspec, 87 : const VariableContainer& variables, 88 : const PropositionalVariableContainer& propositional_variables, 89 : bool type_check = true, 90 : bool translate_user_notation = true, 91 : bool normalize_sorts = true 92 : ) 93 : { 94 1 : pbes_expression x = detail::parse_pbes_expression(text); 95 1 : if (type_check) 96 : { 97 1 : x = pbes_system::typecheck_pbes_expression(x, variables, propositional_variables, dataspec); 98 : } 99 1 : if (translate_user_notation) 100 : { 101 1 : x = pbes_system::translate_user_notation(x); 102 : } 103 1 : if (normalize_sorts) 104 : { 105 1 : x = pbes_system::normalize_sorts(x, dataspec); 106 : } 107 1 : return x; 108 0 : } 109 : 110 : /** \brief Parse a pbes expression. 111 : * Throws an exception if something went wrong. 112 : * \param[in] text A string containing a pbes expression. 113 : * \param[in] pbesspec A PBES used as context. 114 : * \param[in] variables A sequence of data variables that may appear in x. 115 : * \param[in] type_check If true the parsed input is also typechecked. 116 : * \return The parsed PBES expression. 117 : **/ 118 : template <typename VariableContainer> 119 : pbes_expression parse_pbes_expression(const std::string& text, 120 : const pbes& pbesspec, 121 : const VariableContainer& variables, 122 : bool type_check = true, 123 : bool translate_user_notation = true, 124 : bool normalize_sorts = true 125 : ) 126 : { 127 : std::vector<propositional_variable> propositional_variables; 128 : for (const pbes_equation& eqn: pbesspec.equations()) 129 : { 130 : propositional_variables.push_back(eqn.variable()); 131 : } 132 : return parse_pbes_expression(text, pbesspec.data(), variables, propositional_variables, type_check, translate_user_notation, normalize_sorts); 133 : } 134 : 135 : } // namespace pbes_system 136 : 137 : } // namespace mcrl2 138 : 139 : #endif // MCRL2_PBES_PARSE_H