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 17 : 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 17 : " ); \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
|
