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

Generated by: LCOV version 1.13