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

Generated by: LCOV version 1.13