examples/msg/mc/bugged2.tesh

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