LCOV - code coverage report
Current view: top level - lps/test - rewriter_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 79 83 95.2 %
Date: 2020-07-04 00:44:36 Functions: 10 10 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 rewriter_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE rewriter_test
      13             : #include "mcrl2/data/detail/parse_substitution.h"
      14             : #include "mcrl2/lps/detail/specification_property_map.h"
      15             : #include "mcrl2/lps/one_point_rule_rewrite.h"
      16             : #include "mcrl2/lps/parse.h"
      17             : #include "mcrl2/lps/rewrite.h"
      18             : 
      19             : #include <boost/test/included/unit_test_framework.hpp>
      20             : 
      21             : using namespace mcrl2;
      22             : using namespace mcrl2::data;
      23             : using namespace mcrl2::data::detail;
      24             : using namespace mcrl2::lps;
      25             : using namespace mcrl2::lps::detail;
      26             : 
      27           1 : const std::string SPECIFICATION1 =
      28             :   "sort Natural;                                    \n"
      29             :   "                                                 \n"
      30             :   "cons _0: Natural;                                \n"
      31             :   "    S: Natural -> Natural;                       \n"
      32             :   "                                                 \n"
      33             :   "map  eq: Natural # Natural -> Bool;              \n"
      34             :   "    less: Natural # Natural -> Bool;             \n"
      35             :   "    plus: Natural # Natural -> Natural;          \n"
      36             :   "    _1, _2, _3, _4, _5, _6, _7, _8, _9: Natural; \n"
      37             :   "    P: Natural -> Natural;                       \n"
      38             :   "    even: Natural -> Bool;                       \n"
      39             :   "                                                 \n"
      40             :   "var  n, m: Natural;                              \n"
      41             :   "                                                 \n"
      42             :   "eqn  eq(n, n) = true;                            \n"
      43             :   "    eq(S(n), _0) = false;                        \n"
      44             :   "    eq(_0, S(m)) = false;                        \n"
      45             :   "    eq(S(n), S(m)) = eq(n, m);                   \n"
      46             :   "                                                 \n"
      47             :   "    less(n, n) = false;                          \n"
      48             :   "    less(n, _0) = false;                         \n"
      49             :   "    less(_0, S(m)) = true;                       \n"
      50             :   "    less(S(n), S(m)) = less(n, m);               \n"
      51             :   "                                                 \n"
      52             :   "    plus(_0, n) = n;                             \n"
      53             :   "    plus(n, _0) = n;                             \n"
      54             :   "    plus(S(n), m) = S(plus(n, m));               \n"
      55             :   "    plus(n, S(m)) = S(plus(n, m));               \n"
      56             :   "                                                 \n"
      57             :   "    even(_0) = true;                             \n"
      58             :   "    even(S(n)) = !(even(n));                     \n"
      59             :   "                                                 \n"
      60             :   "    P(S(n)) = n;                                 \n"
      61             :   "                                                 \n"
      62             :   "    _1 = S(_0);                                  \n"
      63             :   "    _2 = S(_1);                                  \n"
      64             :   "    _3 = S(_2);                                  \n"
      65             :   "    _4 = S(_3);                                  \n"
      66             :   "    _5 = S(_4);                                  \n"
      67             :   "    _6 = S(_5);                                  \n"
      68             :   "    _7 = S(_6);                                  \n"
      69             :   "    _8 = S(_7);                                  \n"
      70             :   "    _9 = S(_8);                                  \n"
      71             :   "                                                 \n"
      72             :   "act a: Natural;                                  \n"
      73             :   "                                                 \n"
      74             :   "proc P(n: Natural) = sum m: Natural. a(m). P(m); \n"
      75             :   "                                                 \n"
      76             :   "init P(_0);                                      \n"
      77             :   ;
      78             : 
      79           1 : void test1()
      80             : {
      81           2 :   specification spec = parse_linear_process_specification(SPECIFICATION1);
      82           2 :   rewriter r(spec.data());
      83             : 
      84           2 :   data_expression n1    = find_mapping(spec.data(), "_1");
      85           2 :   data_expression n2    = find_mapping(spec.data(), "_2");
      86           2 :   data_expression n3    = find_mapping(spec.data(), "_3");
      87           2 :   data_expression n4    = find_mapping(spec.data(), "_4");
      88           2 :   data_expression n5    = find_mapping(spec.data(), "_5");
      89           2 :   data_expression n6    = find_mapping(spec.data(), "_6");
      90           2 :   data_expression n7    = find_mapping(spec.data(), "_7");
      91           2 :   data_expression n8    = find_mapping(spec.data(), "_8");
      92           2 :   data_expression n9    = find_mapping(spec.data(), "_9");
      93           2 :   data_expression plus  = find_mapping(spec.data(), "plus");
      94             : 
      95           1 :   BOOST_CHECK(r(plus(n4, n5)) == r(plus(n2, n7)));
      96             : 
      97           2 :   specification spec1 = spec;
      98           1 :   lps::rewrite(spec1, r);
      99           2 :   lps::detail::specification_property_map<> info(spec);
     100           2 :   lps::detail::specification_property_map<> info1(spec1);
     101           1 :   BOOST_CHECK(info.to_string() == info1.to_string());
     102             : 
     103             :   // test destructor
     104           1 :   const rewriter& r1 = r;
     105           1 : }
     106             : 
     107           1 : const std::string SPECIFICATION2=
     108             :   "act  c:Pos#Nat;                          \n"
     109             :   "proc P(a:Pos,b:Nat)=c(a,0).P(a+1,b+1+2); \n"
     110             :   "init P(1+1,2+2);                         \n";
     111             : 
     112           1 : void test2()
     113             : {
     114           2 :   specification spec = parse_linear_process_specification(SPECIFICATION2);
     115           2 :   rewriter r(spec.data());
     116             : 
     117           2 :   specification spec1 = spec;
     118           1 :   lps::rewrite(spec1, r);
     119             : 
     120           2 :   specification spec2 = spec1;
     121           1 :   lps::rewrite(spec2, r);
     122             : 
     123           2 :   lps::detail::specification_property_map<> info1(spec1);
     124           2 :   lps::detail::specification_property_map<> info2(spec2);
     125           1 :   BOOST_CHECK(info1.to_string() == info2.to_string());
     126           1 :   BOOST_CHECK(spec1.process().summand_count() == 1);
     127           1 : }
     128             : 
     129           1 : const std::string SPECIFICATION3 =
     130             :   "act  c:Pos#Nat;                          \n"
     131             :   "proc P(a:Pos,b:Nat)=tau.P(a+1,b+1+2)+    \n"
     132             :   "                    tau.P(a+1,pred(a))+  \n"
     133             :   "                    c(a,0).P(a,b);       \n"
     134             :   "init P(1+1,0);                           \n";
     135           1 : void test3()
     136             : {
     137           2 :   specification spec = parse_linear_process_specification(SPECIFICATION3);
     138           2 :   rewriter r(spec.data());
     139             : 
     140           2 :   specification spec1 = spec;
     141           1 :   lps::rewrite(spec1, r);
     142             : 
     143           2 :   specification spec2 = spec1;
     144           1 :   lps::rewrite(spec2, r);
     145             : 
     146           2 :   lps::detail::specification_property_map<> info1(spec1);
     147           2 :   lps::detail::specification_property_map<> info2(spec2);
     148           1 :   BOOST_CHECK(info1.to_string() == info2.to_string());
     149           1 :   BOOST_CHECK(spec1.process().summand_count() == 3);
     150           1 : }
     151             : 
     152             : // Checks if rewriting the specification src with the substitutions sigma
     153             : // results in the specification dest.
     154           1 : void test_lps_rewriter(const std::string& src_text, const std::string& dest_text, const std::string& sigma_text)
     155             : {
     156           2 :   lps::specification src  = parse_linear_process_specification(src_text);
     157           2 :   lps::specification dest = parse_linear_process_specification(dest_text);
     158             : 
     159             :   // rewrite the specification src
     160           2 :   data::rewriter R(src.data());
     161           2 :   data::mutable_map_substitution<> sigma;
     162           1 :   data::detail::parse_substitution(sigma_text, sigma, src.data());
     163           1 :   lps::rewrite(src, R, sigma);
     164             : 
     165           1 :   if (src != dest)
     166             :   {
     167           0 :     std::cerr << "--- test failed ---" << std::endl;
     168           0 :     std::cerr << lps::pp(src) << std::endl;
     169           0 :     std::cerr << "-------------------" << std::endl;
     170           0 :     std::cerr << lps::pp(dest) << std::endl;
     171             :   }
     172           1 :   BOOST_CHECK(src == dest);
     173           1 : }
     174             : 
     175           1 : void test_lps_rewriter()
     176             : {
     177             :   std::string src =
     178             :     "act  c: Bool;                                                       \n"
     179             :     "proc P(b: Bool, c:Bool) = c(true && false).P(b || true, c && true); \n"
     180           2 :     "init P(true || false, true && false);                               \n";
     181             : 
     182             :   std::string dest =
     183             :     "act  c: Bool;                                                       \n"
     184             :     "proc P(b: Bool, c:Bool) = c(false).P(true, c);                      \n"
     185           2 :     "init P(true, false);                                                \n";
     186             : 
     187           1 :   test_lps_rewriter(src, dest, "");
     188           1 : }
     189             : 
     190           1 : void test_one_point_rule_rewriter()
     191             : {
     192             :   std::string src =
     193             :     "act  a: Bool;\n"
     194             :     "\n"
     195             :     "proc P(b: Bool) =\n"
     196             :     "       (forall n: Nat. n != 1 || b) ->\n"
     197             :     "         a(exists m: Nat. m == 1) .\n"
     198             :     "         P(b = b);\n"
     199             :     "\n"
     200           2 :     "init P(true);";
     201             : 
     202             :   std::string expected_result =
     203             :     "act  a: Bool;\n"
     204             :     "\n"
     205             :     "proc P(b: Bool) =\n"
     206             :     "       (1 != 1 || b) ->\n"
     207             :     "         a(1 == 1) .\n"
     208             :     "         P(b = b);\n"
     209             :     "\n"
     210           2 :     "init P(true);";
     211             : 
     212           2 :   specification lpsspec = parse_linear_process_specification(src);
     213           2 :   specification expected_spec = parse_linear_process_specification(expected_result);
     214           1 :   lps::one_point_rule_rewrite(lpsspec);
     215           2 :   std::string result = utilities::trim_copy(lps::pp(lpsspec));
     216           1 :   BOOST_CHECK(result == expected_result);
     217           1 : }
     218             : 
     219           3 : BOOST_AUTO_TEST_CASE(test_main)
     220             : {
     221           1 :   test1();
     222           1 :   test2();
     223           1 :   test3();
     224           1 :   test_lps_rewriter();
     225           1 :   test_one_point_rule_rewriter();
     226           4 : }

Generated by: LCOV version 1.13