LCOV - code coverage report
Current view: top level - lps/test - linearization_test2.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 136 136 100.0 %
Date: 2020-07-04 00:44:36 Functions: 56 56 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_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE linearization_test
      13             : #include <boost/test/included/unit_test_framework.hpp>
      14             : 
      15             : #ifndef MCRL2_SKIP_LONG_TESTS
      16             : 
      17             : #include "mcrl2/data/detail/rewrite_strategies.h"
      18             : #include "mcrl2/lps/linearise.h"
      19             : 
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::lps;
      22             : 
      23             : typedef data::rewriter::strategy rewrite_strategy;
      24             : typedef std::vector<rewrite_strategy> rewrite_strategy_vector;
      25             : 
      26         156 : void run_linearisation_instance(const std::string& spec, const t_lin_options& options, bool expect_success)
      27             : {
      28         156 :   if (expect_success)
      29             :   {
      30         288 :     lps::specification s=remove_stochastic_operators(linearise(spec, options));
      31         144 :     BOOST_CHECK(s != lps::specification());
      32             :   }
      33             :   else
      34             :   {
      35          12 :     BOOST_CHECK_THROW(linearise(spec, options), mcrl2::runtime_error);
      36             :   }
      37         156 : }
      38             : 
      39          26 : void run_linearisation_test_case(const std::string& spec, const bool expect_success = true)
      40             : {
      41             :   // Set various rewrite strategies
      42          52 :   rewrite_strategy_vector rewrite_strategies = data::detail::get_test_rewrite_strategies(false);
      43          26 :   std::clog << "Tested specification:\n" << spec << "\n------------------------------------\n";
      44             : 
      45          52 :   for (rewrite_strategy_vector::const_iterator i = rewrite_strategies.begin(); i != rewrite_strategies.end(); ++i)
      46             :   {
      47          26 :     std::clog << std::endl << "Testing with rewrite strategy " << *i << std::endl;
      48             : 
      49          26 :     t_lin_options options;
      50          26 :     options.rewrite_strategy=*i;
      51             : 
      52          26 :     std::clog << "  Default options" << std::endl;
      53          26 :     run_linearisation_instance(spec, options, expect_success);
      54             : 
      55          26 :     std::clog << "  Linearisation method regular2" << std::endl;
      56          26 :     options.lin_method=lmRegular2;
      57          26 :     run_linearisation_instance(spec, options, expect_success);
      58             : 
      59          26 :     std::clog << "  Linearisation method stack" << std::endl;
      60          26 :     options.lin_method=lmStack;
      61          26 :     run_linearisation_instance(spec, options, expect_success);
      62             : 
      63          26 :     std::clog << "  Linearisation method stack; binary enabled" << std::endl;
      64          26 :     options.binary=true;
      65          26 :     run_linearisation_instance(spec, options, expect_success);
      66             : 
      67          26 :     std::clog << "  Linearisation method regular; binary enabled" << std::endl;
      68          26 :     options.lin_method=lmRegular;
      69          26 :     run_linearisation_instance(spec, options, expect_success);
      70             : 
      71          26 :     std::clog << "  Linearisation method regular; no intermediate clustering" << std::endl;
      72          26 :     options.binary=false; // reset binary
      73          26 :     options.no_intermediate_cluster=true;
      74          26 :     run_linearisation_instance(spec, options, expect_success);
      75             :   }
      76          26 : }
      77             : 
      78           3 : BOOST_AUTO_TEST_CASE(various_case_27)
      79             : {
      80             :   const std::string various_case_27=
      81             :     "act a:Pos;\n"
      82             :     "proc P(id,n:Pos)=(id<n) -> a(n).P(id,n);\n"
      83             :     "     Q(n:Pos)=P(1,n)||P(2,n)||P(3,n);\n"
      84           2 :     "init Q(15);\n";
      85           1 :   run_linearisation_test_case(various_case_27);
      86           1 : }
      87             : 
      88           3 : BOOST_AUTO_TEST_CASE(various_case_28)
      89             : {
      90             :   const std::string various_case_28=
      91             :     "sort A=List(Nat->Nat);"
      92             :     "T=struct f(Nat->Nat);"
      93             :     "act b:A;"
      94             :     "proc P(a:A)=b(a).P([]);"
      95           2 :     "init P([lambda n:Nat.n]);";
      96           1 :   run_linearisation_test_case(various_case_28);
      97           1 : }
      98             : 
      99           3 : BOOST_AUTO_TEST_CASE(various_case_29)
     100             : {
     101             :   const std::string various_case_29=
     102             :     "sort Data = struct x;"
     103             :     "Coloured = struct flow(data : Data) | noflowG | noflowR;"
     104             :     "act A, B : Coloured;"
     105             :     "proc Sync = ( (A(noflowG) | B(noflowR))  + "
     106             :     "     (A(noflowR) | B(noflowR)) + "
     107             :     "     (sum d : Data.(A(flow(d)) | B(flow(d)))) "
     108             :     "  ).Sync;"
     109           2 :     "init Sync;";
     110           1 :   run_linearisation_test_case(various_case_29);
     111           1 : }
     112             : 
     113             : // The test case below is to test whether the elements of a multi-action
     114             : // are dealt with properly when they occur in a subexpression. The linearised
     115             : // process below should have three and not two summand.
     116           3 : BOOST_AUTO_TEST_CASE(various_case_30)
     117             : {
     118             :   const std::string various_case_30=
     119             :     "act a;"
     120             :     "    b,b':Nat;"
     121           2 :     "init a.(b(0)|b'(0))+a.(b(0)|b(0));";
     122           1 :   run_linearisation_test_case(various_case_30);
     123           1 : }
     124             : 
     125           3 : BOOST_AUTO_TEST_CASE(various_case_31)
     126             : {
     127             :   const std::string various_case_31=
     128             :     "act a:List(List(Nat));"
     129             :     "proc X(x:List(List(Nat)))=a(x).delta;"
     130           2 :     "init X([[]]);";
     131           1 :   run_linearisation_test_case(various_case_31);
     132           1 : }
     133             : 
     134             : // Original name: LR2plus.mcrl2
     135             : // This example can only be parsed unambiguously by an LR(k) parser generator
     136             : // for the current grammar, where k > 1. Namely, process expression 'a + tau'
     137             : // cannot be parsed unambiguously. After parsing the identifier 'a', it has to
     138             : // be determined if 'a' is an action or process reference, or if 'a' is a data
     139             : // expression, viz. part of the left hand side of a conditional process
     140             : // expression. With a lookahead of 1, we may only use the '+' as extra
     141             : // information, which is not enough, because this symbol is also ambiguous.
     142             : 
     143           3 : BOOST_AUTO_TEST_CASE(various_case_LR2plus)
     144             : {
     145             :   const std::string various_case_LR2plus=
     146             :     "act\n"
     147             :     " a;\n\n"
     148             :     "init\n"
     149           2 :     " a + tau;";
     150           1 :   run_linearisation_test_case(various_case_LR2plus);
     151           1 : }
     152             : 
     153             : // Original name: LR2par.mcrl2
     154             : // This example can only be parsed unambiguously by an LR(k) parser generator
     155             : // for the current grammar, where k > 1. Namely, process expression '(a)'
     156             : // cannot be parsed unambiguously. After parsing the left parenthesis '(', it
     157             : // has to be determined if it is part of a process or data expression, viz.
     158             : // part of the left hand side of a conditional process expression. With a
     159             : // lookahead of 1, we may only use the identifier 'a' as extra information,
     160             : // which is not enough, because this symbol is also ambiguous.
     161             : 
     162           3 : BOOST_AUTO_TEST_CASE(various_case_LR2par)
     163             : {
     164             :   const std::string various_case_LR2par=
     165             :     "act\n"
     166             :     " a;\n\n"
     167             :     "init\n"
     168           2 :     " (a);";
     169           1 :   run_linearisation_test_case(various_case_LR2par);
     170           1 : }
     171             : 
     172             : 
     173             : // This test case is a simple test to test sort normalisation in the lineariser,
     174             : // added because assertion failures in the domineering example were observed 
     175           3 : BOOST_AUTO_TEST_CASE(various_case_32)
     176             : {
     177             :   const std::string various_case_32 =
     178             :     "sort Position = struct Full | Empty;\n"
     179             :     "     Row = List(Position);\n"
     180             :     "\n"
     181             :     "proc P(r:Row) = delta;\n"
     182           2 :     "init P([Empty]);\n"
     183             :     ;
     184           1 :   run_linearisation_test_case(various_case_32);
     185           1 : }
     186             : 
     187             : // This test case is a test to check whether constant elimination in the
     188             : // linearizer goes well. This testcase is inspired by an example by Chilo
     189             : // van Best. The problem is that the constant x:Nat below may not be
     190             : // recorded in the assignment list of process P, and therefore forgotten 
     191           3 : BOOST_AUTO_TEST_CASE(various_case_33)
     192             : {
     193             :   const std::string various_case_33 =
     194             :     "act  a:Nat; "
     195             :     "proc P(x:Nat,b:Bool,r:Real) = a(x).P(x,!b,r); "
     196             :     "     P(x:Nat) = P(x,true,1); "
     197           2 :     "init P(1); "
     198             :     ;
     199           1 :   run_linearisation_test_case(various_case_33);
     200           1 : }
     201             : 
     202             : // The test case below checks whether the alphabet conversion does not accidentally
     203             : // reverse the order of hide and sum operators. If this happens the linearizer will
     204             : // not be able to linearize this process 
     205           3 : BOOST_AUTO_TEST_CASE(various_case_34)
     206             : {
     207             :   const std::string various_case_34 =
     208             :     "act a; "
     209             : 
     210             :     "proc X = a.X;"
     211             :     "proc Y = sum n:Nat. X;"
     212             : 
     213           2 :     "init hide({a}, sum n:Nat. X);"
     214             :     ;
     215           1 :   run_linearisation_test_case(various_case_34);
     216           1 : }
     217             : 
     218           3 : BOOST_AUTO_TEST_CASE(various_case_par)
     219             : {
     220             :   const std::string various_par =
     221             :     "act a;\n"
     222           2 :     "init a || a;\n"
     223             :     ;
     224           1 :   run_linearisation_test_case(various_par);
     225           1 : }
     226             : 
     227           3 : BOOST_AUTO_TEST_CASE(gpa_10_3)
     228             : {
     229             :   const std::string various_gpa_10_3 =
     230             :     "act\n"
     231             :     "  c,r_dup, s_dup1, s_dup2, r_inc, s_inc, r_mul1, r_mul2, s_mul: Int;\n"
     232             :     "proc\n"
     233             :     "  Dup = sum x:Int. r_dup(x) | s_dup1(x) | s_dup2(x) . Dup;\n"
     234             :     "  Inc = sum x:Int. r_inc(x) | s_inc(x+1) . Inc;\n"
     235             :     "  Mul = sum x,y:Int. r_mul1(x) | r_mul2(y) | s_mul(x*y) . Mul;\n"
     236             :     "  Dim = allow({r_dup | s_mul},\n"
     237             :     "          hide({c},comm({s_dup1 | r_mul1 -> c , s_dup2 | r_inc -> c, s_inc | r_mul2 ->c},\n"
     238             :     "            Dup || Inc || Mul\n"
     239             :     "          ))\n"
     240             :     "        );\n"
     241           2 :     "init Dim;\n"
     242             :     ;
     243           1 :   run_linearisation_test_case(various_gpa_10_3);
     244           1 : }
     245             : 
     246             : /* The following test cases fail because the n-parallel support in the alphabet reductions is broken
     247             :  * (Checked JK 31/8/2010)
     248             :  */
     249             : /*
     250             : BOOST_AUTO_TEST_CASE(philosophers)
     251             : {
     252             :   const std::string various_philosophers =
     253             :     "map K: Pos;\n"
     254             :     "eqn K = 10;\n"
     255             :     "act get,_get,__get,put,_put,__put: Pos#Pos;\n"
     256             :     "    eat: Pos;\n"
     257             :     "proc\n"
     258             :     "  Phil(n:Pos) = _get(n,n)._get(n,if(n==K,1,n+1)).eat(n)._put(n,n)._put(n,if(n==K,1,n+1)).Phil(n);\n"
     259             :     "  Fork(n:Pos) = sum m:Pos.get(m,n).put(m,n).Fork(n);\n"
     260             :     "  ForkPhil(n:Pos) = Fork(n) || Phil(n);\n"
     261             :     "  KForkPhil(p:Pos) =\n"
     262             :     "    (p>1) -> (ForkPhil(p)||KForkPhil(max(p-1,1)))<>ForkPhil(1);\n"
     263             :     "init allow( { __get, __put, eat },\n"
     264             :     "       comm( { get|_get->__get, put|_put->__put },\n"
     265             :     "         KForkPhil(K)\n"
     266             :     "     ));\n"
     267             :     ;
     268             :   run_linearisation_test_case(various_philosophers);
     269             : }
     270             : 
     271             : BOOST_AUTO_TEST_CASE(philosophers_nat)
     272             : {
     273             :   const std::string various_philosophers_nat =
     274             :     "map K: Nat;\n"
     275             :     "eqn K = 10;\n"
     276             :     "act get,_get,__get,put,_put,__put: Nat#Nat;\n"
     277             :     "    eat: Nat;\n"
     278             :     "proc\n"
     279             :     "  Phil(n:Nat) = _get(n,n)._get(n,if(n==K,1,n+1)).eat(n)._put(n,n)._put(n,if(n==K,1,n+1)).Phil(n);\n"
     280             :     "  Fork(n:Nat) = sum m:Nat.get(m,n).put(m,n).Fork(n);\n"
     281             :     "  ForkPhil(n:Nat) = Fork(n) || Phil(n);\n"
     282             :     "  KForkPhil(p:Nat) =\n"
     283             :     "    (p>1) -> (ForkPhil(p)||KForkPhil(max(p-1,1)))<>ForkPhil(1);\n"
     284             :     "init allow( { __get, __put, eat },\n"
     285             :     "       comm( { get|_get->__get, put|_put->__put },\n"
     286             :     "         KForkPhil(K)\n"
     287             :     "     ));\n"
     288             :     ;
     289             :   run_linearisation_test_case(various_philosophers_nat);
     290             : }
     291             : */
     292             : 
     293           3 : BOOST_AUTO_TEST_CASE(sort_aliases)
     294             : {
     295             :   const std::string various_sort_aliases =
     296             :     "sort Bits = struct b0|b1;\n"
     297             :     "     t_sys_regset_fsm_state = Bits;\n"
     298             :     "     t_timer_counter_fsm_state = Bits;\n"
     299             :     "map  timer_counter_fsm_state_idle: t_timer_counter_fsm_state;\n"
     300             :     "act  a:Bits;\n"
     301             :     "proc P(d:Bits)=a(d).delta;\n"
     302             :     "glob globd:Bits;\n"
     303           2 :     "init P(globd);\n"
     304             :     ;
     305           1 :   run_linearisation_test_case(various_sort_aliases);
     306           1 : }
     307             : 
     308           3 : BOOST_AUTO_TEST_CASE(test_aliases_complex)
     309             : {
     310             :   const std::string spec =
     311             :     "sort\n"
     312             :     "  Bits = struct singleBit (bit: Bool)?isSingleBit | bitVector (bitVec:List(Bool))?isBitVector;\n"
     313             :     "  t_sys_regset_fsm_state = Bits;\n"
     314             :     "  t_timer_counter_fsm_state = Bits;\n"
     315             :     "map\n"
     316             :     "  repeat : Bool # Nat -> Bits;\n"
     317             :     "  repeat_rec : Bool # Nat -> List(Bool);\n"
     318             :     "var\n"
     319             :     "  b:Bool;\n"
     320             :     "  n:Nat;\n"
     321             :     "eqn\n"
     322             :     "  repeat(b,n) = if(n <= 1, singleBit(b), bitVector(repeat_rec(b,n)));\n"
     323             :     "act a:Bits;\n"
     324           2 :     "init a(repeat(true,32)).delta;\n";
     325           1 :   run_linearisation_test_case(spec);
     326           1 : }
     327             : 
     328           3 : BOOST_AUTO_TEST_CASE(test_bug_775a)
     329             : {
     330             :   const std::string spec =
     331             :     "sort V = struct v1( l: Bool  );\n"
     332             :     "act  a:  List( Bool );\n"
     333             :     "sort B = Bool -> List(Bool);\n"
     334             :     "proc X( M: B ) = \n"
     335             :     "  sum v:V.  a( [] ) \n"
     336             :     "+ sum v:V.  a( M(l(v)))\n"
     337             :     ";\n"
     338           2 :     "init X( lambda i: Bool. [] );\n";
     339           1 :   run_linearisation_test_case(spec);
     340           1 : }
     341             : 
     342           3 : BOOST_AUTO_TEST_CASE(test_bug_775b)
     343             : {
     344             :   const std::string spec =
     345             :     "sort V = struct v1( l: Bool  );\n"
     346             :     "act  a:  List( Bool );\n"
     347             :     "sort B = Bool -> List(Bool);\n"
     348             :     "proc X( M: B ) = \n"
     349             :     "  sum v:V.  a( M(l(v)))\n"
     350             :     "+ sum v:V.  a( [] ) \n"
     351             :     ";\n"
     352           2 :     "init X( lambda i: Bool. [] );\n";
     353           1 :   run_linearisation_test_case(spec);
     354           1 : }
     355             : 
     356           3 : BOOST_AUTO_TEST_CASE(test_bug_alphabet_reduction)
     357             : {
     358             :   const std::string spec =
     359             :     "sort Variables = struct s;\n"
     360             :     "\n"
     361             :     "act send_c, recv_c, comm_c: Bool;\n"
     362             :     "    chng: Set(Variables);\n"
     363             :     "\n"
     364             :     "init allow( { comm_c | chng | chng } ,\n"
     365             :     "  comm( { send_c | recv_c -> comm_c,\n"
     366             :     "          chng | chng -> chng},\n"
     367             :     "          send_c(false) | chng( {} ) || recv_c(false) | chng( {s} )\n"
     368           2 :     "       ) );\n";
     369           1 :   run_linearisation_test_case(spec);
     370           1 : }
     371             : 
     372           3 : BOOST_AUTO_TEST_CASE(test_bug_alphabet_reduction1)
     373             : {
     374             :   const std::string spec =
     375             :     "act a: Bool;\n"
     376             :     "    b: Nat;\n"
     377             :     "\n"
     378             :     "proc X = allow( {b | a | a },\n"
     379             :     "          a(true)| b(5) | a(false) );\n"
     380             :     "\n"
     381           2 :     "init X;\n";
     382           1 :   run_linearisation_test_case(spec);
     383           1 : }
     384             : 
     385             : // The testcase below is added because the typechecker could not deal with this
     386             : // case. The three options for the action a caused it to become confused.
     387           3 : BOOST_AUTO_TEST_CASE(test_multiple_action_types)
     388             : {
     389             :   const std::string spec =
     390             :      "sort Id = Pos;\n"
     391             :      "\n"
     392             :      "map FALSE: Id -> Bool;\n"
     393             :      "var n: Id;\n"
     394             :      "eqn FALSE(n) = false;\n"
     395             :      "\n"
     396             :      "act a: (Id -> Bool);\n"
     397             :      "    a: Bool;\n"
     398             :      "    a: Pos;\n"
     399             :      "\n"
     400             :      "proc P = a(FALSE) . delta;\n"
     401           2 :      "init P;\n";
     402             : 
     403           1 :   run_linearisation_test_case(spec);
     404           1 : }
     405             : 
     406             : // Test case for bug #1085
     407           3 : BOOST_AUTO_TEST_CASE(bug_1085)
     408             : {
     409             :   const std::string spec =
     410             :     "proc P = tau. a | b | c;\n"
     411             :     "act a,b,c;\n"
     412           2 :     "init P;\n";
     413             : 
     414           1 :   run_linearisation_test_case(spec);
     415           1 : }
     416             : 
     417           3 : BOOST_AUTO_TEST_CASE(bug_978)
     418             : {
     419             :   const std::string spec =
     420             :      "act rd,wr:Bool;\n"
     421             :      "proc R(a,b : Bool) = \n"
     422             :      "        rd(a) . R() +\n"
     423             :      "        rd(b) . R() + \n"
     424             :      "        sum b:Bool. wr(b) . R(a=b);\n"
     425           2 :      "init R(true,true);\n";
     426           1 :   run_linearisation_test_case(spec);
     427           1 : }
     428             : 
     429           3 : BOOST_AUTO_TEST_CASE(not_properly_ordered_assignments)
     430             : {
     431             :   const std::string spec =
     432             :      "proc R(a,b : Bool) = \n"
     433             :      "        tau . R(a=true,b=false) +\n"
     434             :      "        tau . R(b=false,a=false); \n"
     435           2 :      "init R(true,true);\n";
     436           1 :   run_linearisation_test_case(spec);
     437           1 : }
     438             : 
     439           3 : BOOST_AUTO_TEST_CASE(the_bound_c_may_not_show_up_in_linear_process)
     440             : {
     441             :   const std::string spec =
     442             :      "act \n"
     443             :      "rcv_req; \n"
     444             :      "snd_return : Bool; \n"
     445             :      "internal; \n"
     446             :      " \n"
     447             :      "proc \n"
     448             :      " \n"
     449             :      "test1 = \n"
     450             :      "( \n"
     451             :      "    rcv_req. \n"
     452             :      "    sum c:Bool. \n"
     453             :      "    ( \n"
     454             :      "        internal.snd_return(c) \n"
     455             :      "    ). \n"
     456             :      "    test1 \n"
     457             :      "); \n"
     458             :      " \n"
     459           2 :      "init test1; \n";
     460           1 :   run_linearisation_test_case(spec);
     461           1 : }
     462             : 
     463           3 : BOOST_AUTO_TEST_CASE(process_parameters_with_different_types_can_cause_problems)
     464             : {
     465             :   const std::string spec =
     466             :      "proc P(x:Nat)=tau.Q(true); \n"
     467             :      "     Q(x:Bool)=tau.P(1); \n"
     468           2 :      "init P(1);\n";
     469             : 
     470           1 :   run_linearisation_test_case(spec);
     471           1 : }
     472             : 
     473           3 : BOOST_AUTO_TEST_CASE(unguarded_recursion)
     474             : {
     475             :   const std::string spec =
     476             :      "proc P=P; \n"
     477           2 :      "init P;\n";
     478             : 
     479           1 :   run_linearisation_test_case(spec,false);
     480           1 : }
     481             : 
     482           3 : BOOST_AUTO_TEST_CASE(unguarded_recursion_with_parallel_operator)
     483             : {
     484             :   const std::string spec =
     485             :      "proc P=P||P; \n"
     486           2 :      "init P;\n";
     487             : 
     488           1 :   run_linearisation_test_case(spec,false);
     489           4 : }
     490             : 
     491             : #else // ndef MCRL2_SKIP_LONG_TESTS
     492             : 
     493             : BOOST_AUTO_TEST_CASE(skip_linearization_test)
     494             : {
     495             : }
     496             : 
     497             : #endif // ndef MCRL2_SKIP_LONG_TESTS
     498             : 

Generated by: LCOV version 1.13