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