LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/detail - parse.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 64 74 86.5 %
Date: 2024-03-08 02:52:28 Functions: 2 2 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/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

Generated by: LCOV version 1.14