Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
3d65e677e7c82f9503c2aafb715aea629fd7ea7c
[simgrid.git] / examples / msg / mc / bugged2.tesh
1 #! ./tesh
2
3 ! expect signal SIGABRT
4 ! timeout 20
5 $ ${bindir:=.}/bugged2 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
6 > [  0.000000] (0:@) Configuration change: Set 'model-check' to '1'
7 > [  0.000000] (0:@) Check a safety property
8 > [  0.000000] (0:@) Get debug information ...
9 > [  0.000000] (0:@) Get debug information done !
10 > [  0.000000] (2:client@HostB) Send 1!
11 > [  0.000000] (3:client@HostC) Send 2!
12 > [  0.000000] (1:server@HostA) Received 1
13 > [  0.000000] (2:client@HostB) Send 1!
14 > [  0.000000] (1:server@HostA) Received 1
15 > [  0.000000] (1:server@HostA) Received 2
16 > [  0.000000] (3:client@HostC) Send 2!
17 > [  0.000000] (1:server@HostA) Received 2
18 > [  0.000000] (1:server@HostA) OK
19 > [  0.000000] (1:server@HostA) Received 1
20 > [  0.000000] (2:client@HostB) Send 1!
21 > [  0.000000] (1:server@HostA) Received 1
22 > [  0.000000] (1:server@HostA) Received 2
23 > [  0.000000] (3:client@HostC) Send 2!
24 > [  0.000000] (1:server@HostA) Received 1
25 > [  0.000000] (2:client@HostB) Send 1!
26 > [  0.000000] (1:server@HostA) Received 1
27 > [  0.000000] (1:server@HostA) Received 2
28 > [  0.000000] (3:client@HostC) Send 2!
29 > [  0.000000] (1:server@HostA) Received 2
30 > [  0.000000] (1:server@HostA) OK
31 > [  0.000000] (1:server@HostA) Received 1
32 > [  0.000000] (2:client@HostB) Send 1!
33 > [  0.000000] (1:server@HostA) Received 1
34 > [  0.000000] (1:server@HostA) Received 2
35 > [  0.000000] (3:client@HostC) Send 2!
36 > [  0.000000] (1:server@HostA) Received 1
37 > [  0.000000] (2:client@HostB) Send 1!
38 > [  0.000000] (1:server@HostA) Received 1
39 > [  0.000000] (1:server@HostA) Received 1
40 > [  0.000000] (2:client@HostB) Send 1!
41 > [  0.000000] (1:server@HostA) Received 1
42 > [  0.000000] (1:server@HostA) Received 2
43 > [  0.000000] (3:client@HostC) Send 2!
44 > [  0.000000] (1:server@HostA) Received 2
45 > [  0.000000] (1:server@HostA) OK
46 > [  0.000000] (1:server@HostA) Received 1
47 > [  0.000000] (2:client@HostB) Send 1!
48 > [  0.000000] (1:server@HostA) Received 1
49 > [  0.000000] (1:server@HostA) Received 2
50 > [  0.000000] (3:client@HostC) Send 2!
51 > [  0.000000] (1:server@HostA) Received 1
52 > [  0.000000] (2:client@HostB) Send 1!
53 > [  0.000000] (1:server@HostA) Received 1
54 > [  0.000000] (1:server@HostA) Received 2
55 > [  0.000000] (3:client@HostC) Send 2!
56 > [  0.000000] (1:server@HostA) Received 2
57 > [  0.000000] (1:server@HostA) OK
58 > [  0.000000] (1:server@HostA) Received 1
59 > [  0.000000] (2:client@HostB) Send 1!
60 > [  0.000000] (1:server@HostA) Received 1
61 > [  0.000000] (1:server@HostA) Received 2
62 > [  0.000000] (3:client@HostC) Send 2!
63 > [  0.000000] (1:server@HostA) Received 1
64 > [  0.000000] (2:client@HostB) Send 1!
65 > [  0.000000] (1:server@HostA) Received 1
66 > [  0.000000] (1:server@HostA) Received 1
67 > [  0.000000] (2:client@HostB) Send 1!
68 > [  0.000000] (1:server@HostA) Received 2
69 > [  0.000000] (1:server@HostA) Received 1
70 > [  0.000000] (3:client@HostC) Send 2!
71 > [  0.000000] (1:server@HostA) Received 2
72 > [  0.000000] (1:server@HostA) OK
73 > [  0.000000] (1:server@HostA) Received 1
74 > [  0.000000] (2:client@HostB) Send 1!
75 > [  0.000000] (1:server@HostA) Received 2
76 > [  0.000000] (1:server@HostA) Received 1
77 > [  0.000000] (3:client@HostC) Send 2!
78 > [  0.000000] (1:server@HostA) Received 1
79 > [  0.000000] (2:client@HostB) Send 1!
80 > [  0.000000] (1:server@HostA) Received 2
81 > [  0.000000] (1:server@HostA) Received 1
82 > [  0.000000] (3:client@HostC) Send 2!
83 > [  0.000000] (1:server@HostA) Received 2
84 > [  0.000000] (1:server@HostA) OK
85 > [  0.000000] (1:server@HostA) Received 1
86 > [  0.000000] (2:client@HostB) Send 1!
87 > [  0.000000] (1:server@HostA) Received 2
88 > [  0.000000] (1:server@HostA) Received 1
89 > [  0.000000] (3:client@HostC) Send 2!
90 > [  0.000000] (1:server@HostA) Received 1
91 > [  0.000000] (2:client@HostB) Send 1!
92 > [  0.000000] (1:server@HostA) Received 2
93 > [  0.000000] (1:server@HostA) Received 1
94 > [  0.000000] (3:client@HostC) Send 2!
95 > [  0.000000] (1:server@HostA) Received 2
96 > [  0.000000] (1:server@HostA) OK
97 > [  0.000000] (1:server@HostA) Received 1
98 > [  0.000000] (2:client@HostB) Send 1!
99 > [  0.000000] (1:server@HostA) Received 2
100 > [  0.000000] (1:server@HostA) Received 1
101 > [  0.000000] (3:client@HostC) Send 2!
102 > [  0.000000] (1:server@HostA) Received 1
103 > [  0.000000] (2:client@HostB) Send 1!
104 > [  0.000000] (1:server@HostA) Received 2
105 > [  0.000000] (1:server@HostA) Received 1
106 > [  0.000000] (3:client@HostC) Send 2!
107 > [  0.000000] (1:server@HostA) Received 2
108 > [  0.000000] (1:server@HostA) OK
109 > [  0.000000] (1:server@HostA) Received 1
110 > [  0.000000] (2:client@HostB) Send 1!
111 > [  0.000000] (1:server@HostA) Received 2
112 > [  0.000000] (1:server@HostA) Received 1
113 > [  0.000000] (3:client@HostC) Send 2!
114 > [  0.000000] (1:server@HostA) Received 1
115 > [  0.000000] (2:client@HostB) Send 1!
116 > [  0.000000] (1:server@HostA) Received 2
117 > [  0.000000] (1:server@HostA) Received 1
118 > [  0.000000] (3:client@HostC) Send 2!
119 > [  0.000000] (1:server@HostA) Received 2
120 > [  0.000000] (1:server@HostA) OK
121 > [  0.000000] (1:server@HostA) Received 1
122 > [  0.000000] (2:client@HostB) Send 1!
123 > [  0.000000] (1:server@HostA) Received 2
124 > [  0.000000] (1:server@HostA) Received 1
125 > [  0.000000] (3:client@HostC) Send 2!
126 > [  0.000000] (1:server@HostA) Received 1
127 > [  0.000000] (2:client@HostB) Send 1!
128 > [  0.000000] (1:server@HostA) Received 2
129 > [  0.000000] (1:server@HostA) Received 1
130 > [  0.000000] (2:client@HostB) Send 1!
131 > [  0.000000] (1:server@HostA) Received 2
132 > [  0.000000] (3:client@HostC) Send 2!
133 > [  0.000000] (1:server@HostA) Received 1
134 > [  0.000000] (1:server@HostA) Received 2
135 > [  0.000000] (1:server@HostA) OK
136 > [  0.000000] (1:server@HostA) Received 1
137 > [  0.000000] (2:client@HostB) Send 1!
138 > [  0.000000] (1:server@HostA) Received 2
139 > [  0.000000] (3:client@HostC) Send 2!
140 > [  0.000000] (1:server@HostA) Received 1
141 > [  0.000000] (1:server@HostA) Received 1
142 > [  0.000000] (2:client@HostB) Send 1!
143 > [  0.000000] (1:server@HostA) Received 2
144 > [  0.000000] (3:client@HostC) Send 2!
145 > [  0.000000] (1:server@HostA) Received 1
146 > [  0.000000] (1:server@HostA) Received 2
147 > [  0.000000] (1:server@HostA) OK
148 > [  0.000000] (1:server@HostA) Received 1
149 > [  0.000000] (2:client@HostB) Send 1!
150 > [  0.000000] (1:server@HostA) Received 2
151 > [  0.000000] (3:client@HostC) Send 2!
152 > [  0.000000] (1:server@HostA) Received 1
153 > [  0.000000] (1:server@HostA) Received 1
154 > [  0.000000] (2:client@HostB) Send 1!
155 > [  0.000000] (1:server@HostA) Received 2
156 > [  0.000000] (3:client@HostC) Send 2!
157 > [  0.000000] (1:server@HostA) Received 2
158 > [  0.000000] (1:server@HostA) Received 1
159 > [  0.000000] (1:server@HostA) OK
160 > [  0.000000] (1:server@HostA) Received 1
161 > [  0.000000] (2:client@HostB) Send 1!
162 > [  0.000000] (1:server@HostA) Received 2
163 > [  0.000000] (3:client@HostC) Send 2!
164 > [  0.000000] (1:server@HostA) Received 2
165 > [  0.000000] (1:server@HostA) Received 1
166 > [  0.000000] (2:client@HostB) Send 1!
167 > [  0.000000] (1:server@HostA) Received 2
168 > [  0.000000] (3:client@HostC) Send 2!
169 > [  0.000000] (1:server@HostA) Received 2
170 > [  0.000000] (1:server@HostA) Received 1
171 > [  0.000000] (1:server@HostA) OK
172 > [  0.000000] (1:server@HostA) Received 1
173 > [  0.000000] (2:client@HostB) Send 1!
174 > [  0.000000] (1:server@HostA) Received 2
175 > [  0.000000] (3:client@HostC) Send 2!
176 > [  0.000000] (1:server@HostA) Received 2
177 > [  0.000000] (1:server@HostA) Received 1
178 > [  0.000000] (2:client@HostB) Send 1!
179 > [  0.000000] (1:server@HostA) Received 2
180 > [  0.000000] (3:client@HostC) Send 2!
181 > [  0.000000] (1:server@HostA) Received 1
182 > [  0.000000] (2:client@HostB) Send 1!
183 > [  0.000000] (1:server@HostA) Received 1
184 > [  0.000000] (2:client@HostB) Send 1!
185 > [  0.000000] (1:server@HostA) Received 1
186 > [  0.000000] (1:server@HostA) Received 2
187 > [  0.000000] (3:client@HostC) Send 2!
188 > [  0.000000] (1:server@HostA) Received 2
189 > [  0.000000] (1:server@HostA) OK
190 > [  0.000000] (1:server@HostA) Received 1
191 > [  0.000000] (2:client@HostB) Send 1!
192 > [  0.000000] (1:server@HostA) Received 1
193 > [  0.000000] (1:server@HostA) Received 2
194 > [  0.000000] (3:client@HostC) Send 2!
195 > [  0.000000] (1:server@HostA) Received 1
196 > [  0.000000] (2:client@HostB) Send 1!
197 > [  0.000000] (1:server@HostA) Received 1
198 > [  0.000000] (1:server@HostA) Received 2
199 > [  0.000000] (3:client@HostC) Send 2!
200 > [  0.000000] (1:server@HostA) Received 2
201 > [  0.000000] (1:server@HostA) OK
202 > [  0.000000] (1:server@HostA) Received 1
203 > [  0.000000] (2:client@HostB) Send 1!
204 > [  0.000000] (1:server@HostA) Received 1
205 > [  0.000000] (1:server@HostA) Received 2
206 > [  0.000000] (3:client@HostC) Send 2!
207 > [  0.000000] (1:server@HostA) Received 1
208 > [  0.000000] (2:client@HostB) Send 1!
209 > [  0.000000] (1:server@HostA) Received 1
210 > [  0.000000] (1:server@HostA) Received 1
211 > [  0.000000] (2:client@HostB) Send 1!
212 > [  0.000000] (1:server@HostA) Received 1
213 > [  0.000000] (1:server@HostA) Received 2
214 > [  0.000000] (3:client@HostC) Send 2!
215 > [  0.000000] (1:server@HostA) Received 2
216 > [  0.000000] (1:server@HostA) OK
217 > [  0.000000] (1:server@HostA) Received 1
218 > [  0.000000] (2:client@HostB) Send 1!
219 > [  0.000000] (1:server@HostA) Received 1
220 > [  0.000000] (1:server@HostA) Received 2
221 > [  0.000000] (3:client@HostC) Send 2!
222 > [  0.000000] (1:server@HostA) Received 1
223 > [  0.000000] (2:client@HostB) Send 1!
224 > [  0.000000] (1:server@HostA) Received 1
225 > [  0.000000] (1:server@HostA) Received 2
226 > [  0.000000] (3:client@HostC) Send 2!
227 > [  0.000000] (1:server@HostA) Received 2
228 > [  0.000000] (1:server@HostA) OK
229 > [  0.000000] (1:server@HostA) Received 1
230 > [  0.000000] (2:client@HostB) Send 1!
231 > [  0.000000] (1:server@HostA) Received 1
232 > [  0.000000] (1:server@HostA) Received 2
233 > [  0.000000] (3:client@HostC) Send 2!
234 > [  0.000000] (1:server@HostA) Received 1
235 > [  0.000000] (2:client@HostB) Send 1!
236 > [  0.000000] (1:server@HostA) Received 1
237 > [  0.000000] (1:server@HostA) Received 1
238 > [  0.000000] (2:client@HostB) Send 1!
239 > [  0.000000] (1:server@HostA) Received 2
240 > [  0.000000] (1:server@HostA) Received 1
241 > [  0.000000] (3:client@HostC) Send 2!
242 > [  0.000000] (1:server@HostA) Received 2
243 > [  0.000000] (1:server@HostA) OK
244 > [  0.000000] (1:server@HostA) Received 1
245 > [  0.000000] (2:client@HostB) Send 1!
246 > [  0.000000] (1:server@HostA) Received 2
247 > [  0.000000] (1:server@HostA) Received 1
248 > [  0.000000] (3:client@HostC) Send 2!
249 > [  0.000000] (1:server@HostA) Received 1
250 > [  0.000000] (2:client@HostB) Send 1!
251 > [  0.000000] (1:server@HostA) Received 2
252 > [  0.000000] (1:server@HostA) Received 1
253 > [  0.000000] (3:client@HostC) Send 2!
254 > [  0.000000] (1:server@HostA) Received 2
255 > [  0.000000] (1:server@HostA) OK
256 > [  0.000000] (1:server@HostA) Received 1
257 > [  0.000000] (2:client@HostB) Send 1!
258 > [  0.000000] (1:server@HostA) Received 2
259 > [  0.000000] (1:server@HostA) Received 1
260 > [  0.000000] (3:client@HostC) Send 2!
261 > [  0.000000] (1:server@HostA) Received 1
262 > [  0.000000] (2:client@HostB) Send 1!
263 > [  0.000000] (1:server@HostA) Received 2
264 > [  0.000000] (1:server@HostA) Received 1
265 > [  0.000000] (3:client@HostC) Send 2!
266 > [  0.000000] (1:server@HostA) Received 2
267 > [  0.000000] (1:server@HostA) OK
268 > [  0.000000] (1:server@HostA) Received 1
269 > [  0.000000] (2:client@HostB) Send 1!
270 > [  0.000000] (1:server@HostA) Received 2
271 > [  0.000000] (1:server@HostA) Received 1
272 > [  0.000000] (3:client@HostC) Send 2!
273 > [  0.000000] (1:server@HostA) Received 1
274 > [  0.000000] (2:client@HostB) Send 1!
275 > [  0.000000] (1:server@HostA) Received 2
276 > [  0.000000] (1:server@HostA) Received 1
277 > [  0.000000] (3:client@HostC) Send 2!
278 > [  0.000000] (1:server@HostA) Received 2
279 > [  0.000000] (1:server@HostA) OK
280 > [  0.000000] (1:server@HostA) Received 1
281 > [  0.000000] (2:client@HostB) Send 1!
282 > [  0.000000] (1:server@HostA) Received 2
283 > [  0.000000] (1:server@HostA) Received 1
284 > [  0.000000] (3:client@HostC) Send 2!
285 > [  0.000000] (1:server@HostA) Received 1
286 > [  0.000000] (2:client@HostB) Send 1!
287 > [  0.000000] (1:server@HostA) Received 2
288 > [  0.000000] (1:server@HostA) Received 1
289 > [  0.000000] (3:client@HostC) Send 2!
290 > [  0.000000] (1:server@HostA) Received 2
291 > [  0.000000] (1:server@HostA) OK
292 > [  0.000000] (1:server@HostA) Received 1
293 > [  0.000000] (2:client@HostB) Send 1!
294 > [  0.000000] (1:server@HostA) Received 2
295 > [  0.000000] (1:server@HostA) Received 1
296 > [  0.000000] (3:client@HostC) Send 2!
297 > [  0.000000] (1:server@HostA) Received 1
298 > [  0.000000] (2:client@HostB) Send 1!
299 > [  0.000000] (1:server@HostA) Received 2
300 > [  0.000000] (1:server@HostA) Received 1
301 > [  0.000000] (2:client@HostB) Send 1!
302 > [  0.000000] (1:server@HostA) Received 2
303 > [  0.000000] (3:client@HostC) Send 2!
304 > [  0.000000] (1:server@HostA) Received 1
305 > [  0.000000] (1:server@HostA) Received 2
306 > [  0.000000] (1:server@HostA) OK
307 > [  0.000000] (1:server@HostA) Received 1
308 > [  0.000000] (2:client@HostB) Send 1!
309 > [  0.000000] (1:server@HostA) Received 2
310 > [  0.000000] (3:client@HostC) Send 2!
311 > [  0.000000] (1:server@HostA) Received 1
312 > [  0.000000] (1:server@HostA) Received 1
313 > [  0.000000] (2:client@HostB) Send 1!
314 > [  0.000000] (1:server@HostA) Received 2
315 > [  0.000000] (3:client@HostC) Send 2!
316 > [  0.000000] (1:server@HostA) Received 1
317 > [  0.000000] (1:server@HostA) Received 2
318 > [  0.000000] (1:server@HostA) OK
319 > [  0.000000] (1:server@HostA) Received 1
320 > [  0.000000] (2:client@HostB) Send 1!
321 > [  0.000000] (1:server@HostA) Received 2
322 > [  0.000000] (3:client@HostC) Send 2!
323 > [  0.000000] (1:server@HostA) Received 1
324 > [  0.000000] (1:server@HostA) Received 1
325 > [  0.000000] (2:client@HostB) Send 1!
326 > [  0.000000] (1:server@HostA) Received 2
327 > [  0.000000] (3:client@HostC) Send 2!
328 > [  0.000000] (1:server@HostA) Received 2
329 > [  0.000000] (1:server@HostA) Received 1
330 > [  0.000000] (1:server@HostA) OK
331 > [  0.000000] (1:server@HostA) Received 1
332 > [  0.000000] (2:client@HostB) Send 1!
333 > [  0.000000] (1:server@HostA) Received 2
334 > [  0.000000] (3:client@HostC) Send 2!
335 > [  0.000000] (1:server@HostA) Received 2
336 > [  0.000000] (1:server@HostA) Received 1
337 > [  0.000000] (2:client@HostB) Send 1!
338 > [  0.000000] (1:server@HostA) Received 2
339 > [  0.000000] (3:client@HostC) Send 2!
340 > [  0.000000] (1:server@HostA) Received 2
341 > [  0.000000] (1:server@HostA) Received 1
342 > [  0.000000] (1:server@HostA) OK
343 > [  0.000000] (1:server@HostA) Received 1
344 > [  0.000000] (2:client@HostB) Send 1!
345 > [  0.000000] (1:server@HostA) Received 2
346 > [  0.000000] (3:client@HostC) Send 2!
347 > [  0.000000] (1:server@HostA) Received 2
348 > [  0.000000] (1:server@HostA) Received 1
349 > [  0.000000] (2:client@HostB) Send 1!
350 > [  0.000000] (1:server@HostA) Received 2
351 > [  0.000000] (3:client@HostC) Send 2!
352 > [  0.000000] (1:server@HostA) Received 1
353 > [  0.000000] (2:client@HostB) Send 1!
354 > [  0.000000] (1:server@HostA) Received 2
355 > [  0.000000] (1:server@HostA) Received 1
356 > [  0.000000] (2:client@HostB) Send 1!
357 > [  0.000000] (1:server@HostA) Received 1
358 > [  0.000000] (3:client@HostC) Send 2!
359 > [  0.000000] (1:server@HostA) Received 2
360 > [  0.000000] (1:server@HostA) OK
361 > [  0.000000] (1:server@HostA) Received 2
362 > [  0.000000] (1:server@HostA) Received 1
363 > [  0.000000] (2:client@HostB) Send 1!
364 > [  0.000000] (1:server@HostA) Received 1
365 > [  0.000000] (3:client@HostC) Send 2!
366 > [  0.000000] (1:server@HostA) Received 2
367 > [  0.000000] (1:server@HostA) Received 1
368 > [  0.000000] (2:client@HostB) Send 1!
369 > [  0.000000] (1:server@HostA) Received 1
370 > [  0.000000] (3:client@HostC) Send 2!
371 > [  0.000000] (1:server@HostA) Received 2
372 > [  0.000000] (1:server@HostA) OK
373 > [  0.000000] (1:server@HostA) Received 2
374 > [  0.000000] (1:server@HostA) Received 1
375 > [  0.000000] (2:client@HostB) Send 1!
376 > [  0.000000] (1:server@HostA) Received 1
377 > [  0.000000] (3:client@HostC) Send 2!
378 > [  0.000000] (1:server@HostA) Received 2
379 > [  0.000000] (1:server@HostA) Received 1
380 > [  0.000000] (2:client@HostB) Send 1!
381 > [  0.000000] (1:server@HostA) Received 1
382 > [  0.000000] (3:client@HostC) Send 2!
383 > [  0.000000] (1:server@HostA) Received 2
384 > [  0.000000] (1:server@HostA) OK
385 > [  0.000000] (1:server@HostA) Received 2
386 > [  0.000000] (1:server@HostA) Received 1
387 > [  0.000000] (2:client@HostB) Send 1!
388 > [  0.000000] (1:server@HostA) Received 1
389 > [  0.000000] (3:client@HostC) Send 2!
390 > [  0.000000] (1:server@HostA) Received 2
391 > [  0.000000] (1:server@HostA) Received 1
392 > [  0.000000] (2:client@HostB) Send 1!
393 > [  0.000000] (1:server@HostA) Received 1
394 > [  0.000000] (3:client@HostC) Send 2!
395 > [  0.000000] (1:server@HostA) Received 2
396 > [  0.000000] (1:server@HostA) OK
397 > [  0.000000] (1:server@HostA) Received 2
398 > [  0.000000] (1:server@HostA) Received 1
399 > [  0.000000] (2:client@HostB) Send 1!
400 > [  0.000000] (1:server@HostA) Received 1
401 > [  0.000000] (3:client@HostC) Send 2!
402 > [  0.000000] (1:server@HostA) Received 2
403 > [  0.000000] (1:server@HostA) Received 1
404 > [  0.000000] (2:client@HostB) Send 1!
405 > [  0.000000] (1:server@HostA) Received 1
406 > [  0.000000] (3:client@HostC) Send 2!
407 > [  0.000000] (1:server@HostA) Received 2
408 > [  0.000000] (1:server@HostA) OK
409 > [  0.000000] (1:server@HostA) Received 2
410 > [  0.000000] (1:server@HostA) Received 1
411 > [  0.000000] (2:client@HostB) Send 1!
412 > [  0.000000] (1:server@HostA) Received 1
413 > [  0.000000] (3:client@HostC) Send 2!
414 > [  0.000000] (1:server@HostA) Received 2
415 > [  0.000000] (1:server@HostA) Received 1
416 > [  0.000000] (2:client@HostB) Send 1!
417 > [  0.000000] (1:server@HostA) Received 1
418 > [  0.000000] (3:client@HostC) Send 2!
419 > [  0.000000] (1:server@HostA) Received 2
420 > [  0.000000] (1:server@HostA) OK
421 > [  0.000000] (1:server@HostA) Received 2
422 > [  0.000000] (1:server@HostA) Received 1
423 > [  0.000000] (2:client@HostB) Send 1!
424 > [  0.000000] (1:server@HostA) Received 1
425 > [  0.000000] (3:client@HostC) Send 2!
426 > [  0.000000] (1:server@HostA) Received 2
427 > [  0.000000] (1:server@HostA) Received 1
428 > [  0.000000] (2:client@HostB) Send 1!
429 > [  0.000000] (3:client@HostC) Send 2!
430 > [  0.000000] (1:server@HostA) Received 1
431 > [  0.000000] (1:server@HostA) Received 2
432 > [  0.000000] (1:server@HostA) OK
433 > [  0.000000] (1:server@HostA) Received 2
434 > [  0.000000] (1:server@HostA) Received 1
435 > [  0.000000] (2:client@HostB) Send 1!
436 > [  0.000000] (3:client@HostC) Send 2!
437 > [  0.000000] (1:server@HostA) Received 1
438 > [  0.000000] (1:server@HostA) Received 2
439 > [  0.000000] (1:server@HostA) Received 1
440 > [  0.000000] (2:client@HostB) Send 1!
441 > [  0.000000] (3:client@HostC) Send 2!
442 > [  0.000000] (1:server@HostA) Received 1
443 > [  0.000000] (1:server@HostA) Received 2
444 > [  0.000000] (1:server@HostA) OK
445 > [  0.000000] (1:server@HostA) Received 2
446 > [  0.000000] (1:server@HostA) Received 1
447 > [  0.000000] (2:client@HostB) Send 1!
448 > [  0.000000] (3:client@HostC) Send 2!
449 > [  0.000000] (1:server@HostA) Received 1
450 > [  0.000000] (1:server@HostA) Received 2
451 > [  0.000000] (1:server@HostA) Received 1
452 > [  0.000000] (2:client@HostB) Send 1!
453 > [  0.000000] (1:server@HostA) Received 1
454 > [  0.000000] (3:client@HostC) Send 2!
455 > [  0.000000] (1:server@HostA) Received 2
456 > [  0.000000] (1:server@HostA) OK
457 > [  0.000000] (1:server@HostA) Received 2
458 > [  0.000000] (1:server@HostA) Received 1
459 > [  0.000000] (2:client@HostB) Send 1!
460 > [  0.000000] (1:server@HostA) Received 1
461 > [  0.000000] (3:client@HostC) Send 2!
462 > [  0.000000] (1:server@HostA) Received 2
463 > [  0.000000] (1:server@HostA) Received 1
464 > [  0.000000] (2:client@HostB) Send 1!
465 > [  0.000000] (1:server@HostA) Received 1
466 > [  0.000000] (3:client@HostC) Send 2!
467 > [  0.000000] (1:server@HostA) Received 2
468 > [  0.000000] (1:server@HostA) OK
469 > [  0.000000] (1:server@HostA) Received 2
470 > [  0.000000] (1:server@HostA) Received 1
471 > [  0.000000] (2:client@HostB) Send 1!
472 > [  0.000000] (1:server@HostA) Received 1
473 > [  0.000000] (3:client@HostC) Send 2!
474 > [  0.000000] (1:server@HostA) Received 2
475 > [  0.000000] (1:server@HostA) Received 1
476 > [  0.000000] (2:client@HostB) Send 1!
477 > [  0.000000] (3:client@HostC) Send 2!
478 > [  0.000000] (1:server@HostA) Received 1
479 > [  0.000000] (1:server@HostA) Received 2
480 > [  0.000000] (1:server@HostA) OK
481 > [  0.000000] (1:server@HostA) Received 2
482 > [  0.000000] (1:server@HostA) Received 1
483 > [  0.000000] (2:client@HostB) Send 1!
484 > [  0.000000] (3:client@HostC) Send 2!
485 > [  0.000000] (1:server@HostA) Received 1
486 > [  0.000000] (1:server@HostA) Received 2
487 > [  0.000000] (1:server@HostA) Received 1
488 > [  0.000000] (2:client@HostB) Send 1!
489 > [  0.000000] (1:server@HostA) Received 2
490 > [  0.000000] (1:server@HostA) Received 1
491 > [  0.000000] (2:client@HostB) Send 1!
492 > [  0.000000] (1:server@HostA) Received 1
493 > [  0.000000] (3:client@HostC) Send 2!
494 > [  0.000000] (1:server@HostA) Received 2
495 > [  0.000000] (1:server@HostA) OK
496 > [  0.000000] (1:server@HostA) Received 2
497 > [  0.000000] (1:server@HostA) Received 1
498 > [  0.000000] (2:client@HostB) Send 1!
499 > [  0.000000] (1:server@HostA) Received 1
500 > [  0.000000] (3:client@HostC) Send 2!
501 > [  0.000000] (1:server@HostA) Received 2
502 > [  0.000000] (1:server@HostA) Received 1
503 > [  0.000000] (2:client@HostB) Send 1!
504 > [  0.000000] (1:server@HostA) Received 1
505 > [  0.000000] (3:client@HostC) Send 2!
506 > [  0.000000] (1:server@HostA) Received 2
507 > [  0.000000] (1:server@HostA) OK
508 > [  0.000000] (1:server@HostA) Received 2
509 > [  0.000000] (1:server@HostA) Received 1
510 > [  0.000000] (2:client@HostB) Send 1!
511 > [  0.000000] (1:server@HostA) Received 1
512 > [  0.000000] (3:client@HostC) Send 2!
513 > [  0.000000] (1:server@HostA) Received 2
514 > [  0.000000] (1:server@HostA) Received 1
515 > [  0.000000] (2:client@HostB) Send 1!
516 > [  0.000000] (1:server@HostA) Received 1
517 > [  0.000000] (3:client@HostC) Send 2!
518 > [  0.000000] (1:server@HostA) Received 2
519 > [  0.000000] (1:server@HostA) OK
520 > [  0.000000] (1:server@HostA) Received 2
521 > [  0.000000] (1:server@HostA) Received 1
522 > [  0.000000] (2:client@HostB) Send 1!
523 > [  0.000000] (1:server@HostA) Received 1
524 > [  0.000000] (3:client@HostC) Send 2!
525 > [  0.000000] (1:server@HostA) Received 2
526 > [  0.000000] (1:server@HostA) Received 1
527 > [  0.000000] (2:client@HostB) Send 1!
528 > [  0.000000] (1:server@HostA) Received 1
529 > [  0.000000] (3:client@HostC) Send 2!
530 > [  0.000000] (1:server@HostA) Received 2
531 > [  0.000000] (1:server@HostA) OK
532 > [  0.000000] (1:server@HostA) Received 2
533 > [  0.000000] (1:server@HostA) Received 1
534 > [  0.000000] (2:client@HostB) Send 1!
535 > [  0.000000] (1:server@HostA) Received 1
536 > [  0.000000] (3:client@HostC) Send 2!
537 > [  0.000000] (1:server@HostA) Received 2
538 > [  0.000000] (1:server@HostA) Received 1
539 > [  0.000000] (2:client@HostB) Send 1!
540 > [  0.000000] (1:server@HostA) Received 1
541 > [  0.000000] (3:client@HostC) Send 2!
542 > [  0.000000] (1:server@HostA) Received 2
543 > [  0.000000] (1:server@HostA) OK
544 > [  0.000000] (1:server@HostA) Received 2
545 > [  0.000000] (1:server@HostA) Received 1
546 > [  0.000000] (2:client@HostB) Send 1!
547 > [  0.000000] (1:server@HostA) Received 1
548 > [  0.000000] (3:client@HostC) Send 2!
549 > [  0.000000] (1:server@HostA) Received 2
550 > [  0.000000] (1:server@HostA) Received 1
551 > [  0.000000] (2:client@HostB) Send 1!
552 > [  0.000000] (1:server@HostA) Received 1
553 > [  0.000000] (3:client@HostC) Send 2!
554 > [  0.000000] (1:server@HostA) Received 2
555 > [  0.000000] (1:server@HostA) OK
556 > [  0.000000] (1:server@HostA) Received 2
557 > [  0.000000] (1:server@HostA) Received 1
558 > [  0.000000] (2:client@HostB) Send 1!
559 > [  0.000000] (1:server@HostA) Received 1
560 > [  0.000000] (3:client@HostC) Send 2!
561 > [  0.000000] (1:server@HostA) Received 2
562 > [  0.000000] (1:server@HostA) Received 1
563 > [  0.000000] (2:client@HostB) Send 1!
564 > [  0.000000] (3:client@HostC) Send 2!
565 > [  0.000000] (1:server@HostA) Received 1
566 > [  0.000000] (1:server@HostA) Received 2
567 > [  0.000000] (1:server@HostA) OK
568 > [  0.000000] (1:server@HostA) Received 2
569 > [  0.000000] (1:server@HostA) Received 1
570 > [  0.000000] (2:client@HostB) Send 1!
571 > [  0.000000] (3:client@HostC) Send 2!
572 > [  0.000000] (1:server@HostA) Received 1
573 > [  0.000000] (1:server@HostA) Received 2
574 > [  0.000000] (1:server@HostA) Received 1
575 > [  0.000000] (2:client@HostB) Send 1!
576 > [  0.000000] (3:client@HostC) Send 2!
577 > [  0.000000] (1:server@HostA) Received 1
578 > [  0.000000] (1:server@HostA) Received 2
579 > [  0.000000] (1:server@HostA) OK
580 > [  0.000000] (1:server@HostA) Received 2
581 > [  0.000000] (1:server@HostA) Received 1
582 > [  0.000000] (2:client@HostB) Send 1!
583 > [  0.000000] (3:client@HostC) Send 2!
584 > [  0.000000] (1:server@HostA) Received 1
585 > [  0.000000] (1:server@HostA) Received 2
586 > [  0.000000] (1:server@HostA) Received 1
587 > [  0.000000] (2:client@HostB) Send 1!
588 > [  0.000000] (1:server@HostA) Received 1
589 > [  0.000000] (3:client@HostC) Send 2!
590 > [  0.000000] (1:server@HostA) Received 2
591 > [  0.000000] (1:server@HostA) OK
592 > [  0.000000] (1:server@HostA) Received 2
593 > [  0.000000] (1:server@HostA) Received 1
594 > [  0.000000] (2:client@HostB) Send 1!
595 > [  0.000000] (1:server@HostA) Received 1
596 > [  0.000000] (3:client@HostC) Send 2!
597 > [  0.000000] (1:server@HostA) Received 2
598 > [  0.000000] (1:server@HostA) Received 1
599 > [  0.000000] (2:client@HostB) Send 1!
600 > [  0.000000] (1:server@HostA) Received 1
601 > [  0.000000] (3:client@HostC) Send 2!
602 > [  0.000000] (1:server@HostA) Received 2
603 > [  0.000000] (1:server@HostA) OK
604 > [  0.000000] (1:server@HostA) Received 2
605 > [  0.000000] (1:server@HostA) Received 1
606 > [  0.000000] (2:client@HostB) Send 1!
607 > [  0.000000] (1:server@HostA) Received 1
608 > [  0.000000] (3:client@HostC) Send 2!
609 > [  0.000000] (1:server@HostA) Received 2
610 > [  0.000000] (1:server@HostA) Received 1
611 > [  0.000000] (2:client@HostB) Send 1!
612 > [  0.000000] (3:client@HostC) Send 2!
613 > [  0.000000] (1:server@HostA) Received 1
614 > [  0.000000] (1:server@HostA) Received 2
615 > [  0.000000] (1:server@HostA) OK
616 > [  0.000000] (1:server@HostA) Received 2
617 > [  0.000000] (1:server@HostA) Received 1
618 > [  0.000000] (2:client@HostB) Send 1!
619 > [  0.000000] (3:client@HostC) Send 2!
620 > [  0.000000] (1:server@HostA) Received 1
621 > [  0.000000] (1:server@HostA) Received 2
622 > [  0.000000] (1:server@HostA) Received 1
623 > [  0.000000] (2:client@HostB) Send 1!
624 > [  0.000000] (1:server@HostA) Received 2
625 > [  0.000000] (1:server@HostA) Received 1
626 > [  0.000000] (2:client@HostB) Send 1!
627 > [  0.000000] (3:client@HostC) Send 2!
628 > [  0.000000] (1:server@HostA) Received 1
629 > [  0.000000] (1:server@HostA) Received 2
630 > [  0.000000] (1:server@HostA) OK
631 > [  0.000000] (1:server@HostA) Received 2
632 > [  0.000000] (1:server@HostA) Received 1
633 > [  0.000000] (2:client@HostB) Send 1!
634 > [  0.000000] (3:client@HostC) Send 2!
635 > [  0.000000] (1:server@HostA) Received 1
636 > [  0.000000] (1:server@HostA) Received 2
637 > [  0.000000] (1:server@HostA) Received 1
638 > [  0.000000] (2:client@HostB) Send 1!
639 > [  0.000000] (3:client@HostC) Send 2!
640 > [  0.000000] (1:server@HostA) Received 1
641 > [  0.000000] (1:server@HostA) Received 2
642 > [  0.000000] (1:server@HostA) OK
643 > [  0.000000] (1:server@HostA) Received 2
644 > [  0.000000] (1:server@HostA) Received 1
645 > [  0.000000] (2:client@HostB) Send 1!
646 > [  0.000000] (3:client@HostC) Send 2!
647 > [  0.000000] (1:server@HostA) Received 1
648 > [  0.000000] (1:server@HostA) Received 2
649 > [  0.000000] (1:server@HostA) Received 1
650 > [  0.000000] (2:client@HostB) Send 1!
651 > [  0.000000] (3:client@HostC) Send 2!
652 > [  0.000000] (1:server@HostA) Received 2
653 > [  0.000000] (1:server@HostA) Received 1
654 > [  0.000000] (1:server@HostA) OK
655 > [  0.000000] (1:server@HostA) Received 2
656 > [  0.000000] (1:server@HostA) Received 1
657 > [  0.000000] (2:client@HostB) Send 1!
658 > [  0.000000] (3:client@HostC) Send 2!
659 > [  0.000000] (1:server@HostA) Received 2
660 > [  0.000000] (1:server@HostA) Received 2
661 > [  0.000000] (1:server@HostA) Received 1
662 > [  0.000000] (2:client@HostB) Send 1!
663 > [  0.000000] (3:client@HostC) Send 2!
664 > [  0.000000] (1:server@HostA) Received 2
665 > [  0.000000] (1:server@HostA) Received 1
666 > [  0.000000] (1:server@HostA) OK
667 > [  0.000000] (1:server@HostA) Received 2
668 > [  0.000000] (1:server@HostA) Received 1
669 > [  0.000000] (2:client@HostB) Send 1!
670 > [  0.000000] (3:client@HostC) Send 2!
671 > [  0.000000] (1:server@HostA) Received 2
672 > [  0.000000] (1:server@HostA) Received 2
673 > [  0.000000] (1:server@HostA) Received 1
674 > [  0.000000] (2:client@HostB) Send 1!
675 > [  0.000000] (3:client@HostC) Send 2!
676 > [  0.000000] (1:server@HostA) Received 2
677 > [  0.000000] (1:server@HostA) Received 1
678 > [  0.000000] (3:client@HostC) Send 2!
679 > [  0.000000] (2:client@HostB) Send 1!
680 > [  0.000000] (1:server@HostA) Received 1
681 > [  0.000000] (1:server@HostA) Received 2
682 > [  0.000000] (1:server@HostA) OK
683 > [  0.000000] (1:server@HostA) Received 2
684 > [  0.000000] (1:server@HostA) Received 1
685 > [  0.000000] (3:client@HostC) Send 2!
686 > [  0.000000] (2:client@HostB) Send 1!
687 > [  0.000000] (1:server@HostA) Received 1
688 > [  0.000000] (1:server@HostA) Received 2
689 > [  0.000000] (1:server@HostA) Received 1
690 > [  0.000000] (3:client@HostC) Send 2!
691 > [  0.000000] (2:client@HostB) Send 1!
692 > [  0.000000] (1:server@HostA) Received 1
693 > [  0.000000] (1:server@HostA) Received 2
694 > [  0.000000] (1:server@HostA) OK
695 > [  0.000000] (1:server@HostA) Received 2
696 > [  0.000000] (1:server@HostA) Received 1
697 > [  0.000000] (3:client@HostC) Send 2!
698 > [  0.000000] (2:client@HostB) Send 1!
699 > [  0.000000] (1:server@HostA) Received 1
700 > [  0.000000] (1:server@HostA) Received 2
701 > [  0.000000] (1:server@HostA) Received 1
702 > [  0.000000] (3:client@HostC) Send 2!
703 > [  0.000000] (2:client@HostB) Send 1!
704 > [  0.000000] (1:server@HostA) Received 2
705 > [  0.000000] (1:server@HostA) Received 1
706 > [  0.000000] (1:server@HostA) OK
707 > [  0.000000] (1:server@HostA) Received 2
708 > [  0.000000] (1:server@HostA) Received 1
709 > [  0.000000] (3:client@HostC) Send 2!
710 > [  0.000000] (2:client@HostB) Send 1!
711 > [  0.000000] (1:server@HostA) Received 2
712 > [  0.000000] (1:server@HostA) Received 2
713 > [  0.000000] (1:server@HostA) Received 1
714 > [  0.000000] (3:client@HostC) Send 2!
715 > [  0.000000] (2:client@HostB) Send 1!
716 > [  0.000000] (1:server@HostA) Received 2
717 > [  0.000000] (1:server@HostA) Received 1
718 > [  0.000000] (1:server@HostA) OK
719 > [  0.000000] (1:server@HostA) Received 2
720 > [  0.000000] (1:server@HostA) Received 1
721 > [  0.000000] (3:client@HostC) Send 2!
722 > [  0.000000] (2:client@HostB) Send 1!
723 > [  0.000000] (1:server@HostA) Received 2
724 > [  0.000000] (1:server@HostA) Received 2
725 > [  0.000000] (1:server@HostA) Received 1
726 > [  0.000000] (3:client@HostC) Send 2!
727 > [  0.000000] (2:client@HostB) Send 1!
728 > [  0.000000] (1:server@HostA) Received 2
729 > [  0.000000] (1:server@HostA) Received 1
730 > [  0.000000] (3:client@HostC) Send 2!
731 > [  0.000000] (2:client@HostB) Send 1!
732 > [  0.000000] (1:server@HostA) Received 1
733 > [  0.000000] (1:server@HostA) Received 2
734 > [  0.000000] (1:server@HostA) OK
735 > [  0.000000] (1:server@HostA) Received 2
736 > [  0.000000] (1:server@HostA) Received 1
737 > [  0.000000] (3:client@HostC) Send 2!
738 > [  0.000000] (2:client@HostB) Send 1!
739 > [  0.000000] (1:server@HostA) Received 1
740 > [  0.000000] (1:server@HostA) Received 2
741 > [  0.000000] (1:server@HostA) Received 1
742 > [  0.000000] (3:client@HostC) Send 2!
743 > [  0.000000] (2:client@HostB) Send 1!
744 > [  0.000000] (1:server@HostA) Received 1
745 > [  0.000000] (1:server@HostA) Received 2
746 > [  0.000000] (1:server@HostA) OK
747 > [  0.000000] (1:server@HostA) Received 2
748 > [  0.000000] (1:server@HostA) Received 1
749 > [  0.000000] (3:client@HostC) Send 2!
750 > [  0.000000] (2:client@HostB) Send 1!
751 > [  0.000000] (1:server@HostA) Received 1
752 > [  0.000000] (1:server@HostA) Received 2
753 > [  0.000000] (1:server@HostA) Received 1
754 > [  0.000000] (3:client@HostC) Send 2!
755 > [  0.000000] (2:client@HostB) Send 1!
756 > [  0.000000] (1:server@HostA) Received 2
757 > [  0.000000] (1:server@HostA) Received 1
758 > [  0.000000] (1:server@HostA) OK
759 > [  0.000000] (1:server@HostA) Received 2
760 > [  0.000000] (1:server@HostA) Received 1
761 > [  0.000000] (3:client@HostC) Send 2!
762 > [  0.000000] (2:client@HostB) Send 1!
763 > [  0.000000] (1:server@HostA) Received 2
764 > [  0.000000] (1:server@HostA) Received 2
765 > [  0.000000] (1:server@HostA) Received 1
766 > [  0.000000] (3:client@HostC) Send 2!
767 > [  0.000000] (2:client@HostB) Send 1!
768 > [  0.000000] (1:server@HostA) Received 2
769 > [  0.000000] (1:server@HostA) Received 1
770 > [  0.000000] (1:server@HostA) OK
771 > [  0.000000] (1:server@HostA) Received 2
772 > [  0.000000] (1:server@HostA) Received 1
773 > [  0.000000] (3:client@HostC) Send 2!
774 > [  0.000000] (2:client@HostB) Send 1!
775 > [  0.000000] (1:server@HostA) Received 2
776 > [  0.000000] (1:server@HostA) Received 2
777 > [  0.000000] (1:server@HostA) Received 1
778 > [  0.000000] (3:client@HostC) Send 2!
779 > [  0.000000] (2:client@HostB) Send 1!
780 > [  0.000000] (1:server@HostA) Received 2
781 > [  0.000000] (1:server@HostA) Received 2
782 > [  0.000000] (3:client@HostC) Send 2!
783 > [  0.000000] (1:server@HostA) Received 1
784 > [  0.000000] (2:client@HostB) Send 1!
785 > [  0.000000] (1:server@HostA) Received 1
786 > [  0.000000] (1:server@HostA) Received 2
787 > [  0.000000] (1:server@HostA) OK
788 > [  0.000000] (1:server@HostA) Received 2
789 > [  0.000000] (3:client@HostC) Send 2!
790 > [  0.000000] (1:server@HostA) Received 1
791 > [  0.000000] (2:client@HostB) Send 1!
792 > [  0.000000] (1:server@HostA) Received 1
793 > [  0.000000] (1:server@HostA) Received 2
794 > [  0.000000] (3:client@HostC) Send 2!
795 > [  0.000000] (1:server@HostA) Received 1
796 > [  0.000000] (2:client@HostB) Send 1!
797 > [  0.000000] (1:server@HostA) Received 1
798 > [  0.000000] (1:server@HostA) Received 2
799 > [  0.000000] (1:server@HostA) OK
800 > [  0.000000] (1:server@HostA) Received 2
801 > [  0.000000] (3:client@HostC) Send 2!
802 > [  0.000000] (1:server@HostA) Received 1
803 > [  0.000000] (2:client@HostB) Send 1!
804 > [  0.000000] (1:server@HostA) Received 1
805 > [  0.000000] (1:server@HostA) Received 2
806 > [  0.000000] (3:client@HostC) Send 2!
807 > [  0.000000] (1:server@HostA) Received 1
808 > [  0.000000] (2:client@HostB) Send 1!
809 > [  0.000000] (1:server@HostA) Received 2
810 > [  0.000000] (1:server@HostA) Received 1
811 > [  0.000000] (1:server@HostA) OK
812 > [  0.000000] (1:server@HostA) Received 2
813 > [  0.000000] (3:client@HostC) Send 2!
814 > [  0.000000] (1:server@HostA) Received 1
815 > [  0.000000] (2:client@HostB) Send 1!
816 > [  0.000000] (1:server@HostA) Received 2
817 > [  0.000000] (1:server@HostA) Received 2
818 > [  0.000000] (3:client@HostC) Send 2!
819 > [  0.000000] (1:server@HostA) Received 1
820 > [  0.000000] (2:client@HostB) Send 1!
821 > [  0.000000] (1:server@HostA) Received 2
822 > [  0.000000] (1:server@HostA) Received 1
823 > [  0.000000] (1:server@HostA) OK
824 > [  0.000000] (1:server@HostA) Received 2
825 > [  0.000000] (3:client@HostC) Send 2!
826 > [  0.000000] (1:server@HostA) Received 1
827 > [  0.000000] (2:client@HostB) Send 1!
828 > [  0.000000] (1:server@HostA) Received 2
829 > [  0.000000] (1:server@HostA) Received 2
830 > [  0.000000] (3:client@HostC) Send 2!
831 > [  0.000000] (1:server@HostA) Received 1
832 > [  0.000000] (2:client@HostB) Send 1!
833 > [  0.000000] (1:server@HostA) Received 2
834 > [  0.000000] (3:client@HostC) Send 2!
835 > [  0.000000] (1:server@HostA) Received 1
836 > [  0.000000] (2:client@HostB) Send 1!
837 > [  0.000000] (1:server@HostA) Received 1
838 > [  0.000000] (1:server@HostA) Received 2
839 > [  0.000000] (1:server@HostA) OK
840 > [  0.000000] (1:server@HostA) Received 2
841 > [  0.000000] (3:client@HostC) Send 2!
842 > [  0.000000] (1:server@HostA) Received 1
843 > [  0.000000] (2:client@HostB) Send 1!
844 > [  0.000000] (1:server@HostA) Received 1
845 > [  0.000000] (1:server@HostA) Received 2
846 > [  0.000000] (3:client@HostC) Send 2!
847 > [  0.000000] (1:server@HostA) Received 1
848 > [  0.000000] (2:client@HostB) Send 1!
849 > [  0.000000] (1:server@HostA) Received 1
850 > [  0.000000] (1:server@HostA) Received 2
851 > [  0.000000] (1:server@HostA) OK
852 > [  0.000000] (1:server@HostA) Received 2
853 > [  0.000000] (3:client@HostC) Send 2!
854 > [  0.000000] (1:server@HostA) Received 1
855 > [  0.000000] (2:client@HostB) Send 1!
856 > [  0.000000] (1:server@HostA) Received 1
857 > [  0.000000] (1:server@HostA) Received 2
858 > [  0.000000] (3:client@HostC) Send 2!
859 > [  0.000000] (1:server@HostA) Received 1
860 > [  0.000000] (2:client@HostB) Send 1!
861 > [  0.000000] (1:server@HostA) Received 2
862 > [  0.000000] (1:server@HostA) Received 1
863 > [  0.000000] (1:server@HostA) OK
864 > [  0.000000] (1:server@HostA) Received 2
865 > [  0.000000] (3:client@HostC) Send 2!
866 > [  0.000000] (1:server@HostA) Received 1
867 > [  0.000000] (2:client@HostB) Send 1!
868 > [  0.000000] (1:server@HostA) Received 2
869 > [  0.000000] (1:server@HostA) Received 2
870 > [  0.000000] (3:client@HostC) Send 2!
871 > [  0.000000] (1:server@HostA) Received 1
872 > [  0.000000] (2:client@HostB) Send 1!
873 > [  0.000000] (1:server@HostA) Received 2
874 > [  0.000000] (1:server@HostA) Received 1
875 > [  0.000000] (1:server@HostA) OK
876 > [  0.000000] (1:server@HostA) Received 2
877 > [  0.000000] (3:client@HostC) Send 2!
878 > [  0.000000] (1:server@HostA) Received 1
879 > [  0.000000] (2:client@HostB) Send 1!
880 > [  0.000000] (1:server@HostA) Received 2
881 > [  0.000000] (1:server@HostA) Received 2
882 > [  0.000000] (3:client@HostC) Send 2!
883 > [  0.000000] (1:server@HostA) Received 1
884 > [  0.000000] (2:client@HostB) Send 1!
885 > [  0.000000] (1:server@HostA) Received 2
886 > [  0.000000] (3:client@HostC) Send 2!
887 > [  0.000000] (1:server@HostA) Received 2
888 > [  0.000000] (1:server@HostA) **************************
889 > [  0.000000] (1:server@HostA) *** PROPERTY NOT VALID ***
890 > [  0.000000] (1:server@HostA) **************************
891 > [  0.000000] (1:server@HostA) Counter-example execution trace:
892 > [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
893 > [  0.000000] (1:server@HostA) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
894 > [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
895 > [  0.000000] (1:server@HostA) [(3)HostC (client)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
896 > [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
897 > [  0.000000] (1:server@HostA) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
898 > [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
899 > [  0.000000] (1:server@HostA) Expanded states = 461
900 > [  0.000000] (1:server@HostA) Visited states = 2271
901 > [  0.000000] (1:server@HostA) Executed transitions = 2117
902