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/parse.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PBES_DETAIL_PARSE_H 13 : #define MCRL2_PBES_DETAIL_PARSE_H 14 : 15 : #include "mcrl2/pbes/parse.h" 16 : 17 : namespace mcrl2 { 18 : 19 : namespace pbes_system { 20 : 21 : /// \brief Parses a sequence of pbes expressions. The format of the text is as 22 : /// follows: 23 : /// <ul> 24 : /// <li><tt>"datavar"</tt>, followed by a sequence of data variable declarations</li> 25 : /// <li><tt>"predvar"</tt>, followed by a sequence of predicate variable declarations</li> 26 : /// <li><tt>"expressions"</tt>, followed by a sequence of pbes expressions separated by newlines</li> 27 : /// </ul> 28 : /// An example of this is: 29 : /// \code 30 : /// datavar 31 : /// n: Nat; 32 : /// predvar 33 : /// X: Pos; 34 : /// Y: Nat, Bool; 35 : /// \endcode 36 : /// \param text A string 37 : /// \param data_spec A string 38 : /// N.B. A side effect of the data specification is that it determines whether rewrite rules 39 : /// for types like Pos and Nat are generated or not. 40 : /// \return The parsed expression and the data specification that was used. 41 : inline 42 274 : std::pair<std::vector<pbes_expression>, data::data_specification> parse_pbes_expressions(std::string text, const std::string& data_spec = "") 43 : { 44 274 : std::string unique_prefix("UNIQUE_PREFIX"); 45 274 : std::size_t unique_prefix_index = 0; 46 : 47 274 : text = utilities::remove_comments(text); 48 274 : const std::string separator1 = "datavar"; 49 274 : const std::string separator2 = "predvar"; 50 274 : const std::string separator3 = "expressions"; 51 : 52 274 : std::string::size_type i = text.find(separator1); 53 274 : std::string::size_type j = text.find(separator2); 54 274 : std::string::size_type k = text.find(separator3); 55 274 : if (i == std::string::npos) 56 : { 57 0 : throw std::runtime_error("Error in parse_pbes_expressions: could not find keyword " + separator1); 58 : } 59 274 : if (j == std::string::npos) 60 : { 61 0 : throw std::runtime_error("Error in parse_pbes_expressions: could not find keyword " + separator2); 62 : } 63 274 : if (k == std::string::npos) 64 : { 65 0 : throw std::runtime_error("Error in parse_pbes_expressions: could not find keyword " + separator3); 66 : } 67 : 68 274 : std::string datavar_text = text.substr(i + separator1.size(), j - i - separator1.size()); 69 274 : std::string predvar_text = text.substr(j + separator2.size(), k - j - separator2.size()); 70 274 : std::string expressions_text = text.substr(k + separator3.size()); 71 : 72 : // the generated pbes specification 73 274 : std::string pbesspec = "pbes"; 74 : 75 548 : std::vector<std::string> pwords = utilities::split(predvar_text, ";"); 76 2431 : for (const std::string& pword: pwords) 77 : { 78 2157 : if (boost::trim_copy(pword).empty()) 79 : { 80 273 : continue; 81 : } 82 1884 : std::vector<std::string> args; 83 3768 : std::vector<std::string> words = utilities::split(pword, ":"); 84 1884 : std::string var = boost::trim_copy(words[0]); 85 1884 : if (words.size() >= 2 && !boost::trim_copy(words[1]).empty()) 86 : { 87 1466 : args = utilities::split(boost::trim_copy(words[1]), "#"); 88 : } 89 3350 : for (std::string& arg: args) 90 : { 91 2932 : std::vector<std::string> w = utilities::split(arg, ","); 92 3759 : for (std::string& k: w) 93 : { 94 2293 : k = unique_prefix + utilities::number2string(unique_prefix_index++) + ": " + k; 95 : } 96 1466 : arg = boost::algorithm::join(w, ", "); 97 1466 : } 98 1884 : std::string arg; 99 1884 : if (!args.empty()) 100 : { 101 1466 : arg = "(" + boost::algorithm::join(args, ", ") + ")"; 102 : } 103 1884 : pbesspec = pbesspec + "\nmu " + var + arg + " = true;"; 104 1884 : } 105 : 106 274 : datavar_text = utilities::remove_whitespace(datavar_text); 107 274 : if (!datavar_text.empty() && datavar_text[datavar_text.size() - 1] == ';') 108 : { 109 260 : datavar_text = datavar_text.erase(datavar_text.size() - 1); 110 : } 111 274 : datavar_text = utilities::regex_replace(";", ", ", datavar_text); 112 : 113 : // add a dummy propositional variable to the pbes, that is used for the initialization 114 274 : pbesspec = pbesspec + "\nmu dummy1 = true;"; 115 : 116 : // for each expression add an equation to the pbes 117 548 : std::vector<std::string> expressions = utilities::split(expressions_text, ";"); 118 274 : if (!expressions.empty() && boost::trim_copy(expressions.back()).empty()) 119 : { 120 0 : expressions.pop_back(); 121 : } 122 549 : for (std::string& expression: expressions) 123 : { 124 : pbesspec = pbesspec 125 275 : + "\nmu " 126 550 : + unique_prefix 127 1100 : + utilities::number2string(unique_prefix_index++) 128 825 : + (datavar_text.empty() ? "" : "(") 129 550 : + datavar_text 130 825 : + (datavar_text.empty() ? "" : ")") 131 550 : + " = " 132 825 : + boost::trim_copy(expression) + ";"; 133 : } 134 : 135 : // add an initialization section to the pbes 136 274 : pbesspec = data_spec + (data_spec.empty() ? "" : "\n") + pbesspec + "\ninit dummy1;"; 137 : 138 274 : pbes p; 139 274 : std::stringstream in(pbesspec); 140 : try 141 : { 142 274 : in >> p; 143 : } 144 0 : catch (const std::runtime_error& e) 145 : { 146 0 : mCRL2log(log::error) << "parse_pbes_expression: parse error detected in the generated specification\n" 147 0 : << pbesspec 148 0 : << std::endl; 149 0 : throw e; 150 0 : } 151 : 152 274 : std::vector<pbes_expression> result; 153 549 : for (auto i = p.equations().end() - expressions.size(); i != p.equations().end(); ++i) 154 : { 155 275 : result.push_back(i->formula()); 156 : } 157 : 158 548 : return std::make_pair(result, p.data()); 159 274 : } 160 : 161 : /// \brief Parses a single pbes expression. 162 : /// \param text A string 163 : /// \param var_decl A string 164 : /// with their types.<br> 165 : /// An example of this is: 166 : /// \code 167 : /// datavar 168 : /// n: Nat; 169 : /// predvar 170 : /// X: Pos; 171 : /// Y: Nat, Bool; 172 : /// \endcode 173 : /// \param data_spec A string 174 : /// \return The parsed expression 175 : inline 176 273 : pbes_expression parse_pbes_expression(const std::string& text, const std::string& var_decl = "datavar\npredvar\n", const std::string& data_spec = "") 177 : { 178 273 : return parse_pbes_expressions(var_decl + "\nexpressions\n" + text, data_spec).first.front(); 179 : } 180 : 181 : /// \brief Parses a pbes expression. 182 : /// \param expr A string 183 : /// \param subst A string 184 : /// \param p A PBES 185 : /// \param sigma A substitution function 186 : /// \return The parsed expression 187 : template <typename SubstitutionFunction> 188 : pbes_expression parse_pbes_expression(const std::string& expr, const std::string& subst, const pbes& p, SubstitutionFunction& sigma) 189 : { 190 : data::detail::parse_substitution(subst, sigma, p.data()); 191 : 192 : std::string datavar_text; 193 : for (auto i = sigma.begin(); i != sigma.end(); ++i) 194 : { 195 : data::variable v = i->first; 196 : datavar_text = datavar_text + (i == sigma.begin() ? "" : ", ") + data::pp(v) + ": " + data::pp(v.sort()); 197 : } 198 : 199 : pbes q = p; 200 : q.initial_state() = atermpp::down_cast<propositional_variable_instantiation>(true_()); 201 : std::string pbesspec = pbes_system::pp(q); 202 : std::string init("init"); 203 : // remove the init declaration 204 : pbesspec = pbesspec.substr(0, std::find_end(pbesspec.begin(), pbesspec.end(), init.begin(), init.end()) - pbesspec.begin()); 205 : 206 : // add an equation mu dummy1(vars) = (expr = expr) 207 : pbesspec = pbesspec 208 : + "\nmu " 209 : + "dummy1" 210 : + (datavar_text.empty() ? "" : "(") 211 : + datavar_text 212 : + (datavar_text.empty() ? "" : ")") 213 : + " = " 214 : + boost::trim_copy(expr) + ";"; 215 : 216 : // add a dummy propositional variable to the pbes, that is used for the initialization 217 : pbesspec = pbesspec + "\nmu dummy2 = true;"; 218 : 219 : // add an initialization section to the pbes 220 : pbesspec = pbesspec + "\ninit dummy2;"; 221 : 222 : std::stringstream in(pbesspec); 223 : try 224 : { 225 : in >> q; 226 : } 227 : catch (const std::runtime_error& e) 228 : { 229 : mCRL2log(log::error) << "parse_pbes_expression: parse error detected in the generated specification\n" 230 : << pbesspec 231 : << std::endl; 232 : throw e; 233 : } 234 : 235 : pbes_expression result = q.equations()[q.equations().size() - 2].formula(); 236 : return result; 237 : } 238 : 239 : } // namespace pbes_system 240 : 241 : } // namespace mcrl2 242 : 243 : #endif // MCRL2_PBES_DETAIL_PARSE_H