mCRL2
Loading...
Searching...
No Matches
test_input.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_LPS_DETAIL_TEST_INPUT_H
13#define MCRL2_LPS_DETAIL_TEST_INPUT_H
14
15#include <string>
16
17namespace mcrl2 {
18
19namespace lps {
20
21namespace detail {
22
23inline
24std::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 " ); \n"
65 ;
66}
67
68inline
69std::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
106inline
107std::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
174inline
175std::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 "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
mcrl2::lps::detail::LINEAR_ABP_SPECIFICATION
std::string LINEAR_ABP_SPECIFICATION()
Definition test_input.h:175
mcrl2::lps::detail::DINING3_SPECIFICATION
std::string DINING3_SPECIFICATION()
Definition test_input.h:69
mcrl2::lps::detail::ONE_BIT_SLIDING_WINDOW_SPECIFICATION
std::string ONE_BIT_SLIDING_WINDOW_SPECIFICATION()
Definition test_input.h:107
mcrl2::lps::detail::ABP_SPECIFICATION
std::string ABP_SPECIFICATION()
Definition test_input.h:24
mcrl2
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72