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