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 suminst_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE suminst_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/lps/linearise.h"
      16             : #include "mcrl2/lps/suminst.h"
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::data;
      20             : using namespace mcrl2::lps;
      21             : 
      22             : ///sum d:D should be unfolded
      23           1 : void test_case_1()
      24             : {
      25             :   const std::string text(
      26             :     "sort D = struct d1|d2;\n"
      27             :     "act a;\n"
      28             :     "proc X = sum d:D . a . X;\n"
      29             :     "init X;\n"
      30           1 :   );
      31             : 
      32           1 :   specification s0=remove_stochastic_operators(linearise(text));
      33           1 :   rewriter r(s0.data());
      34           1 :   specification s1(s0);
      35           1 :   suminst_algorithm<rewriter, specification>(s1,r).run();
      36           1 :   std::clog << lps::pp(s0) << std::endl;
      37           1 :   std::clog << lps::pp(s1) << std::endl;
      38           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
      39           3 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
      40             :   {
      41           2 :     BOOST_CHECK(i->summation_variables().empty());
      42             :   }
      43             : 
      44             :   // TODO: Check that d1 and d2 actually occur in the process.
      45           1 : }
      46             : 
      47             : ///sum d:D should be unfolded (multiple occurrences of d per summand)
      48           1 : void test_case_2()
      49             : {
      50             :   const std::string text(
      51             :     "sort D = struct d1|d2;\n"
      52             :     "act a:D;\n"
      53             :     "    b;\n"
      54             :     "proc X(x:D) = sum d:D . a(d) . b . X(d);\n"
      55             :     "init X(d1);\n"
      56           1 :   );
      57             : 
      58           1 :   specification s0=remove_stochastic_operators(linearise(text));
      59           1 :   rewriter r(s0.data());
      60           1 :   specification s1(s0);
      61           1 :   suminst_algorithm<rewriter, specification>(s1, r).run();
      62           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
      63           4 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
      64             :   {
      65           3 :     BOOST_CHECK(i->summation_variables().empty());
      66             :   }
      67             : 
      68             :   // TODO: Check that d1 and d2 actually occur in the process.
      69           1 : }
      70             : 
      71             : ///sum d:D should not be removed, hence there should be a summand for
      72             : ///which d is a sum variable.
      73           1 : void test_case_3()
      74             : {
      75             :   const std::string text(
      76             :     "sort D;\n"
      77             :     "act a:D;\n"
      78             :     "proc X = sum d:D . a(d) . X;\n"
      79             :     "init X;\n"
      80           1 :   );
      81             : 
      82           1 :   specification s0=remove_stochastic_operators(linearise(text));
      83           1 :   rewriter r(s0.data());
      84           1 :   specification s1(s0);
      85           1 :   suminst_algorithm<rewriter, specification>(s1, r).run();
      86           1 :   bool sum_occurs = false;
      87           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
      88           2 :   for (const action_summand& i : summands1)
      89             :   {
      90           1 :     sum_occurs = sum_occurs || !i.summation_variables().empty();
      91             :   }
      92           1 :   BOOST_CHECK(sum_occurs);
      93           1 : }
      94             : 
      95             : ///This is a test in which tau summands occur.
      96             : ///We override opts such that only tau summands are instantiated.
      97             : ///Note: Test case 5 tests the same specification, but uses the defaults.
      98           1 : void test_case_4()
      99             : {
     100             :   const std::string text(
     101             :     "sort S = struct s1 | s2 | s3;\n"
     102             :     "     T = struct t1 | t2 | t3;\n"
     103             :     "act a;\n"
     104             :     "proc P = sum s : S . tau . P\n"
     105             :     "       + sum t : T . a . P;\n"
     106             :     "init P;\n"
     107           1 :   );
     108             : 
     109           1 :   specification s0=remove_stochastic_operators(linearise(text));
     110           1 :   rewriter r(s0.data());
     111           1 :   specification s1(s0);
     112           1 :   suminst_algorithm<rewriter, specification>(s1, r, finite_sorts(s1.data()), true).run();
     113           1 :   bool tau_sum_occurs = false;
     114           1 :   bool sum_occurs = false;
     115           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     116           5 :   for (const action_summand& i : summands1)
     117             :   {
     118           4 :     if (i.is_tau())
     119             :     {
     120           3 :       tau_sum_occurs = tau_sum_occurs || !i.summation_variables().empty();
     121             :     }
     122             :     else
     123             :     {
     124           1 :       sum_occurs = sum_occurs || !i.summation_variables().empty();
     125             :     }
     126             :   }
     127           1 :   BOOST_CHECK(!tau_sum_occurs);
     128           1 :   BOOST_CHECK(sum_occurs);
     129           1 : }
     130             : 
     131             : ///This is a test in which tau summands occur.
     132             : ///Both sum variables should be expanded, hence no sum variable may occur in the
     133             : ///result.
     134             : ///Note: Test case 4 tests the same specification, but only expands the tau
     135             : ///summands.
     136           1 : void test_case_5()
     137             : {
     138             :   const std::string text(
     139             :     "sort S = struct s1 | s2 | s3;\n"
     140             :     "     T = struct t1 | t2 | t3;\n"
     141             :     "act a;\n"
     142             :     "proc P = sum s : S . tau . P\n"
     143             :     "       + sum t : T . a . P;\n"
     144             :     "init P;\n"
     145           1 :   );
     146             : 
     147           1 :   specification s0=remove_stochastic_operators(linearise(text));
     148           1 :   rewriter r(s0.data());
     149           1 :   specification s1(s0);
     150           1 :   suminst_algorithm<rewriter, specification>(s1, r).run();
     151           1 :   bool tau_sum_occurs = false;
     152           1 :   bool sum_occurs = false;
     153           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     154           7 :   for (const action_summand& i: summands1)
     155             :   {
     156           6 :     if (i.is_tau())
     157             :     {
     158           3 :       tau_sum_occurs = tau_sum_occurs || !i.summation_variables().empty();
     159             :     }
     160             :     else
     161             :     {
     162           3 :       sum_occurs = sum_occurs || !i.summation_variables().empty();
     163             :     }
     164             :   }
     165           1 :   BOOST_CHECK(!tau_sum_occurs);
     166           1 :   BOOST_CHECK(!sum_occurs);
     167           1 : }
     168             : 
     169           1 : void test_case_6()
     170             : {
     171             :   const std::string text(
     172             :     "proc P(n0:Nat) = sum n : Nat . (n == n0) -> delta@n . P(n);\n"
     173             :     "init P(5);\n"
     174           1 :   );
     175             : 
     176           1 :   specification s0=remove_stochastic_operators(linearise(text));
     177           1 :   rewriter r(s0.data());
     178           1 :   specification s1(s0);
     179           1 :   suminst_algorithm<rewriter, specification>(s1, r, std::set<data::sort_expression>(s1.data().sorts().begin(),s1.data().sorts().end())).run();
     180           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     181           1 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
     182             :   {
     183           0 :     BOOST_CHECK(i->summation_variables().empty());
     184             :   }
     185           1 : }
     186             : 
     187           0 : void test_case_7()
     188             : {
     189             :   const std::string text(
     190             :     "sort S;\n"
     191             :     "act a:S;\n"
     192             :     "proc P = sum s : S . a(s) . P;\n"
     193             :     "init P;\n"
     194           0 :   );
     195             : 
     196           0 :   specification s0=remove_stochastic_operators(linearise(text));
     197           0 :   rewriter r(s0.data());
     198           0 :   specification s1(s0);
     199           0 :   suminst_algorithm<rewriter, specification>(s1, r, std::set<data::sort_expression>(s1.data().sorts().begin(),s1.data().sorts().end())).run();
     200           0 :   int sum_count = 0;
     201           0 :   const action_summand_vector& summands1 = s1.process().action_summands();
     202           0 :   for (const action_summand& i: summands1)
     203             :   {
     204           0 :     sum_count += i.summation_variables().size();
     205             :   }
     206           0 :   BOOST_CHECK(sum_count == 1);
     207           0 : }
     208             : 
     209           2 : BOOST_AUTO_TEST_CASE(test_main)
     210             : {
     211           1 :   std::clog << "test case 1" << std::endl;
     212           1 :   test_case_1();
     213           1 :   std::clog << "test case 2" << std::endl;
     214           1 :   test_case_2();
     215           1 :   std::clog << "test case 3" << std::endl;
     216           1 :   test_case_3();
     217           1 :   std::clog << "test case 4" << std::endl;
     218           1 :   test_case_4();
     219           1 :   std::clog << "test case 5" << std::endl;
     220           1 :   test_case_5();
     221           1 :   std::clog << "test case 6" << std::endl;
     222           1 :   test_case_6();
     223           1 : }
     224             :