-
Notifications
You must be signed in to change notification settings - Fork 3
/
testreport.txt
522 lines (503 loc) · 62.1 KB
/
testreport.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
CPN Tools state space report for:
/cygdrive/D/Documents/Master/Thesis/WebSocket SS.cpn
Report generated: Tue Feb 7 15:07:48 2012
Statistics
------------------------------------------------------------------------
State Space
Nodes: 47633
Arcs: 183017
Secs: 1800
Status: Partial
Scc Graph
Nodes: 47633
Arcs: 183017
Secs: 16
Boundedness Properties
------------------------------------------------------------------------
Best Integer Bounds
Upper Lower
ClientApplication'Active_Connection 1
1 0
ClientApplication'Conn_Result 1
1 0
ClientApplication'Connection_failed 1
0 0
ClientApplication'Messages_received 1
1 1
ClientApplication'Messages_to_be_sent 1
1 1
ClientApplication'Target_URL 1
1 0
ClientApplication'Target_server 1
1 0
ClientWebSocket'Client_Connection_Request 1
1 0
ClientWebSocket'Client_Connection_Response 1
1 0
ClientWebSocket'Client_Incoming_Message 1
1 1
ClientWebSocket'Client_Outgoing_Message 1
1 1
ClientWebSocket'Connection_status 1
1 0
ClientWebSocket'To_send 1
1 1
ClientWebSocket'Waiting_for_HTTP_response 1
1 0
Defrag'Buffer 1 1 0
Defrag'Buffer 2 0 0
FragmentAndQueue'Control 1
1 1
FragmentAndQueue'Control 2
1 1
FragmentAndQueue'Data 1 1 1
FragmentAndQueue'Data 2 1 1
NewConnection'HTTP_Request 1
1 0
Overview'Client_Call 1 1 1
Overview'Client_Event 1 1 1
Overview'Client_Receive 1
1 1
Overview'Client_Send 1 1 1
Overview'Server_Call 1 1 1
Overview'Server_Event 1 1 1
Overview'Server_Receieve 1
1 1
Overview'Server_Send 1 1 1
ServerApplication'Active_Connection 1
1 0
ServerApplication'Received 1
1 1
ServerApplication'To_send 1
1 1
ServerWebSocket'Connection_Reply 1
1 0
ServerWebSocket'Connection_Request 1
1 0
ServerWebSocket'Connection_Status 1
1 0
ServerWebSocket'Pending_Connection 1
1 0
ServerWebSocket'Server_Incoming_Message 1
1 1
ServerWebSocket'Server_Outgoing_Message 1
1 1
ServerWebSocket'Valid_WS_Frame 1
1 1
UnwrapAndReceive'Closing_Connection 1
1 0
UnwrapAndReceive'Closing_Connection 2
0 0
UnwrapAndReceive'Received_WS_Frame 1
1 1
UnwrapAndReceive'Received_WS_Frame 2
1 1
WrapAndSend'Next 1 1 1
WrapAndSend'Next 2 1 1
Best Upper Multi-set Bounds
ClientApplication'Active_Connection 1
1`()
ClientApplication'Conn_Result 1
1`success
ClientApplication'Connection_failed 1
empty
ClientApplication'Messages_received 1
1`[]++
1`[{Op=PONG,Message="Heartbeat 1"}]++
1`[{Op=PONG,Message="Hello"}]
ClientApplication'Messages_to_be_sent 1
1`[]++
1`[{Op=TEXT,Message="Long message CLIENT ONE"},{Op=PING,Message="Hello"},{Op=CLOSE,Message="Goodbye"}]++
1`[{Op=PING,Message="Hello"},{Op=CLOSE,Message="Goodbye"}]++
1`[{Op=CLOSE,Message="Goodbye"}]
ClientApplication'Target_URL 1
1`{Protocol="ws",Host="websocket.com",Port=80,Path="/chat"}
ClientApplication'Target_server 1
1`"websocket.com/chat"
ClientWebSocket'Client_Connection_Request 1
1`{Protocol="ws",Host="websocket.com",Port=80,Path="/chat"}
ClientWebSocket'Client_Connection_Response 1
1`true
ClientWebSocket'Client_Incoming_Message 1
1`[]++
1`[{Op=PONG,Message="Heartbeat 1"}]++
1`[{Op=PONG,Message="Heartbeat 1"},{Op=PONG,Message="Hello"}]++
1`[{Op=PONG,Message="Hello"}]++
1`[{Op=PONG,Message="Hello"},{Op=PONG,Message="Heartbeat 1"}]
ClientWebSocket'Client_Outgoing_Message 1
1`[]++
1`[{Op=TEXT,Message="Long message CLIENT ONE"}]++
1`[{Op=TEXT,Message="Long message CLIENT ONE"},{Op=PING,Message="Hello"}]++
1`[{Op=TEXT,Message="Long message CLIENT ONE"},{Op=PING,Message="Hello"},{Op=CLOSE,Message="Goodbye"}]++
1`[{Op=PING,Message="Hello"}]++
1`[{Op=PING,Message="Hello"},{Op=CLOSE,Message="Goodbye"}]++
1`[{Op=CLOSE,Message="Goodbye"}]
ClientWebSocket'Connection_status 1
1`CONN_OPEN++
1`CONN_CLOSING++
1`CONN_CLOSED
ClientWebSocket'To_send 1
1`[]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]
ClientWebSocket'Waiting_for_HTTP_response 1
1`{RequestLine={Verb=GET,Path="/chat",Version="HTTP/1.1"},Headers=[{Key="Host",Value="websocket.com"},{Key="Upgrade",Value="websocket"},{Key="Connection",Value="Upgrade"},{Key="Sec-WebSocket-Key",Value="B64(nonce)"},{Key="Sec-WebSocket-Version",Value="13"}]}
Defrag'Buffer 1 1`{Op=TEXT,Message="Long message CLIENT "}
Defrag'Buffer 2 empty
FragmentAndQueue'Control 1
1`[]++
1`[{Op=PONG,Message="Heartbeat 1"}]++
1`[{Op=PONG,Message="Heartbeat 1"},{Op=PONG,Message="Hello"}]++
1`[{Op=PONG,Message="Hello"}]++
1`[{Op=PONG,Message="Hello"},{Op=PONG,Message="Heartbeat 1"}]
FragmentAndQueue'Control 2
1`[]++
1`[{Op=PING,Message="Hello"}]++
1`[{Op=PING,Message="Hello"},{Op=CLOSE,Message="Goodbye"}]++
1`[{Op=CLOSE,Message="Goodbye"}]
FragmentAndQueue'Data 1
1`[]
FragmentAndQueue'Data 2
1`[]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]
NewConnection'HTTP_Request 1
1`{RequestLine={Verb=GET,Path="/chat",Version="HTTP/1.1"},Headers=[{Key="Host",Value="websocket.com"},{Key="Upgrade",Value="websocket"},{Key="Connection",Value="Upgrade"},{Key="Sec-WebSocket-Key",Value="B64(nonce)"},{Key="Sec-WebSocket-Version",Value="13"}]}
Overview'Client_Call 1
1`[]++
1`[Connect({Protocol="ws",Host="websocket.com",Port=80,Path="/chat"})]++
1`[CliSendMsg({Op=TEXT,Message="Long message CLIENT ONE"})]++
1`[CliSendMsg({Op=TEXT,Message="Long message CLIENT ONE"}),CliSendMsg({Op=PING,Message="Hello"})]++
1`[CliSendMsg({Op=TEXT,Message="Long message CLIENT ONE"}),CliSendMsg({Op=PING,Message="Hello"}),CliSendMsg({Op=CLOSE,Message="Goodbye"})]++
1`[CliSendMsg({Op=PING,Message="Hello"})]++
1`[CliSendMsg({Op=PING,Message="Hello"}),CliSendMsg({Op=CLOSE,Message="Goodbye"})]++
1`[CliSendMsg({Op=CLOSE,Message="Goodbye"})]
Overview'Client_Event 1
1`[]++
1`[CliGetMsg({Op=PONG,Message="Heartbeat 1"})]++
1`[CliGetMsg({Op=PONG,Message="Heartbeat 1"}),ConnResult(success)]++
1`[CliGetMsg({Op=PONG,Message="Hello"})]++
1`[ConnResult(success)]++
1`[ConnResult(success),CliGetMsg({Op=PONG,Message="Heartbeat 1"})]
Overview'Client_Receive 1
1`[]++
1`[HttpRes({ResponseLine={Version="HTTP/1.1",Status=101,Message="Switching Protocols"},Headers=[{Key="Upgrade",Value="websocket"},{Key="Connection",Value="Upgrade"},{Key="Sec-WebSocket-Accept",Value="B64(SHA1(B64(nonce)258EAFA5-E914-47DA-95CA-C5AB0DC85B11))"}]})]++
1`[HttpRes({ResponseLine={Version="HTTP/1.1",Status=101,Message="Switching Protocols"},Headers=[{Key="Upgrade",Value="websocket"},{Key="Connection",Value="Upgrade"},{Key="Sec-WebSocket-Accept",Value="B64(SHA1(B64(nonce)258EAFA5-E914-47DA-95CA-C5AB0DC85B11))"}]}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=0,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="1000"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=0,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="1000"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]
Overview'Client_Send 1
1`[]++
1`[HttpReq({RequestLine={Verb=GET,Path="/chat",Version="HTTP/1.1"},Headers=[{Key="Host",Value="websocket.com"},{Key="Upgrade",Value="websocket"},{Key="Connection",Value="Upgrade"},{Key="Sec-WebSocket-Key",Value="B64(nonce)"},{Key="Sec-WebSocket-Version",Value="13"}]})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]
Overview'Server_Call 1
1`[]++
1`[Msg'({Op=PONG,Message="Heartbeat 1"})]++
1`[ConnReply(accept)]++
1`[ConnReply(accept),Msg'({Op=PONG,Message="Heartbeat 1"})]
Overview'Server_Event 1
1`[]++
1`[SerGetMsg({Op=TEXT,Message="Long message CLIENT ONE"})]++
1`[SerGetMsg({Op=PING,Message="Hello"})]++
1`[ConnRequest(())]
Overview'Server_Receieve 1
1`[]++
1`[HttpReq({RequestLine={Verb=GET,Path="/chat",Version="HTTP/1.1"},Headers=[{Key="Host",Value="websocket.com"},{Key="Upgrade",Value="websocket"},{Key="Connection",Value="Upgrade"},{Key="Sec-WebSocket-Key",Value="B64(nonce)"},{Key="Sec-WebSocket-Version",Value="13"}]})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=set,Payload_length=20,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=set,Payload_length=3,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=set,Payload_length=5,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=7,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="Goodbye"})]
Overview'Server_Send 1
1`[]++
1`[HttpRes({ResponseLine={Version="HTTP/1.1",Status=101,Message="Switching Protocols"},Headers=[{Key="Upgrade",Value="websocket"},{Key="Connection",Value="Upgrade"},{Key="Sec-WebSocket-Accept",Value="B64(SHA1(B64(nonce)258EAFA5-E914-47DA-95CA-C5AB0DC85B11))"}]})]++
1`[HttpRes({ResponseLine={Version="HTTP/1.1",Status=101,Message="Switching Protocols"},Headers=[{Key="Upgrade",Value="websocket"},{Key="Connection",Value="Upgrade"},{Key="Sec-WebSocket-Accept",Value="B64(SHA1(B64(nonce)258EAFA5-E914-47DA-95CA-C5AB0DC85B11))"}]}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=set,Payload_length=0,Masking_key=Mask([Byte(0),Byte(0),Byte(0),Byte(0)]),Payload="1000"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]
ServerApplication'Active_Connection 1
1`()
ServerApplication'Received 1
1`[]++
1`[{Op=TEXT,Message="Long message CLIENT ONE"}]++
1`[{Op=PING,Message="Hello"}]
ServerApplication'To_send 1
1`[]++
1`[{Op=PONG,Message="Heartbeat 1"}]
ServerWebSocket'Connection_Reply 1
1`accept
ServerWebSocket'Connection_Request 1
1`()
ServerWebSocket'Connection_Status 1
1`CONN_OPEN++
1`CONN_CLOSED
ServerWebSocket'Pending_Connection 1
1`{RequestLine={Verb=GET,Path="/chat",Version="HTTP/1.1"},Headers=[{Key="Host",Value="websocket.com"},{Key="Upgrade",Value="websocket"},{Key="Connection",Value="Upgrade"},{Key="Sec-WebSocket-Key",Value="B64(nonce)"},{Key="Sec-WebSocket-Version",Value="13"}]}
ServerWebSocket'Server_Incoming_Message 1
1`[]++
1`[{Op=TEXT,Message="Long message CLIENT ONE"}]++
1`[{Op=TEXT,Message="Long message CLIENT ONE"},{Op=PING,Message="Hello"}]++
1`[{Op=PING,Message="Hello"}]++
1`[{Op=PING,Message="Hello"},{Op=TEXT,Message="Long message CLIENT ONE"}]
ServerWebSocket'Server_Outgoing_Message 1
1`[]++
1`[{Op=PONG,Message="Heartbeat 1"}]++
1`[{Op=PONG,Message="Heartbeat 1"},{Op=PONG,Message="Hello"}]++
1`[{Op=PONG,Message="Hello"}]++
1`[{Op=PONG,Message="Hello"},{Op=PONG,Message="Heartbeat 1"}]
ServerWebSocket'Valid_WS_Frame 1
1`[]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"})]++
1`[WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"})]++
1`[WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}),WsFrame({Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"})]
UnwrapAndReceive'Closing_Connection 1
1`()
UnwrapAndReceive'Closing_Connection 2
empty
UnwrapAndReceive'Received_WS_Frame 1
1`[]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]
UnwrapAndReceive'Received_WS_Frame 2
1`[]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]
WrapAndSend'Next 1 1`[]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=11,Masking_key=Nomask,Payload="Heartbeat 1"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=10,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]
WrapAndSend'Next 2 1`[]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"},{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"},{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"},{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"},{Fin=clear,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=1,Masked=clear,Payload_length=20,Masking_key=Nomask,Payload="Long message CLIENT "},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]++
1`[{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=9,Masked=clear,Payload_length=5,Masking_key=Nomask,Payload="Hello"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=8,Masked=clear,Payload_length=7,Masking_key=Nomask,Payload="Goodbye"},{Fin=set,Rsv1=clear,Rsv2=clear,Rsv3=clear,Opcode=0,Masked=clear,Payload_length=3,Masking_key=Nomask,Payload="ONE"}]
Best Lower Multi-set Bounds
ClientApplication'Active_Connection 1
empty
ClientApplication'Conn_Result 1
empty
ClientApplication'Connection_failed 1
empty
ClientApplication'Messages_received 1
empty
ClientApplication'Messages_to_be_sent 1
empty
ClientApplication'Target_URL 1
empty
ClientApplication'Target_server 1
empty
ClientWebSocket'Client_Connection_Request 1
empty
ClientWebSocket'Client_Connection_Response 1
empty
ClientWebSocket'Client_Incoming_Message 1
empty
ClientWebSocket'Client_Outgoing_Message 1
empty
ClientWebSocket'Connection_status 1
empty
ClientWebSocket'To_send 1
empty
ClientWebSocket'Waiting_for_HTTP_response 1
empty
Defrag'Buffer 1 empty
Defrag'Buffer 2 empty
FragmentAndQueue'Control 1
empty
FragmentAndQueue'Control 2
empty
FragmentAndQueue'Data 1
1`[]
FragmentAndQueue'Data 2
empty
NewConnection'HTTP_Request 1
empty
Overview'Client_Call 1
empty
Overview'Client_Event 1
empty
Overview'Client_Receive 1
empty
Overview'Client_Send 1
empty
Overview'Server_Call 1
empty
Overview'Server_Event 1
empty
Overview'Server_Receieve 1
empty
Overview'Server_Send 1
empty
ServerApplication'Active_Connection 1
empty
ServerApplication'Received 1
empty
ServerApplication'To_send 1
empty
ServerWebSocket'Connection_Reply 1
empty
ServerWebSocket'Connection_Request 1
empty
ServerWebSocket'Connection_Status 1
empty
ServerWebSocket'Pending_Connection 1
empty
ServerWebSocket'Server_Incoming_Message 1
empty
ServerWebSocket'Server_Outgoing_Message 1
empty
ServerWebSocket'Valid_WS_Frame 1
empty
UnwrapAndReceive'Closing_Connection 1
empty
UnwrapAndReceive'Closing_Connection 2
empty
UnwrapAndReceive'Received_WS_Frame 1
empty
UnwrapAndReceive'Received_WS_Frame 2
empty
WrapAndSend'Next 1 empty
WrapAndSend'Next 2 empty
Home Properties
------------------------------------------------------------------------
Home Markings
None
Liveness Properties
------------------------------------------------------------------------
Dead Markings
7635 [47633,47632,47631,47630,47629,...]
Dead Transition Instances
ClientApplication'Fail 1
ConnectionResponse'Send_Reject 1
Defrag'First 2
Defrag'Last 2
Defrag'Mid 1
Defrag'Mid 2
FragmentAndQueue'Queue_data 1
UnwrapAndReceive'Close 2
UnwrapAndReceive'Send_close_frame 2
UnwrapAndReceive'Waiting_for_Close 1
Live Transition Instances
None
Fairness Properties
------------------------------------------------------------------------
No infinite occurrence sequences.