LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps/detail - test_input.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 4 4 100.0 %
Date: 2020-09-22 00:46:14 Functions: 2 2 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 mcrl2/lps/detail/test_input.h
      10             : /// \brief This file contains some specifications used for testing.
      11             : 
      12             : #ifndef MCRL2_LPS_DETAIL_TEST_INPUT_H
      13             : #define MCRL2_LPS_DETAIL_TEST_INPUT_H
      14             : 
      15             : #include <string>
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace lps {
      20             : 
      21             : namespace detail {
      22             : 
      23             : inline
      24          16 : std::string ABP_SPECIFICATION()
      25             : {
      26             :   return
      27             : 
      28             :   "% This file contains the alternating bit protocol, as described in W.J.    \n"
      29             :   "% Fokkink, J.F. Groote and M.A. Reniers, Modelling Reactive Systems.       \n"
      30             :   "%                                                                          \n"
      31             :   "% The only exception is that the domain D consists of two data elements to \n"
      32             :   "% facilitate simulation.                                                   \n"
      33             :   "                                                                           \n"
      34             :   "sort                                                                       \n"
      35             :   "  D     = struct d1 | d2;                                                  \n"
      36             :   "  Error = struct e;                                                        \n"
      37             :   "                                                                           \n"
      38             :   "act                                                                        \n"
      39             :   "  r1,s4: D;                                                                \n"
      40             :   "  s2,r2,c2: D # Bool;                                                      \n"
      41             :   "  s3,r3,c3: D # Bool;                                                      \n"
      42             :   "  s3,r3,c3: Error;                                                         \n"
      43             :   "  s5,r5,c5: Bool;                                                          \n"
      44             :   "  s6,r6,c6: Bool;                                                          \n"
      45             :   "  s6,r6,c6: Error;                                                         \n"
      46             :   "  i;                                                                       \n"
      47             :   "                                                                           \n"
      48             :   "proc                                                                       \n"
      49             :   "  S(b:Bool)     = sum d:D. r1(d).T(d,b);                                   \n"
      50             :   "  T(d:D,b:Bool) = s2(d,b).(r6(b).S(!b)+(r6(!b)+r6(e)).T(d,b));             \n"
      51             :   "                                                                           \n"
      52             :   "  R(b:Bool)     = sum d:D. r3(d,b).s4(d).s5(b).R(!b)+                      \n"
      53             :   "                  (sum d:D.r3(d,!b)+r3(e)).s5(!b).R(b);                    \n"
      54             :   "                                                                           \n"
      55             :   "  K             = sum d:D,b:Bool. r2(d,b).(i.s3(d,b)+i.s3(e)).K;           \n"
      56             :   "                                                                           \n"
      57             :   "  L             = sum b:Bool. r5(b).(i.s6(b)+i.s6(e)).L;                   \n"
      58             :   "                                                                           \n"
      59             :   "init                                                                       \n"
      60             :   "  allow({r1,s4,c2,c3,c5,c6,i},                                             \n"
      61             :   "    comm({r2|s2->c2, r3|s3->c3, r5|s5->c5, r6|s6->c6},                     \n"
      62             :   "        S(true) || K || L || R(true)                                       \n"
      63             :   "    )                                                                      \n"
      64          16 :   "  );                                                                       \n"
      65             :   ;
      66             : }
      67             : 
      68             : inline
      69             : std::string DINING3_SPECIFICATION()
      70             : {
      71             :   return
      72             :     "% This is a specification of the dining philosophers problem                               \n"
      73             :     "% for 3 philosophers.                                                                      \n"
      74             :     "                                                                                           \n"
      75             :     "sort Phil = struct p1 | p2 | p3;                                                           \n"
      76             :     "     Fork = struct f1 | f2 | f3;                                                           \n"
      77             :     "                                                                                           \n"
      78             :     "map lf, rf: Phil -> Fork;                                                                  \n"
      79             :     "eqn lf(p1) = f1;                                                                           \n"
      80             :     "    lf(p2) = f2;                                                                           \n"
      81             :     "    lf(p3) = f3;                                                                           \n"
      82             :     "    rf(p1) = f3;                                                                           \n"
      83             :     "    rf(p2) = f1;                                                                           \n"
      84             :     "    rf(p3) = f2;                                                                           \n"
      85             :     "                                                                                           \n"
      86             :     "act get, put, up, down, lock, free: Phil # Fork;                                           \n"
      87             :     "    eat: Phil;                                                                             \n"
      88             :     "                                                                                           \n"
      89             :     "proc P_Phil(p: Phil) =                                                                     \n"
      90             :     "       %The following line implements the expression (get(p,lf(p))||get(p,rf(p)))          \n"
      91             :     "       (get(p,lf(p)).get(p,rf(p)) + get(p,rf(p)).get(p,lf(p)) + get(p,lf(p))|get(p,rf(p))) \n"
      92             :     "       . eat(p) .                                                                          \n"
      93             :     "       %The following line implements the expression (put(p,lf(p))||put(p,rf(p)))          \n"
      94             :     "       (put(p,lf(p)).put(p,rf(p)) + put(p,rf(p)).put(p,lf(p)) + put(p,lf(p))|put(p,rf(p))) \n"
      95             :     "       . P_Phil(p);                                                                        \n"
      96             :     "     P_Fork(f: Fork) = sum p:Phil. up(p,f) . down(p,f) . P_Fork(f);                        \n"
      97             :     "                                                                                           \n"
      98             :     "init block( { get, put, up, down },                                                        \n"
      99             :     "       comm( { get|up->lock, put|down->free },                                             \n"
     100             :     "         P_Fork(f1) || P_Fork(f2) || P_Fork(f3) ||                                         \n"
     101             :     "         P_Phil(p1) || P_Phil(p2) || P_Phil(p3)                                            \n"
     102             :     "     ));                                                                                   \n"
     103             :     ;
     104             : }
     105             : 
     106             : inline
     107             : std::string ONE_BIT_SLIDING_WINDOW_SPECIFICATION()
     108             : {
     109             :   return
     110             :     "% This file describes the onebit sliding window protocol as documented     \n"
     111             :     "% M.A. Bezem and J.F. Groote. A correctness proof of a one bit sliding     \n"
     112             :     "% window protocol in muCRL. The Computer Journal, 37(4): 289-307, 1994.    \n"
     113             :     "% This sliding window protocol is a bidirectional sliding window protocol  \n"
     114             :     "% with piggy backing, where the window sizes at the receiving and          \n"
     115             :     "% sending side have size 1. The behaviour of this sliding window protocol  \n"
     116             :     "% is that of two bidirectional buffers sending data from channel ra to     \n"
     117             :     "% sb, and from rc to sd. Both buffers have capacity 2.                     \n"
     118             :     "%   The external behaviour of the onebit protocol is rather complex.       \n"
     119             :     "% However, making only the behaviour visible at gates ra and sb reduced    \n"
     120             :     "% modulo branching bisimulation clearly shows the behaviour of             \n"
     121             :     "% a buffer of capacity 2.                                                  \n"
     122             :     "%                                                                          \n"
     123             :     "% Jan Friso Groote, translated from muCRL 30/12/2006                       \n"
     124             :     "                                                                           \n"
     125             :     "sort Bit = struct e0 | e1;                                                 \n"
     126             :     "     D= struct d1;                                                         \n"
     127             :     "     Frame=struct frame(dat:D,bit1:Bit,bit2:Bit);                          \n"
     128             :     "     Status=struct read?eq_read | choice?eq_choice | del?eq_del;           \n"
     129             :     "                                                                           \n"
     130             :     "map inv:Bit-> Bit;                                                         \n"
     131             :     "eqn  inv(e0)=e1;                                                           \n"
     132             :     "     inv(e1)=e0;                                                           \n"
     133             :     "                                                                           \n"
     134             :     "act  r,w,rc,sd:D;                                                          \n"
     135             :     "     rcl,scl,i_del,i_lost,ccl;                                             \n"
     136             :     "     r1,s1,c1,s2,r2,c2,s4,r4,c4:Frame;                                     \n"
     137             :     "                                                                           \n"
     138             :     "proc S(ready:Bool,rec:Bool,sts:Bool,d:D,e:D,p:Bit,q:Bit)=                  \n"
     139             :     "       ready -> sum d:D.r(d).S(false,rec,false,d,e,inv(p),q) +             \n"
     140             :     "       !rec -> w(e).S(ready,true,sts,d,e,p,q) +                            \n"
     141             :     "       rcl.S(ready,rec,false,d,e,p,q)+                                     \n"
     142             :     "       sum f:D,b1:Bit,b2:Bit.                                              \n"
     143             :     "           r4(frame(f,b1,b2)).                                             \n"
     144             :     "              (rec && b1==inv(q)) -> S(b2==p,false,sts,d,f,p,inv(q))       \n"
     145             :     "                                  <> S(b2==p,rec,sts,d,e,p,q) +            \n"
     146             :     "       !sts -> s1(frame(d,p,q)).S(ready,rec,true,d,e,p,q) +                \n"
     147             :     "       delta;                                                              \n"
     148             :     "                                                                           \n"
     149             :     "proc Tim= scl.Tim;                                                         \n"
     150             :     "                                                                           \n"
     151             :     "proc C(f:Frame,st:Status)=                                                 \n"
     152             :     "       eq_read(st) -> sum f:Frame.r1(f).C(f,choice)<>delta+                \n"
     153             :     "       eq_choice(st) -> (i_del.C(f,del)+i_lost.C(f,read))<>delta+          \n"
     154             :     "       eq_del(st) -> s2(f).C(f,read)<>delta ;                              \n"
     155             :     "                                                                           \n"
     156             :     "init hide ({c4,c2,ccl,c1,i_del,i_lost},                                    \n"
     157             :     "       allow({c1,ccl,c2,c4,i_del,i_lost,r,w,rc,sd},                        \n"
     158             :     "         comm({r2|s2->c2,r4|s4->c4},                                       \n"
     159             :     "           rename({w->sd},                                                 \n"
     160             :     "             allow({c1,ccl,r,w,s2,r4,i_del,i_lost},                        \n"
     161             :     "               comm({rcl|scl->ccl,r1|s1->c1},                              \n"
     162             :     "                 S(true,true,true,d1,d1,e0,e0)||                           \n"
     163             :     "                 Tim||                                                     \n"
     164             :     "                 C(frame(d1,e0,e0),read))))||                              \n"
     165             :     "           rename({r->rc,s2->s4,r4->r2},                                   \n"
     166             :     "             allow({c1,ccl,r,w,s2,r4,i_del,i_lost},                        \n"
     167             :     "               comm({rcl|scl->ccl,r1|s1->c1},                              \n"
     168             :     "                 S(true,true,true,d1,d1,e0,e0)||                           \n"
     169             :     "                 Tim||                                                     \n"
     170             :     "                 C(frame(d1,e0,e0) ,read)))))));                           \n"
     171             :     ;
     172             : }
     173             : 
     174             : inline
     175           8 : std::string LINEAR_ABP_SPECIFICATION()
     176             : {
     177             :   return
     178             : 
     179             :       "sort D = struct d1 | d2;\n"
     180             :       "     Error = struct e;\n"
     181             :       "act  r1,s4: D;\n"
     182             :       "     s2,r2,c2,s3,r3,c3: D # Bool;\n"
     183             :       "     s3,r3,c3: Error;\n"
     184             :       "     s5,r5,c5,s6,r6,c6: Bool;\n"
     185             :       "     s6,r6,c6: Error;\n"
     186             :       "     i;\n"
     187             :       "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"
     188             :       "       sum d0_S: D.\n"
     189             :       "         (s30_S == 1) ->\n"
     190             :       "         r1(d0_S) .\n"
     191             :       "         P(s30_S = 2, d_S = d0_S)\n"
     192             :       "     + ((s31_K == 3 && s33_R == 1) && !b_R == b_K) ->\n"
     193             :       "         c3(d_K, !b_R) .\n"
     194             :       "         P(s31_K = 1, d_K = d1, b_K = true, s33_R = 4, d_R = d1)\n"
     195             :       "     + ((s31_K == 3 && s33_R == 1) && b_R == b_K) ->\n"
     196             :       "         c3(d_K, b_R) .\n"
     197             :       "         P(s31_K = 1, d_K = d1, b_K = true, s33_R = 2, d_R = d_K)\n"
     198             :       "     + (s31_K == 4 && s33_R == 1) ->\n"
     199             :       "         c3(e) .\n"
     200             :       "         P(s31_K = 1, d_K = d1, b_K = true, s33_R = 4, d_R = d1)\n"
     201             :       "     + (s32_L == 2) ->\n"
     202             :       "         i .\n"
     203             :       "         P(s32_L = 4, b_L = true)\n"
     204             :       "     + (s32_L == 2) ->\n"
     205             :       "         i .\n"
     206             :       "         P(s32_L = 3)\n"
     207             :       "     + (s33_R == 2) ->\n"
     208             :       "         s4(d_R) .\n"
     209             :       "         P(s33_R = 3, d_R = d1)\n"
     210             :       "     + (s32_L == 1 && s33_R == 4) ->\n"
     211             :       "         c5(!b_R) .\n"
     212             :       "         P(s32_L = 2, b_L = !b_R, s33_R = 1, d_R = d1)\n"
     213             :       "     + (s32_L == 1 && s33_R == 3) ->\n"
     214             :       "         c5(b_R) .\n"
     215             :       "         P(s32_L = 2, b_L = b_R, s33_R = 1, d_R = d1, b_R = !b_R)\n"
     216             :       "     + (s31_K == 2) ->\n"
     217             :       "         i .\n"
     218             :       "         P(s31_K = 3)\n"
     219             :       "     + (s31_K == 2) ->\n"
     220             :       "         i .\n"
     221             :       "         P(s31_K = 4, d_K = d1, b_K = true)\n"
     222             :       "     + (s30_S == 3 && s32_L == 4) ->\n"
     223             :       "         c6(e) .\n"
     224             :       "         P(s30_S = 2, s32_L = 1, b_L = true)\n"
     225             :       "     + ((s30_S == 3 && s32_L == 3) && !b_S == b_L) ->\n"
     226             :       "         c6(!b_S) .\n"
     227             :       "         P(s30_S = 2, s32_L = 1, b_L = true)\n"
     228             :       "     + ((s30_S == 3 && s32_L == 3) && b_S == b_L) ->\n"
     229             :       "         c6(b_S) .\n"
     230             :       "         P(s30_S = 1, d_S = d1, b_S = !b_S, s32_L = 1, b_L = true)\n"
     231             :       "     + (s30_S == 2 && s31_K == 1) ->\n"
     232             :       "         c2(d_S, b_S) .\n"
     233             :       "         P(s30_S = 3, s31_K = 2, d_K = d_S, b_K = b_S)\n"
     234             :       "     + delta;\n"
     235           8 :       "init P(1, d1, true, 1, d1, true, 1, true, 1, d1, true);\n"
     236             :   ;
     237             : }
     238             : 
     239             : } // namespace detail
     240             : 
     241             : } // namespace lps
     242             : 
     243             : } // namespace mcrl2
     244             : 
     245             : #endif // MCRL2_LPS_DETAIL_TEST_INPUT_H

Generated by: LCOV version 1.13