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