LCOV - code coverage report
Current view: top level - lps/test - sumelm_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 157 158 99.4 %
Date: 2020-07-04 00:44:36 Functions: 25 25 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 sumelm_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE sumelm_test
      13             : #include "mcrl2/lps/linearise.h"
      14             : #include "mcrl2/lps/parse.h"
      15             : #include "mcrl2/lps/sumelm.h"
      16             : 
      17             : #include <boost/test/included/unit_test_framework.hpp>
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::data;
      21             : using namespace mcrl2::lps;
      22             : 
      23          11 : void print_specifications(const specification& s0, const specification& s1)
      24             : {
      25          11 :   if (!(s0 == s1))
      26             :   {
      27           9 :     std::clog << "=== Specifications differ ===" << std::endl;
      28          18 :     std::clog << "    Input specification  : " << lps::pp(s0) << std::endl
      29           9 :               << "    Output specification : " << lps::pp(s1) << std::endl;
      30             :   }
      31             :   else
      32             :   {
      33           2 :     std::clog << "=== Specification are the same ===" << std::endl;
      34             :   }
      35          11 : }
      36             : 
      37             : /*
      38             :  * Test case which tries to test all possibilities for substitutions. This is a
      39             :  * test for issue #367
      40             :  */
      41           3 : BOOST_AUTO_TEST_CASE(bug_367)
      42             : {
      43           1 :   std::clog << "Test case 1" << std::endl;
      44             :   const std::string text(
      45             :     "sort S = struct s1 | s2;\n"
      46             :     "map f : S -> Bool;\n"
      47             :     "act a : S # Bool;\n"
      48             :     "proc P = sum c : S, b : Bool . (b == f(c) && c == s2) -> a(c, b) . P;\n"
      49             :     "init P;\n"
      50           2 :   );
      51             : 
      52           2 :   specification s0 = parse_linear_process_specification(text);
      53           2 :   specification s1 = s0;
      54           1 :   sumelm_algorithm<>(s1).run();
      55           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
      56           2 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
      57             :   {
      58           1 :     BOOST_CHECK(i->summation_variables().empty());
      59           1 :     BOOST_CHECK(data::find_all_variables(i->condition()).empty());
      60           1 :     BOOST_CHECK(lps::find_all_variables(i->multi_action()).empty());
      61             :   }
      62             : 
      63           1 :   print_specifications(s0,s1);
      64           1 : }
      65             : 
      66             : /// Sum variable y does not occur in the summand, and therefore must be removed.
      67           3 : BOOST_AUTO_TEST_CASE(no_occurrence_of_variable)
      68             : {
      69           1 :   std::clog << "Test case 2" << std::endl;
      70             :   const std::string text(
      71             :     "act a,b;\n"
      72             :     "proc P(s3_P: Pos) = sum y_P: Int. (s3_P == 1) -> a . P(2)\n"
      73             :     "                  + (s3_P == 2) -> b . P(1);\n"
      74             :     "init P(1);\n"
      75           2 :   );
      76             : 
      77           2 :   specification s0 = parse_linear_process_specification(text);
      78           2 :   specification s1 = s0;
      79           1 :   sumelm_algorithm<>(s1).run();
      80           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
      81           3 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
      82             :   {
      83           2 :     BOOST_CHECK(i->summation_variables().empty());
      84             :   }
      85             : 
      86           1 :   print_specifications(s0,s1);
      87           1 : }
      88             : 
      89             : /*
      90             :  * The sum variable y is equal to 4 in the condition, hence 4 should be
      91             :  * substituted for y in the summand, and sum y should be removed
      92             :  * In this case, this boils down to removing sum y, and removing 4==y from the
      93             :  * condition. The rest of the specification can be left untouched
      94             :  */
      95           3 : BOOST_AUTO_TEST_CASE(reverse_equality)
      96             : {
      97           1 :   std::clog << "Test case 3" << std::endl;
      98             :   const std::string text(
      99             :     "act a;\n"
     100             :     "proc P = sum y:Int . (4 == y) -> a . P;\n"
     101             :     "init P;\n"
     102           2 :   );
     103             : 
     104           2 :   specification s0 = parse_linear_process_specification(text);
     105           2 :   specification s1 = s0;
     106           1 :   sumelm_algorithm<>(s1).run();
     107           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     108           2 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
     109             :   {
     110           1 :     BOOST_CHECK(i->summation_variables().empty());
     111           1 :     BOOST_CHECK(data::find_all_variables(i->condition()).empty());
     112             :   }
     113             : 
     114           1 :   print_specifications(s0,s1);
     115           1 : }
     116             : 
     117             : /*
     118             :  * This is the same as test case 3, except with the equality in different order.
     119             :  */
     120           3 : BOOST_AUTO_TEST_CASE(equality)
     121             : {
     122           1 :   std::clog << "Test case 4" << std::endl;
     123             :   const std::string text(
     124             :     "act a;\n"
     125             :     "proc P = sum y:Int . (y == 4) -> a . P;\n"
     126             :     "init P;\n"
     127           2 :   );
     128             : 
     129           2 :   specification s0 = parse_linear_process_specification(text);
     130           2 :   specification s1 = s0;
     131           1 :   sumelm_algorithm<>(s1).run();
     132           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     133           2 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
     134             :   {
     135           1 :     BOOST_CHECK(i->summation_variables().empty());
     136           1 :     BOOST_CHECK(data::find_all_variables(i->condition()).empty());
     137             :   }
     138             : 
     139           1 :   print_specifications(s0,s1);
     140           1 : }
     141             : 
     142             : /*
     143             :  * Test whether sum variables are correctly removed from actions and timing.
     144             :  */
     145           3 : BOOST_AUTO_TEST_CASE(actions_and_time)
     146             : {
     147           1 :   std::clog << "Test case 5" << std::endl;
     148             :   const std::string text(
     149             :     "act a,b:Int;\n"
     150             :     "proc P = sum y:Int . (y == 4) -> a(y)@y . b(y*2)@(y+1) . P;\n"
     151             :     "init P;\n"
     152           2 :   );
     153             : 
     154             :   // FIXME, this test case requires the parser to allow parsing of free
     155             :   // variables.
     156           2 :   specification s0=remove_stochastic_operators(linearise(text));
     157           2 :   specification s1 = s0;
     158           1 :   sumelm_algorithm<>(s1).run();
     159           2 :   std::set<variable> parameters = mcrl2::data::find_all_variables(s1.process().process_parameters());
     160           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     161           3 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
     162             :   {
     163           2 :     BOOST_CHECK(i->summation_variables().empty());
     164             : 
     165             :     // Check that the only data variables in the condition and time
     166             :     // are process parameters
     167           4 :     std::set<variable> condition_vars = data::find_all_variables(i->condition());
     168           4 :     for (const auto & condition_var : condition_vars)
     169             :     {
     170           2 :       BOOST_CHECK(parameters.find(condition_var) != parameters.end());
     171             :     }
     172             : 
     173           2 :     if (i->has_time())
     174             :     {
     175           4 :       std::set<variable> time_vars = data::find_all_variables(i->multi_action().time());
     176           3 :       for (const auto & time_var : time_vars)
     177             :       {
     178           1 :         BOOST_CHECK(parameters.find(time_var) != parameters.end());
     179             :       }
     180             :     }
     181             :   }
     182             : 
     183           1 :   print_specifications(s0,s1);
     184           1 : }
     185             : 
     186             : /*
     187             :  * Test that a sum variable is not removed when it occurs in both sides of a
     188             :  * variable.
     189             :  */
     190           3 : BOOST_AUTO_TEST_CASE(both_sides_of_equality)
     191             : {
     192           1 :   std::clog << "Test case 6" << std::endl;
     193             :   const std::string text(
     194             :     "act a;\n"
     195             :     "proc P = sum y:Int . (y == y + 1) -> a . P;\n"
     196             :     "init P;\n"
     197           2 :   );
     198             : 
     199           2 :   specification s0 = parse_linear_process_specification(text);
     200           2 :   specification s1 = s0;
     201           1 :   sumelm_algorithm<>(s1).run();
     202           1 :   int sumvar_count = 0;
     203           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     204           2 :   for (const auto & i : summands1)
     205             :   {
     206           1 :     if (!i.summation_variables().empty())
     207             :     {
     208           1 :       ++sumvar_count;
     209             :     }
     210             :   }
     211           1 :   BOOST_CHECK(sumvar_count == 1);
     212           1 :   BOOST_CHECK(s0 == s1);
     213             : 
     214           1 :   print_specifications(s0,s1);
     215           1 : }
     216             : 
     217             : /*
     218             :  * The sum variable e occurs in the condition in the following ways:
     219             :  * - As righthandside of an equality
     220             :  * - Both as lefthandside and righthandside of an equality
     221             :  * - As lefthandside of an equality
     222             :  * The sum variable d occurs in the lefthandside of an equality in the
     223             :  * condition.
     224             :  * The sum variable f occurs in the righthandside of an equality in the
     225             :  * condition.
     226             :  *
     227             :  * Result:
     228             :  * - The summation over d is removed by substituting e for d
     229             :  * - The summation over e is removed by substituting f for e
     230             :  * This should leave only a sum f:D . f == g(f) -> a . X(f).
     231             :  */
     232           3 : BOOST_AUTO_TEST_CASE(three_sums_remove_two)
     233             : {
     234           1 :   std::clog << "Test case 7" << std::endl;
     235             :   const std::string text(
     236             :     "sort D = struct d1 | d2 | d3;\n"
     237             :     "map g : D -> D;\n"
     238             :     "act a;\n"
     239             :     "proc P(c:D) = sum d:D . sum e:D . sum f:D . (d == e && e == g(e) && e == f) -> a . P(d);\n"
     240             :     "init P(d1);\n"
     241           2 :   );
     242             : 
     243           2 :   specification s0 = parse_linear_process_specification(text);
     244           2 :   specification s1 = s0;
     245           1 :   sumelm_algorithm<>(s1).run();
     246           1 :   int sumvar_count = 0;
     247           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     248           2 :   for (const auto & i : summands1)
     249             :   {
     250           1 :     if (!i.summation_variables().empty())
     251             :     {
     252           1 :       ++sumvar_count;
     253             :     }
     254             :   }
     255           1 :   BOOST_CHECK(sumvar_count == 1);
     256             : 
     257           1 :   print_specifications(s0,s1);
     258           1 : }
     259             : 
     260             : /*
     261             :  * Sum variable d occurs twice in the lefthandside of an equality
     262             :  * The strongest set of substitutions possible is e := d; f := d, hence removing
     263             :  * two summations.
     264             :  * (Test introduced after a bugreport by M. Voorhoeve)
     265             :  */
     266           3 : BOOST_AUTO_TEST_CASE(twice_lhs)
     267             : {
     268           1 :   std::clog << "Test case 8" << std::endl;
     269             :   const std::string text(
     270             :     "sort D = struct d1 | d2 | d3;\n"
     271             :     "act a;\n"
     272             :     "proc P(c:D) = sum d:D . sum e:D . sum f:D . (d == e && d == f) -> a . P(d);\n"
     273             :     "init P(d1);\n"
     274           2 :   );
     275             : 
     276           2 :   specification s0 = parse_linear_process_specification(text);
     277           2 :   specification s1 = s0;
     278           1 :   sumelm_algorithm<>(s1).run();
     279           1 :   int sumvar_count = 0;
     280           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     281           2 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
     282             :   {
     283           1 :     if (!i->summation_variables().empty())
     284             :     {
     285           1 :       ++sumvar_count;
     286           1 :       BOOST_CHECK(data::find_all_variables(i->condition()).empty());
     287             :     }
     288             :   }
     289           1 :   BOOST_CHECK(sumvar_count == 1);
     290             : 
     291           1 :   print_specifications(s0,s1);
     292           1 : }
     293             : 
     294             : /*
     295             :  * Test introduced after a bug report by Bas Ploeger. In contrary to what was
     296             :  * assumed before, sum variables may not be unconditionally removed from delta summands.
     297             :  */
     298           3 : BOOST_AUTO_TEST_CASE(no_unconditional_sum_removal_from_delta)
     299             : {
     300           1 :   std::clog << "Test case 9" << std::endl;
     301             :   const std::string text(
     302             :     "proc P = sum y:Nat . (y > 10) -> delta;\n"
     303             :     "init P;\n"
     304           2 :   );
     305             : 
     306           2 :   specification s0 = parse_linear_process_specification(text);
     307           2 :   specification s1 = s0;
     308           1 :   sumelm_algorithm<>(s1).run();
     309           1 :   int sumvar_count = 0;
     310           1 :   const deadlock_summand_vector& summands1 = s1.process().deadlock_summands();
     311           2 :   for (const auto & i : summands1)
     312             :   {
     313           1 :     if (!i.summation_variables().empty())
     314             :     {
     315           1 :       ++sumvar_count;
     316             :     }
     317             :   }
     318           1 :   BOOST_CHECK(sumvar_count == 1);
     319             : 
     320           1 :   print_specifications(s0,s1);
     321           1 : }
     322             : 
     323             : ///Test case for issue #380
     324           3 : BOOST_AUTO_TEST_CASE(bug_380)
     325             : {
     326           1 :   std::clog << "Test case 10" << std::endl;
     327             :   const std::string text(
     328             :     "act a:Nat;\n"
     329             :     "proc P(n0: Nat) = sum n: Nat. (n == n0 && n == 1) -> a(n0) . P(n);\n"
     330             :     "init P(0);\n"
     331           2 :   );
     332             : 
     333           2 :   specification s0 = parse_linear_process_specification(text);
     334           2 :   specification s1 = s0;
     335           1 :   sumelm_algorithm<>(s1).run();
     336           1 :   int sumvar_count = 0;
     337           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     338           2 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
     339             :   {
     340           1 :     BOOST_CHECK(i->condition() != sort_bool::true_());
     341           1 :     if (!i->summation_variables().empty())
     342             :     {
     343           0 :       ++sumvar_count;
     344             :     }
     345             :   }
     346           1 :   BOOST_CHECK(sumvar_count == 0);
     347             : 
     348           1 :   print_specifications(s0, s1);
     349           1 : }
     350             : 
     351             : ///Test case for issue #380
     352           3 : BOOST_AUTO_TEST_CASE(test_boolean_variables)
     353             : {
     354           1 :   std::clog << "Test case 11" << std::endl;
     355             :   const std::string text(
     356             :     "act a:Bool#Bool;\n"
     357             :     "proc P = sum b,c: Bool. (b && !c) -> a(b,c) . P;\n"
     358             :     "init P;\n"
     359           2 :   );
     360             : 
     361           2 :   specification s0 = parse_linear_process_specification(text);
     362           2 :   specification s1 = s0;
     363           1 :   sumelm_algorithm<>(s1).run();
     364             : 
     365           2 :   action_summand_vector v(s1.process().action_summands());
     366           2 :   for(action_summand_vector::const_iterator i = v.begin(); i != v.end(); ++i)
     367             :   {
     368           1 :     BOOST_CHECK_EQUAL(i->summation_variables().size(), 0u);
     369             :   }
     370             : 
     371           1 :   print_specifications(s0, s1);
     372           4 : }
     373             : 

Generated by: LCOV version 1.13