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 replace_test.cpp
      10             : /// \brief Regression test for replace functions
      11             : 
      12             : #define BOOST_TEST_MODULE replace_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      16             : #include "mcrl2/process/parse.h"
      17             : #include "mcrl2/process/replace.h"
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::process;
      21             : 
      22           1 : void check_result(const std::string& expression, const std::string& result, const std::string& expected_result, const std::string& title)
      23             : {
      24           1 :   if (result != expected_result)
      25             :   {
      26           0 :     std::cout << "--- failure in " << title << " ---" << std::endl;
      27           0 :     std::cout << "expression      = " << expression << std::endl;
      28           0 :     BOOST_CHECK_EQUAL(result, expected_result);
      29             :   }
      30           1 : }
      31             : 
      32             : inline
      33          24 : data::variable make_bool(const std::string& s)
      34             : {
      35          24 :   return data::variable(s, data::sort_bool::bool_());
      36             : }
      37             : 
      38             : inline
      39           1 : std::vector<data::variable> variable_context()
      40             : {
      41           1 :   std::vector<data::variable> result;
      42           1 :   result.push_back(make_bool("k"));
      43           1 :   result.push_back(make_bool("m"));
      44           1 :   result.push_back(make_bool("n"));
      45           1 :   result.push_back(make_bool("v"));
      46           1 :   result.push_back(make_bool("w"));
      47           1 :   result.push_back(make_bool("x"));
      48           1 :   result.push_back(make_bool("y"));
      49           1 :   result.push_back(make_bool("z"));
      50           1 :   result.push_back(make_bool("k1"));
      51           1 :   result.push_back(make_bool("m1"));
      52           1 :   result.push_back(make_bool("n1"));
      53           1 :   result.push_back(make_bool("v1"));
      54           1 :   result.push_back(make_bool("w1"));
      55           1 :   result.push_back(make_bool("x1"));
      56           1 :   result.push_back(make_bool("y1"));
      57           1 :   result.push_back(make_bool("z1"));
      58           1 :   result.push_back(make_bool("k2"));
      59           1 :   result.push_back(make_bool("m2"));
      60           1 :   result.push_back(make_bool("n2"));
      61           1 :   result.push_back(make_bool("v2"));
      62           1 :   result.push_back(make_bool("w2"));
      63           1 :   result.push_back(make_bool("x2"));
      64           1 :   result.push_back(make_bool("y2"));
      65           1 :   result.push_back(make_bool("z2"));
      66           1 :   return result;
      67           0 : }
      68             : 
      69             : inline
      70           1 : process_expression parse_expression(const std::string& text)
      71             : {
      72             :   std::string DATA_DECL =
      73             :     "glob k, m, n, k1, m1, n1, k2, m2, n2: Bool;\n"
      74           1 :     "act a, b, c: Bool;                         \n"
      75             :     ;
      76           1 :   std::string PROC_DECL = "proc P(n: Nat); proc Q(n: Nat); proc R(n: Nat); proc S(n: Nat);\n";
      77           2 :   return process::parse_process_expression(text, DATA_DECL, PROC_DECL);
      78           1 : }
      79             : 
      80             : /// \brief Parses a string of the form "b: Bool := v, c: Bool := !w", and adds
      81             : inline
      82           1 : data::mutable_map_substitution<> parse_substitution(const std::string& text, const std::vector<data::variable>& variables = variable_context())
      83             : {
      84           1 :   data::mutable_map_substitution<> sigma;
      85           2 :   std::vector<std::string> substitutions = utilities::split(text, ";");
      86           2 :   for (auto & substitution : substitutions)
      87             :   {
      88           2 :     std::vector<std::string> words = utilities::regex_split(substitution, ":=");
      89           1 :     if (words.size() != 2)
      90             :     {
      91           0 :       continue;
      92             :     }
      93           1 :     data::variable v = data::parse_variable(words[0]);
      94           1 :     data::data_expression e = data::parse_data_expression(words[1], variables);
      95           1 :     sigma[v] = e;
      96           1 :   }
      97           2 :   return sigma;
      98           1 : }
      99             : 
     100             : // Returns the free variables in the right hand side of sigma.
     101           0 : std::set<data::variable> sigma_variables(const data::mutable_map_substitution<>& sigma)
     102             : {
     103           0 :   std::set<data::variable> result;
     104           0 :   for (const auto & i : sigma)
     105             :   {
     106           0 :     std::set<data::variable> V = data::find_free_variables(i.second);
     107           0 :     V.erase(i.first);
     108           0 :     result.insert(V.begin(), V.end());
     109           0 :   }
     110           0 :   return result;
     111           0 : }
     112             : 
     113           1 : void test_replace_variables_capture_avoiding(const std::string& x_text, const std::string& sigma_text, const std::string& expected_result)
     114             : {
     115           1 :   process_expression x = parse_expression(x_text);
     116           1 :   data::mutable_map_substitution<> sigma = parse_substitution(sigma_text);
     117           1 :   std::string result = process::pp(process::replace_variables_capture_avoiding(x, sigma));
     118           1 :   check_result(x_text + " sigma = " + sigma_text, result, expected_result, "replace_variables_capture_avoiding");
     119           1 : }
     120             : 
     121           2 : BOOST_AUTO_TEST_CASE(replace_variables_capture_avoiding_test)
     122             : {
     123           1 :   test_replace_variables_capture_avoiding("sum n: Bool. a(n) . sum k: Bool. a(k) . a(m)", "m: Bool := n", "sum n1: Bool. a(n1) . (sum k1: Bool. a(k1) . a(n))");
     124           1 : }
     125             : 
     126           2 : BOOST_AUTO_TEST_CASE(process_instance_assignment_test)
     127             : {
     128             :   std::string text =
     129             :     "proc P(b: Bool, c: Bool) = P(c = true); \n"
     130             :     "                                        \n"
     131           1 :     "init P(true, true);                     \n"
     132             :     ;
     133             : 
     134           1 :   process_specification p = parse_process_specification(text);
     135           1 :   data::mutable_map_substitution<> sigma;
     136           2 :   data::variable b("b", data::sort_bool::bool_());
     137           2 :   data::variable c("c", data::sort_bool::bool_());
     138           1 :   sigma[c] = data::sort_bool::false_();
     139             : 
     140           1 :   process_expression x = p.equations().front().expression();
     141           1 :   process_expression x1 = process::replace_variables_capture_avoiding(x, sigma);
     142           1 :   std::cerr << process::pp(x1) << std::endl;
     143           1 :   BOOST_CHECK(process::pp(x1) == "P(c = true)");
     144             : 
     145           1 :   sigma[b] = data::sort_bool::false_();
     146           1 :   process_expression x2 = process::replace_variables_capture_avoiding(x, sigma);
     147           1 :   std::cerr << process::pp(x2) << std::endl;
     148           1 :   BOOST_CHECK(process::pp(x2) == "P(b = false, c = true)");
     149           1 : }
     150             : 
     151           2 : BOOST_AUTO_TEST_CASE(replace_process_identifiers_test)
     152             : {
     153             :   std::string text =
     154             :     "proc P(b: Bool, c: Bool) = P(c = true) . P(false, false); \n"
     155             :     "proc Q(b: Bool, c: Bool) = P(c = true);                   \n"
     156             :     "proc R(b: Bool, c: Bool) = Q(c = true) . Q(false, false); \n"
     157             :     "                                                          \n"
     158           1 :     "init P(true, true);                                       \n"
     159             :     ;
     160             : 
     161           1 :   process_specification p = parse_process_specification(text);
     162           1 :   process_equation eqP = p.equations()[0];
     163           1 :   process_equation eqQ = p.equations()[1];
     164           1 :   process_equation eqR = p.equations()[2];
     165             : 
     166           2 :   process_expression rhs = replace_process_identifiers(eqP.expression(), process_identifier_assignment(eqP.identifier(), eqQ.identifier()));
     167           1 :   BOOST_CHECK(rhs == eqR.expression());
     168           1 : }