LCOV - code coverage report
Current view: top level - process/test - sort_traverser_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 34 34 100.0 %
Date: 2020-09-22 00:46:14 Functions: 5 5 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 sort_traverser_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE sort_traverser_test
      13             : 
      14             : #include "mcrl2/process/find.h"
      15             : #include "mcrl2/process/parse.h"
      16             : 
      17             : #include <boost/test/included/unit_test_framework.hpp>
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::process;
      21             : 
      22           1 : const std::string SPEC1 =
      23             :   "act a;                  \n"
      24             :   "proc X = a;             \n"
      25             :   "init X;                 \n"
      26             :   ;
      27             : 
      28           1 : const std::string SPEC2 =
      29             :   "act a;                  \n"
      30             :   "proc X(i: Nat) = a.X(i);\n"
      31             :   "init X(2);              \n"
      32             :   ;
      33             : 
      34           1 : const std::string ABS_SPEC_LINEARIZED =
      35             :   "sort D = struct d1 | d2;                                                                                                     \n"
      36             :   "     Error = struct e;                                                                                                       \n"
      37             :   "                                                                                                                             \n"
      38             :   "act  r1,s4: D;                                                                                                               \n"
      39             :   "     s2,r2,c2,s3,r3,c3: D # Bool;                                                                                            \n"
      40             :   "     s3,r3,c3: Error;                                                                                                        \n"
      41             :   "     s5,r5,c5,s6,r6,c6: Bool;                                                                                                \n"
      42             :   "     s6,r6,c6: Error;                                                                                                        \n"
      43             :   "     i;                                                                                                                      \n"
      44             :   "                                                                                                                             \n"
      45             :   "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"
      46             :   "       sum e1_S: Bool.                                                                                                       \n"
      47             :   "         ((s31_S == 3 && s33_L == 3) && if(e1_S, !b_S, b_S) == b_L) ->                                                       \n"
      48             :   "         c6(if(e1_S, !b_S, b_S)) .                                                                                           \n"
      49             :   "         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"
      50             :   "     + (s31_S == 3 && s33_L == 4) ->                                                                                         \n"
      51             :   "         c6(e) .                                                                                                             \n"
      52             :   "         P(2, d_S, b_S, s32_K, d_K, b_K, 1, false, s34_R, d_R, b_R)                                                          \n"
      53             :   "     + (s31_S == 2 && s32_K == 1) ->                                                                                         \n"
      54             :   "         c2(d_S, b_S) .                                                                                                      \n"
      55             :   "         P(3, d_S, b_S, 2, d_S, b_S, s33_L, b_L, s34_R, d_R, b_R)                                                            \n"
      56             :   "     + sum e2_K: Bool.                                                                                                       \n"
      57             :   "         (s32_K == 2) ->                                                                                                     \n"
      58             :   "         i .                                                                                                                 \n"
      59             :   "         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"
      60             :   "     + sum e4_R: Bool.                                                                                                       \n"
      61             :   "         (s33_L == 1 && if(e4_R, s34_R == 4, s34_R == 3)) ->                                                                 \n"
      62             :   "         c5(if(e4_R, !b_R, b_R)) .                                                                                           \n"
      63             :   "         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"
      64             :   "     + (s34_R == 2) ->                                                                                                       \n"
      65             :   "         s4(d_R) .                                                                                                           \n"
      66             :   "         P(s31_S, d_S, b_S, s32_K, d_K, b_K, s33_L, b_L, 3, d2, b_R)                                                         \n"
      67             :   "     + sum e3_L: Bool.                                                                                                       \n"
      68             :   "         (s33_L == 2) ->                                                                                                     \n"
      69             :   "         i .                                                                                                                 \n"
      70             :   "         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"
      71             :   "     + (s32_K == 4 && s34_R == 1) ->                                                                                         \n"
      72             :   "         c3(e) .                                                                                                             \n"
      73             :   "         P(s31_S, d_S, b_S, 1, d2, false, s33_L, b_L, 4, d2, b_R)                                                            \n"
      74             :   "     + sum e5_R: Bool.                                                                                                       \n"
      75             :   "         ((s32_K == 3 && s34_R == 1) && if(e5_R, b_R, !b_R) == b_K) ->                                                       \n"
      76             :   "         c3(d_K, if(e5_R, b_R, !b_R)) .                                                                                      \n"
      77             :   "         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"
      78             :   "     + sum d3_S: D.                                                                                                          \n"
      79             :   "         (s31_S == 1) ->                                                                                                     \n"
      80             :   "         r1(d3_S) .                                                                                                          \n"
      81             :   "         P(2, d3_S, b_S, s32_K, d_K, b_K, s33_L, b_L, s34_R, d_R, b_R)                                                       \n"
      82             :   "     + true ->                                                                                                               \n"
      83             :   "         delta;                                                                                                              \n"
      84             :   "                                                                                                                             \n"
      85             :   "init P(1, d2, true, 1, d2, false, 1, false, 1, d2, true);                                                                    \n"
      86             :   ;
      87             : 
      88             : // CASE?? specifications were borrowed from sumelm_test.
      89             : 
      90           1 : std::string CASE1 =
      91             :   "sort S = struct s1 | s2;\n"
      92             :   "map f : S -> Bool;\n"
      93             :   "act a : S # Bool;\n"
      94             :   "proc P = sum c : S, b : Bool . (b == f(c) && c == s2) -> a(c, b) . P;\n"
      95             :   "init P;\n"
      96             :   ;
      97             : 
      98           1 : std::string CASE2 =
      99             :   "act a,b;\n"
     100             :   "proc P(s3_P: Pos) = sum y_P: Int. (s3_P == 1) -> a . P(2)\n"
     101             :   "                  + (s3_P == 2) -> b . P(1);\n"
     102             :   "init P(1);\n"
     103             :   ;
     104             : 
     105           1 : std::string CASE3 =
     106             :   "act a;\n"
     107             :   "proc P = sum y:Int . (4 == y) -> a . P;\n"
     108             :   "init P;\n"
     109             :   ;
     110             : 
     111           1 : std::string CASE4 =
     112             :   "act a;\n"
     113             :   "proc P = sum y:Int . (y == 4) -> a . P;\n"
     114             :   "init P;\n"
     115             :   ;
     116             : 
     117           1 : std::string CASE5 =
     118             :   "act a,b:Int;\n"
     119             :   "proc P = sum y:Int . (y == 4) -> a(y)@y . b(y*2)@(y+1) . P;\n"
     120             :   "init P;\n"
     121             :   ;
     122             : 
     123           1 : std::string CASE6 =
     124             :   "act a;\n"
     125             :   "proc P = sum y:Int . (y == y + 1) -> a . P;\n"
     126             :   "init P;\n"
     127             :   ;
     128             : 
     129           1 : std::string CASE7 =
     130             :   "sort D = struct d1 | d2 | d3;\n"
     131             :   "map g : D -> D;\n"
     132             :   "act a;\n"
     133             :   "proc P(c:D) = sum d:D . sum e:D . sum f:D . (d == e && e == g(e) && e == f) -> a . P(d);\n"
     134             :   "init P(d1);\n"
     135             :   ;
     136             : 
     137           1 : std::string CASE8 =
     138             :   "sort D = struct d1 | d2 | d3;\n"
     139             :   "act a;\n"
     140             :   "proc P(c:D) = sum d:D . sum e:D . sum f:D . (d == e && d == f) -> a . P(d);\n"
     141             :   "init P(d1);\n"
     142             :   ;
     143             : 
     144           1 : std::string CASE9 =
     145             :   "proc P = sum y:Bool . y -> delta;\n"
     146             :   "init P;\n"
     147             :   ;
     148             : 
     149           1 : std::string CASE10 =
     150             :   "act a:Nat;\n"
     151             :   "proc P(n0: Nat) = sum n: Nat. (n == n0 && n == 1) -> a(n0) . P(n);\n"
     152             :   "init P(0);\n"
     153             :   ;
     154             : 
     155          13 : void test_process(const std::string& text)
     156             : {
     157          26 :   process_specification spec = parse_process_specification(text);
     158          26 :   std::set<data::sort_expression> sorts;
     159          13 :   process::find_sort_expressions(spec, std::inserter(sorts, sorts.end()));
     160          13 :   std::cerr << "sorts: " << data::pp(data::sort_expression_list(sorts.begin(), sorts.end())) << std::endl;
     161          13 : }
     162             : 
     163           3 : BOOST_AUTO_TEST_CASE(test_main)
     164             : {
     165           1 :   test_process(CASE1);
     166           1 :   test_process(CASE2);
     167           1 :   test_process(CASE3);
     168           1 :   test_process(CASE4);
     169           1 :   test_process(CASE5);
     170           1 :   test_process(CASE6);
     171           1 :   test_process(CASE7);
     172           1 :   test_process(CASE8);
     173           1 :   test_process(CASE9);
     174           1 :   test_process(CASE10);
     175           1 :   test_process(SPEC1);
     176           1 :   test_process(SPEC2);
     177           1 :   test_process(ABS_SPEC_LINEARIZED);
     178           4 : }
     179             : 

Generated by: LCOV version 1.13