LCOV - code coverage report
Current view: top level - lps/test - linearization_test3.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 28 28 100.0 %
Date: 2024-03-08 02:52:28 Functions: 14 14 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.hpp>
      14             : 
      15             : #include "mcrl2/data/detail/rewrite_strategies.h"
      16             : #include "mcrl2/lps/is_well_typed.h"
      17             : #include "mcrl2/lps/linearise.h"
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::lps;
      21             : 
      22             : #include "utility.h"
      23             : 
      24           2 : BOOST_AUTO_TEST_CASE(The_unreachability_of_tau_is_not_properly_recognized)
      25             : {
      26             :   const std::string spec =
      27           1 :      "init (true -> delta <> delta) . tau;";
      28             : 
      29           1 :   run_linearisation_test_case(spec,true);
      30           1 : }
      31             : 
      32           2 : BOOST_AUTO_TEST_CASE(Moving_a_distribution_out_of_a_process_is_tricky)
      33             : {
      34             :   const std::string spec =
      35             :      "map  N:Pos;\n"
      36             :      "eqn  N=2;\n"
      37             :      "\n"
      38             :      "act  last_passenger_has_his_own_seat:Bool;\n"
      39             :      "     enter_plane:Bool#Bool;\n"
      40             :      "     enter;\n"
      41             :      "\n"
      42             :      "\n"
      43             :      "proc Plane(everybody_has_his_own_seat:Bool, number_of_empty_seats:Int)=\n"
      44             :      "             (enter.\n"
      45             :      "                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"
      46             :      "                b0 -> enter_plane(true,false).delta.Plane(everybody_has_his_own_seat,number_of_empty_seats-1)\n"
      47             :      "                   <>dist b1:Bool[if(b1,1/number_of_empty_seats,1-1/number_of_empty_seats)].\n"
      48             :      "                      enter_plane(false,b1).delta\n"
      49             :      "             );\n"
      50             :      "\n"
      51             :      "\n"
      52           1 :      "init dist b:Bool[if(b,1/N,(N-1)/N)].Plane(b,N-1);\n";
      53             : 
      54           1 :   run_linearisation_test_case(spec,true);
      55           1 : }
      56             : 
      57             : /* The test below failed with type checking (only in debug mode). The reason
      58             :  * is that the set {0,1} would obtain terms with different types (int, nat),
      59             :  * which is not a well typed set. This was reported by Muhammad Atif, error #1526. */
      60           2 : BOOST_AUTO_TEST_CASE(type_checking_a_finite_set_with_numbers_can_go_astray)
      61             : {
      62             :   const std::string spec =
      63             :      "act sendInt, rcvInt, transferInt:Int;\n"
      64             :      "\n"
      65             :      "proc P (bg:Bag(Int))=(count(2,bg)<2)->sum i:Int.rcvInt(i).P(Set2Bag({i})+bg);\n"
      66             :      "     Px(c:Nat)= (c<2)->sum x:Int.(x<3&&x>-2)->sendInt(x).Px(c+1);\n"
      67             :      "     Py(c:Nat)= (c<2)->sum x:Int.(x<3&&x>-2)->sendInt(x).Py(c+1);\n"
      68             :      "\n"
      69             :      "init allow({transferInt},\n"
      70             :      "       comm({sendInt|rcvInt->transferInt},\n"
      71           1 :      "           P(Set2Bag({0,1}))||Px(0)||Py(0) ));\n";
      72             : 
      73           1 :   run_linearisation_test_case(spec,true);
      74           1 : }
      75             : 
      76             : #ifndef MCRL2_SKIP_LONG_TESTS 
      77             : 
      78           2 : BOOST_AUTO_TEST_CASE(Type_checking_of_function_can_be_problematic)
      79             : {
      80             :   const std::string spec =
      81             :      "sort  State = struct S;\n"
      82             :      "proc X = ((lambda x: Nat. S)(3) == S)->tau.X;\n"
      83           1 :      "init X;\n";
      84             : 
      85           1 :   run_linearisation_test_case(spec,true);
      86           1 : }
      87             : 
      88           2 : BOOST_AUTO_TEST_CASE(Check_whether_the_sum_variable_will_not_get_the_same_name_as_the_newly_introduced_process_parameter)
      89             : {
      90             :   const std::string spec =
      91             :      "act  base ;\n"
      92             :      "     exponent: Real;\n"
      93             :      "proc Test_exponentation =\n"
      94             :      "       sum r: Real. base . exponent(r).delta ;\n"
      95             :      "\n"
      96           1 :      "init Test_exponentation+delta;\n";
      97             : 
      98           1 :   run_linearisation_test_case(spec,true);
      99           1 : }
     100             : 
     101           2 : BOOST_AUTO_TEST_CASE(Check_whether_the_sum_variable_will_not_get_the_same_name_as_the_newly_introduced_process_parameter2)
     102             : {
     103             :   const std::string spec =
     104             :      "act\n"
     105             :      "  a,c,b,d;\n"
     106             :      "\n"
     107             :      "proc\n"
     108             :      "  P = b;\n"
     109             :      "  Q = (((tau) . (sum b1: Bool . (sum b2: Bool . (R)))) . (tau)) + (((delta) . (tau)) . (R));\n"
     110             :      "  R = ((true) -> (a)) + ((true) -> (sum b1: Bool . ((d) + ((d) + (a)))) <> ((d) + (a)));\n"
     111             :      "\n"
     112             :      "init\n"
     113           1 :      "  hide({b}, ((R) || (Q)) || (P));\n";
     114             : 
     115           1 :   run_linearisation_test_case(spec,true);
     116           1 : } 
     117             : 
     118           2 : BOOST_AUTO_TEST_CASE(linearisation_of_the_enclosed_spec_caused_a_name_conflict_with_the_option_lstack)
     119             : {
     120             :   const std::string spec =
     121             :      "act\n"
     122             :      "  c;\n"
     123             :      "\n"
     124             :      "proc\n"
     125             :      "  Q = sum b1: Bool . R;\n"
     126             :      "  R = sum b1: Bool . c.delta;\n"
     127             :      "\n"
     128           1 :      "init Q;\n";
     129             : 
     130           1 :   run_linearisation_test_case(spec,true);
     131           1 : } 
     132             : 
     133             : #else // ndef MCRL2_SKIP_LONG_TESTS
     134             : 
     135             : BOOST_AUTO_TEST_CASE(skip_linearization_test)
     136             : {
     137             : }
     138             : 
     139             : #endif // ndef MCRL2_SKIP_LONG_TESTS
     140             : 

Generated by: LCOV version 1.14