LCOV - code coverage report
Current view: top level - lps/test - linearization_test3.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 58 59 98.3 %
Date: 2020-07-04 00:44:36 Functions: 18 18 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Wieger Wesselink, Jan Friso Groote
       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 linearization_test3.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE linearization_test3
      13             : #include <boost/test/included/unit_test_framework.hpp>
      14             : 
      15             : #include "mcrl2/data/detail/rewrite_strategies.h"
      16             : #include "mcrl2/lps/linearise.h"
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::lps;
      20             : 
      21             : typedef data::rewriter::strategy rewrite_strategy;
      22             : typedef std::vector<rewrite_strategy> rewrite_strategy_vector;
      23             : 
      24          42 : void run_linearisation_instance(const std::string& spec, const t_lin_options& options, bool expect_success)
      25             : {
      26          42 :   if (expect_success)
      27             :   {
      28          84 :     lps::stochastic_specification s=linearise(spec, options);
      29          42 :     BOOST_CHECK(s != lps::stochastic_specification());
      30             :   }
      31             :   else
      32             :   {
      33           0 :     BOOST_CHECK_THROW(linearise(spec, options), mcrl2::runtime_error);
      34             :   }
      35          42 : }
      36             : 
      37           7 : void run_linearisation_test_case(const std::string& spec, const bool expect_success = true)
      38             : {
      39             :   // Set various rewrite strategies
      40          14 :   rewrite_strategy_vector rewrite_strategies = data::detail::get_test_rewrite_strategies(false);
      41             : 
      42          14 :   for (rewrite_strategy_vector::const_iterator i = rewrite_strategies.begin(); i != rewrite_strategies.end(); ++i)
      43             :   {
      44           7 :     std::clog << std::endl << "Testing with rewrite strategy " << *i << std::endl;
      45             : 
      46           7 :     t_lin_options options;
      47           7 :     options.rewrite_strategy=*i;
      48             : 
      49           7 :     std::clog << "  Default options" << std::endl;
      50           7 :     run_linearisation_instance(spec, options, expect_success);
      51             : 
      52           7 :     std::clog << "  Linearisation method regular2" << std::endl;
      53           7 :     options.lin_method=lmRegular2;
      54           7 :     run_linearisation_instance(spec, options, expect_success);
      55             : 
      56           7 :     std::clog << "  Linearisation method stack" << std::endl;
      57           7 :     options.lin_method=lmStack;
      58           7 :     run_linearisation_instance(spec, options, expect_success);
      59             : 
      60           7 :     std::clog << "  Linearisation method stack; binary enabled" << std::endl;
      61           7 :     options.binary=true;
      62           7 :     run_linearisation_instance(spec, options, expect_success);
      63             : 
      64           7 :     std::clog << "  Linearisation method regular; binary enabled" << std::endl;
      65           7 :     options.lin_method=lmRegular;
      66           7 :     run_linearisation_instance(spec, options, expect_success);
      67             : 
      68           7 :     std::clog << "  Linearisation method regular; no intermediate clustering" << std::endl;
      69           7 :     options.binary=false; // reset binary
      70           7 :     options.no_intermediate_cluster=true;
      71           7 :     run_linearisation_instance(spec, options, expect_success);
      72             :   }
      73           7 : }
      74             : 
      75           3 : BOOST_AUTO_TEST_CASE(The_unreachability_of_tau_is_not_properly_recognized)
      76             : {
      77             :   const std::string spec =
      78           2 :      "init (true -> delta <> delta) . tau;";
      79             : 
      80           1 :   run_linearisation_test_case(spec,true);
      81           1 : }
      82             : 
      83           3 : BOOST_AUTO_TEST_CASE(Moving_a_distribution_out_of_a_process_is_tricky)
      84             : {
      85             :   const std::string spec =
      86             :      "map  N:Pos;\n"
      87             :      "eqn  N=2;\n"
      88             :      "\n"
      89             :      "act  last_passenger_has_his_own_seat:Bool;\n"
      90             :      "     enter_plane:Bool#Bool;\n"
      91             :      "     enter;\n"
      92             :      "\n"
      93             :      "\n"
      94             :      "proc Plane(everybody_has_his_own_seat:Bool, number_of_empty_seats:Int)=\n"
      95             :      "             (enter.\n"
      96             :      "                dist b0:Bool[if(everybody_has_his_own_seat,if(b0,1,0),if(b0,1-1/number_of_empty_seats,1/number_of_empty_seats))].\n"
      97             :      "                b0 -> enter_plane(true,false).delta.Plane(everybody_has_his_own_seat,number_of_empty_seats-1)\n"
      98             :      "                   <>dist b1:Bool[if(b1,1/number_of_empty_seats,1-1/number_of_empty_seats)].\n"
      99             :      "                      enter_plane(false,b1).delta\n"
     100             :      "             );\n"
     101             :      "\n"
     102             :      "\n"
     103           2 :      "init dist b:Bool[if(b,1/N,(N-1)/N)].Plane(b,N-1);\n";
     104             : 
     105           1 :   run_linearisation_test_case(spec,true);
     106           1 : }
     107             : 
     108             : /* The test below failed with type checking (only in debug mode). The reason
     109             :  * is that the set {0,1} would obtain terms with different types (int, nat),
     110             :  * which is not a well typed set. This was reported by Muhammad Atif, error #1526. */
     111           3 : BOOST_AUTO_TEST_CASE(type_checking_a_finite_set_with_numbers_can_go_astray)
     112             : {
     113             :   const std::string spec =
     114             :      "act sendInt, rcvInt, transferInt:Int;\n"
     115             :      "\n"
     116             :      "proc P (bg:Bag(Int))=(count(2,bg)<2)->sum i:Int.rcvInt(i).P(Set2Bag({i})+bg);\n"
     117             :      "     Px(c:Nat)= (c<2)->sum x:Int.(x<3&&x>-2)->sendInt(x).Px(c+1);\n"
     118             :      "     Py(c:Nat)= (c<2)->sum x:Int.(x<3&&x>-2)->sendInt(x).Py(c+1);\n"
     119             :      "\n"
     120             :      "init allow({transferInt},\n"
     121             :      "       comm({sendInt|rcvInt->transferInt},\n"
     122           2 :      "           P(Set2Bag({0,1}))||Px(0)||Py(0) ));\n";
     123             : 
     124           1 :   run_linearisation_test_case(spec,true);
     125           1 : }
     126             : 
     127             : #ifndef MCRL2_SKIP_LONG_TESTS 
     128             : 
     129           3 : BOOST_AUTO_TEST_CASE(Type_checking_of_function_can_be_problematic)
     130             : {
     131             :   const std::string spec =
     132             :      "sort  State = struct S;\n"
     133             :      "proc X = ((lambda x: Nat. S)(3) == S)->tau.X;\n"
     134           2 :      "init X;\n";
     135             : 
     136           1 :   run_linearisation_test_case(spec,true);
     137           1 : }
     138             : 
     139           3 : BOOST_AUTO_TEST_CASE(Check_whether_the_sum_variable_will_not_get_the_same_name_as_the_newly_introduced_process_parameter)
     140             : {
     141             :   const std::string spec =
     142             :      "act  base ;\n"
     143             :      "     exponent: Real;\n"
     144             :      "proc Test_exponentation =\n"
     145             :      "       sum r: Real. base . exponent(r).delta ;\n"
     146             :      "\n"
     147           2 :      "init Test_exponentation+delta;\n";
     148             : 
     149           1 :   run_linearisation_test_case(spec,true);
     150           1 : }
     151             : 
     152           3 : BOOST_AUTO_TEST_CASE(Check_whether_the_sum_variable_will_not_get_the_same_name_as_the_newly_introduced_process_parameter2)
     153             : {
     154             :   const std::string spec =
     155             :      "act\n"
     156             :      "  a,c,b,d;\n"
     157             :      "\n"
     158             :      "proc\n"
     159             :      "  P = b;\n"
     160             :      "  Q = (((tau) . (sum b1: Bool . (sum b2: Bool . (R)))) . (tau)) + (((delta) . (tau)) . (R));\n"
     161             :      "  R = ((true) -> (a)) + ((true) -> (sum b1: Bool . ((d) + ((d) + (a)))) <> ((d) + (a)));\n"
     162             :      "\n"
     163             :      "init\n"
     164           2 :      "  hide({b}, ((R) || (Q)) || (P));\n";
     165             : 
     166           1 :   run_linearisation_test_case(spec,true);
     167           1 : } 
     168             : 
     169           3 : BOOST_AUTO_TEST_CASE(linearisation_of_the_enclosed_spec_caused_a_name_conflict_with_the_option_lstack)
     170             : {
     171             :   const std::string spec =
     172             :      "act\n"
     173             :      "  c;\n"
     174             :      "\n"
     175             :      "proc\n"
     176             :      "  Q = sum b1: Bool . R;\n"
     177             :      "  R = sum b1: Bool . c.delta;\n"
     178             :      "\n"
     179           2 :      "init Q;\n";
     180             : 
     181           1 :   run_linearisation_test_case(spec,true);
     182           4 : } 
     183             : 
     184             : #else // ndef MCRL2_SKIP_LONG_TESTS
     185             : 
     186             : BOOST_AUTO_TEST_CASE(skip_linearization_test)
     187             : {
     188             : }
     189             : 
     190             : #endif // ndef MCRL2_SKIP_LONG_TESTS
     191             : 

Generated by: LCOV version 1.13