LCOV - code coverage report
Current view: top level - lps/test - binary_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 118 118 100.0 %
Date: 2020-07-11 00:44:39 Functions: 20 20 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jeroen Keiren
       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 binary_test.cpp
      10             : /// \brief Some simple tests for the binary algorithm.
      11             : 
      12             : #define BOOST_TEST_MODULE binary_test
      13             : #include <boost/test/included/unit_test_framework.hpp>
      14             : 
      15             : #include "mcrl2/lps/binary.h"
      16             : #include "mcrl2/lps/detail/test_input.h"
      17             : #include "mcrl2/lps/linearise.h"
      18             : #include "mcrl2/lps/parse.h"
      19             : 
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::data;
      22             : using namespace mcrl2::lps;
      23             : 
      24             : 
      25             : ///All process parameters of sort D should have been translated to
      26             : ///parameters of sort Bool. This leaves only parameters of sort Bool and Pos.
      27           3 : BOOST_AUTO_TEST_CASE(case_1)
      28             : {
      29             :   const std::string text(
      30             :     "sort D = struct d1|d2;\n"
      31             :     "act a:D;\n"
      32             :     "proc P(e:D) = sum d:D . a(e) . P(d);\n"
      33             :     "init P(d1);\n"
      34           2 :   );
      35             : 
      36           2 :   specification s0=remove_stochastic_operators(linearise(text));
      37           2 :   rewriter r(s0.data());
      38           2 :   specification s1 = s0;
      39           1 :   binary_algorithm<rewriter, specification>(s1, r).run();
      40             : 
      41           2 :   variable_list parameters1 = s1.process().process_parameters();
      42             : 
      43           1 :   int bool_param_count = 0;
      44           2 :   for (variable_list::iterator i = parameters1.begin(); i != parameters1.end(); ++i)
      45             :   {
      46           1 :     BOOST_CHECK_EQUAL(i->sort(), sort_bool::bool_());
      47           1 :     if (i->sort() == sort_bool::bool_())
      48             :     {
      49           1 :       ++bool_param_count;
      50             :     }
      51             :   }
      52           1 :   BOOST_CHECK_EQUAL(bool_param_count, 1);
      53           1 : }
      54             : 
      55             : /*
      56             :  * Sort D has got 8 constructors, which can therefore be encoded exactly in
      57             :  * a vector of 3 boolean variables. This means that all combinations of the
      58             :  * boolean variables encode a constructor.
      59             :  * Process parameter e should be replaced by a vector of boolean variables,
      60             :  * and should be replaced in nextstate.
      61             :  * The initial state should be altered accordingly.
      62             :  */
      63           3 : BOOST_AUTO_TEST_CASE(case_2)
      64             : {
      65             :   const std::string text(
      66             :     "sort D = struct d1|d2|d3|d4|d5|d6|d7|d8;\n"
      67             :     "act a:D;\n"
      68             :     "proc P(e:D) = sum d:D . a(e) . P(d);\n"
      69             :     "init P(d1);\n"
      70           2 :   );
      71             : 
      72           2 :   specification s0=remove_stochastic_operators(linearise(text));
      73           2 :   rewriter r(s0.data());
      74           2 :   specification s1 = s0;
      75           1 :   binary_algorithm<rewriter, specification>(s1, r).run();
      76             : 
      77           1 :   int bool_param_count = 0;
      78           4 :   for (variable_list::iterator i = s1.process().process_parameters().begin();
      79           4 :        i != s1.process().process_parameters().end();
      80             :        ++i)
      81             :   {
      82           3 :     BOOST_CHECK_EQUAL(i->sort(), sort_bool::bool_());
      83           3 :     if (i->sort() == sort_bool::bool_())
      84             :     {
      85           3 :       ++bool_param_count;
      86             :     }
      87             :   }
      88           1 :   BOOST_CHECK_EQUAL(bool_param_count, 3);
      89           1 : }
      90             : 
      91             : /*
      92             :  * Sort D has got 7 constructors, which can therefore be encoded in
      93             :  * a vector of 3 boolean variables. This means that there is one combination
      94             :  * of the boolean variables that does not encode a constructor.
      95             :  * Process parameter e should be replaced by a vector of boolean variables,
      96             :  * and should be replaced in nextstate.
      97             :  * The initial state should be altered accordingly.
      98             :  */
      99           3 : BOOST_AUTO_TEST_CASE(case_3)
     100             : {
     101             :   const std::string text(
     102             :     "sort D = struct d1|d2|d3|d4|d5|d6|d7;\n"
     103             :     "act a:D;\n"
     104             :     "proc P(e:D) = sum d:D . a(e) . P(d);\n"
     105             :     "init P(d1);\n"
     106           2 :   );
     107             : 
     108           2 :   specification s0=remove_stochastic_operators(linearise(text));
     109           2 :   rewriter r(s0.data());
     110           2 :   specification s1 = s0;
     111           1 :   binary_algorithm<rewriter, specification>(s1, r).run();
     112             : 
     113           1 :   int bool_param_count = 0;
     114           4 :   for (variable_list::iterator i = s1.process().process_parameters().begin();
     115           4 :        i != s1.process().process_parameters().end();
     116             :        ++i)
     117             :   {
     118           3 :     BOOST_CHECK_EQUAL(i->sort(), sort_bool::bool_());
     119           3 :     if (i->sort() == sort_bool::bool_())
     120             :     {
     121           3 :       ++bool_param_count;
     122             :     }
     123             :   }
     124           1 :   BOOST_CHECK_EQUAL(bool_param_count, 3);
     125           1 : }
     126             : 
     127             : /*
     128             :  * Sort D has got 2 constructors, and should be encoded into one boolean
     129             :  * variable. Process parameter e should be replaced by a single boolean variable
     130             :  * and the action a(e) and the initial state should be altered accordingly.
     131             :  *
     132             :  * Note there is parameter of sort Pos because of linearisation.
     133             :  */
     134           3 : BOOST_AUTO_TEST_CASE(case_4)
     135             : {
     136             :   const std::string text(
     137             :     "sort D = struct d1|d2;\n"
     138             :     "act a,b:D;\n"
     139             :     "proc P(e:D) = sum d:D . a(e) . b(d) . P(d);\n"
     140             :     "init P(d1);\n"
     141           2 :   );
     142             : 
     143           2 :   specification s0=remove_stochastic_operators(linearise(text));
     144           2 :   rewriter r(s0.data());
     145           2 :   specification s1 = s0;
     146           1 :   binary_algorithm<rewriter, specification>(s1, r).run();
     147             : 
     148           1 :   int bool_param_count = 0;
     149           4 :   for (variable_list::iterator i = s1.process().process_parameters().begin();
     150           4 :        i != s1.process().process_parameters().end();
     151             :        ++i)
     152             :   {
     153           3 :     BOOST_CHECK(i->sort() == sort_pos::pos() || i->sort() == sort_bool::bool_());
     154           3 :     if (i->sort() == sort_bool::bool_())
     155             :     {
     156           2 :       ++bool_param_count;
     157             :     }
     158             :   }
     159           1 :   BOOST_CHECK_EQUAL(bool_param_count, 2);
     160           1 : }
     161             : 
     162             : /*
     163             :  * Sort D has got 9 constructors, therefore it should be encoded in
     164             :  * a vector of 4 boolean variables. Note that this does leave a lot of
     165             :  * combinations of booleans that are not used (7 to be precise).
     166             :  * Process parameter e should be replaced by a vector of boolean variables,
     167             :  * and should be replaced in nextstate.
     168             :  * The initial state should be altered accordingly.
     169             :  */
     170           3 : BOOST_AUTO_TEST_CASE(case_5)
     171             : {
     172             :   const std::string text(
     173             :     "sort D = struct d1|d2|d3|d4|d5|d6|d7|d8|d9;\n"
     174             :     "act a:D;\n"
     175             :     "proc P(e:D) = sum d:D . a(e) . P(d);\n"
     176             :     "init P(d1);\n"
     177           2 :   );
     178             : 
     179           2 :   specification s0=remove_stochastic_operators(linearise(text));
     180           2 :   rewriter r(s0.data());
     181           2 :   specification s1 = s0;
     182           1 :   binary_algorithm<rewriter, specification>(s1, r).run();
     183             : 
     184           1 :   int bool_param_count = 0;
     185           5 :   for (variable_list::iterator i = s1.process().process_parameters().begin();
     186           5 :        i != s1.process().process_parameters().end();
     187             :        ++i)
     188             :   {
     189           4 :     BOOST_CHECK_EQUAL(i->sort(), sort_bool::bool_());
     190           4 :     if (i->sort() == sort_bool::bool_())
     191             :     {
     192           4 :       ++bool_param_count;
     193             :     }
     194             :   }
     195           1 :   BOOST_CHECK_EQUAL(bool_param_count, 4);
     196           1 : }
     197             : 
     198             : /*
     199             :  * Sort D is a sort with 4 constructors. It is a recursive construct of two
     200             :  * constructors parameterized with sort E, which is in turn a sort which has
     201             :  * got two simple constructors.
     202             :  * Sort D can be coded in a vector of 2 boolean variables, in which all
     203             :  * combinations are used.
     204             :  * Process parameter e should be replaced by a vector of boolean variables,
     205             :  * and should be replaced in nextstate.
     206             :  * The initial state should be altered accordingly.
     207             :  */
     208           3 : BOOST_AUTO_TEST_CASE(case_6)
     209             : {
     210             :   const std::string text(
     211             :     "sort D = struct d1(E) | d2(E);\n"
     212             :     "     E = struct e1 | e2;\n"
     213             :     "act a:D;\n"
     214             :     "proc P(e:D) = sum d:D . a(e) . P(d);\n"
     215             :     "init P(d1(e1));\n"
     216           2 :   );
     217             : 
     218           2 :   specification s0=remove_stochastic_operators(linearise(text));
     219           2 :   rewriter r(s0.data());
     220           2 :   specification s1 = s0;
     221           1 :   binary_algorithm<rewriter, specification>(s1, r).run();
     222             : 
     223           1 :   int bool_param_count = 0;
     224           3 :   for (variable_list::iterator i = s1.process().process_parameters().begin();
     225           3 :        i != s1.process().process_parameters().end();
     226             :        ++i)
     227             :   {
     228           2 :     BOOST_CHECK_EQUAL(i->sort(), sort_bool::bool_());
     229           2 :     if (i->sort() == sort_bool::bool_())
     230             :     {
     231           2 :       ++bool_param_count;
     232             :     }
     233             :   }
     234           1 :   BOOST_CHECK_EQUAL(bool_param_count, 2);
     235           1 : }
     236             : 
     237             : // This test case shows a bug where apparently d1 and d2 are mapped to the
     238             : // same boolean value. Test case was provided by Jan Friso Groote along with
     239             : // bug 623.
     240           3 : BOOST_AUTO_TEST_CASE(bug_623)
     241             : {
     242             :   const std::string text(
     243             :     "sort D;\n"
     244             :     "cons d1,d2:D;\n"
     245             :     "act a:D#D;\n"
     246             :     "proc X(e1,e2:D) = a(e1,e2) . X(d1,d2);\n"
     247             :     "init X(d2,d1);\n"
     248           2 :   );
     249             : 
     250           2 :   specification s0=remove_stochastic_operators(linearise(text));
     251           2 :   rewriter r(s0.data());
     252           2 :   specification s1 = s0;
     253           1 :   binary_algorithm<rewriter, specification>(s1, r).run();
     254           2 :   action_summand_vector summands1 = s1.process().action_summands();
     255           2 :   for (auto & i : summands1)
     256             :   {
     257           2 :     data_expression_list next_state = i.next_state(s1.process().process_parameters());
     258           1 :     BOOST_CHECK_EQUAL(next_state.size(), 2u);
     259           1 :     BOOST_CHECK_NE(*next_state.begin(), *(++next_state.begin()));
     260           1 :     std::clog << "erroneous next state " << data::pp(next_state) << std::endl;
     261             :   }
     262             : 
     263           1 : }
     264             : 
     265           3 : BOOST_AUTO_TEST_CASE(abp)
     266             : {
     267           2 :   specification spec=remove_stochastic_operators(linearise(lps::detail::ABP_SPECIFICATION()));
     268           1 :   std::clog << "--- before ---\n" << lps::pp(spec) << std::endl;
     269           2 :   rewriter r(spec.data());
     270           1 :   binary_algorithm<rewriter, specification>(spec, r).run();
     271           1 :   std::clog << "--- after ---\n" << lps::pp(spec) << std::endl;
     272           1 :   BOOST_CHECK(check_well_typedness(spec));
     273           1 : }
     274             : 
     275           3 : BOOST_AUTO_TEST_CASE(parameter_selection)
     276             : {
     277             :   const std::string text =
     278             :   "sort Enum6 = struct e6_1 | e6_2 | e6_3 | e6_4 | e6_5 | e6_6;\n"
     279             :   "sort Enum5 = struct e5_1 | e5_2 | e5_3 | e5_4 | e5_5;\n"
     280             :   "act z;\n"
     281             :   "proc P(b:Pos, c:Enum6, d:Enum5) = z . P();\n"
     282           2 :   "init P(5, e6_2, e5_5);";
     283             : 
     284           2 :   specification s0 = parse_linear_process_specification(text);
     285           2 :   rewriter r(s0.data());
     286           2 :   specification s1 = s0;
     287           1 :   binary_algorithm<rewriter, specification>(s1, r, "*:Enum6").run();
     288             : 
     289           1 :   int bool_param_count = 0;
     290           6 :   for (const variable& v: s1.process().process_parameters())
     291             :   {
     292           5 :     BOOST_CHECK(v.sort() == sort_pos::pos() || v.sort() == sort_bool::bool_() || v.sort() == parse_sort_expression("Enum5", s0.data()));
     293           5 :     if (v.sort() == sort_bool::bool_())
     294             :     {
     295           3 :       ++bool_param_count;
     296             :     }
     297             :   }
     298           1 :   BOOST_CHECK_EQUAL(bool_param_count, 3);
     299           4 : }

Generated by: LCOV version 1.13