5 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged2 "--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:maestro@) Check a safety property. Reduction is: dpor.
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:maestro@) **************************
886 > [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
887 > [ 0.000000] (0:maestro@) **************************
888 > [ 0.000000] (0:maestro@) Counter-example execution trace:
889 > [ 0.000000] (0:maestro@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
890 > [ 0.000000] (0:maestro@) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
891 > [ 0.000000] (0:maestro@) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
892 > [ 0.000000] (0:maestro@) [(3)HostC (client)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
893 > [ 0.000000] (0:maestro@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
894 > [ 0.000000] (0:maestro@) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
895 > [ 0.000000] (0:maestro@) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
896 > [ 0.000000] (0:maestro@) Expanded states = 461
897 > [ 0.000000] (0:maestro@) Visited states = 2271
898 > [ 0.000000] (0:maestro@) Executed transitions = 2117
