LCOV - code coverage report
Current view: top level - process/test - alphabet_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 211 217 97.2 %
Date: 2024-03-08 02:52:28 Functions: 47 47 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 alphabet_test.cpp
      10             : /// \brief Test for alphabet reduction.
      11             : 
      12             : #define BOOST_TEST_MODULE alphabet_test
      13             : #include <boost/algorithm/string/predicate.hpp>
      14             : #include <boost/test/included/unit_test.hpp>
      15             : 
      16             : #include "mcrl2/process/alphabet_reduce.h"
      17             : #include "mcrl2/process/detail/alphabet_intersection.h"
      18             : #include "mcrl2/process/detail/alphabet_parse.h"
      19             : #include "mcrl2/process/detail/alphabet_push_block.h"
      20             : 
      21             : using namespace mcrl2;
      22             : using namespace mcrl2::process;
      23             : 
      24             : struct LogDebug
      25             : {
      26           1 :   LogDebug()
      27             :   {
      28           1 :     log::logger::set_reporting_level(log::debug);
      29           1 :   }
      30             : };
      31             : BOOST_GLOBAL_FIXTURE(LogDebug);
      32             : 
      33             : inline
      34             : multi_action_name name(const process::action& x)
      35             : {
      36             :   multi_action_name result;
      37             :   result.insert(x.label().name());
      38             :   return result;
      39             : }
      40             : 
      41             : inline
      42             : multi_action_name name(const core::identifier_string& x)
      43             : {
      44             :   multi_action_name result;
      45             :   result.insert(x);
      46             :   return result;
      47             : }
      48             : 
      49         115 : std::string print(const multi_action_name& alpha)
      50             : {
      51         115 :   if (alpha.empty())
      52             :   {
      53           3 :     return "tau";
      54             :   }
      55         112 :   std::ostringstream out;
      56         311 :   for (const auto & i : alpha)
      57             :   {
      58         199 :     out << std::string(i);
      59             :   }
      60         112 :   std::string result = out.str();
      61         112 :   std::sort(result.begin(), result.end());
      62         112 :   return result;
      63         112 : }
      64             : 
      65          47 : std::string print(const multi_action_name_set& A, bool A_includes_subsets = false)
      66             : {
      67          47 :   std::multiset<std::string> V;
      68         162 :   for (const auto & i : A)
      69             :   {
      70         115 :     V.insert(print(i));
      71             :   }
      72         141 :   return core::detail::print_set(V, "", false, false) + (A_includes_subsets ? "@" : "");
      73          47 : }
      74             : 
      75          12 : std::string print(const allow_set& x)
      76             : {
      77          12 :   return print(x.A, x.A_includes_subsets);
      78             : }
      79             : 
      80           2 : BOOST_AUTO_TEST_CASE(test_print)
      81             : {
      82           2 :   auto [A, dummy] = detail::parse_simple_multi_action_name_set("{a}");
      83           1 :   multi_action_name tau;
      84           1 :   A.insert(tau);
      85           1 :   std::cout << print(A) << std::endl;
      86           1 :   BOOST_CHECK(print(A) == "{a, tau}");
      87           1 : }
      88             : 
      89           2 : BOOST_AUTO_TEST_CASE(test_parse)
      90             : {
      91           1 :   multi_action_name_set B;
      92             :   bool dummy;
      93           1 :   std::tie(B, dummy) = detail::parse_simple_multi_action_name_set("{a, ab}");
      94           1 :   std::cout << "B = " << print(B) << std::endl;
      95           1 :   BOOST_CHECK(print(B) == "{a, ab}");
      96           1 : }
      97             : 
      98           2 : BOOST_AUTO_TEST_CASE(test_includes)
      99             : {
     100           2 :   multi_action_name alpha = detail::parse_simple_multi_action_name("abb");
     101           2 :   multi_action_name beta = detail::parse_simple_multi_action_name("aabb");
     102           1 :   BOOST_CHECK(!alphabet_operations::includes(alpha, beta));
     103           1 :   BOOST_CHECK(alphabet_operations::includes(beta, alpha));
     104           1 : }
     105             : 
     106           2 : BOOST_AUTO_TEST_CASE(test_alphabet_reduce)
     107             : {
     108             :   std::string text =
     109             :     "act a;        \n"
     110             :     "proc P = a.P; \n"
     111           1 :     "init P;       \n"
     112             :     ;
     113           1 :   process_specification procspec = parse_process_specification(text);
     114           1 :   alphabet_reduce(procspec);
     115           1 : }
     116             : 
     117          44 : void check_result(const std::string& expression, const std::string& result, const std::string& expected_result, const std::string& title)
     118             : {
     119          44 :   if (result != expected_result)
     120             :   {
     121           0 :     std::cout << "--- failure in " << title << " ---" << std::endl;
     122           0 :     std::cout << "expression      = " << expression << std::endl;
     123           0 :     std::cout << "result          = " << result << std::endl;
     124           0 :     std::cout << "expected result = " << expected_result << std::endl;
     125           0 :     BOOST_CHECK(result == expected_result);
     126             :   }
     127          44 : }
     128             : 
     129           7 : void test_alphabet(const std::string& expression, const std::string& expected_result, const std::string& equations = "")
     130             : {
     131          14 :   std::string text = "act a, b, c, d;\n" + equations + "\ninit " + expression + ";\n";
     132           7 :   process_specification procspec = parse_process_specification(text);
     133           7 :   multi_action_name_set A = alphabet(procspec.init(), procspec.equations());
     134           7 :   std::string result = print(A);
     135           7 :   check_result(expression, result, expected_result, "alphabet");
     136           7 : }
     137             : 
     138           2 : BOOST_AUTO_TEST_CASE(test_alphabet1)
     139             : {
     140           1 :   test_alphabet("a || b", "{a, ab, b}");
     141           1 :   test_alphabet("allow({ a, a | b }, a || b)", "{a, ab}");
     142           1 :   test_alphabet("allow({a}, a || a)", "{a}");
     143           1 :   test_alphabet("a", "{a}");
     144           1 :   test_alphabet("c|c", "{cc}");
     145           1 :   test_alphabet("a.c|c", "{a, cc}");
     146           1 :   test_alphabet("tau.a", "{a, tau}");
     147           1 : }
     148             : 
     149             : template <typename Operation>
     150           7 : void test_alphabet_operation(const std::string& text1, const std::string& text2, const std::string& expected_result, Operation op, const std::string& title)
     151             : {
     152             :   bool dummy;
     153           7 :   multi_action_name_set A1, A2;
     154           7 :   std::tie(A1, dummy) = detail::parse_simple_multi_action_name_set(text1);
     155           7 :   std::tie(A2, dummy) = detail::parse_simple_multi_action_name_set(text2);
     156           7 :   multi_action_name_set A3 = op(A1, A2);
     157           7 :   std::string result = print(A3);
     158           7 :   check_result(text1 + ", " + text2, result, expected_result, title);
     159           7 : }
     160             : 
     161           2 : BOOST_AUTO_TEST_CASE(test_alphabet_operations)
     162             : {
     163             :   using namespace alphabet_operations;
     164           1 :   test_alphabet_operation("{a}", "{b}", "{ab}", concat, "concat");
     165           1 :   test_alphabet_operation("{ab}", "{b, c}", "{abb, abc}", concat, "concat");
     166           1 :   test_alphabet_operation("{ab, aabc}", "{b, bc}", "{a, aa, aabc, aac, ab}", left_arrow1, "left_arrow1");
     167           1 :   test_alphabet_operation("{aa, b}", "{a}", "{a, aa, b}", left_arrow1, "left_arrow1");
     168           1 :   test_alphabet_operation("{ab, b}", "{b}", "{a, ab, b}", left_arrow1, "left_arrow1"); // N.B. tau is excluded!
     169           1 :   test_alphabet_operation("{bc}", "{c}", "{b, bc}", left_arrow1, "left_arrow1");
     170           1 :   test_alphabet_operation("{a}", "{a}", "{a}", left_arrow1, "left_arrow1");
     171           1 : }
     172             : 
     173           1 : void test_push_allow(const std::string& expression, const std::string& Atext, const std::string& expected_result, const std::string& equations = "")
     174             : {
     175           2 :   std::string text = "act a, b, c, d;\n" + equations + "\ninit " + expression + ";\n";
     176           1 :   process_specification procspec = parse_process_specification(text);
     177           1 :   auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
     178           1 :   data::set_identifier_generator id_generator;
     179             : 
     180           1 :   std::map<process_identifier, multi_action_name_set> pcrl_equation_cache = detail::compute_pcrl_equation_cache(procspec.equations());
     181           1 :   process::detail::push_allow_cache W(id_generator, pcrl_equation_cache);
     182           2 :   process::detail::push_allow_node node = process::detail::push_allow(procspec.init(), allow_set(A, A_includes_subsets), procspec.equations(), W);
     183           1 :   std::string result = process::pp(node.expression);
     184           1 :   check_result(expression, result, expected_result, "push_allow");
     185           1 : }
     186             : 
     187           2 : BOOST_AUTO_TEST_CASE(test_push_allow1)
     188             : {
     189           1 :   test_push_allow("a || a", "{a}", "allow({a}, a || a)");
     190           1 : }
     191             : 
     192             : template <typename Operation>
     193           4 : void test_comm_operation(const std::string& comm_text, const std::string& Atext, const std::string& expected_result, Operation op, const std::string& title)
     194             : {
     195           4 :   communication_expression_list C = detail::parse_comm_set(comm_text);
     196           4 :   auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
     197           4 :   multi_action_name_set A1 = op(C, A, A_includes_subsets);
     198           4 :   std::string result = print(A1, A_includes_subsets);
     199           4 :   check_result(comm_text + ", " + Atext, result, expected_result, title);
     200             : 
     201           4 :   if (title == "comm_inverse")
     202             :   {
     203           4 :     allow_set A2 = alphabet_operations::comm_inverse(C, allow_set(A, A_includes_subsets));
     204           2 :     std::string result_allow = print(A2);
     205           2 :     check_result(comm_text + ", " + Atext, result_allow, expected_result, title + "<allow>");
     206           2 :   }
     207           4 : }
     208             : 
     209           2 : BOOST_AUTO_TEST_CASE(test_comm_operations)
     210             : {
     211             :   // resolve ambiguity
     212           2 :   auto comm_inverse = [](const communication_expression_list& C, const multi_action_name_set& A, bool A_includes_subsets) { return alphabet_operations::comm_inverse(C, A, A_includes_subsets); };
     213           1 :   test_comm_operation("{a|b -> c}", "{c}", "{ab, c}", comm_inverse, "comm_inverse");
     214           1 :   test_comm_operation("{a|a -> b}", "{b, bb}", "{aa, aaaa, aab, b, bb}", comm_inverse, "comm_inverse");
     215           1 :   test_comm_operation("{a|b -> c}", "{ab, aab, aabb, abd}", "{aab, aabb, ab, abc, abd, ac, c, cc, cd}", alphabet_operations::comm, "comm");
     216           1 :   test_comm_operation("{a|b -> c}", "{ab, aab, aabb, abd}@", "{aab, aabb, ab, abc, abd, ac, c, cc, cd}@", alphabet_operations::comm, "comm");
     217           1 : }
     218             : 
     219             : template <typename Operation>
     220           8 : void test_rename_operation(const std::string& rename_text, const std::string& Atext, const std::string& expected_result, Operation op, const std::string& title)
     221             : {
     222           8 :   rename_expression_list R = detail::parse_rename_set(rename_text);
     223           8 :   auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
     224           8 :   multi_action_name_set A1 = op(R, A, A_includes_subsets);
     225           8 :   std::string result = print(A1, A_includes_subsets);
     226           8 :   check_result(rename_text + ", " + Atext, result, expected_result, title);
     227             : 
     228           8 :   if (title == "rename_inverse")
     229             :   {
     230          12 :     allow_set A2 = alphabet_operations::rename_inverse(R, allow_set(A, A_includes_subsets));
     231           6 :     std::string result_allow = print(A2);
     232           6 :     check_result(rename_text + ", " + Atext, result_allow, expected_result, title + "<allow>");
     233           6 :   }
     234           8 : }
     235             : 
     236           2 : BOOST_AUTO_TEST_CASE(test_rename_operations)
     237             : {
     238             :   // resolve ambiguity
     239           6 :   auto rename_inverse = [](const rename_expression_list& R, const multi_action_name_set& A, bool A_includes_subsets) { return alphabet_operations::rename_inverse(R, A, A_includes_subsets); };
     240           1 :   test_rename_operation("{a -> b, c -> d}", "{ab, aacc}", "{bb, bbdd}", alphabet_operations::rename, "rename");
     241           1 :   test_rename_operation("{a -> b, c -> d}", "{ab, aacc}@", "{bb, bbdd}@", alphabet_operations::rename, "rename");
     242           1 :   test_rename_operation("{a -> b, c -> d}", "{abd, bcdd}", "{}", rename_inverse, "rename_inverse");
     243           1 :   test_rename_operation("{a -> b}", "{b, bb}", "{a, aa, ab, b, bb}", rename_inverse, "rename_inverse");
     244           1 :   test_rename_operation("{a -> b}", "{bb}@", "{aa, ab, bb}@", rename_inverse, "rename_inverse");
     245           1 :   test_rename_operation("{a -> b}", "{b}", "{a, b}", rename_inverse, "rename_inverse");
     246           1 :   test_rename_operation("{a -> b}", "{a}", "{}", rename_inverse, "rename_inverse");
     247           1 :   test_rename_operation("{b -> a}", "{a, bc}@", "{a, b, c}@", rename_inverse, "rename_inverse");
     248           1 : }
     249             : 
     250             : template <typename Operation>
     251           1 : void test_hide_operation(const std::string& hide_text, const std::string& Atext, const std::string& expected_result, Operation op, const std::string& title)
     252             : {
     253           1 :   core::identifier_string_list I = detail::parse_block_set(hide_text);
     254           1 :   auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
     255           1 :   multi_action_name_set A1 = op(I, A, A_includes_subsets);
     256           1 :   std::string result = print(A1, A_includes_subsets);
     257           1 :   check_result(hide_text + ", " + Atext, result, expected_result, title);
     258           1 : }
     259             : 
     260           2 : BOOST_AUTO_TEST_CASE(test_hide_operations)
     261             : {
     262           1 :   auto hide_inverse = [](const core::identifier_string_list& I, const multi_action_name_set& A, bool A_includes_subsets) { return alphabet_operations::hide_inverse(I, A, A_includes_subsets); };
     263           1 :   test_hide_operation("{b}", "{ab}", "{}", hide_inverse, "hide_inverse");
     264           1 : }
     265             : 
     266           2 : void test_allow(const std::string& allow_text, const std::string& Atext, const std::string& expected_result, const std::string& title)
     267             : {
     268           2 :   action_name_multiset_list V = detail::parse_allow_set(allow_text);
     269           2 :   auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
     270           2 :   multi_action_name_set A1 = alphabet_operations::allow(V, A, A_includes_subsets);
     271           2 :   std::string result = print(A1);
     272           2 :   check_result(allow_text + ", " + Atext, result, expected_result, title);
     273             : 
     274           4 :   allow_set A2 = alphabet_operations::allow(V, allow_set(A, A_includes_subsets));
     275           2 :   std::string result_allow = print(A2);
     276           2 :   check_result(allow_text + ", " + Atext, result_allow, expected_result, title + "<allow>");
     277           2 : }
     278             : 
     279           2 : BOOST_AUTO_TEST_CASE(test_allow1)
     280             : {
     281           1 :   test_allow("{a|b, a|b|b, c}", "{ab, abbc, c}", "{ab, c}", "allow");
     282           1 :   test_allow("{a, b, c}", "{ab}@", "{a, b}", "allow");
     283             :   // test_allow("{a|b}", "{a}@{b, c}", "{a|b}", "allow");
     284           1 : }
     285             : 
     286           2 : void test_block(const std::string& block_text, const std::string& Atext, const std::string& expected_result, const std::string& title)
     287             : {
     288           2 :   core::identifier_string_list B = detail::parse_block_set(block_text);
     289           2 :   auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
     290           2 :   multi_action_name_set A1 = alphabet_operations::block(B, A, A_includes_subsets);
     291           2 :   std::string result = print(A1, A_includes_subsets);
     292           2 :   check_result(block_text + ", " + Atext, result, expected_result, title);
     293             : 
     294           4 :   allow_set A2 = alphabet_operations::block(B, allow_set(A, A_includes_subsets));
     295           2 :   std::string result_allow = print(A2);
     296           2 :   check_result(block_text + ", " + Atext, result_allow, expected_result, title + "<allow>");
     297           2 : }
     298             : 
     299           2 : BOOST_AUTO_TEST_CASE(test_block1)
     300             : {
     301           1 :   test_block("{b}", "{ab, abbc, c}", "{c}", "block");
     302           1 :   test_block("{b}", "{ab, abbc, c}@", "{a, ac, c}@", "block");
     303           1 : }
     304             : 
     305          19 : multi_action_name make_multi_action_name(const std::string& x)
     306             : {
     307          19 :   multi_action_name result;
     308          19 :   result.insert(core::identifier_string(x));
     309          19 :   return result;
     310           0 : }
     311             : 
     312           2 : BOOST_AUTO_TEST_CASE(test_alphabet_parallel)
     313             : {
     314             :   std::string text =
     315             :     "act a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20; \n"
     316           1 :     "init a1 || a2 || a3 || a4 || a5 || a6 || a7 || a8 || a9 || a10 || a11 || a12 || a13 || a14 || a15 || a16 || a17 || a18 || a19 || a20;  \n"
     317             :     ;
     318             : //    "init allow({a1, a2, a3, a4, a5, a6, a7, a8, a9, a10}, a1 || a2 || a3 || a4 || a5 || a6 || a7 || a8 || a9 || a10);  \n"
     319           1 :   process_specification procspec = parse_process_specification(text);
     320           1 :   multi_action_name_set A;
     321           1 :   A.insert(make_multi_action_name("a1"));
     322           1 :   A.insert(make_multi_action_name("a2"));
     323           1 :   A.insert(make_multi_action_name("a3"));
     324           1 :   A.insert(make_multi_action_name("a4"));
     325           1 :   A.insert(make_multi_action_name("a5"));
     326           1 :   A.insert(make_multi_action_name("a6"));
     327           1 :   A.insert(make_multi_action_name("a7"));
     328           1 :   A.insert(make_multi_action_name("a8"));
     329           1 :   A.insert(make_multi_action_name("a9"));
     330           1 :   A.insert(make_multi_action_name("a11"));
     331           1 :   A.insert(make_multi_action_name("a12"));
     332           1 :   A.insert(make_multi_action_name("a13"));
     333           1 :   A.insert(make_multi_action_name("a14"));
     334           1 :   A.insert(make_multi_action_name("a15"));
     335           1 :   A.insert(make_multi_action_name("a16"));
     336           1 :   A.insert(make_multi_action_name("a17"));
     337           1 :   A.insert(make_multi_action_name("a18"));
     338           1 :   A.insert(make_multi_action_name("a19"));
     339           1 :   A.insert(make_multi_action_name("a20"));
     340             : 
     341           1 :   multi_action_name_set B = detail::alphabet_intersection(procspec.init(), procspec.equations(), A);
     342             :   //BOOST_CHECK_EQUAL(lps::pp(B),"{a1, a2, a3, a4, a5, a6, a7, a8, a9, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20}");
     343           1 :   BOOST_CHECK_EQUAL(process::pp(B), process::pp(A));
     344           1 : }
     345             : 
     346           2 : BOOST_AUTO_TEST_CASE(test_alphabet_new)
     347             : {
     348             :   std::string text =
     349             :     "act a: Bool;                             \n"
     350             :     "proc S(d: Bool) = sum d:Bool. a(d).S(d); \n"
     351           1 :     "init allow({a}, S(true)) ;               \n"
     352             :     ;
     353           1 :   process_specification procspec = parse_process_specification(text);
     354           1 :   alphabet_reduce(procspec);
     355           1 : }
     356             : 

Generated by: LCOV version 1.14