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

Generated by: LCOV version 1.13