{"abstract":"While receive_closed, event local_data produces closed/discard instead of receive_closed/send.","category":"Protocols","checks":14,"contract":"For the stipulated Bidirectional orderly-close controller, initialize the explicitly shown resource registers from seed (1..5), then consume classified events sequentially. After each event return a deep snapshot of phase, resource registers, and cumulative emitted control frames. The explicit ten phase/event rules and their resource effects define admission and response semantics. Unlisted events preserve phase and emit rejection. Payload is the consecutive integers seed through 2*seed+1. Empty event input returns no observations.","evaluation_group":"s3-protocols-half_close","failed_approach":"The partial repair chooses open/send, which still violates this phase-specific event contract.","family":"s3-protocols-half_close-receive_closed-local_data","id":"FA-18856","implementations":{"attempt":{"sha256":"5b07a448156379becf871d9d4a6a6f1b3bdde7c99e418df0d2332622f9546c3b","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(phase, events, seed):\n    payload = list(range(seed, seed * 2 + 2))\n    r = {'tx_open': phase not in ('send_closed','closing','closed'), 'rx_open': phase not in ('receive_closed','closing','closed'), 'received': [], 'sent': [], 'owned': phase!='closed', 'fin_pending': phase in ('send_closed','closing'), 'payload_pending': payload[:]}\n    frames = []\n    observed = []\n    table = {('open', 'local_eof'): ('send_closed', 'send_fin'), ('open', 'remote_fin'): ('receive_closed', 'ack_fin'), ('send_closed', 'fin_receipt'): ('send_closed', 'retire_fin'), ('receive_closed', 'local_data'): ('open', 'send'), ('send_closed', 'remote_fin'): ('closing', 'ack_fin'), ('receive_closed', 'local_eof'): ('closing', 'send_fin'), ('closing', 'fin_confirmed'): ('closed', 'release'), ('closed', 'late_data'): ('closed', 'reject'), ('send_closed', 'local_data'): ('send_closed', 'reject'), ('receive_closed', 'remote_data'): ('receive_closed', 'reject')}\n    for event in events:\n        phase, action = table.get((phase, event), (phase, \"reject\"))\n        if action == 'send_fin':\n            r['tx_open']=False; frames.append(['FIN',seed])\n        elif action == 'send_two_fins':\n            r['tx_open']=False; frames.extend([['FIN',seed],['FIN',seed]])\n        elif action == 'send_fin_as_data':\n            r['tx_open']=False; frames.append(['DATA',['FIN',seed]])\n        elif action == 'retire_fin':\n            r['fin_pending']=False\n        elif action == 'retire_payload_too':\n            r['fin_pending']=False; r['payload_pending']=[]\n        elif action == 'ack_fin':\n            r['rx_open']=False; frames.append(['ACK_FIN',seed])\n        elif action == 'deliver':\n            r['received'].extend(payload)\n        elif action == 'send':\n            r['sent'].extend(payload)\n        elif action == 'release':\n            r['owned']=False\n        elif action == 'reject':\n            frames.append(['REJECT',event])\n        elif action == 'drop_both':\n            r['tx_open']=False; r['rx_open']=False; r['owned']=False\n        elif action == 'discard':\n            r['received']=[]; r['sent']=[]\n        else:\n            if action not in (\"wait\", \"ignore\", \"keep\", \"retain\", \"keep_peer\", \"keep_offer\", \"keep_hold\", \"keep_batch\", \"retain_staging\", \"keep_staging\", \"keep_local_owner\", \"keep_old_session\", \"keep_address\", \"keep_old_expiry\", \"ignore_conflict\", \"keep_service\", \"keep_subscription\", \"retain_shadow\", \"keep_live\", \"keep_suspicion\", \"keep_roles\", \"keep_staged\"):\n                frames.append([action, payload[:]])\n        observed.append(json.loads(json.dumps({\"phase\": phase, \"registers\": r, \"frames\": frames})))\n    return observed\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = {1: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['ACK_FIN', 1]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [1, 2, 3]}, 'frames': [['ACK_FIN', 1]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [1, 2, 3]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['ACK_FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['ACK_FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['ACK_FIN', 1], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'unsupported']]}])], 2: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['ACK_FIN', 2]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['ACK_FIN', 2]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'unsupported']]}])], 3: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['ACK_FIN', 3]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['ACK_FIN', 3]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'unsupported']]}])], 4: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['ACK_FIN', 4]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['ACK_FIN', 4]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'unsupported']]}])], 5: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['ACK_FIN', 5]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['ACK_FIN', 5]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'unsupported']]}])]}\nfor label, phase, events, expected in cases[N]:\n    check(label, solve(phase, events, N), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"82342c49d77faeb5e2dce917b74f9c455c68678fb1262fc0623540737829e3f6","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(phase, events, seed):\n    payload = list(range(seed, seed * 2 + 2))\n    r = {'tx_open': phase not in ('send_closed','closing','closed'), 'rx_open': phase not in ('receive_closed','closing','closed'), 'received': [], 'sent': [], 'owned': phase!='closed', 'fin_pending': phase in ('send_closed','closing'), 'payload_pending': payload[:]}\n    frames = []\n    observed = []\n    table = {('open', 'local_eof'): ('send_closed', 'send_fin'), ('open', 'remote_fin'): ('receive_closed', 'ack_fin'), ('send_closed', 'fin_receipt'): ('send_closed', 'retire_fin'), ('receive_closed', 'local_data'): ('closed', 'discard'), ('send_closed', 'remote_fin'): ('closing', 'ack_fin'), ('receive_closed', 'local_eof'): ('closing', 'send_fin'), ('closing', 'fin_confirmed'): ('closed', 'release'), ('closed', 'late_data'): ('closed', 'reject'), ('send_closed', 'local_data'): ('send_closed', 'reject'), ('receive_closed', 'remote_data'): ('receive_closed', 'reject')}\n    for event in events:\n        phase, action = table.get((phase, event), (phase, \"reject\"))\n        if action == 'send_fin':\n            r['tx_open']=False; frames.append(['FIN',seed])\n        elif action == 'send_two_fins':\n            r['tx_open']=False; frames.extend([['FIN',seed],['FIN',seed]])\n        elif action == 'send_fin_as_data':\n            r['tx_open']=False; frames.append(['DATA',['FIN',seed]])\n        elif action == 'retire_fin':\n            r['fin_pending']=False\n        elif action == 'retire_payload_too':\n            r['fin_pending']=False; r['payload_pending']=[]\n        elif action == 'ack_fin':\n            r['rx_open']=False; frames.append(['ACK_FIN',seed])\n        elif action == 'deliver':\n            r['received'].extend(payload)\n        elif action == 'send':\n            r['sent'].extend(payload)\n        elif action == 'release':\n            r['owned']=False\n        elif action == 'reject':\n            frames.append(['REJECT',event])\n        elif action == 'drop_both':\n            r['tx_open']=False; r['rx_open']=False; r['owned']=False\n        elif action == 'discard':\n            r['received']=[]; r['sent']=[]\n        else:\n            if action not in (\"wait\", \"ignore\", \"keep\", \"retain\", \"keep_peer\", \"keep_offer\", \"keep_hold\", \"keep_batch\", \"retain_staging\", \"keep_staging\", \"keep_local_owner\", \"keep_old_session\", \"keep_address\", \"keep_old_expiry\", \"ignore_conflict\", \"keep_service\", \"keep_subscription\", \"retain_shadow\", \"keep_live\", \"keep_suspicion\", \"keep_roles\", \"keep_staged\"):\n                frames.append([action, payload[:]])\n        observed.append(json.loads(json.dumps({\"phase\": phase, \"registers\": r, \"frames\": frames})))\n    return observed\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = {1: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['ACK_FIN', 1]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [1, 2, 3]}, 'frames': [['ACK_FIN', 1]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [1, 2, 3]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['ACK_FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['ACK_FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['ACK_FIN', 1], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'unsupported']]}])], 2: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['ACK_FIN', 2]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['ACK_FIN', 2]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'unsupported']]}])], 3: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['ACK_FIN', 3]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['ACK_FIN', 3]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'unsupported']]}])], 4: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['ACK_FIN', 4]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['ACK_FIN', 4]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'unsupported']]}])], 5: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['ACK_FIN', 5]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['ACK_FIN', 5]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'unsupported']]}])]}\nfor label, phase, events, expected in cases[N]:\n    check(label, solve(phase, events, N), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"fixed":{"sha256":"651ff0b3ac7970a25269653735d533049cc749648d2e14bd45dbd8fc2a90cd03","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(phase, events, seed):\n    payload = list(range(seed, seed * 2 + 2))\n    r = {'tx_open': phase not in ('send_closed','closing','closed'), 'rx_open': phase not in ('receive_closed','closing','closed'), 'received': [], 'sent': [], 'owned': phase!='closed', 'fin_pending': phase in ('send_closed','closing'), 'payload_pending': payload[:]}\n    frames = []\n    observed = []\n    table = {('open', 'local_eof'): ('send_closed', 'send_fin'), ('open', 'remote_fin'): ('receive_closed', 'ack_fin'), ('send_closed', 'fin_receipt'): ('send_closed', 'retire_fin'), ('receive_closed', 'local_data'): ('receive_closed', 'send'), ('send_closed', 'remote_fin'): ('closing', 'ack_fin'), ('receive_closed', 'local_eof'): ('closing', 'send_fin'), ('closing', 'fin_confirmed'): ('closed', 'release'), ('closed', 'late_data'): ('closed', 'reject'), ('send_closed', 'local_data'): ('send_closed', 'reject'), ('receive_closed', 'remote_data'): ('receive_closed', 'reject')}\n    for event in events:\n        phase, action = table.get((phase, event), (phase, \"reject\"))\n        if action == 'send_fin':\n            r['tx_open']=False; frames.append(['FIN',seed])\n        elif action == 'send_two_fins':\n            r['tx_open']=False; frames.extend([['FIN',seed],['FIN',seed]])\n        elif action == 'send_fin_as_data':\n            r['tx_open']=False; frames.append(['DATA',['FIN',seed]])\n        elif action == 'retire_fin':\n            r['fin_pending']=False\n        elif action == 'retire_payload_too':\n            r['fin_pending']=False; r['payload_pending']=[]\n        elif action == 'ack_fin':\n            r['rx_open']=False; frames.append(['ACK_FIN',seed])\n        elif action == 'deliver':\n            r['received'].extend(payload)\n        elif action == 'send':\n            r['sent'].extend(payload)\n        elif action == 'release':\n            r['owned']=False\n        elif action == 'reject':\n            frames.append(['REJECT',event])\n        elif action == 'drop_both':\n            r['tx_open']=False; r['rx_open']=False; r['owned']=False\n        elif action == 'discard':\n            r['received']=[]; r['sent']=[]\n        else:\n            if action not in (\"wait\", \"ignore\", \"keep\", \"retain\", \"keep_peer\", \"keep_offer\", \"keep_hold\", \"keep_batch\", \"retain_staging\", \"keep_staging\", \"keep_local_owner\", \"keep_old_session\", \"keep_address\", \"keep_old_expiry\", \"ignore_conflict\", \"keep_service\", \"keep_subscription\", \"retain_shadow\", \"keep_live\", \"keep_suspicion\", \"keep_roles\", \"keep_staged\"):\n                frames.append([action, payload[:]])\n        observed.append(json.loads(json.dumps({\"phase\": phase, \"registers\": r, \"frames\": frames})))\n    return observed\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = {1: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['ACK_FIN', 1]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [1, 2, 3]}, 'frames': [['ACK_FIN', 1]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [1, 2, 3]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['ACK_FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['ACK_FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['ACK_FIN', 1], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [1, 2, 3], 'owned': False, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['FIN', 1], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [1, 2, 3]}, 'frames': [['REJECT', 'unsupported']]}])], 2: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['ACK_FIN', 2]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['ACK_FIN', 2]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['ACK_FIN', 2], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [2, 3, 4, 5], 'owned': False, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['FIN', 2], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [2, 3, 4, 5]}, 'frames': [['REJECT', 'unsupported']]}])], 3: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['ACK_FIN', 3]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['ACK_FIN', 3]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['ACK_FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [3, 4, 5, 6, 7], 'owned': False, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['FIN', 3], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [3, 4, 5, 6, 7]}, 'frames': [['REJECT', 'unsupported']]}])], 4: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['ACK_FIN', 4]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['ACK_FIN', 4]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['ACK_FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [4, 5, 6, 7, 8, 9], 'owned': False, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['FIN', 4], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [4, 5, 6, 7, 8, 9]}, 'frames': [['REJECT', 'unsupported']]}])], 5: [('open/local_eof', 'open', ['local_eof'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}]), ('open/remote_fin', 'open', ['remote_fin'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['ACK_FIN', 5]]}]), ('send_closed/fin_receipt', 'send_closed', ['fin_receipt'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}]), ('receive_closed/local_data', 'receive_closed', ['local_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}]), ('send_closed/remote_fin', 'send_closed', ['remote_fin'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['ACK_FIN', 5]]}]), ('receive_closed/local_eof', 'receive_closed', ['local_eof'], [{'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}]), ('closing/fin_confirmed', 'closing', ['fin_confirmed'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': True, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}]), ('closed/late_data', 'closed', ['late_data'], [{'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'late_data']]}]), ('send_closed/local_data', 'send_closed', ['local_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': True, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'local_data']]}]), ('receive_closed/remote_data', 'receive_closed', ['remote_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'remote_data']]}]), ('ordered trace 0', 'open', ['local_eof', 'remote_fin', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'send_closed', 'registers': {'tx_open': False, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['ACK_FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('ordered trace 3', 'receive_closed', ['local_data', 'local_eof', 'fin_confirmed', 'late_data', 'late_data', 'late_data', 'late_data', 'late_data'], [{'phase': 'receive_closed', 'registers': {'tx_open': True, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': []}, {'phase': 'closing', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5]]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}, {'phase': 'closed', 'registers': {'tx_open': False, 'rx_open': False, 'received': [], 'sent': [5, 6, 7, 8, 9, 10, 11], 'owned': False, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['FIN', 5], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data'], ['REJECT', 'late_data']]}]), ('empty input', 'open', [], []), ('unknown event', 'open', ['unsupported'], [{'phase': 'open', 'registers': {'tx_open': True, 'rx_open': True, 'received': [], 'sent': [], 'owned': True, 'fin_pending': False, 'payload_pending': [5, 6, 7, 8, 9, 10, 11]}, 'frames': [['REJECT', 'unsupported']]}])]}\nfor label, phase, events, expected in cases[N]:\n    check(label, solve(phase, events, N), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":"Bounded offline control-plane abstraction with prescribed initial registers and classified events. Not a named protocol implementation or conformance test; excludes wire parsing, transport retries, physical execution, authentication, crash persistence, and timing. Related event faults share the full corrected controller and evaluation group. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"s3-protocols-half_close-receive_closed-local_data","generated_at":"2026-09-29T14:40:01.812248+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"Incorrect event admission now changes concrete queued data, resource ownership, or emitted protocol frames and subsequent trace behavior.","repair":"In phase receive_closed, classify local_data as transition to receive_closed and emit send.","root_cause":"In receive closed, the local data handler runs discard and enters closed; it must instead run send and enter receive closed.","sha256":"4c0bbfe08060fa2f22722e9d051f34df4cf34ca388a85ad036f4ee903a4ada10","title":"Bidirectional orderly-close controller: receive closed / local data · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":45.248,"exit_code":1,"observations":[{"actual":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"check":"open/local_eof","expected":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["ACK_FIN",1]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"check":"open/remote_fin","expected":[{"frames":[["ACK_FIN",1]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"passed":true},{"actual":[{"frames":[],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"check":"send_closed/fin_receipt","expected":[{"frames":[],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[],"phase":"open","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":true}}],"check":"receive_closed/local_data","expected":[{"frames":[],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":true}}],"passed":false},{"actual":[{"frames":[["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"send_closed/remote_fin","expected":[{"frames":[["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"receive_closed/local_eof","expected":[{"frames":[["FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[],"phase":"closed","registers":{"fin_pending":true,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"closing/fin_confirmed","expected":[{"frames":[],"phase":"closed","registers":{"fin_pending":true,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"closed/late_data","expected":[{"frames":[["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["REJECT","local_data"]],"phase":"send_closed","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"check":"send_closed/local_data","expected":[{"frames":[["REJECT","local_data"]],"phase":"send_closed","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["REJECT","remote_data"]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"check":"receive_closed/remote_data","expected":[{"frames":[["REJECT","remote_data"]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"passed":true},{"actual":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1],["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"ordered trace 0","expected":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1],["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[],"phase":"open","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":true}},{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}},{"frames":[["FIN",1],["REJECT","fin_confirmed"]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}},{"frames":[["FIN",1],["REJECT","fin_confirmed"],["REJECT","late_data"]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}}],"check":"ordered trace 3","expected":[{"frames":[],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":true}},{"frames":[["FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}},{"frames":[["FIN",1]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}},{"frames":[["FIN",1],["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}}],"passed":false},{"actual":[],"check":"empty input","expected":[],"passed":true},{"actual":[{"frames":[["REJECT","unsupported"]],"phase":"open","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":true}}],"check":"unknown event","expected":[{"frames":[["REJECT","unsupported"]],"phase":"open","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":true}}],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"open/local_eof\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"passed\": true}, {\"check\": \"open/remote_fin\", \"actual\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"passed\": true}, {\"check\": \"send_closed/fin_receipt\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"passed\": true}, {\"check\": \"receive_closed/local_data\", \"actual\": [{\"phase\": \"open\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"passed\": false}, {\"check\": \"send_closed/remote_fin\", \"actual\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"expected\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"passed\": true}, {\"check\": \"receive_closed/local_eof\", \"actual\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"expected\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"passed\": true}, {\"check\": \"closing/fin_confirmed\", \"actual\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"expected\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"passed\": true}, {\"check\": \"closed/late_data\", \"actual\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"late_data\"]]}], \"expected\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"late_data\"]]}], \"passed\": true}, {\"check\": \"send_closed/local_data\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"local_data\"]]}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"local_data\"]]}], \"passed\": true}, {\"check\": \"receive_closed/remote_data\", \"actual\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"remote_data\"]]}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"remote_data\"]]}], \"passed\": true}, {\"check\": \"ordered trace 0\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1], [\"REJECT\", \"late_data\"]]}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1], [\"REJECT\", \"late_data\"]]}], \"passed\": true}, {\"check\": \"ordered trace 3\", \"actual\": [{\"phase\": \"open\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}, {\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"REJECT\", \"fin_confirmed\"]]}, {\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"REJECT\", \"fin_confirmed\"], [\"REJECT\", \"late_data\"]]}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}, {\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"REJECT\", \"late_data\"]]}], \"passed\": false}, {\"check\": \"empty input\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"unknown event\", \"actual\": [{\"phase\": \"open\", \"registers\": {\"tx_open\": true, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"unsupported\"]]}], \"expected\": [{\"phase\": \"open\", \"registers\": {\"tx_open\": true, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"unsupported\"]]}], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":47.885,"exit_code":1,"observations":[{"actual":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"check":"open/local_eof","expected":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["ACK_FIN",1]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"check":"open/remote_fin","expected":[{"frames":[["ACK_FIN",1]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"passed":true},{"actual":[{"frames":[],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"check":"send_closed/fin_receipt","expected":[{"frames":[],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[],"phase":"closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"check":"receive_closed/local_data","expected":[{"frames":[],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":true}}],"passed":false},{"actual":[{"frames":[["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"send_closed/remote_fin","expected":[{"frames":[["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"receive_closed/local_eof","expected":[{"frames":[["FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[],"phase":"closed","registers":{"fin_pending":true,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"closing/fin_confirmed","expected":[{"frames":[],"phase":"closed","registers":{"fin_pending":true,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"closed/late_data","expected":[{"frames":[["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["REJECT","local_data"]],"phase":"send_closed","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"check":"send_closed/local_data","expected":[{"frames":[["REJECT","local_data"]],"phase":"send_closed","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["REJECT","remote_data"]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"check":"receive_closed/remote_data","expected":[{"frames":[["REJECT","remote_data"]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"passed":true},{"actual":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1],["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"ordered trace 0","expected":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1],["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[],"phase":"closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}},{"frames":[["REJECT","local_eof"]],"phase":"closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}},{"frames":[["REJECT","local_eof"],["REJECT","fin_confirmed"]],"phase":"closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}},{"frames":[["REJECT","local_eof"],["REJECT","fin_confirmed"],["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"check":"ordered trace 3","expected":[{"frames":[],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":true}},{"frames":[["FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}},{"frames":[["FIN",1]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}},{"frames":[["FIN",1],["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}}],"passed":false},{"actual":[],"check":"empty input","expected":[],"passed":true},{"actual":[{"frames":[["REJECT","unsupported"]],"phase":"open","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":true}}],"check":"unknown event","expected":[{"frames":[["REJECT","unsupported"]],"phase":"open","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":true}}],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"open/local_eof\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"passed\": true}, {\"check\": \"open/remote_fin\", \"actual\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"passed\": true}, {\"check\": \"send_closed/fin_receipt\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"passed\": true}, {\"check\": \"receive_closed/local_data\", \"actual\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"passed\": false}, {\"check\": \"send_closed/remote_fin\", \"actual\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"expected\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"passed\": true}, {\"check\": \"receive_closed/local_eof\", \"actual\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"expected\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"passed\": true}, {\"check\": \"closing/fin_confirmed\", \"actual\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"expected\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"passed\": true}, {\"check\": \"closed/late_data\", \"actual\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"late_data\"]]}], \"expected\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"late_data\"]]}], \"passed\": true}, {\"check\": \"send_closed/local_data\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"local_data\"]]}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"local_data\"]]}], \"passed\": true}, {\"check\": \"receive_closed/remote_data\", \"actual\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"remote_data\"]]}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"remote_data\"]]}], \"passed\": true}, {\"check\": \"ordered trace 0\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1], [\"REJECT\", \"late_data\"]]}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1], [\"REJECT\", \"late_data\"]]}], \"passed\": true}, {\"check\": \"ordered trace 3\", \"actual\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"local_eof\"]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"local_eof\"], [\"REJECT\", \"fin_confirmed\"]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"local_eof\"], [\"REJECT\", \"fin_confirmed\"], [\"REJECT\", \"late_data\"]]}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}, {\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"REJECT\", \"late_data\"]]}], \"passed\": false}, {\"check\": \"empty input\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"unknown event\", \"actual\": [{\"phase\": \"open\", \"registers\": {\"tx_open\": true, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"unsupported\"]]}], \"expected\": [{\"phase\": \"open\", \"registers\": {\"tx_open\": true, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"unsupported\"]]}], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":46.717,"exit_code":0,"observations":[{"actual":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"check":"open/local_eof","expected":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["ACK_FIN",1]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"check":"open/remote_fin","expected":[{"frames":[["ACK_FIN",1]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"passed":true},{"actual":[{"frames":[],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"check":"send_closed/fin_receipt","expected":[{"frames":[],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":true}}],"check":"receive_closed/local_data","expected":[{"frames":[],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":true}}],"passed":true},{"actual":[{"frames":[["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"send_closed/remote_fin","expected":[{"frames":[["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"receive_closed/local_eof","expected":[{"frames":[["FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[],"phase":"closed","registers":{"fin_pending":true,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"closing/fin_confirmed","expected":[{"frames":[],"phase":"closed","registers":{"fin_pending":true,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"closed/late_data","expected":[{"frames":[["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["REJECT","local_data"]],"phase":"send_closed","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"check":"send_closed/local_data","expected":[{"frames":[["REJECT","local_data"]],"phase":"send_closed","registers":{"fin_pending":true,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[["REJECT","remote_data"]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"check":"receive_closed/remote_data","expected":[{"frames":[["REJECT","remote_data"]],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":true}}],"passed":true},{"actual":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1],["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"check":"ordered trace 0","expected":[{"frames":[["FIN",1]],"phase":"send_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}},{"frames":[["FIN",1],["ACK_FIN",1],["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[],"tx_open":false}}],"passed":true},{"actual":[{"frames":[],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":true}},{"frames":[["FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}},{"frames":[["FIN",1]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}},{"frames":[["FIN",1],["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}}],"check":"ordered trace 3","expected":[{"frames":[],"phase":"receive_closed","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":true}},{"frames":[["FIN",1]],"phase":"closing","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}},{"frames":[["FIN",1]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}},{"frames":[["FIN",1],["REJECT","late_data"]],"phase":"closed","registers":{"fin_pending":false,"owned":false,"payload_pending":[1,2,3],"received":[],"rx_open":false,"sent":[1,2,3],"tx_open":false}}],"passed":true},{"actual":[],"check":"empty input","expected":[],"passed":true},{"actual":[{"frames":[["REJECT","unsupported"]],"phase":"open","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":true}}],"check":"unknown event","expected":[{"frames":[["REJECT","unsupported"]],"phase":"open","registers":{"fin_pending":false,"owned":true,"payload_pending":[1,2,3],"received":[],"rx_open":true,"sent":[],"tx_open":true}}],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"open/local_eof\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"passed\": true}, {\"check\": \"open/remote_fin\", \"actual\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"passed\": true}, {\"check\": \"send_closed/fin_receipt\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"passed\": true}, {\"check\": \"receive_closed/local_data\", \"actual\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"passed\": true}, {\"check\": \"send_closed/remote_fin\", \"actual\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"expected\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"ACK_FIN\", 1]]}], \"passed\": true}, {\"check\": \"receive_closed/local_eof\", \"actual\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"expected\": [{\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}], \"passed\": true}, {\"check\": \"closing/fin_confirmed\", \"actual\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"expected\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": []}], \"passed\": true}, {\"check\": \"closed/late_data\", \"actual\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"late_data\"]]}], \"expected\": [{\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"late_data\"]]}], \"passed\": true}, {\"check\": \"send_closed/local_data\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"local_data\"]]}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": true, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"local_data\"]]}], \"passed\": true}, {\"check\": \"receive_closed/remote_data\", \"actual\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"remote_data\"]]}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"remote_data\"]]}], \"passed\": true}, {\"check\": \"ordered trace 0\", \"actual\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1], [\"REJECT\", \"late_data\"]]}], \"expected\": [{\"phase\": \"send_closed\", \"registers\": {\"tx_open\": false, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"ACK_FIN\", 1], [\"REJECT\", \"late_data\"]]}], \"passed\": true}, {\"check\": \"ordered trace 3\", \"actual\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}, {\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"REJECT\", \"late_data\"]]}], \"expected\": [{\"phase\": \"receive_closed\", \"registers\": {\"tx_open\": true, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": []}, {\"phase\": \"closing\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1]]}, {\"phase\": \"closed\", \"registers\": {\"tx_open\": false, \"rx_open\": false, \"received\": [], \"sent\": [1, 2, 3], \"owned\": false, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"FIN\", 1], [\"REJECT\", \"late_data\"]]}], \"passed\": true}, {\"check\": \"empty input\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"unknown event\", \"actual\": [{\"phase\": \"open\", \"registers\": {\"tx_open\": true, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"unsupported\"]]}], \"expected\": [{\"phase\": \"open\", \"registers\": {\"tx_open\": true, \"rx_open\": true, \"received\": [], \"sent\": [], \"owned\": true, \"fin_pending\": false, \"payload_pending\": [1, 2, 3]}, \"frames\": [[\"REJECT\", \"unsupported\"]]}], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}