LCOV - code coverage report
Current view: top level - process/test - process_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 90 92 97.8 %
Date: 2020-09-22 00:46:14 Functions: 10 10 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Wieger Wesselink
       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 process_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE process_test
      13             : 
      14             : #include "mcrl2/process/balance_nesting_depth.h"
      15             : #include "mcrl2/process/is_guarded.h"
      16             : #include "mcrl2/process/is_linear.h"
      17             : #include "mcrl2/process/parse.h"
      18             : 
      19             : #include <boost/test/included/unit_test_framework.hpp>
      20             : 
      21             : using namespace mcrl2;
      22             : using namespace mcrl2::process;
      23             : 
      24           1 : const std::string SPEC1 =
      25             :   "act a;                  \n"
      26             :   "proc X = a;             \n"
      27             :   "init X;                 \n"
      28             :   ;
      29             : 
      30           1 : const std::string SPEC2 =
      31             :   "act a;                  \n"
      32             :   "proc X(i: Nat) = a.X(i);\n"
      33             :   "init X(2);              \n"
      34             :   ;
      35             : 
      36           1 : const std::string ABS_SPEC_LINEARIZED =
      37             :   "sort D = struct d1 | d2;                                                                                                     \n"
      38             :   "     Error = struct e;                                                                                                       \n"
      39             :   "                                                                                                                             \n"
      40             :   "act  r1,s4: D;                                                                                                               \n"
      41             :   "     s2,r2,c2,s3,r3,c3: D # Bool;                                                                                            \n"
      42             :   "     s3,r3,c3: Error;                                                                                                        \n"
      43             :   "     s5,r5,c5,s6,r6,c6: Bool;                                                                                                \n"
      44             :   "     s6,r6,c6: Error;                                                                                                        \n"
      45             :   "     i;                                                                                                                      \n"
      46             :   "                                                                                                                             \n"
      47             :   "proc P(s31_S: Pos, d_S: D, b_S: Bool, s32_K: Pos, d_K: D, b_K: Bool, s33_L: Pos, b_L: Bool, s34_R: Pos, d_R: D, b_R: Bool) = \n"
      48             :   "       sum e1_S: Bool.                                                                                                       \n"
      49             :   "         ((s31_S == 3 && s33_L == 3) && if(e1_S, !b_S, b_S) == b_L) ->                                                       \n"
      50             :   "         c6(if(e1_S, !b_S, b_S)) .                                                                                           \n"
      51             :   "         P(if(e1_S, 2, 1), if(e1_S, d_S, d2), if(e1_S, b_S, !b_S), s32_K, d_K, b_K, 1, false, s34_R, d_R, b_R)               \n"
      52             :   "     + (s31_S == 3 && s33_L == 4) ->                                                                                         \n"
      53             :   "         c6(e) .                                                                                                             \n"
      54             :   "         P(2, d_S, b_S, s32_K, d_K, b_K, 1, false, s34_R, d_R, b_R)                                                          \n"
      55             :   "     + (s31_S == 2 && s32_K == 1) ->                                                                                         \n"
      56             :   "         c2(d_S, b_S) .                                                                                                      \n"
      57             :   "         P(3, d_S, b_S, 2, d_S, b_S, s33_L, b_L, s34_R, d_R, b_R)                                                            \n"
      58             :   "     + sum e2_K: Bool.                                                                                                       \n"
      59             :   "         (s32_K == 2) ->                                                                                                     \n"
      60             :   "         i .                                                                                                                 \n"
      61             :   "         P(s31_S, d_S, b_S, if(e2_K, 4, 3), if(e2_K, d2, d_K), if(e2_K, false, b_K), s33_L, b_L, s34_R, d_R, b_R)            \n"
      62             :   "     + sum e4_R: Bool.                                                                                                       \n"
      63             :   "         (s33_L == 1 && if(e4_R, s34_R == 4, s34_R == 3)) ->                                                                 \n"
      64             :   "         c5(if(e4_R, !b_R, b_R)) .                                                                                           \n"
      65             :   "         P(s31_S, d_S, b_S, s32_K, d_K, b_K, 2, if(e4_R, !b_R, b_R), 1, d2, if(e4_R, b_R, !b_R))                             \n"
      66             :   "     + (s34_R == 2) ->                                                                                                       \n"
      67             :   "         s4(d_R) .                                                                                                           \n"
      68             :   "         P(s31_S, d_S, b_S, s32_K, d_K, b_K, s33_L, b_L, 3, d2, b_R)                                                         \n"
      69             :   "     + sum e3_L: Bool.                                                                                                       \n"
      70             :   "         (s33_L == 2) ->                                                                                                     \n"
      71             :   "         i .                                                                                                                 \n"
      72             :   "         P(s31_S, d_S, b_S, s32_K, d_K, b_K, if(e3_L, 4, 3), if(e3_L, false, b_L), s34_R, d_R, b_R)                          \n"
      73             :   "     + (s32_K == 4 && s34_R == 1) ->                                                                                         \n"
      74             :   "         c3(e) .                                                                                                             \n"
      75             :   "         P(s31_S, d_S, b_S, 1, d2, false, s33_L, b_L, 4, d2, b_R)                                                            \n"
      76             :   "     + sum e5_R: Bool.                                                                                                       \n"
      77             :   "         ((s32_K == 3 && s34_R == 1) && if(e5_R, b_R, !b_R) == b_K) ->                                                       \n"
      78             :   "         c3(d_K, if(e5_R, b_R, !b_R)) .                                                                                      \n"
      79             :   "         P(s31_S, d_S, b_S, 1, d2, false, s33_L, b_L, if(e5_R, 2, 4), if(e5_R, d_K, d2), b_R)                                \n"
      80             :   "     + sum d3_S: D.                                                                                                          \n"
      81             :   "         (s31_S == 1) ->                                                                                                     \n"
      82             :   "         r1(d3_S) .                                                                                                          \n"
      83             :   "         P(2, d3_S, b_S, s32_K, d_K, b_K, s33_L, b_L, s34_R, d_R, b_R)                                                       \n"
      84             :   "     + true ->                                                                                                               \n"
      85             :   "         delta;                                                                                                              \n"
      86             :   "                                                                                                                             \n"
      87             :   "init P(1, d2, true, 1, d2, false, 1, false, 1, d2, true);                                                                    \n"
      88             :   ;
      89             : 
      90             : // CASE?? specifications were borrowed from sumelm_test.
      91             : 
      92           1 : std::string CASE1 =
      93             :   "sort S = struct s1 | s2;\n"
      94             :   "map f : S -> Bool;\n"
      95             :   "act a : S # Bool;\n"
      96             :   "proc P = sum c : S, b : Bool . (b == f(c) && c == s2) -> a(c, b) . P;\n"
      97             :   "init P;\n"
      98             :   ;
      99             : 
     100           1 : std::string CASE2 =
     101             :   "act a,b;\n"
     102             :   "proc P(s3_P: Pos) = sum y_P: Int. (s3_P == 1) -> a . P(2)\n"
     103             :   "                  + (s3_P == 2) -> b . P(1);\n"
     104             :   "init P(1);\n"
     105             :   ;
     106             : 
     107           1 : std::string CASE3 =
     108             :   "act a;\n"
     109             :   "proc P = sum y:Int . (4 == y) -> a . P;\n"
     110             :   "init P;\n"
     111             :   ;
     112             : 
     113           1 : std::string CASE4 =
     114             :   "act a;\n"
     115             :   "proc P = sum y:Int . (y == 4) -> a . P;\n"
     116             :   "init P;\n"
     117             :   ;
     118             : 
     119           1 : std::string CASE5 =
     120             :   "act a,b:Int;\n"
     121             :   "proc P = sum y:Int . (y == 4) -> a(y)@y . b(y*2)@(y+1) . P;\n"
     122             :   "init P;\n"
     123             :   ;
     124             : 
     125           1 : std::string CASE6 =
     126             :   "act a;\n"
     127             :   "proc P = sum y:Int . (y == y + 1) -> a . P;\n"
     128             :   "init P;\n"
     129             :   ;
     130             : 
     131           1 : std::string CASE7 =
     132             :   "sort D = struct d1 | d2 | d3;\n"
     133             :   "map g : D -> D;\n"
     134             :   "act a;\n"
     135             :   "proc P(c:D) = sum d:D . sum e:D . sum f:D . (d == e && e == g(e) && e == f) -> a . P(d);\n"
     136             :   "init P(d1);\n"
     137             :   ;
     138             : 
     139           1 : std::string CASE8 =
     140             :   "sort D = struct d1 | d2 | d3;\n"
     141             :   "act a;\n"
     142             :   "proc P(c:D) = sum d:D . sum e:D . sum f:D . (d == e && d == f) -> a . P(d);\n"
     143             :   "init P(d1);\n"
     144             :   ;
     145             : 
     146           1 : std::string CASE9 =
     147             :   "proc P = sum y:Bool . y -> delta;\n"
     148             :   "init P;\n"
     149             :   ;
     150             : 
     151           1 : std::string CASE10 =
     152             :   "act a:Nat;\n"
     153             :   "proc P(n0: Nat) = sum n: Nat. (n == n0 && n == 1) -> a(n0) . P(n);\n"
     154             :   "init P(0);\n"
     155             :   ;
     156             : 
     157             : // provided by Jeroen Keiren
     158           1 : std::string CASE11 =
     159             :   "act  a,b: Int;                       \n"
     160             :   "glob dc,dc0: Int;                    \n"
     161             :   "proc P(s3_P: Pos, y_P: Int) =        \n"
     162             :   "       sum y0_P: Int.                \n"
     163             :   "         (s3_P == 1 && y0_P == 4) -> \n"
     164             :   "         a(y0_P) @ y0_P .            \n"
     165             :   "         P(s3_P = 2, y_P = y0_P)     \n"
     166             :   "     + (s3_P == 2) ->                \n"
     167             :   "         b(y_P * 2) @ (y_P + 1) .    \n"
     168             :   "         P(s3_P = 1, y_P = dc0);     \n"
     169             :   "init P(1, dc);                       \n"
     170             :   ;
     171             : 
     172             : // test case containing a global variable
     173           1 : std::string CASE12 =
     174             :   " act a: Nat ;                      \n"
     175             :   " glob  v: Nat ;                    \n"
     176             :   " proc P(i, j: Nat) =               \n"
     177             :   "        (i == j) -> a(i) . P(1, 1) \n"
     178             :   "        ;                          \n"
     179             :   "                                   \n"
     180             :   " init P(i = 1, j = v) ;            \n"
     181             :   ;
     182             : 
     183             : // this process is considered to be NOT linear
     184           1 : std::string CASE13a =
     185             :   "proc X = tau; \n"
     186             :   "              \n"
     187             :   "init delta;   \n"
     188             :   ;
     189             : 
     190             : // this process is considered to be NOT linear
     191           1 : std::string CASE13b =
     192             :   "proc X = delta; \n"
     193             :   "                \n"
     194             :   "init X;         \n"
     195             :   ;
     196             : 
     197             : // this process is considered to be NOT linear
     198           1 : std::string CASE14 =
     199             :   "act a;        \n"
     200             :   "              \n"
     201             :   "proc X = tau; \n"
     202             :   "              \n"
     203             :   "init a;       \n"
     204             :   ;
     205             : 
     206             : // This process is considered linear, although it cannot be directly represented as an LPS.
     207           1 : const std::string CASE15 =
     208             :   "proc P = tau; \n"
     209             :   "              \n"
     210             :   "init P;       \n"
     211             :   ;
     212             : 
     213          16 : void test_linear(const std::string& text, bool result = true)
     214             : {
     215          32 :   process_specification p = parse_process_specification(text);
     216          16 :   if (is_linear(p) != result)
     217             :   {
     218           0 :     std::cerr << "--- Failed linearity test ---" << std::endl;
     219           0 :     std::cerr << text << std::endl;
     220             :   }
     221          16 :   bool verbose = true;
     222          16 :   BOOST_CHECK(is_linear(p, verbose) == result);
     223          16 : }
     224             : 
     225             : // Test case supplied by Frank Stappers. A segmentation fault is reported on Suse 64 bit.
     226           1 : void test_data_spec()
     227             : {
     228           2 :   process_specification spec = parse_process_specification("sort  X; init tau;");
     229           1 :   data::pp(spec.data());
     230           1 : }
     231             : 
     232           1 : void test_guarded()
     233             : {
     234             :   std::string PROCSPEC =
     235             :     "act a;                  \n"
     236             :     "proc P(n: Nat) = Q(n);  \n"
     237             :     "proc Q(n: Nat) = a.P(n);\n"
     238             :     "proc R(n: Nat) = S(n);  \n"
     239             :     "proc S(n: Nat) = R(n);  \n"
     240           2 :     "init P(2);              \n"
     241             :     ;
     242             : 
     243           2 :   std::string DATA_DECL = "act a;\n";
     244           2 :   std::string PROC_DECL = "proc P(n: Nat); proc Q(n: Nat); proc R(n: Nat); proc S(n: Nat);\n";
     245             :   process_specification procspec =
     246           2 :       parse_process_specification(PROCSPEC);
     247           2 :   process_expression x;
     248             : 
     249           1 :   x = parse_process_expression("delta", DATA_DECL, PROC_DECL);
     250           1 :   BOOST_CHECK(is_guarded(x, procspec.equations()));
     251             : 
     252           1 :   x = parse_process_expression("tau", DATA_DECL, PROC_DECL);
     253           1 :   BOOST_CHECK(is_guarded(x, procspec.equations()));
     254             : 
     255           1 :   x = parse_process_expression("a", DATA_DECL, PROC_DECL);
     256           1 :   BOOST_CHECK(is_guarded(x, procspec.equations()));
     257             : 
     258           1 :   x = parse_process_expression("P(0)", DATA_DECL, PROC_DECL);
     259           1 :   BOOST_CHECK(is_guarded(x, procspec.equations()));
     260             : 
     261           1 :   x = parse_process_expression("a.P(0) + P(1)", DATA_DECL, PROC_DECL);
     262           1 :   BOOST_CHECK(is_guarded(x, procspec.equations()));
     263             : 
     264           1 :   x = parse_process_expression("a.P(0) || P(1)", DATA_DECL, PROC_DECL);
     265           1 :   BOOST_CHECK(is_guarded(x, procspec.equations()));
     266             : 
     267           1 :   x = parse_process_expression("a.P(0) . P(1)", DATA_DECL, PROC_DECL);
     268           1 :   BOOST_CHECK(is_guarded(x, procspec.equations()));
     269             : 
     270           1 :   x = parse_process_expression("R(0)", DATA_DECL, PROC_DECL);
     271           1 :   BOOST_CHECK(!is_guarded(x, procspec.equations()));
     272           1 : }
     273             : 
     274           3 : BOOST_AUTO_TEST_CASE(balance_summands_test)
     275             : {
     276           2 :   std::function<std::size_t(process_expression)> nesting_depth;
     277         403 :   nesting_depth = [&nesting_depth](const process_expression& x) -> std::size_t
     278         400 :   {
     279         402 :     if (is_choice(x))
     280             :     {
     281         200 :       const auto& x_ = atermpp::down_cast<choice>(x);
     282         400 :       return std::max(nesting_depth(x_.left()), nesting_depth(x_.right())) + 1;
     283             :     }
     284         202 :     return 0;
     285           2 :   };
     286             : 
     287           2 :   process_expression x = delta();
     288         101 :   for (int i = 0; i < 100; i++)
     289             :   {
     290         100 :     x = choice(x, delta());
     291             :   }
     292           1 :   auto depth1 = nesting_depth(x);
     293           1 :   x = balance_summands(x);
     294           1 :   auto depth2 = nesting_depth(x);
     295           1 :   BOOST_CHECK_EQUAL(depth1, 100);
     296           1 :   BOOST_CHECK_EQUAL(depth2, 7);
     297           1 : }
     298             : 
     299           3 : BOOST_AUTO_TEST_CASE(test_main)
     300             : {
     301           1 :   test_linear(CASE1);
     302           1 :   test_linear(CASE2);
     303           1 :   test_linear(CASE3);
     304           1 :   test_linear(CASE4);
     305           1 :   test_linear(CASE5, false);
     306           1 :   test_linear(CASE6);
     307           1 :   test_linear(CASE7);
     308           1 :   test_linear(CASE8);
     309           1 :   test_linear(CASE9);
     310           1 :   test_linear(CASE10);
     311           1 :   test_linear(CASE11);
     312           1 :   test_linear(CASE12);
     313           1 :   test_linear(CASE13a, false);
     314           1 :   test_linear(CASE13b);
     315           1 :   test_linear(CASE14, false);
     316           1 :   test_linear(CASE15);
     317             : 
     318           1 :   test_data_spec();
     319             : 
     320           1 :   test_guarded();
     321           4 : }

Generated by: LCOV version 1.13