examples/msg/mc/bugged2.tesh

   1 #! ./tesh
   2
   3 ! expect signal SIGABRT
   4 ! timeout 20
   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))
 891 > [  0.000000] (1:server@HostA) [(3)HostC (client)] iSend (src=(3)HostC (client), buff=(verbose only), size=(verbose only))
 892 > [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait (comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
 893 > [  0.000000] (1:server@HostA) [(3)HostC (client)] Wait (comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
 894 > [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv (dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
 895 > [  0.000000] (1:server@HostA) [(3)HostC (client)] iSend (src=(3)HostC (client), buff=(verbose only), size=(verbose only))
 896 > [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait (comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
 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