LCOV - code coverage report
Current view: top level - data/test - replace_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 136 140 97.1 %
Date: 2024-03-08 02:52:28 Functions: 20 20 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 replace_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE replace_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/data/parse.h"
      16             : #include "mcrl2/data/replace.h"
      17             : #include "mcrl2/data/substitutions/assignment_sequence_substitution.h"
      18             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      19             : #include "mcrl2/data/substitutions/sequence_sequence_substitution.h"
      20             : 
      21             : using namespace mcrl2;
      22             : 
      23             : inline
      24         584 : data::variable bool_(const std::string& name)
      25             : {
      26        1168 :   return data::variable(core::identifier_string(name), data::sort_bool::bool_());
      27             : }
      28             : 
      29             : inline
      30             : data::variable nat(const std::string& name)
      31             : {
      32             :   return data::variable(core::identifier_string(name), data::sort_nat::nat());
      33             : }
      34             : 
      35             : inline
      36             : data::variable pos(const std::string& name)
      37             : {
      38             :   return data::variable(core::identifier_string(name), data::sort_pos::pos());
      39             : }
      40             : 
      41             : inline
      42          20 : std::vector<data::variable> variable_context()
      43             : {
      44             :   return std::vector<data::variable>
      45             :   {
      46             :     bool_("b"),
      47             :     bool_("b1"),
      48             :     bool_("b2"),
      49             :     bool_("b3"),
      50             :     bool_("b4"),
      51             :     bool_("k"),
      52             :     bool_("m"),
      53             :     bool_("n"),
      54             :     bool_("v"),
      55             :     bool_("w"),
      56             :     bool_("x"),
      57             :     bool_("y"),
      58             :     bool_("z"),
      59             :     bool_("k1"),
      60             :     bool_("m1"),
      61             :     bool_("n1"),
      62             :     bool_("v1"),
      63             :     bool_("w1"),
      64             :     bool_("x1"),
      65             :     bool_("y1"),
      66             :     bool_("z1"),
      67             :     bool_("k2"),
      68             :     bool_("m2"),
      69             :     bool_("n2"),
      70             :     bool_("v2"),
      71             :     bool_("w2"),
      72             :     bool_("x2"),
      73             :     bool_("y2"),
      74             :     bool_("z2")
      75         600 :   };
      76             : }
      77             : 
      78             : inline
      79          10 : data::data_expression parse_data_expression(const std::string& text)
      80             : {
      81          20 :   return data::parse_data_expression(text, variable_context());
      82             : };
      83             : 
      84             : /// \brief Parses a string of the form "b: Bool := v, c: Bool := !w", and adds
      85             : inline
      86          10 : data::mutable_map_substitution<> parse_substitution(const std::string& text, const std::vector<data::variable>& variables = variable_context())
      87             : {
      88          10 :   data::mutable_map_substitution<> sigma;
      89          20 :   std::vector<std::string> substitutions = utilities::split(text, ";");
      90          20 :   for (const std::string& substitution: substitutions)
      91             :   {
      92          20 :     std::vector<std::string> words = utilities::regex_split(substitution, ":=");
      93          10 :     if (words.size() != 2)
      94             :     {
      95           0 :       continue;
      96             :     }
      97          10 :     data::variable v = data::parse_variable(words[0]);
      98          10 :     data::data_expression e = data::parse_data_expression(words[1], variables);
      99          10 :     sigma[v] = e;
     100          10 :   }
     101          20 :   return sigma;
     102          10 : }
     103             : 
     104           2 : BOOST_AUTO_TEST_CASE(test_assignment_list)
     105             : {
     106             :   using namespace mcrl2::data::sort_bool;
     107             : 
     108           2 :   data::variable d1("d1", data::basic_sort("D"));
     109           2 :   data::variable d2("d2", data::basic_sort("D"));
     110           2 :   data::variable d3("d3", data::basic_sort("D"));
     111           2 :   data::variable e1("e1", data::basic_sort("D"));
     112           2 :   data::variable e2("e2", data::basic_sort("D"));
     113           2 :   data::variable e3("e3", data::basic_sort("D"));
     114             : 
     115           1 :   data::assignment_vector l;
     116           1 :   l.push_back(data::assignment(d1, e1));
     117           1 :   l.push_back(data::assignment(e1, e2));
     118           1 :   l.push_back(data::assignment(e2, e3));
     119             : 
     120           2 :   data::data_expression t  = and_(equal_to(d1, e1), not_equal_to(e2, d3));
     121           2 :   data::data_expression t0 = and_(equal_to(e1, e2), not_equal_to(e3, d3));
     122           1 :   data::data_expression t2 = data::replace_variables(t, data::assignment_sequence_substitution(data::assignment_list(l.begin(), l.end())));
     123           1 :   BOOST_CHECK(t0 == t2);
     124           1 : }
     125             : 
     126           2 : BOOST_AUTO_TEST_CASE(test_variable_replace)
     127             : {
     128             :   using namespace mcrl2::data::sort_bool;
     129             : 
     130           2 :   data::variable d1("d1", data::basic_sort("D"));
     131           2 :   data::variable d2("d2", data::basic_sort("D"));
     132           2 :   data::variable d3("d3", data::basic_sort("D"));
     133           2 :   data::variable x("x", data::basic_sort("D"));
     134           2 :   data::variable y("y", data::basic_sort("D"));
     135           2 :   data::variable z("z", data::basic_sort("D"));
     136             : 
     137           5 :   data::variable_vector variables{d1, d2, d3};
     138           5 :   data::data_expression_vector replacements{x, y, z};
     139           5 :   std::vector<data::variable> v{d1, d2, d3};
     140           5 :   std::list<data::data_expression> l{x, y, z};
     141             : 
     142           2 :   data::data_expression t  = and_(equal_to(d1, d2), not_equal_to(d2, d3));
     143           1 :   data::data_expression t1 = data::replace_variables(t, make_sequence_sequence_substitution(variables, replacements));
     144           1 :   data::data_expression t2 = data::replace_variables(t, make_sequence_sequence_substitution(v, l));
     145           1 :   BOOST_CHECK(t1 == t2);
     146             : 
     147           1 :   t = and_(equal_to(d1, d2), not_equal_to(d2, d3));
     148           1 :   BOOST_CHECK(t1 == replace_variables(t, make_sequence_sequence_substitution(variables, replacements)));
     149           1 :   BOOST_CHECK(t1 == replace_variables(t, make_sequence_sequence_substitution(variables, replacements)));
     150           1 :   BOOST_CHECK(t1 == replace_variables(t, make_sequence_sequence_substitution(v, l)));
     151           1 :   BOOST_CHECK(t1 == replace_variables(t, make_mutable_map_substitution(variables, replacements)));
     152           1 : }
     153             : 
     154           2 : BOOST_AUTO_TEST_CASE(test_replace_with_binders)
     155             : {
     156           1 :   data::mutable_map_substitution< > sigma;
     157           2 :   data::data_expression input1(data::variable("c", data::sort_bool::bool_()));
     158           2 :   data::data_expression input2(data::parse_data_expression("exists b: Bool, c: Bool. if(b, c, b)"));
     159             : 
     160           1 :   sigma[data::variable("c", data::sort_bool::bool_())] = data::sort_bool::false_();
     161             : 
     162           1 :   BOOST_CHECK(replace_free_variables(input1, sigma) == data::sort_bool::false_());
     163             : 
     164             :   // variable c is bound and should not be replaced
     165           1 :   BOOST_CHECK(replace_free_variables(input2, sigma) == input2);
     166           1 : }
     167             : 
     168           2 : BOOST_AUTO_TEST_CASE(test_variables)
     169             : {
     170           2 :   data::variable d1 = bool_("d1");
     171           2 :   data::variable d2 = bool_("d2");
     172           2 :   data::variable d3 = bool_("d3");
     173           2 :   data::variable d4 = bool_("d4");
     174           1 :   data::data_expression e1 = data::sort_bool::not_(d1);
     175           1 :   data::data_expression e2 = data::sort_bool::not_(d2);
     176           1 :   data::data_expression e3 = data::sort_bool::not_(d3);
     177             : 
     178           1 :   data::mutable_map_substitution<> sigma;
     179           1 :   sigma[d1] = e1;
     180           1 :   sigma[d2] = e2;
     181           1 :   sigma[d3] = e3;
     182             : 
     183             :   // the variable in an assignment is not replaced by replace_free_variables
     184           1 :   data::assignment a(d1, d4);
     185           1 :   data::assignment b = replace_free_variables(a, sigma);
     186           1 :   BOOST_CHECK(b == a);
     187             : 
     188             :   // the variable in an assignment is not replaced by replace_variables
     189           1 :   data::assignment c = replace_variables(a, sigma);
     190           1 :   BOOST_CHECK(c == a);
     191             : 
     192             :   // the variable d1 in the right hand side is replaced by replace_free_variables, since
     193             :   // we do not consider the left hand side a binding variable
     194           1 :   a = data::assignment(d1, data::sort_bool::and_(d1, d2));
     195           1 :   b = replace_free_variables(a, sigma);
     196           1 :   BOOST_CHECK(b == data::assignment(d1, data::sort_bool::and_(e1, e2)));
     197             : 
     198             :   // the variable d1 in the right hand side is replaced by replace_free_variables
     199           1 :   c = replace_variables(a, sigma);
     200           1 :   BOOST_CHECK(c == data::assignment(d1, data::sort_bool::and_(e1, e2)));
     201             : 
     202             :   // this will lead to an assertion failure, because an attempt will be made to store
     203             :   // a data expression in a variable
     204           1 :   sigma[d1] = data::sort_bool::and_(d1, d2);
     205             :   // data::data_expression z1 = replace_variables(d1, sigma);
     206             : 
     207             :   // therefore one should first convert d1 to a data expression:
     208           2 :   data::data_expression z2 = replace_variables(data::data_expression(d1), sigma);
     209           1 :   BOOST_CHECK(z2 == data::sort_bool::and_(d1, d2));
     210           1 : }
     211             : 
     212          10 : void check_result(const std::string& expression, const std::string& result, const std::string& expected_result, const std::string& title)
     213             : {
     214          10 :   if (result != expected_result)
     215             :   {
     216           0 :     std::cout << "--- failure in " << title << " ---" << std::endl;
     217           0 :     std::cout << "expression      = " << expression << std::endl;
     218           0 :     BOOST_CHECK_EQUAL(result, expected_result);
     219             :   }
     220          10 : }
     221             : 
     222          10 : void test_replace_variables_capture_avoiding(const std::string& x_text, const std::string& sigma_text, const std::string& expected_result)
     223             : {
     224          10 :   data::data_expression x = parse_data_expression(x_text);
     225          10 :   data::mutable_map_substitution<> sigma = parse_substitution(sigma_text);
     226          10 :   std::string result = data::pp(data::replace_variables_capture_avoiding(x, sigma));
     227          10 :   check_result(x_text + " sigma = " + sigma_text, result, expected_result, "replace_variables_capture_avoiding");
     228          10 : }
     229             : 
     230           2 : BOOST_AUTO_TEST_CASE(replace_variables_capture_avoiding_test)
     231             : {
     232           1 :   test_replace_variables_capture_avoiding("v", "v: Bool := w", "w");
     233           1 :   test_replace_variables_capture_avoiding("forall x: Bool . x => y", "x: Bool := z", "forall x1: Bool. x1 => y");
     234           1 :   test_replace_variables_capture_avoiding("forall x: Bool . x => y", "y: Bool := z", "forall x1: Bool. x1 => z");
     235           1 :   test_replace_variables_capture_avoiding("forall x: Bool . x => y", "y: Bool := x", "forall x1: Bool. x1 => x");
     236           1 :   test_replace_variables_capture_avoiding("forall x: Bool . x => x1 => y", "y: Bool := x", "forall x2: Bool. x2 => x1 => x");
     237           1 :   test_replace_variables_capture_avoiding("x => x1 => y whr x = y end", "y: Bool := x", "x2 => x1 => x whr x2 = x end");
     238           1 :   test_replace_variables_capture_avoiding("forall n: Bool. n => forall k: Bool. k => m", "m: Bool := n", "forall n1: Bool. n1 => (forall k1: Bool. k1 => n)");
     239           1 :   test_replace_variables_capture_avoiding("forall n: Bool. n => forall n: Bool. n => m", "m: Bool := n", "forall n1: Bool. n1 => (forall n2: Bool. n2 => n)");
     240           1 :   test_replace_variables_capture_avoiding("forall n: Bool. n => forall k: Bool. k => m", "m: Bool := n", "forall n1: Bool. n1 => (forall k1: Bool. k1 => n)");
     241           1 :   test_replace_variables_capture_avoiding("forall n: Bool. n => forall n: Bool. n => m", "m: Bool := n", "forall n1: Bool. n1 => (forall n2: Bool. n2 => n)");
     242           1 : }
     243             : 
     244           2 : BOOST_AUTO_TEST_CASE(test_replace_free_variables)
     245             : {
     246           1 :   data::mutable_map_substitution<> sigma;
     247           2 :   data::variable x("x", data::sort_bool::bool_());
     248           1 :   data::data_expression y = data::sort_bool::not_(x);
     249           1 :   sigma[x] = y;
     250           1 :   data::assignment a(x, x);
     251           1 :   data::assignment b(x, y);
     252           1 :   data::assignment c = data::replace_free_variables(a, sigma);
     253           1 :   BOOST_CHECK(b == c);
     254             : 
     255           2 :   data::assignment_list va{a};
     256           2 :   data::assignment_list vb{b};
     257           1 :   data::assignment_list vc = data::replace_free_variables(va, sigma);
     258           1 :   BOOST_CHECK_EQUAL(vb, vc);
     259           1 : }
     260             : 
     261           2 : BOOST_AUTO_TEST_CASE(test_ticket_1209)
     262             : {
     263           1 :   std::string text = "n whr n = m, m = 3 end whr m = 255 end";
     264           1 :   std::string expected_result = "n1 whr n1 = m2, m3 = 3 end whr m2 = 255 end";
     265           1 :   data::data_expression x = data::parse_data_expression(text);
     266           1 :   data::mutable_map_substitution<> sigma;
     267           2 :   data::variable m("m", data::sort_pos::pos());
     268           2 :   data::variable m1("m1", data::sort_pos::pos());
     269           1 :   sigma[m] = m1;
     270           1 :   data::data_expression x1 = data::replace_variables_capture_avoiding(x, sigma);
     271           1 :   std::string result = data::pp(x1);
     272           1 :   BOOST_CHECK_EQUAL(result, expected_result);
     273           1 : }

Generated by: LCOV version 1.14