LCOV - code coverage report
Current view: top level - lps/test - test_specifications.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 2 2 100.0 %
Date: 2020-07-04 00:44:36 Functions: 0 0 -
Legend: Lines: hit not hit

          Line data    Source code
       1             : #ifndef LPS_TEST_SPECIFICATIONS_H
       2             : #define LPS_TEST_SPECIFICATIONS_H
       3             : 
       4             : #include <string>
       5             : 
       6           2 : const std::string SPEC1 =
       7             :   "act a:Nat;                               \n"
       8             :   "                                         \n"
       9             :   "map smaller: Nat#Nat -> Bool;            \n"
      10             :   "                                         \n"
      11             :   "var x,y : Nat;                           \n"
      12             :   "                                         \n"
      13             :   "eqn smaller(x,y) = x < y;                \n"
      14             :   "                                         \n"
      15             :   "proc P(n:Nat) = sum m: Nat. a(m). P(m);  \n"
      16             :   "                                         \n"
      17             :   "init P(0);                               \n";
      18             : 
      19           2 : const std::string LINEAR_ABP =
      20             :   "sort Error = struct e;\n"
      21             :   "    D = struct d1 | d2;\n"
      22             : 
      23             :   "act  i;\n"
      24             :   "     c6,r6,s6: Error;\n"
      25             :   "     c6,r6,s6,c5,r5,s5: Bool;\n"
      26             :   "     c3,r3,s3: Error;\n"
      27             :   "     c3,r3,s3,c2,r2,s2: D # Bool;\n"
      28             :   "     s4,r1: D;\n"
      29             : 
      30             :   "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"
      31             :   "       sum d0_S: D.\n"
      32             :   "         (s30_S == 1) ->\n"
      33             :   "         r1(d0_S) .\n"
      34             :   "         P(s30_S = 2, d_S = d0_S)\n"
      35             :   "     + sum e0_K: Bool.\n"
      36             :   "         (s31_K == 2) ->\n"
      37             :   "         i .\n"
      38             :   "         P(s31_K = if(e0_K, 4, 3), d_K = if(e0_K, d1, d_K), b_K = if(e0_K, true, b_K))\n"
      39             :   "     + sum e1_L: Bool.\n"
      40             :   "         (s32_L == 2) ->\n"
      41             :   "         i .\n"
      42             :   "         P(s32_L = if(e1_L, 4, 3), b_L = if(e1_L, true, b_L))\n"
      43             :   "     + (s33_R == 2) ->\n"
      44             :   "         s4(d_R) .\n"
      45             :   "         P(s33_R = 3, d_R = d1)\n"
      46             :   "     + sum e2_R: Bool.\n"
      47             :   "         (s32_L == 1 && if(e2_R, s33_R == 4, s33_R == 3)) ->\n"
      48             :   "         c5(if(e2_R, !b_R, b_R)) .\n"
      49             :   "         P(s32_L = 2, b_L = if(e2_R, !b_R, b_R), s33_R = 1, d_R = d1, b_R = if(e2_R, b_R, !b_R))\n"
      50             :   "     + (s31_K == 4 && s33_R == 1) ->\n"
      51             :   "         c3(e) .\n"
      52             :   "         P(s31_K = 1, d_K = d1, b_K = true, s33_R = 4, d_R = d1)\n"
      53             :   "     + sum e3_R: Bool.\n"
      54             :   "         ((s31_K == 3 && s33_R == 1) && if(e3_R, !b_R, b_R) == b_K) ->\n"
      55             :   "         c3(d_K, if(e3_R, !b_R, b_R)) .\n"
      56             :   "         P(s31_K = 1, d_K = d1, b_K = true, s33_R = if(e3_R, 4, 2), d_R = if(e3_R, d1, d_K))\n"
      57             :   "     + (s30_S == 2 && s31_K == 1) ->\n"
      58             :   "         c2(d_S, b_S) .\n"
      59             :   "         P(s30_S = 3, s31_K = 2, d_K = d_S, b_K = b_S)\n"
      60             :   "     + (s30_S == 3 && s32_L == 4) ->\n"
      61             :   "         c6(e) .\n"
      62             :   "         P(s30_S = 2, s32_L = 1, b_L = true)\n"
      63             :   "     + sum e_S: Bool.\n"
      64             :   "         ((s30_S == 3 && s32_L == 3) && if(e_S, b_S, !b_S) == b_L) ->\n"
      65             :   "         c6(if(e_S, b_S, !b_S)) .\n"
      66             :   "         P(s30_S = if(e_S, 1, 2), d_S = if(e_S, d1, d_S), b_S = if(e_S, !b_S, b_S), s32_L = 1, b_L = true)\n"
      67             :   "     + delta;\n"
      68             : 
      69             :   "init P(1, d1, true, 1, d1, true, 1, true, 1, d1, true);\n";
      70             : 
      71             : #endif // LPS_TEST_SPECIFICATIONS_H

Generated by: LCOV version 1.13