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_test4
      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             : 
      27           2 : BOOST_AUTO_TEST_CASE(various_case_27)
      28             : {
      29             :   const std::string various_case_27=
      30             :     "act a:Pos;\n"
      31             :     "proc P(id,n:Pos)=(id<n) -> a(n).P(id,n);\n"
      32             :     "     Q(n:Pos)=P(1,n)||P(2,n)||P(3,n);\n"
      33           1 :     "init Q(15);\n";
      34           1 :   run_linearisation_test_case(various_case_27);
      35           1 : }
      36             : 
      37           2 : BOOST_AUTO_TEST_CASE(various_case_28)
      38             : {
      39             :   const std::string various_case_28=
      40             :     "sort A=List(Nat->Nat);"
      41             :     "T=struct f(Nat->Nat);"
      42             :     "act b:A;"
      43             :     "proc P(a:A)=b(a).P([]);"
      44           1 :     "init P([lambda n:Nat.n]);";
      45           1 :   run_linearisation_test_case(various_case_28);
      46           1 : }
      47             : 
      48           2 : BOOST_AUTO_TEST_CASE(various_case_29)
      49             : {
      50             :   const std::string various_case_29=
      51             :     "sort Data = struct x;"
      52             :     "Coloured = struct flow(data : Data) | noflowG | noflowR;"
      53             :     "act A, B : Coloured;"
      54             :     "proc Sync = ( (A(noflowG) | B(noflowR))  + "
      55             :     "     (A(noflowR) | B(noflowR)) + "
      56             :     "     (sum d : Data.(A(flow(d)) | B(flow(d)))) "
      57             :     "  ).Sync;"
      58           1 :     "init Sync;";
      59           1 :   run_linearisation_test_case(various_case_29);
      60           1 : }
      61             : 
      62             : // The test case below is to test whether the elements of a multi-action
      63             : // are dealt with properly when they occur in a subexpression. The linearised
      64             : // process below should have three and not two summand.
      65           2 : BOOST_AUTO_TEST_CASE(various_case_30)
      66             : {
      67             :   const std::string various_case_30=
      68             :     "act a;"
      69             :     "    b,b':Nat;"
      70           1 :     "init a.(b(0)|b'(0))+a.(b(0)|b(0));";
      71           1 :   run_linearisation_test_case(various_case_30);
      72           1 : }
      73             : 
      74           2 : BOOST_AUTO_TEST_CASE(various_case_31)
      75             : {
      76             :   const std::string various_case_31=
      77             :     "act a:List(List(Nat));"
      78             :     "proc X(x:List(List(Nat)))=a(x).delta;"
      79           1 :     "init X([[]]);";
      80           1 :   run_linearisation_test_case(various_case_31);
      81           1 : }
      82             : 
      83             : // Original name: LR2plus.mcrl2
      84             : // This example can only be parsed unambiguously by an LR(k) parser generator
      85             : // for the current grammar, where k > 1. Namely, process expression 'a + tau'
      86             : // cannot be parsed unambiguously. After parsing the identifier 'a', it has to
      87             : // be determined if 'a' is an action or process reference, or if 'a' is a data
      88             : // expression, viz. part of the left hand side of a conditional process
      89             : // expression. With a lookahead of 1, we may only use the '+' as extra
      90             : // information, which is not enough, because this symbol is also ambiguous.
      91             : 
      92           2 : BOOST_AUTO_TEST_CASE(various_case_LR2plus)
      93             : {
      94             :   const std::string various_case_LR2plus=
      95             :     "act\n"
      96             :     " a;\n\n"
      97             :     "init\n"
      98           1 :     " a + tau;";
      99           1 :   run_linearisation_test_case(various_case_LR2plus);
     100           1 : }
     101             : 
     102             : // Original name: LR2par.mcrl2
     103             : // This example can only be parsed unambiguously by an LR(k) parser generator
     104             : // for the current grammar, where k > 1. Namely, process expression '(a)'
     105             : // cannot be parsed unambiguously. After parsing the left parenthesis '(', it
     106             : // has to be determined if it is part of a process or data expression, viz.
     107             : // part of the left hand side of a conditional process expression. With a
     108             : // lookahead of 1, we may only use the identifier 'a' as extra information,
     109             : // which is not enough, because this symbol is also ambiguous.
     110             : 
     111           2 : BOOST_AUTO_TEST_CASE(various_case_LR2par)
     112             : {
     113             :   const std::string various_case_LR2par=
     114             :     "act\n"
     115             :     " a;\n\n"
     116             :     "init\n"
     117           1 :     " (a);";
     118           1 :   run_linearisation_test_case(various_case_LR2par);
     119           1 : }
     120             : 
     121             : 
     122             : // This test case is a simple test to test sort normalisation in the lineariser,
     123             : // added because assertion failures in the domineering example were observed 
     124           2 : BOOST_AUTO_TEST_CASE(various_case_32)
     125             : {
     126             :   const std::string various_case_32 =
     127             :     "sort Position = struct Full | Empty;\n"
     128             :     "     Row = List(Position);\n"
     129             :     "\n"
     130             :     "proc P(r:Row) = delta;\n"
     131           1 :     "init P([Empty]);\n"
     132             :     ;
     133           1 :   run_linearisation_test_case(various_case_32);
     134           1 : }
     135             : 
     136             : // This test case is a test to check whether constant elimination in the
     137             : // linearizer goes well. This testcase is inspired by an example by Chilo
     138             : // van Best. The problem is that the constant x:Nat below may not be
     139             : // recorded in the assignment list of process P, and therefore forgotten 
     140           2 : BOOST_AUTO_TEST_CASE(various_case_33)
     141             : {
     142             :   const std::string various_case_33 =
     143             :     "act  a:Nat; "
     144             :     "proc P(x:Nat,b:Bool,r:Real) = a(x).P(x,!b,r); "
     145             :     "     P(x:Nat) = P(x,true,1); "
     146           1 :     "init P(1); "
     147             :     ;
     148           1 :   run_linearisation_test_case(various_case_33);
     149           1 : }
     150             : 
     151             : // The test case below checks whether the alphabet conversion does not accidentally
     152             : // reverse the order of hide and sum operators. If this happens the linearizer will
     153             : // not be able to linearize this process 
     154           2 : BOOST_AUTO_TEST_CASE(various_case_34)
     155             : {
     156             :   const std::string various_case_34 =
     157             :     "act a; "
     158             : 
     159             :     "proc X = a.X;"
     160             :     "proc Y = sum n:Nat. X;"
     161             : 
     162           1 :     "init hide({a}, sum n:Nat. X);"
     163             :     ;
     164           1 :   run_linearisation_test_case(various_case_34);
     165           1 : }
     166             : 
     167             : // In the test below, the value 1 for the parameter step should be properly substituted,
     168             : // also in the distribution.
     169           2 : BOOST_AUTO_TEST_CASE(linearisation_of_distribution_over_initial_process)
     170             : {
     171             :   const std::string spec =
     172             :      "act RequestReading_;\n"
     173             :      "    SWFault;\n"
     174             :      "\n"
     175             :      "map sw_fault_prob: Pos -> Real;\n"
     176             :      "var x: Pos;\n"
     177             :      "eqn sw_fault_prob(x) = if(x == 2, 1/20, if(x == 1, 1/10, Int2Real(0)));\n"
     178             :      "\n"
     179             :      "proc Software(step: Pos) = (\n"
     180             :      "    (dist f:Bool[if(f, sw_fault_prob(step), 1-sw_fault_prob(step))] . (f -> SWFault . delta <> (\n"
     181             :      "        (step == 1) -> (\n"
     182             :      "            % First step: get sensor reading\n"
     183             :      "            RequestReading_ . delta\n"
     184             :      "        )))));\n"
     185             :      "\n"
     186           1 :      "init Software(1);\n";
     187             : 
     188           1 :   run_linearisation_test_case(spec,true);
     189           1 : }   
     190             : 
     191             : #else // ndef MCRL2_SKIP_LONG_TESTS
     192             : 
     193             : BOOST_AUTO_TEST_CASE(skip_linearization_test)
     194             : {
     195             : }
     196             : 
     197             : #endif // ndef MCRL2_SKIP_LONG_TESTS
     198             :