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