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 :