LCOV - code coverage report
Current view: top level - lps/test - linearization_test1.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 190 190 100.0 %
Date: 2020-07-04 00:44:36 Functions: 70 70 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_test1.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE linearization_test1
      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         210 : void run_linearisation_instance(const std::string& spec, const t_lin_options& options, bool expect_success)
      27             : {
      28         210 :   if (expect_success)
      29             :   {
      30         396 :     lps::specification s=remove_stochastic_operators(linearise(spec, options));
      31         198 :     BOOST_CHECK(s != lps::specification());
      32             :   }
      33             :   else
      34             :   {
      35          12 :     BOOST_CHECK_THROW(linearise(spec, options), mcrl2::runtime_error);
      36             :   }
      37         210 : }
      38             : 
      39          35 : void run_linearisation_test_case(const std::string& spec, const bool expect_success = true)
      40             : {
      41             :   // Set various rewrite strategies
      42          70 :   rewrite_strategy_vector rewrite_strategies = data::detail::get_test_rewrite_strategies(false);
      43             : 
      44          70 :   for (rewrite_strategy_vector::const_iterator i = rewrite_strategies.begin(); i != rewrite_strategies.end(); ++i)
      45             :   {
      46          35 :     std::clog << std::endl << "Testing with rewrite strategy " << *i << std::endl;
      47             : 
      48          35 :     t_lin_options options;
      49          35 :     options.rewrite_strategy=*i;
      50             : 
      51          35 :     std::clog << "  Default options" << std::endl;
      52          35 :     run_linearisation_instance(spec, options, expect_success);
      53             : 
      54          35 :     std::clog << "  Linearisation method regular2" << std::endl;
      55          35 :     options.lin_method=lmRegular2;
      56          35 :     run_linearisation_instance(spec, options, expect_success);
      57             : 
      58          35 :     std::clog << "  Linearisation method stack" << std::endl;
      59          35 :     options.lin_method=lmStack;
      60          35 :     run_linearisation_instance(spec, options, expect_success);
      61             : 
      62          35 :     std::clog << "  Linearisation method stack; binary enabled" << std::endl;
      63          35 :     options.binary=true;
      64          35 :     run_linearisation_instance(spec, options, expect_success);
      65             : 
      66          35 :     std::clog << "  Linearisation method regular; binary enabled" << std::endl;
      67          35 :     options.lin_method=lmRegular;
      68          35 :     run_linearisation_instance(spec, options, expect_success);
      69             : 
      70          35 :     std::clog << "  Linearisation method regular; no intermediate clustering" << std::endl;
      71          35 :     options.binary=false; // reset binary
      72          35 :     options.no_intermediate_cluster=true;
      73          35 :     run_linearisation_instance(spec, options, expect_success);
      74             :   }
      75          35 : }
      76             : 
      77           3 : BOOST_AUTO_TEST_CASE(test_multiple_linearization_calls)
      78             : {
      79             :   // Parameter i should be removed
      80             :   const std::string case_1(
      81             :     "act a;\n\n"
      82             :     "proc X(i: Nat) = a.X(i);\n\n"
      83           2 :     "init X(2);\n");
      84             : 
      85             :   // Parameter j should be removed
      86             :   const std::string case_2(
      87             :     "act a: Nat;\n\n"
      88             :     "proc X(i,j: Nat) = a(i). X(i,j);\n\n"
      89           2 :     "init X(0,1);\n");
      90             : 
      91             :   // Parameter j should be removed
      92             :   const std::string case_3(
      93             :     "act a;\n\n"
      94             :     "proc X(i,j: Nat)   = (i == 5) -> a. X(i,j);\n\n"
      95           2 :     "init X(0,1);\n");
      96             : 
      97             :   // Parameter j should be removed
      98             :   const std::string case_4(
      99             :     "act a;\n\n"
     100             :     "proc X(i,j: Nat) = a@i.X(i,j);\n\n"
     101           2 :     "init X(0,4);\n");
     102             : 
     103             :   // Nothing should be removed
     104             :   const std::string case_5(
     105             :     "act a: Nat;\n"
     106             :     "act b;\n\n"
     107             :     "proc X(i,j,k: Nat) =  a(i).X(k,j,k) +\n"
     108             :     "                         b.X(j,j,k);\n\n"
     109           2 :     "init X(1,2,3);");
     110             : 
     111             :   // Nothing should be removed
     112             :   const std::string case_6(
     113             :     "act act1, act2, act3: Nat;\n\n"
     114             :     "proc X(i: Nat)   = (i <  5) -> act1(i).X(i+1) +\n"
     115             :     "                   (i == 5) -> act3(i).Y(i, i);\n"
     116             :     "     Y(i,j: Nat) = act2(j).Y(i,j+1);\n\n"
     117           2 :     "init X(0);\n");
     118             : 
     119             :   const std::string case_7(
     120             :     "act act1, act2, act3: Nat;\n\n"
     121             :     "proc X(i,z,j: Nat)   = (i <  5) -> act1(i)@z.X(i+1,z, j) +\n"
     122             :     "                       (i == 5) -> act3(i).X(i, j, 4);\n\n"
     123             :     "init X(0,5, 1);\n"
     124           2 :   );
     125             : 
     126             :   const std::string case_8(
     127             :     "act a;\n"
     128             :     "init sum t:Nat. a@t;\n"
     129           2 :   );
     130             : 
     131             :   // Check that rewriting of non explicitly declared lists
     132             :   // works properly.
     133             :   const std::string case_9
     134             :   (
     135             :     "act c;\n"
     136             :     "init sum t:List(struct a | b) . c;\n"
     137           2 :   );
     138             : 
     139           2 :   stochastic_specification spec;
     140           1 :   spec = linearise(case_1);
     141           1 :   spec = linearise(case_2);
     142           1 :   spec = linearise(case_3);
     143           1 :   spec = linearise(case_4);
     144           1 :   spec = linearise(case_5);
     145           1 :   spec = linearise(case_6);
     146           1 :   spec = linearise(case_7);
     147           1 :   spec = linearise(case_8);
     148           1 :   spec = linearise(case_9);
     149           1 : }
     150             : 
     151           3 : BOOST_AUTO_TEST_CASE(test_process_assignments)
     152             : {
     153             :   const std::string assignment_case_1
     154             :   ("act a,b,c;"
     155             :    "proc X(v:Nat)=a.X(v=3)+Y(1,2);"
     156             :    "Y(v1:Nat, v2:Nat)=a.Y(v1=3)+b.X(5)+c.Y(v2=7);"
     157             :    "init X(3);"
     158           2 :   );
     159             : 
     160             :   const std::string assignment_case_2
     161             :   ("act a;"
     162             :    "proc X(v:Nat)=a.Y(w=true);"
     163             :    "Y(w:Bool)=a.X(v=0);"
     164             :    "init X(v=3);"
     165           2 :   );
     166             : 
     167             :   const std::string assignment_case_3
     168             :   ("act a;"
     169             :    "    b:Nat;"
     170             :    "proc X(v:Nat,w:List(Bool))=a.X(w=[])+"
     171             :    "                         (v>0) ->b(v).X(v=max(v,0));"
     172             :    "init X(v=3,w=[]);"
     173             : 
     174           2 :   );
     175             : 
     176             :   const std::string assignment_case_4
     177             :   ("act a;"
     178             :    "proc X(v:Pos,w:Nat)=sum w:Pos.a.X(v=w)+"
     179             :    "                    sum u:Pos.a.X(v=u);"
     180             :    "init X(3,4);"
     181             : 
     182           2 :   );
     183             : 
     184             :   const std::string assignment_case_5
     185             :   ("act a;"
     186             :    "proc X(v:Pos)=sum v:Pos.a@4.X();"
     187             :    "init X(3);"
     188           2 :   );
     189             : 
     190           1 :   run_linearisation_test_case(assignment_case_1);
     191           1 :   run_linearisation_test_case(assignment_case_2);
     192           1 :   run_linearisation_test_case(assignment_case_3);
     193           1 :   run_linearisation_test_case(assignment_case_4);
     194           1 :   run_linearisation_test_case(assignment_case_5);
     195           1 : }
     196             : 
     197           3 : BOOST_AUTO_TEST_CASE(test_struct)
     198             : {
     199             :   std::string text =
     200             :     "sort D = struct d1(Nat)?is_d1 | d2(arg2:Nat)?is_d2;\n"
     201             :     "                                                   \n"
     202           2 :     "init true->delta;                                  \n"
     203             :     ;
     204           1 :   run_linearisation_test_case(text);
     205           1 : }
     206             : 
     207           3 : BOOST_AUTO_TEST_CASE(test_lambda)
     208             : {
     209           1 :   run_linearisation_test_case(
     210             :     "map select : (Nat -> Bool) # List(Nat) -> List(Nat);\n"
     211             :     "var f : Nat -> Bool;\n"
     212             :     "    x : Nat;\n"
     213             :     "    xs : List(Nat);\n"
     214             :     "eqn select(f,[]) = [];\n"
     215             :     "    select(f,x|>xs) = if(f(x), x|>sxs, sxs) whr sxs = select(f, xs) end;\n"
     216             :     "act a : Nat;\n"
     217             :     "init sum n : Nat.\n"
     218             :     "  (n in select(lambda x : Nat.x mod 2 == 0, [1, 2, 3])) -> a(n).delta;\n");
     219           1 : }
     220             : 
     221           3 : BOOST_AUTO_TEST_CASE(test_no_free_variables)
     222             : {
     223             :   const std::string no_free_variables_case_1(
     224             :     "act a,b:Int;\n"
     225             :     "proc P = sum y:Int . (y == 4) -> a(y)@y . b(y*2)@(y+1) . P;\n"
     226             :     "init P;\n"
     227           2 :   );
     228             : 
     229           1 :   t_lin_options options;
     230           1 :   options.noglobalvars = true;
     231             : 
     232           2 :   stochastic_specification spec;
     233           1 :   spec = linearise(no_free_variables_case_1, options);
     234           1 :   BOOST_CHECK(spec.global_variables().empty());
     235           1 : }
     236             : 
     237             : // Here various testcases are checked, which have been used in
     238             : // debugging the translation of the linearizer to the new data
     239             : // library. 
     240           3 : BOOST_AUTO_TEST_CASE(various_case_1)
     241             : {
     242           1 :   run_linearisation_test_case(
     243             :     "init delta;"
     244             :   );
     245           1 : }
     246             : 
     247           3 : BOOST_AUTO_TEST_CASE(various_case_2)
     248             : {
     249             :   const std::string various_case_2=
     250             :     "act a;"
     251             :     "proc X=a.X;"
     252           2 :     "init X;";
     253           1 :   run_linearisation_test_case(various_case_2);
     254           1 : }
     255             : 
     256           3 : BOOST_AUTO_TEST_CASE(various_case_3)
     257             : {
     258             :   const std::string various_case_3=
     259             :     "sort D     = struct d1 | d2;"
     260             :     "             Error = struct e;"
     261             :     "act r2: D # Bool;"
     262             :     "    s3: D # Bool;"
     263             :     "    s3: Error;"
     264             :     "    i;"
     265             :     "proc K = sum d:D,b:Bool. r2(d,b).(i.s3(d,b)+i.s3(e)).K;"
     266           2 :     "init K;";
     267           1 :   run_linearisation_test_case(various_case_3);
     268           1 : }
     269             : 
     270           3 : BOOST_AUTO_TEST_CASE(various_case_4)
     271             : {
     272             :   const std::string various_case_4=
     273             :     "act a:Nat;"
     274             :     "proc X=sum n:Nat. (n==0)->a(n).X;"
     275           2 :     "init X;";
     276           1 :   run_linearisation_test_case(various_case_4);
     277           1 : }
     278             : 
     279           3 : BOOST_AUTO_TEST_CASE(various_case_5)
     280             : {
     281             :   const std::string various_case_5=
     282             :     "act a,b,c;"
     283             :     "proc X=a.X;"
     284             :     "     Y=b.Y;"
     285           2 :     "init X||Y;";
     286           1 :   run_linearisation_test_case(various_case_5);
     287           1 : }
     288             : 
     289           3 : BOOST_AUTO_TEST_CASE(various_case_6)
     290             : {
     291             :   const std::string various_case_6=
     292             :     "act a1,a2,b,c;"
     293             :     "proc X=a1.a2.X;"
     294             :     "     Y=b.Y;"
     295           2 :     "init comm({a1|b->c},X||Y);";
     296           1 :   run_linearisation_test_case(various_case_6);
     297           1 : }
     298             : 
     299           3 : BOOST_AUTO_TEST_CASE(various_case_7)
     300             : {
     301             :   const std::string various_case_7=
     302             :     "proc X=tau.X;"
     303           2 :     "init X;";
     304           1 :   run_linearisation_test_case(various_case_7);
     305           1 : }
     306             : 
     307           3 : BOOST_AUTO_TEST_CASE(various_case_8)
     308             : {
     309             :   const std::string various_case_8=
     310             :     "act a,b;"
     311             :     "proc X= (a|b).X;"
     312           2 :     "init X;";
     313           1 :   run_linearisation_test_case(various_case_8);
     314           1 : }
     315             : 
     316           3 : BOOST_AUTO_TEST_CASE(various_case_9)
     317             : {
     318             :   const std::string various_case_9=
     319             :     "act a;"
     320           2 :     "init allow({a},a.a.delta);";
     321           1 :   run_linearisation_test_case(various_case_9);
     322           1 : }
     323             : 
     324           3 : BOOST_AUTO_TEST_CASE(various_case_10)
     325             : {
     326             :   const std::string various_case_10=
     327             :     "act a,b,c;"
     328           2 :     "init comm({a|b->c},(a|b).delta);";
     329           1 :   run_linearisation_test_case(various_case_10);
     330           1 : }
     331             : 
     332           3 : BOOST_AUTO_TEST_CASE(various_case_11)
     333             : {
     334             :   const std::string various_case_11=
     335             :     "act a,b,c:Nat;"
     336             :     "map n:Nat;"
     337           2 :     "init comm({a|b->c},(a(3)|b(n)));";
     338           1 :   run_linearisation_test_case(various_case_11);
     339           1 : }
     340             : 
     341           3 : BOOST_AUTO_TEST_CASE(various_case_12)
     342             : {
     343             :   const std::string various_case_12=
     344             :     "act c2:Nat#Nat;"
     345           2 :     "init allow({c2},c2(3,5));";
     346           1 :   run_linearisation_test_case(various_case_12);
     347           1 : }
     348             : 
     349           3 : BOOST_AUTO_TEST_CASE(various_case_13)
     350             : {
     351             :   const std::string various_case_13=
     352             :     "sort D = struct d1 | d2;"
     353             :     "act r1,s4: D;"
     354             :     "proc S(b:Bool)     = sum d:D. r1(d).S(true);"
     355           2 :     "init S(false);";
     356           1 :   run_linearisation_test_case(various_case_13);
     357           1 : }
     358             : 
     359           3 : BOOST_AUTO_TEST_CASE(various_case_14)
     360             : {
     361             :   const std::string various_case_14=
     362             :     "act r1: Bool;"
     363             :     "proc S(d:Bool) = sum d:Bool. r1(d).S(true);"
     364           2 :     "init S(false);";
     365           1 :   run_linearisation_test_case(various_case_14);
     366           1 : }
     367             : 
     368           3 : BOOST_AUTO_TEST_CASE(various_case_15)
     369             : {
     370             :   const std::string various_case_15=
     371             :     "act a;"
     372           2 :     "init (a+a.a+a.a.a+a.a.a.a).delta;";
     373           1 :   run_linearisation_test_case(various_case_15);
     374           1 : }
     375             : 
     376           3 : BOOST_AUTO_TEST_CASE(various_case_16)
     377             : {
     378             :   const std::string various_case_16=
     379             :     "act s6,r6,c6, i;"
     380             :     "proc T = r6.T;"
     381             :     "     K = i.K;"
     382             :     "     L = s6.L;"
     383           2 :     "init comm({r6|s6->c6},T || K || L);";
     384           1 :   run_linearisation_test_case(various_case_16);
     385           1 : }
     386             : 
     387           3 : BOOST_AUTO_TEST_CASE(various_case_17)
     388             : {
     389             :   const std::string various_case_17=
     390             :     "act s3,r3,c3,s6;"
     391             :     "proc R = r3.R;"
     392             :     "     K = s3.K;"
     393             :     "     L = s6.L;"
     394           2 :     "init comm({r3|s3->c3}, K || L || R);";
     395           1 :   run_linearisation_test_case(various_case_17);
     396           1 : }
     397             : 
     398           3 : BOOST_AUTO_TEST_CASE(various_case_18)
     399             : {
     400             :   const std::string various_case_18=
     401             :     "act a,b,c,d,e;"
     402           2 :     "init comm({c|d->b},(a|b|c|d|e).delta);";
     403           1 :   run_linearisation_test_case(various_case_18);
     404           1 : }
     405             : 
     406           3 : BOOST_AUTO_TEST_CASE(various_case_19)
     407             : {
     408             :   const std::string various_case_19=
     409             :     "act a,b,c,d,e;"
     410           2 :     "init comm({e|d->b},(a|b|c|d|e).delta);";
     411           1 :   run_linearisation_test_case(various_case_19);
     412           1 : }
     413             : 
     414           3 : BOOST_AUTO_TEST_CASE(various_case_20)
     415             : {
     416             :   const std::string various_case_20=
     417             :     "act a:Nat;"
     418             :     "proc X(n:Nat)="
     419             :     "  sum n:Nat.(n>25) -> a(n).X(n)+"
     420             :     "  sum n:Nat.(n>25) -> a(n).X(n)+"
     421             :     "  (n>25) -> a(n).X(n);"
     422           2 :     "init X(1);";
     423           1 :   run_linearisation_test_case(various_case_20);
     424           1 : } 
     425             : 
     426           3 : BOOST_AUTO_TEST_CASE(various_case_21)
     427             : {
     428             :   const std::string various_case_21=
     429             :     "act a,b:Pos;"
     430             :     "proc X(m:Pos)= sum n:Nat. (n<1) -> a(1)|b(1)@1.X(1)+"
     431             :     "               sum n:Nat. (n<2) -> a(2)|b(2)@2.X(2)+"
     432             :     "               sum n:Nat. (n<3) -> a(3)|b(3)@3.X(3)+"
     433             :     "               sum n:Nat. (n<4) -> a(4)|b(4)@4.X(4)+"
     434             :     "               sum n:Nat. (n<5) -> a(5)|b(5)@5.X(5);"
     435           2 :     "init X(1);";
     436           1 :   run_linearisation_test_case(various_case_21);
     437           1 : }
     438             : 
     439           3 : BOOST_AUTO_TEST_CASE(various_case_22)
     440             : {
     441             :   const std::string various_case_22=
     442             :     "% This test is expected to fail with a proper error message.\n"
     443             :     "act a;\n"
     444             :     "proc P = (a || a) . P;\n"
     445           2 :     "init P;\n";
     446           1 :   run_linearisation_test_case(various_case_22, false);
     447           1 : }
     448             : 
     449           3 : BOOST_AUTO_TEST_CASE(various_case_23)
     450             : {
     451             :   const std::string various_case_23=
     452             :     "act a,b;"
     453           2 :     "init a@1.b@2.delta||tau.tau;";
     454           1 :   run_linearisation_test_case(various_case_23);
     455           1 : }
     456             : 
     457           3 : BOOST_AUTO_TEST_CASE(various_case_24)
     458             : {
     459             :   const std::string various_case_24=
     460             :     "act  a: Pos;"
     461             :     "glob x: Pos;"
     462             :     "proc P = a(x).P;"
     463           2 :     "init P;";
     464           1 :   run_linearisation_test_case(various_case_24);
     465           1 : }
     466             : 
     467             : // The testcase below is designed to test the constant elimination in the lineariser.
     468             : // Typically, x1 and x2 can be eliminated as they are always constant. Care must be
     469             : // taken however that the variable y does not become unbound in the process.
     470           3 : BOOST_AUTO_TEST_CASE(various_case_25)
     471             : {
     472             :   const std::string various_case_25=
     473             :     "act a:Pos#Pos#Pos;"
     474             :     "    b;"
     475             :     "proc Q(y:Pos)=P(y,1,1)||delta;"
     476             :     "     P(x1,x2,x3:Pos)=a(x1,x2,x3).P(x1,x2,x3+1);"
     477           2 :     "init Q(2);";
     478           1 :   run_linearisation_test_case(various_case_25);
     479           1 : }
     480             : 
     481             : // The following testcase exhibits a problem that occurred in the lineariser in
     482             : // August 2009. The variable m would only be partly renamed, and show up as an
     483             : // undeclared variable in the resulting LPS. The LPS turned out to be not well
     484             : // typed.
     485           3 : BOOST_AUTO_TEST_CASE(various_case_26)
     486             : {
     487             :   const std::string various_case_26=
     488             :     "act  r,s1,s2:Nat;\n"
     489             :     "proc P=sum m:Nat.r(m).((m==1)->s1(m).P+(m==2)->P+P);\n"
     490           2 :     "init P;\n";
     491           1 :   run_linearisation_test_case(various_case_26);
     492           1 : }
     493             : 
     494             : // The following testcase exhibits a problem that occurred with sorts without explicit elements.
     495             : // See bug report #1553. 
     496           3 : BOOST_AUTO_TEST_CASE(bug_report_1553)
     497             : {
     498             :   const std::string report_1553=
     499             :     "act  a: D;\n"
     500             :     "sort D;\n"
     501             :     "\n"
     502             :     "proc X1 = sum d: D. a(d) . X1;\n"
     503             :     "\n"
     504           2 :     "init sum d1: D. a(d1) . X1;\n";
     505           1 :   run_linearisation_test_case(report_1553);
     506           1 : }
     507             : 
     508             : // The following testcase showed a problem with typechecking where the ambiguous type 
     509             : // of the function f was not detected. This problem cannot be linearised, due to a type problem. 
     510           3 : BOOST_AUTO_TEST_CASE(bug_report_1576)
     511             : {
     512             :   const std::string report_1576=
     513             :     "map\n"
     514             :     "  f : Nat # Nat -> Nat;\n"
     515             :     "  f : Nat -> Nat;\n"
     516             :     "  g : Nat # Nat -> Nat;\n"
     517             :     "  g : Nat -> Nat;\n"
     518             :     "\n"
     519             :     "eqn\n"
     520             :     "  f = g;\n"
     521             :     "\n"
     522           2 :     "init delta;\n";
     523           1 :   run_linearisation_test_case(report_1576, false);
     524           4 : }
     525             : 
     526             : #else // ndef MCRL2_SKIP_LONG_TESTS
     527             : 
     528             : BOOST_AUTO_TEST_CASE(skip_linearization_test)
     529             : {
     530             : }
     531             : 
     532             : #endif // ndef MCRL2_SKIP_LONG_TESTS
     533             : 

Generated by: LCOV version 1.13