LCOV - code coverage report
Current view: top level - lps/test - linear_process_conversion_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 27 31 87.1 %
Date: 2020-07-04 00:44:36 Functions: 5 5 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Wieger Wesselink, Jeroen van der Wulp
       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 linear_process_conversion_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE linear_process_conversion_test
      13             : #include "mcrl2/lps/parse.h"
      14             : 
      15             : #include <boost/test/included/unit_test_framework.hpp>
      16             : 
      17             : using namespace mcrl2;
      18             : using namespace mcrl2::process;
      19             : using namespace mcrl2::lps;
      20             : 
      21             : // Although this process is linear, the linear_process_conversion_traverser algorithm
      22             : // is expected to generate an exception. The reason for this is that this process
      23             : // cannot be directly represented as an LPS.
      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 SPEC3 =
      37             :   "act a : Bool;                      \n"
      38             :   "proc X = sum b,c:Bool . (b && c) -> a(b).X; \n"
      39             :   "init X;                            \n"
      40             :   ;
      41             : 
      42             : // Although this process is linear, the linear_process_conversion_traverser algorithm
      43             : // is expected to generate an exception. The reason for this is that this process
      44             : // cannot be directly represented as an LPS.
      45           1 : const std::string SPEC4 =
      46             :   "proc P = tau; \n"
      47             :   "              \n"
      48             :   "init P;       \n"
      49             :   ;
      50             : 
      51           1 : const std::string ABS_SPEC_LINEARIZED =
      52             : //  "sort D = struct d1 | d2;                                                                                                     \n"
      53             : //  "     Error = struct e;                                                                                                       \n"
      54             : //  "                                                                                                                             \n"
      55             : //  "act  r1,s4: D;                                                                                                               \n"
      56             : //  "     s2,r2,c2,s3,r3,c3: D # Bool;                                                                                            \n"
      57             : //  "     s3,r3,c3: Error;                                                                                                        \n"
      58             : //  "     s5,r5,c5,s6,r6,c6: Bool;                                                                                                \n"
      59             : //  "     s6,r6,c6: Error;                                                                                                        \n"
      60             : //  "     i;                                                                                                                      \n"
      61             : //  "                                                                                                                             \n"
      62             : //  "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"
      63             : //  "       sum e1_S: Bool.                                                                                                       \n"
      64             : //  "         ((s31_S == 3 && s33_L == 3) && if(e1_S, !b_S, b_S) == b_L) ->                                                       \n"
      65             : //  "         c6(if(e1_S, !b_S, b_S)) .                                                                                           \n"
      66             : //  "         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"
      67             : //  "     + (s31_S == 3 && s33_L == 4) ->                                                                                         \n"
      68             : //  "         c6(e) .                                                                                                             \n"
      69             : //  "         P(2, d_S, b_S, s32_K, d_K, b_K, 1, false, s34_R, d_R, b_R)                                                          \n"
      70             : //  "     + (s31_S == 2 && s32_K == 1) ->                                                                                         \n"
      71             : //  "         c2(d_S, b_S) .                                                                                                      \n"
      72             : //  "         P(3, d_S, b_S, 2, d_S, b_S, s33_L, b_L, s34_R, d_R, b_R)                                                            \n"
      73             : //  "     + sum e2_K: Bool.                                                                                                       \n"
      74             : //  "         (s32_K == 2) ->                                                                                                     \n"
      75             : //  "         i .                                                                                                                 \n"
      76             : //  "         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"
      77             : //  "     + sum e4_R: Bool.                                                                                                       \n"
      78             : //  "         (s33_L == 1 && if(e4_R, s34_R == 4, s34_R == 3)) ->                                                                 \n"
      79             : //  "         c5(if(e4_R, !b_R, b_R)) .                                                                                           \n"
      80             : //  "         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"
      81             : //  "     + (s34_R == 2) ->                                                                                                       \n"
      82             : //  "         s4(d_R) .                                                                                                           \n"
      83             : //  "         P(s31_S, d_S, b_S, s32_K, d_K, b_K, s33_L, b_L, 3, d2, b_R)                                                         \n"
      84             : //  "     + sum e3_L: Bool.                                                                                                       \n"
      85             : //  "         (s33_L == 2) ->                                                                                                     \n"
      86             : //  "         i .                                                                                                                 \n"
      87             : //  "         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"
      88             : //  "     + (s32_K == 4 && s34_R == 1) ->                                                                                         \n"
      89             : //  "         c3(e) .                                                                                                             \n"
      90             : //  "         P(s31_S, d_S, b_S, 1, d2, false, s33_L, b_L, 4, d2, b_R)                                                            \n"
      91             : //  "     + sum e5_R: Bool.                                                                                                       \n"
      92             : //  "         ((s32_K == 3 && s34_R == 1) && if(e5_R, b_R, !b_R) == b_K) ->                                                       \n"
      93             : //  "         c3(d_K, if(e5_R, b_R, !b_R)) .                                                                                      \n"
      94             : //  "         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"
      95             : //  "     + sum d3_S: D.                                                                                                          \n"
      96             : //  "         (s31_S == 1) ->                                                                                                     \n"
      97             : //  "         r1(d3_S) .                                                                                                          \n"
      98             : //  "         P(2, d3_S, b_S, s32_K, d_K, b_K, s33_L, b_L, s34_R, d_R, b_R)                                                       \n"
      99             : //  "     + true ->                                                                                                               \n"
     100             : //  "         delta;                                                                                                              \n"
     101             : //  "                                                                                                                             \n"
     102             : //  "init P(1, d2, true, 1, d2, false, 1, false, 1, d2, true);                                                                    \n"
     103             : //  ;
     104             :   "sort D = struct d1 | d2;                                                                                                     \n"
     105             :   "     Error = struct e;                                                                                                       \n"
     106             :   "                                                                                                                             \n"
     107             :   "act  r1,s4: D;                                                                                                               \n"
     108             :   "     s2,r2,c2,s3,r3,c3: D # Bool;                                                                                            \n"
     109             :   "     s3,r3,c3: Error;                                                                                                        \n"
     110             :   "     s5,r5,c5,s6,r6,c6: Bool;                                                                                                \n"
     111             :   "     s6,r6,c6: Error;                                                                                                        \n"
     112             :   "     i;                                                                                                                      \n"
     113             :   "                                                                                                                             \n"
     114             :   "glob dc,dc0,dc1,dc3,dc5,dc7,dc13,dc14,dc15,dc16,dc17,dc18: D;                                                                \n"
     115             :   "     dc2,dc4,dc6,dc8,dc9,dc10,dc11,dc12: Bool;                                                                               \n"
     116             :   "                                                                                                                             \n"
     117             :   "proc P(s30_S: Pos, d_S: D, b_S: Bool, s31_K: Pos, d_K: D, b_K: Bool, s32_L: Pos, b_L: Bool, s33_R: Pos, d_R: D, b_R: Bool) = \n"
     118             :   "       sum e_S: Bool.                                                                                                        \n"
     119             :   "         ((s30_S == 3 && s32_L == 3) && if(e_S, b_S, !b_S) == b_L) ->                                                        \n"
     120             :   "         c6(if(e_S, b_S, !b_S)) .                                                                                            \n"
     121             :   "         P(s30_S = if(e_S, 1, 2), d_S = if(e_S, dc0, d_S), b_S = if(e_S, !b_S, b_S), s32_L = 1, b_L = dc11)                  \n"
     122             :   "     + (s30_S == 3 && s32_L == 4) ->                                                                                         \n"
     123             :   "         c6(e) .                                                                                                             \n"
     124             :   "         P(s30_S = 2, s32_L = 1, b_L = dc12)                                                                                 \n"
     125             :   "     + (s30_S == 2 && s31_K == 1) ->                                                                                         \n"
     126             :   "         c2(d_S, b_S) .                                                                                                      \n"
     127             :   "         P(s30_S = 3, s31_K = 2, d_K = d_S, b_K = b_S)                                                                       \n"
     128             :   "     + sum e3_R: Bool.                                                                                                       \n"
     129             :   "         ((s31_K == 3 && s33_R == 1) && if(e3_R, !b_R, b_R) == b_K) ->                                                       \n"
     130             :   "         c3(d_K, if(e3_R, !b_R, b_R)) .                                                                                      \n"
     131             :   "         P(s31_K = 1, d_K = dc5, b_K = dc6, s33_R = if(e3_R, 4, 2), d_R = if(e3_R, dc14, d_K))                               \n"
     132             :   "     + (s31_K == 4 && s33_R == 1) ->                                                                                         \n"
     133             :   "         c3(e) .                                                                                                             \n"
     134             :   "         P(s31_K = 1, d_K = dc7, b_K = dc8, s33_R = 4, d_R = dc15)                                                           \n"
     135             :   "     + sum e2_R: Bool.                                                                                                       \n"
     136             :   "         (s32_L == 1 && if(e2_R, s33_R == 4, s33_R == 3)) ->                                                                 \n"
     137             :   "         c5(if(e2_R, !b_R, b_R)) .                                                                                           \n"
     138             :   "         P(s32_L = 2, b_L = if(e2_R, !b_R, b_R), s33_R = 1, d_R = if(e2_R, dc18, dc17), b_R = if(e2_R, b_R, !b_R))           \n"
     139             :   "     + (s33_R == 2) ->                                                                                                       \n"
     140             :   "         s4(d_R) .                                                                                                           \n"
     141             :   "         P(s33_R = 3, d_R = dc16)                                                                                            \n"
     142             :   "     + sum e1_L: Bool.                                                                                                       \n"
     143             :   "         (s32_L == 2) ->                                                                                                     \n"
     144             :   "         i .                                                                                                                 \n"
     145             :   "         P(s32_L = if(e1_L, 4, 3), b_L = if(e1_L, dc10, b_L))                                                                \n"
     146             :   "     + sum e0_K: Bool.                                                                                                       \n"
     147             :   "         (s31_K == 2) ->                                                                                                     \n"
     148             :   "         i .                                                                                                                 \n"
     149             :   "         P(s31_K = if(e0_K, 4, 3), d_K = if(e0_K, dc3, d_K), b_K = if(e0_K, dc4, b_K))                                       \n"
     150             :   "     + sum d0_S: D.                                                                                                          \n"
     151             :   "         (s30_S == 1) ->                                                                                                     \n"
     152             :   "         r1(d0_S) .                                                                                                          \n"
     153             :   "         P(s30_S = 2, d_S = d0_S)                                                                                            \n"
     154             :   "     + delta;                                                                                                                \n"
     155             :   "                                                                                                                             \n"
     156             :   "init P(1, dc, true, 1, dc1, dc2, 1, dc9, 1, dc13, true);                                                                     \n"
     157             :   ;
     158             : 
     159             : // The flag expect_exception should be set for linear processes that cannot be represented by an LPS.
     160           5 : void test_process(const std::string& text, bool expect_exception = false)
     161             : {
     162           8 :   process_specification pspec = parse_process_specification(text);
     163           5 :   bool linear = is_linear(pspec, true);
     164           5 :   if (linear)
     165             :   {
     166             :     try
     167             :     {
     168          10 :       process::detail::linear_process_conversion_traverser visitor;
     169           5 :       specification spec = visitor.convert(pspec);
     170             :     }
     171           4 :     catch (mcrl2::runtime_error&)
     172             :     {
     173           2 :       BOOST_CHECK(expect_exception);
     174           2 :       return;
     175             :     }
     176           3 :     BOOST_CHECK(!expect_exception);
     177             :   }
     178             :   else
     179             :   {
     180             :     try
     181             :     {
     182           0 :       process::detail::linear_process_conversion_traverser visitor;
     183           0 :       specification spec = visitor.convert(pspec);
     184           0 :       BOOST_CHECK(false); // not supposed to arrive here
     185             :     }
     186           0 :     catch (...)
     187             :     {
     188             :       // skip
     189             :     }
     190             :   }
     191             : }
     192             : 
     193           3 : BOOST_AUTO_TEST_CASE(test_main)
     194             : {
     195           1 :   std::clog << "SPEC1" << std::endl;
     196           1 :   test_process(SPEC1, true);
     197           1 :   std::clog << "SPEC2" << std::endl;
     198           1 :   test_process(SPEC2);
     199           1 :   std::clog << "SPEC3" << std::endl;
     200           1 :   test_process(SPEC3);
     201           1 :   std::clog << "SPEC4" << std::endl;
     202           1 :   test_process(SPEC4, true);
     203           1 :   std::clog << "ABS_SPEC_LINEARIZED" << std::endl;
     204           1 :   test_process(ABS_SPEC_LINEARIZED);
     205           4 : }
     206             : 

Generated by: LCOV version 1.13