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