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 find_test.cpp
      10             : /// \brief Test for find functions.
      11             : 
      12             : #define BOOST_TEST_MODULE find_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/core/detail/print_utility.h"
      16             : #include "mcrl2/data/parse.h"
      17             : 
      18             : using namespace mcrl2;
      19             : 
      20             : inline
      21          56 : data::variable bool_(const std::string& name)
      22             : {
      23         112 :   return data::variable(core::identifier_string(name), data::sort_bool::bool_());
      24             : }
      25             : 
      26             : inline
      27          54 : data::variable nat(const std::string& name)
      28             : {
      29         108 :   return data::variable(core::identifier_string(name), data::sort_nat::nat());
      30             : }
      31             : 
      32             : inline
      33          54 : data::variable pos(const std::string& name)
      34             : {
      35         108 :   return data::variable(core::identifier_string(name), data::sort_pos::pos());
      36             : }
      37             : 
      38             : inline
      39          10 : data::data_expression parse_data_expression(const std::string& text)
      40             : {
      41             :   std::vector<data::variable> variable_context
      42             :   {
      43             :     nat("n"),
      44             :     nat("n1"),
      45             :     nat("n2"),
      46             :     nat("n3"),
      47             :     nat("n4"),
      48             :     bool_("b"),
      49             :     bool_("b1"),
      50             :     bool_("b2"),
      51             :     bool_("b3"),
      52             :     bool_("b4"),
      53             :     pos("p"),
      54             :     pos("p1"),
      55             :     pos("p2"),
      56             :     pos("p3"),
      57             :     pos("p4")
      58         180 :   };
      59          20 :   return data::parse_data_expression(text, variable_context);
      60          10 : };
      61             : 
      62             : template <typename T>
      63          18 : std::string print_set(const std::set<T>& v)
      64             : {
      65          18 :   std::set<std::string> s;
      66          52 :   for (const T& v_i: v)
      67             :   {
      68          34 :     s.insert(data::pp(v_i));
      69             :   }
      70          36 :   return core::detail::print_set(s);
      71          18 : }
      72             : 
      73           2 : BOOST_AUTO_TEST_CASE(test_containers)
      74             : {
      75           2 :   data::variable b = bool_("b");
      76           2 :   data::variable c = bool_("c");
      77           5 :   data::variable_vector v{b, c};
      78           1 :   BOOST_CHECK_EQUAL(print_set(find_all_variables(v)), "{ b, c }");
      79           1 :   BOOST_CHECK(data::search_variable(v, b));
      80           1 :   BOOST_CHECK(data::search_variable(v, c));
      81             : 
      82           4 :   data::variable_list l{b, c};
      83           1 :   BOOST_CHECK_EQUAL(print_set(find_all_variables(l)), "{ b, c }");
      84           1 :   BOOST_CHECK(data::search_variable(l, b));
      85           1 :   BOOST_CHECK(data::search_variable(l, c));
      86           1 : }
      87             : 
      88           2 : BOOST_AUTO_TEST_CASE(test_find)
      89             : {
      90             :   using utilities::detail::contains;
      91             : 
      92           2 :   data::variable n1 = nat("n1");
      93           2 :   data::variable n2 = nat("n2");
      94           2 :   data::variable n3 = nat("n3");
      95           2 :   data::variable n4 = nat("n4");
      96             : 
      97           2 :   data::variable b1 = bool_("b1");
      98           2 :   data::variable b2 = bool_("b2");
      99           2 :   data::variable b3 = bool_("b3");
     100           2 :   data::variable b4 = bool_("b4");
     101             : 
     102           2 :   data::variable p1 = pos("p1");
     103           2 :   data::variable p2 = pos("p2");
     104           2 :   data::variable p3 = pos("p3");
     105           2 :   data::variable p4 = pos("p4");
     106             : 
     107           6 :   std::set<data::variable> S{b1, p1, n1};
     108           1 :   BOOST_CHECK_EQUAL(print_set(find_all_variables(S)), "{ b1, n1, p1 }");
     109           1 :   BOOST_CHECK_EQUAL(print_set(find_sort_expressions(S)), "{ Bool, Nat, Pos }");
     110           1 :   BOOST_CHECK(search_variable(S, n1));
     111           1 :   BOOST_CHECK(!search_variable(S, n2));
     112             : 
     113           6 :   std::vector<data::variable> V{b1, p1, n1};
     114           1 :   BOOST_CHECK_EQUAL(print_set(find_all_variables(S)), "{ b1, n1, p1 }");
     115           1 :   BOOST_CHECK(search_variable(V, n1));
     116           1 :   BOOST_CHECK(!search_variable(V, n2));
     117             : 
     118           4 :   data::sort_expression_vector domain {data::sort_pos::pos(), data::sort_bool::bool_()};
     119           1 :   data::sort_expression sexpr = data::function_sort(domain, data::sort_nat::nat());
     120           2 :   data::variable q1(core::identifier_string("q1"), sexpr);
     121           1 :   BOOST_CHECK_EQUAL(print_set(find_sort_expressions(q1)), "{ Bool, Nat, Pos, Pos # Bool -> Nat }");
     122             : 
     123           2 :   data::data_expression x = parse_data_expression("(n1 == n2) && (n2 != n3)");
     124           1 :   BOOST_CHECK_EQUAL(print_set(find_all_variables(x)), "{ n1, n2, n3 }");
     125           1 :   BOOST_CHECK_EQUAL(print_set(find_free_variables(x)), "{ n1, n2, n3 }");
     126           1 :   BOOST_CHECK(search_variable(x, n1));
     127           1 :   BOOST_CHECK(search_variable(x, n2));
     128           1 :   BOOST_CHECK(search_variable(x, n3));
     129           1 :   BOOST_CHECK(!search_variable(x, n4));
     130             : 
     131           1 :   std::set<data::sort_expression> Z;
     132           1 :   find_sort_expressions(q1, std::inserter(Z, Z.end()));
     133           1 :   find_sort_expressions(S, std::inserter(Z, Z.end()));
     134           1 :   BOOST_CHECK_EQUAL(print_set(Z), "{ Bool, Nat, Pos, Pos # Bool -> Nat }");
     135           1 : }
     136             : 
     137           2 : BOOST_AUTO_TEST_CASE(find_all_variables_test)
     138             : {
     139           5 :   auto all_variables = [&](const std::string& text)
     140             :   {
     141          10 :     return print_set(data::find_all_variables(parse_data_expression(text)));
     142             :   };
     143             : 
     144           1 :   BOOST_CHECK_EQUAL(all_variables("n"), "{ n }");
     145           1 :   BOOST_CHECK_EQUAL(all_variables("exists n: Nat. (n == n)"), "{ n }");
     146           1 :   BOOST_CHECK_EQUAL(all_variables("exists n: Nat. true"), "{ n }");
     147           1 :   BOOST_CHECK_EQUAL(all_variables("2 whr n = n end"), "{ n }");
     148           1 :   BOOST_CHECK_EQUAL(all_variables("2 whr p = 3 end"), "{ p }");
     149           1 : }
     150             : 
     151           2 : BOOST_AUTO_TEST_CASE(find_free_variables_test)
     152             : {
     153           4 :   auto free_variables = [&](const std::string& text)
     154             :   {
     155           8 :     return print_set(data::find_free_variables(parse_data_expression(text)));
     156             :   };
     157             : 
     158           1 :   BOOST_CHECK_EQUAL(free_variables("n"), "{ n }");
     159           1 :   BOOST_CHECK_EQUAL(free_variables("exists n: Nat. (n == n)"), "{  }");
     160           1 :   BOOST_CHECK_EQUAL(free_variables("2 whr n = n end"), "{ n }");
     161           1 :   BOOST_CHECK_EQUAL(free_variables("2 whr p = 3 end"), "{  }");
     162           1 : }