{"abstract":"While usable, event spend_last produces usable/send_one instead of exhausted/send_one.","category":"Protocols","checks":14,"contract":"For the stipulated Receiver-issued transmission-credit lease 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-credit_lease","failed_approach":"The partial repair chooses exhausted/drop, which still violates this phase-specific event contract.","family":"s3-protocols-credit_lease-usable-spend_last","id":"FA-18996","implementations":{"attempt":{"sha256":"4a1bc53980178214c12fa6e3fe2ec2d750d5ad59dd40208f28cd7a52b238cc44","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 = {'credits': int(phase=='usable'), 'lease': seed, 'inflight': [seed], 'queue': payload[:], 'stale_records': [], 'sent': []}\n    frames = []\n    observed = []\n    table = {('none', 'grant'): ('usable', 'record_grant'), ('usable', 'spend_last'): ('exhausted', 'drop'), ('exhausted', 'payload'): ('exhausted', 'backpressure'), ('usable', 'revoke'): ('revoked', 'stop_new_sends'), ('revoked', 'inflight_ack'): ('revoked', 'retire_inflight'), ('revoked', 'new_grant'): ('usable', 'replace_lease'), ('usable', 'lease_expired'): ('expired', 'stop_new_sends'), ('expired', 'old_grant'): ('expired', 'reject_stale'), ('exhausted', 'refresh'): ('usable', 'record_grant'), ('none', 'ack'): ('none', 'reject_unsolicited')}\n    for event in events:\n        phase, action = table.get((phase, event), (phase, \"reject\"))\n        if action == 'record_grant':\n            r['credits']=len(payload)\n        elif action == 'send_one':\n            r['credits']-=1; r['sent'].append(r['queue'].pop(0)) if r['queue'] else None\n        elif action == 'backpressure':\n            frames.append(['BLOCKED',len(r['queue'])])\n        elif action == 'stop_new_sends':\n            r['credits']=0\n        elif action == 'retire_inflight':\n            r['inflight']=[]\n        elif action == 'replace_lease':\n            r['lease']=seed+1; r['credits']=len(payload)\n        elif action == 'reject_stale':\n            frames.append(['STALE',seed])\n        elif action == 'reject_unsolicited':\n            frames.append(['UNSOLICITED_ACK',seed])\n        elif action == 'send_all':\n            r['sent'].extend(r['queue']); r['queue']=[]\n        elif action == 'drop':\n            r['queue']=[]\n        elif action == 'discard_inflight':\n            r['inflight']=[]; r['queue']=[]\n        elif action == 'grant_credit':\n            r['credits']+=1\n        elif action == 'merge_lease':\n            r['credits']+=len(payload)\n        elif action == 'record_ack':\n            r['stale_records'].append(seed)\n        elif action == 'double_grant':\n            r['credits']=2*len(payload)\n        elif action == 'send_probe':\n            r['sent'].append('probe')\n        elif action == 'continue':\n            r['sent'].extend(r['queue'])\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: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 3]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 2, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 1]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 1]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 3, 'lease': 2, 'inflight': [], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': [['BLOCKED', 2]]}, {'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': [['BLOCKED', 2]]}, {'phase': 'exhausted', 'registers': {'credits': 2, 'lease': 1, 'inflight': [1], 'queue': [3], 'stale_records': [], 'sent': [1, 2]}, 'frames': [['BLOCKED', 2]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['reject', [1, 2, 3]]]}])], 2: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 4]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 3, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 2]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 2]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 4, 'lease': 3, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': [['BLOCKED', 3]]}, {'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': [['BLOCKED', 3]]}, {'phase': 'exhausted', 'registers': {'credits': 3, 'lease': 2, 'inflight': [2], 'queue': [4, 5], 'stale_records': [], 'sent': [2, 3]}, 'frames': [['BLOCKED', 3]]}, {'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [4, 5], 'stale_records': [], 'sent': [2, 3]}, 'frames': [['BLOCKED', 3]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['reject', [2, 3, 4, 5]]]}])], 3: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 5]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 4, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 3]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 3]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke', 'new_grant'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 4, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 4, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh', 'lease_expired'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'exhausted', 'registers': {'credits': 4, 'lease': 3, 'inflight': [3], 'queue': [5, 6, 7], 'stale_records': [], 'sent': [3, 4]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [5, 6, 7], 'stale_records': [], 'sent': [3, 4]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [5, 6, 7], 'stale_records': [], 'sent': [3, 4]}, 'frames': [['BLOCKED', 4]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['reject', [3, 4, 5, 6, 7]]]}])], 4: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 6]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 5, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 4]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 4]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke', 'new_grant', 'spend_last'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 5, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 5, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 5, 'lease': 5, 'inflight': [], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh', 'lease_expired', 'old_grant'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'exhausted', 'registers': {'credits': 5, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5], ['STALE', 4]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['reject', [4, 5, 6, 7, 8, 9]]]}])], 5: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 7]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 5]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 5]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke', 'new_grant', 'spend_last', 'refresh'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 6, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 6, 'lease': 6, 'inflight': [], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh', 'lease_expired', 'old_grant', 'old_grant'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'exhausted', 'registers': {'credits': 6, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6], ['STALE', 5]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6], ['STALE', 5], ['STALE', 5]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['reject', [5, 6, 7, 8, 9, 10, 11]]]}])]}\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":"dd1b81767407f1928f298201a077c2fb1f8b567bf0cac0b31694b27b55ec9a66","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 = {'credits': int(phase=='usable'), 'lease': seed, 'inflight': [seed], 'queue': payload[:], 'stale_records': [], 'sent': []}\n    frames = []\n    observed = []\n    table = {('none', 'grant'): ('usable', 'record_grant'), ('usable', 'spend_last'): ('usable', 'send_one'), ('exhausted', 'payload'): ('exhausted', 'backpressure'), ('usable', 'revoke'): ('revoked', 'stop_new_sends'), ('revoked', 'inflight_ack'): ('revoked', 'retire_inflight'), ('revoked', 'new_grant'): ('usable', 'replace_lease'), ('usable', 'lease_expired'): ('expired', 'stop_new_sends'), ('expired', 'old_grant'): ('expired', 'reject_stale'), ('exhausted', 'refresh'): ('usable', 'record_grant'), ('none', 'ack'): ('none', 'reject_unsolicited')}\n    for event in events:\n        phase, action = table.get((phase, event), (phase, \"reject\"))\n        if action == 'record_grant':\n            r['credits']=len(payload)\n        elif action == 'send_one':\n            r['credits']-=1; r['sent'].append(r['queue'].pop(0)) if r['queue'] else None\n        elif action == 'backpressure':\n            frames.append(['BLOCKED',len(r['queue'])])\n        elif action == 'stop_new_sends':\n            r['credits']=0\n        elif action == 'retire_inflight':\n            r['inflight']=[]\n        elif action == 'replace_lease':\n            r['lease']=seed+1; r['credits']=len(payload)\n        elif action == 'reject_stale':\n            frames.append(['STALE',seed])\n        elif action == 'reject_unsolicited':\n            frames.append(['UNSOLICITED_ACK',seed])\n        elif action == 'send_all':\n            r['sent'].extend(r['queue']); r['queue']=[]\n        elif action == 'drop':\n            r['queue']=[]\n        elif action == 'discard_inflight':\n            r['inflight']=[]; r['queue']=[]\n        elif action == 'grant_credit':\n            r['credits']+=1\n        elif action == 'merge_lease':\n            r['credits']+=len(payload)\n        elif action == 'record_ack':\n            r['stale_records'].append(seed)\n        elif action == 'double_grant':\n            r['credits']=2*len(payload)\n        elif action == 'send_probe':\n            r['sent'].append('probe')\n        elif action == 'continue':\n            r['sent'].extend(r['queue'])\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: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 3]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 2, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 1]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 1]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 3, 'lease': 2, 'inflight': [], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': [['BLOCKED', 2]]}, {'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': [['BLOCKED', 2]]}, {'phase': 'exhausted', 'registers': {'credits': 2, 'lease': 1, 'inflight': [1], 'queue': [3], 'stale_records': [], 'sent': [1, 2]}, 'frames': [['BLOCKED', 2]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['reject', [1, 2, 3]]]}])], 2: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 4]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 3, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 2]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 2]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 4, 'lease': 3, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': [['BLOCKED', 3]]}, {'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': [['BLOCKED', 3]]}, {'phase': 'exhausted', 'registers': {'credits': 3, 'lease': 2, 'inflight': [2], 'queue': [4, 5], 'stale_records': [], 'sent': [2, 3]}, 'frames': [['BLOCKED', 3]]}, {'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [4, 5], 'stale_records': [], 'sent': [2, 3]}, 'frames': [['BLOCKED', 3]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['reject', [2, 3, 4, 5]]]}])], 3: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 5]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 4, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 3]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 3]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke', 'new_grant'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 4, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 4, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh', 'lease_expired'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'exhausted', 'registers': {'credits': 4, 'lease': 3, 'inflight': [3], 'queue': [5, 6, 7], 'stale_records': [], 'sent': [3, 4]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [5, 6, 7], 'stale_records': [], 'sent': [3, 4]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [5, 6, 7], 'stale_records': [], 'sent': [3, 4]}, 'frames': [['BLOCKED', 4]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['reject', [3, 4, 5, 6, 7]]]}])], 4: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 6]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 5, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 4]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 4]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke', 'new_grant', 'spend_last'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 5, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 5, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 5, 'lease': 5, 'inflight': [], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh', 'lease_expired', 'old_grant'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'exhausted', 'registers': {'credits': 5, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5], ['STALE', 4]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['reject', [4, 5, 6, 7, 8, 9]]]}])], 5: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 7]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 5]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 5]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke', 'new_grant', 'spend_last', 'refresh'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 6, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 6, 'lease': 6, 'inflight': [], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh', 'lease_expired', 'old_grant', 'old_grant'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'exhausted', 'registers': {'credits': 6, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6], ['STALE', 5]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6], ['STALE', 5], ['STALE', 5]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['reject', [5, 6, 7, 8, 9, 10, 11]]]}])]}\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":"475ff93ce59d85abfb61ba5f99d016636afa40c20785cc5a44c9ac38bdd8d75b","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 = {'credits': int(phase=='usable'), 'lease': seed, 'inflight': [seed], 'queue': payload[:], 'stale_records': [], 'sent': []}\n    frames = []\n    observed = []\n    table = {('none', 'grant'): ('usable', 'record_grant'), ('usable', 'spend_last'): ('exhausted', 'send_one'), ('exhausted', 'payload'): ('exhausted', 'backpressure'), ('usable', 'revoke'): ('revoked', 'stop_new_sends'), ('revoked', 'inflight_ack'): ('revoked', 'retire_inflight'), ('revoked', 'new_grant'): ('usable', 'replace_lease'), ('usable', 'lease_expired'): ('expired', 'stop_new_sends'), ('expired', 'old_grant'): ('expired', 'reject_stale'), ('exhausted', 'refresh'): ('usable', 'record_grant'), ('none', 'ack'): ('none', 'reject_unsolicited')}\n    for event in events:\n        phase, action = table.get((phase, event), (phase, \"reject\"))\n        if action == 'record_grant':\n            r['credits']=len(payload)\n        elif action == 'send_one':\n            r['credits']-=1; r['sent'].append(r['queue'].pop(0)) if r['queue'] else None\n        elif action == 'backpressure':\n            frames.append(['BLOCKED',len(r['queue'])])\n        elif action == 'stop_new_sends':\n            r['credits']=0\n        elif action == 'retire_inflight':\n            r['inflight']=[]\n        elif action == 'replace_lease':\n            r['lease']=seed+1; r['credits']=len(payload)\n        elif action == 'reject_stale':\n            frames.append(['STALE',seed])\n        elif action == 'reject_unsolicited':\n            frames.append(['UNSOLICITED_ACK',seed])\n        elif action == 'send_all':\n            r['sent'].extend(r['queue']); r['queue']=[]\n        elif action == 'drop':\n            r['queue']=[]\n        elif action == 'discard_inflight':\n            r['inflight']=[]; r['queue']=[]\n        elif action == 'grant_credit':\n            r['credits']+=1\n        elif action == 'merge_lease':\n            r['credits']+=len(payload)\n        elif action == 'record_ack':\n            r['stale_records'].append(seed)\n        elif action == 'double_grant':\n            r['credits']=2*len(payload)\n        elif action == 'send_probe':\n            r['sent'].append('probe')\n        elif action == 'continue':\n            r['sent'].extend(r['queue'])\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: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 3]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 2, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 1]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 1]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant'], [{'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 1, 'inflight': [], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 3, 'lease': 2, 'inflight': [], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': [['BLOCKED', 2]]}, {'phase': 'usable', 'registers': {'credits': 3, 'lease': 1, 'inflight': [1], 'queue': [2, 3], 'stale_records': [], 'sent': [1]}, 'frames': [['BLOCKED', 2]]}, {'phase': 'exhausted', 'registers': {'credits': 2, 'lease': 1, 'inflight': [1], 'queue': [3], 'stale_records': [], 'sent': [1, 2]}, 'frames': [['BLOCKED', 2]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 1, 'inflight': [1], 'queue': [1, 2, 3], 'stale_records': [], 'sent': []}, 'frames': [['reject', [1, 2, 3]]]}])], 2: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 4]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 3, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 2]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 2]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke'], [{'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 2, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 4, 'lease': 3, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': [['BLOCKED', 3]]}, {'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [3, 4, 5], 'stale_records': [], 'sent': [2]}, 'frames': [['BLOCKED', 3]]}, {'phase': 'exhausted', 'registers': {'credits': 3, 'lease': 2, 'inflight': [2], 'queue': [4, 5], 'stale_records': [], 'sent': [2, 3]}, 'frames': [['BLOCKED', 3]]}, {'phase': 'usable', 'registers': {'credits': 4, 'lease': 2, 'inflight': [2], 'queue': [4, 5], 'stale_records': [], 'sent': [2, 3]}, 'frames': [['BLOCKED', 3]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 2, 'inflight': [2], 'queue': [2, 3, 4, 5], 'stale_records': [], 'sent': []}, 'frames': [['reject', [2, 3, 4, 5]]]}])], 3: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 5]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 4, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 3]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 3]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke', 'new_grant'], [{'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 3, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 4, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 4, 'inflight': [], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh', 'lease_expired'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [4, 5, 6, 7], 'stale_records': [], 'sent': [3]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'exhausted', 'registers': {'credits': 4, 'lease': 3, 'inflight': [3], 'queue': [5, 6, 7], 'stale_records': [], 'sent': [3, 4]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'usable', 'registers': {'credits': 5, 'lease': 3, 'inflight': [3], 'queue': [5, 6, 7], 'stale_records': [], 'sent': [3, 4]}, 'frames': [['BLOCKED', 4]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [5, 6, 7], 'stale_records': [], 'sent': [3, 4]}, 'frames': [['BLOCKED', 4]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 3, 'inflight': [3], 'queue': [3, 4, 5, 6, 7], 'stale_records': [], 'sent': []}, 'frames': [['reject', [3, 4, 5, 6, 7]]]}])], 4: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 6]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 5, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 4]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 4]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke', 'new_grant', 'spend_last'], [{'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 4, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 5, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 5, 'inflight': [], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 5, 'lease': 5, 'inflight': [], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh', 'lease_expired', 'old_grant'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [5, 6, 7, 8, 9], 'stale_records': [], 'sent': [4]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'exhausted', 'registers': {'credits': 5, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'usable', 'registers': {'credits': 6, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [6, 7, 8, 9], 'stale_records': [], 'sent': [4, 5]}, 'frames': [['BLOCKED', 5], ['STALE', 4]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 4, 'inflight': [4], 'queue': [4, 5, 6, 7, 8, 9], 'stale_records': [], 'sent': []}, 'frames': [['reject', [4, 5, 6, 7, 8, 9]]]}])], 5: [('none/grant', 'none', ['grant'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/spend_last', 'usable', ['spend_last'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}]), ('exhausted/payload', 'exhausted', ['payload'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['BLOCKED', 7]]}]), ('usable/revoke', 'usable', ['revoke'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/inflight_ack', 'revoked', ['inflight_ack'], [{'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('revoked/new_grant', 'revoked', ['new_grant'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('usable/lease_expired', 'usable', ['lease_expired'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('expired/old_grant', 'expired', ['old_grant'], [{'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['STALE', 5]]}]), ('exhausted/refresh', 'exhausted', ['refresh'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}]), ('none/ack', 'none', ['ack'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['UNSOLICITED_ACK', 5]]}]), ('ordered trace 0', 'none', ['grant', 'revoke', 'inflight_ack', 'new_grant', 'revoke', 'new_grant', 'spend_last', 'refresh'], [{'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 5, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'revoked', 'registers': {'credits': 0, 'lease': 6, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 6, 'lease': 6, 'inflight': [], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 6, 'inflight': [], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}]), ('ordered trace 3', 'usable', ['spend_last', 'payload', 'refresh', 'spend_last', 'refresh', 'lease_expired', 'old_grant', 'old_grant'], [{'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': []}, {'phase': 'exhausted', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'exhausted', 'registers': {'credits': 6, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'usable', 'registers': {'credits': 7, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6], ['STALE', 5]]}, {'phase': 'expired', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [7, 8, 9, 10, 11], 'stale_records': [], 'sent': [5, 6]}, 'frames': [['BLOCKED', 6], ['STALE', 5], ['STALE', 5]]}]), ('empty input', 'none', [], []), ('unknown event', 'none', ['unsupported'], [{'phase': 'none', 'registers': {'credits': 0, 'lease': 5, 'inflight': [5], 'queue': [5, 6, 7, 8, 9, 10, 11], 'stale_records': [], 'sent': []}, 'frames': [['reject', [5, 6, 7, 8, 9, 10, 11]]]}])]}\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-credit_lease-usable-spend_last","generated_at":"2026-09-29T14:40:03.295078+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 usable, classify spend_last as transition to exhausted and emit send_one.","root_cause":"In usable, the spend last handler runs send one and enters usable; it must instead run send one and enter exhausted.","sha256":"7ceac1cc2dbcae549936b02e8d07af64fa9b576d048428530eee9fc7db03f867","title":"Receiver-issued transmission-credit lease controller: usable / spend last · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":48.861,"exit_code":1,"observations":[{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"none/grant","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"exhausted","registers":{"credits":1,"inflight":[1],"lease":1,"queue":[],"sent":[],"stale_records":[]}}],"check":"usable/spend_last","expected":[{"frames":[],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}}],"passed":false},{"actual":[{"frames":[["BLOCKED",3]],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"exhausted/payload","expected":[{"frames":[["BLOCKED",3]],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"usable/revoke","expected":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"revoked/inflight_ack","expected":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"revoked/new_grant","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"usable/lease_expired","expected":[{"frames":[],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[["STALE",1]],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"expired/old_grant","expected":[{"frames":[["STALE",1]],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"exhausted/refresh","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[["UNSOLICITED_ACK",1]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"none/ack","expected":[{"frames":[["UNSOLICITED_ACK",1]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"ordered trace 0","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"exhausted","registers":{"credits":1,"inflight":[1],"lease":1,"queue":[],"sent":[],"stale_records":[]}},{"frames":[["BLOCKED",0]],"phase":"exhausted","registers":{"credits":1,"inflight":[1],"lease":1,"queue":[],"sent":[],"stale_records":[]}},{"frames":[["BLOCKED",0]],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[],"sent":[],"stale_records":[]}},{"frames":[["BLOCKED",0]],"phase":"exhausted","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[],"sent":[],"stale_records":[]}}],"check":"ordered trace 3","expected":[{"frames":[],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"exhausted","registers":{"credits":2,"inflight":[1],"lease":1,"queue":[3],"sent":[1,2],"stale_records":[]}}],"passed":false},{"actual":[],"check":"empty input","expected":[],"passed":true},{"actual":[{"frames":[["reject",[1,2,3]]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"unknown event","expected":[{"frames":[["reject",[1,2,3]]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"none/grant\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"usable/spend_last\", \"actual\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 1, \"lease\": 1, \"inflight\": [1], \"queue\": [], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": []}], \"passed\": false}, {\"check\": \"exhausted/payload\", \"actual\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"BLOCKED\", 3]]}], \"expected\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"BLOCKED\", 3]]}], \"passed\": true}, {\"check\": \"usable/revoke\", \"actual\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"revoked/inflight_ack\", \"actual\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"revoked/new_grant\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"usable/lease_expired\", \"actual\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"expired/old_grant\", \"actual\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"STALE\", 1]]}], \"expected\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"STALE\", 1]]}], \"passed\": true}, {\"check\": \"exhausted/refresh\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"none/ack\", \"actual\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"UNSOLICITED_ACK\", 1]]}], \"expected\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"UNSOLICITED_ACK\", 1]]}], \"passed\": true}, {\"check\": \"ordered trace 0\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"ordered trace 3\", \"actual\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 1, \"lease\": 1, \"inflight\": [1], \"queue\": [], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"exhausted\", \"registers\": {\"credits\": 1, \"lease\": 1, \"inflight\": [1], \"queue\": [], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"BLOCKED\", 0]]}, {\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"BLOCKED\", 0]]}, {\"phase\": \"exhausted\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"BLOCKED\", 0]]}], \"expected\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": []}, {\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": [[\"BLOCKED\", 2]]}, {\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": [[\"BLOCKED\", 2]]}, {\"phase\": \"exhausted\", \"registers\": {\"credits\": 2, \"lease\": 1, \"inflight\": [1], \"queue\": [3], \"stale_records\": [], \"sent\": [1, 2]}, \"frames\": [[\"BLOCKED\", 2]]}], \"passed\": false}, {\"check\": \"empty input\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"unknown event\", \"actual\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"reject\", [1, 2, 3]]]}], \"expected\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"reject\", [1, 2, 3]]]}], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":46.233,"exit_code":1,"observations":[{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"none/grant","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"usable","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}}],"check":"usable/spend_last","expected":[{"frames":[],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}}],"passed":false},{"actual":[{"frames":[["BLOCKED",3]],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"exhausted/payload","expected":[{"frames":[["BLOCKED",3]],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"usable/revoke","expected":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"revoked/inflight_ack","expected":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"revoked/new_grant","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"usable/lease_expired","expected":[{"frames":[],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[["STALE",1]],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"expired/old_grant","expected":[{"frames":[["STALE",1]],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"exhausted/refresh","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[["UNSOLICITED_ACK",1]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"none/ack","expected":[{"frames":[["UNSOLICITED_ACK",1]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"ordered trace 0","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"usable","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["reject",[1,2,3]]],"phase":"usable","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["reject",[1,2,3]],["reject",[1,2,3]]],"phase":"usable","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["reject",[1,2,3]],["reject",[1,2,3]]],"phase":"usable","registers":{"credits":-1,"inflight":[1],"lease":1,"queue":[3],"sent":[1,2],"stale_records":[]}}],"check":"ordered trace 3","expected":[{"frames":[],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"exhausted","registers":{"credits":2,"inflight":[1],"lease":1,"queue":[3],"sent":[1,2],"stale_records":[]}}],"passed":false},{"actual":[],"check":"empty input","expected":[],"passed":true},{"actual":[{"frames":[["reject",[1,2,3]]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"unknown event","expected":[{"frames":[["reject",[1,2,3]]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"none/grant\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"usable/spend_last\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": []}], \"expected\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": []}], \"passed\": false}, {\"check\": \"exhausted/payload\", \"actual\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"BLOCKED\", 3]]}], \"expected\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"BLOCKED\", 3]]}], \"passed\": true}, {\"check\": \"usable/revoke\", \"actual\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"revoked/inflight_ack\", \"actual\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"revoked/new_grant\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"usable/lease_expired\", \"actual\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"expired/old_grant\", \"actual\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"STALE\", 1]]}], \"expected\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"STALE\", 1]]}], \"passed\": true}, {\"check\": \"exhausted/refresh\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"none/ack\", \"actual\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"UNSOLICITED_ACK\", 1]]}], \"expected\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"UNSOLICITED_ACK\", 1]]}], \"passed\": true}, {\"check\": \"ordered trace 0\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"ordered trace 3\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": []}, {\"phase\": \"usable\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": [[\"reject\", [1, 2, 3]]]}, {\"phase\": \"usable\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": [[\"reject\", [1, 2, 3]], [\"reject\", [1, 2, 3]]]}, {\"phase\": \"usable\", \"registers\": {\"credits\": -1, \"lease\": 1, \"inflight\": [1], \"queue\": [3], \"stale_records\": [], \"sent\": [1, 2]}, \"frames\": [[\"reject\", [1, 2, 3]], [\"reject\", [1, 2, 3]]]}], \"expected\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": []}, {\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": [[\"BLOCKED\", 2]]}, {\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": [[\"BLOCKED\", 2]]}, {\"phase\": \"exhausted\", \"registers\": {\"credits\": 2, \"lease\": 1, \"inflight\": [1], \"queue\": [3], \"stale_records\": [], \"sent\": [1, 2]}, \"frames\": [[\"BLOCKED\", 2]]}], \"passed\": false}, {\"check\": \"empty input\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"unknown event\", \"actual\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"reject\", [1, 2, 3]]]}], \"expected\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"reject\", [1, 2, 3]]]}], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":46.388,"exit_code":0,"observations":[{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"none/grant","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}}],"check":"usable/spend_last","expected":[{"frames":[],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[["BLOCKED",3]],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"exhausted/payload","expected":[{"frames":[["BLOCKED",3]],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"usable/revoke","expected":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"revoked/inflight_ack","expected":[{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"revoked/new_grant","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"usable/lease_expired","expected":[{"frames":[],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[["STALE",1]],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"expired/old_grant","expected":[{"frames":[["STALE",1]],"phase":"expired","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"exhausted/refresh","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[["UNSOLICITED_ACK",1]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"none/ack","expected":[{"frames":[["UNSOLICITED_ACK",1]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"ordered trace 0","expected":[{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"revoked","registers":{"credits":0,"inflight":[],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}},{"frames":[],"phase":"usable","registers":{"credits":3,"inflight":[],"lease":2,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true},{"actual":[{"frames":[],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"exhausted","registers":{"credits":2,"inflight":[1],"lease":1,"queue":[3],"sent":[1,2],"stale_records":[]}}],"check":"ordered trace 3","expected":[{"frames":[],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"exhausted","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"usable","registers":{"credits":3,"inflight":[1],"lease":1,"queue":[2,3],"sent":[1],"stale_records":[]}},{"frames":[["BLOCKED",2]],"phase":"exhausted","registers":{"credits":2,"inflight":[1],"lease":1,"queue":[3],"sent":[1,2],"stale_records":[]}}],"passed":true},{"actual":[],"check":"empty input","expected":[],"passed":true},{"actual":[{"frames":[["reject",[1,2,3]]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"check":"unknown event","expected":[{"frames":[["reject",[1,2,3]]],"phase":"none","registers":{"credits":0,"inflight":[1],"lease":1,"queue":[1,2,3],"sent":[],"stale_records":[]}}],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"none/grant\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"usable/spend_last\", \"actual\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": []}], \"expected\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": []}], \"passed\": true}, {\"check\": \"exhausted/payload\", \"actual\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"BLOCKED\", 3]]}], \"expected\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"BLOCKED\", 3]]}], \"passed\": true}, {\"check\": \"usable/revoke\", \"actual\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"revoked/inflight_ack\", \"actual\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"revoked/new_grant\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"usable/lease_expired\", \"actual\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"expired/old_grant\", \"actual\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"STALE\", 1]]}], \"expected\": [{\"phase\": \"expired\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"STALE\", 1]]}], \"passed\": true}, {\"check\": \"exhausted/refresh\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"none/ack\", \"actual\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"UNSOLICITED_ACK\", 1]]}], \"expected\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"UNSOLICITED_ACK\", 1]]}], \"passed\": true}, {\"check\": \"ordered trace 0\", \"actual\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"expected\": [{\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"revoked\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}, {\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 2, \"inflight\": [], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": []}], \"passed\": true}, {\"check\": \"ordered trace 3\", \"actual\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": []}, {\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": [[\"BLOCKED\", 2]]}, {\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": [[\"BLOCKED\", 2]]}, {\"phase\": \"exhausted\", \"registers\": {\"credits\": 2, \"lease\": 1, \"inflight\": [1], \"queue\": [3], \"stale_records\": [], \"sent\": [1, 2]}, \"frames\": [[\"BLOCKED\", 2]]}], \"expected\": [{\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": []}, {\"phase\": \"exhausted\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": [[\"BLOCKED\", 2]]}, {\"phase\": \"usable\", \"registers\": {\"credits\": 3, \"lease\": 1, \"inflight\": [1], \"queue\": [2, 3], \"stale_records\": [], \"sent\": [1]}, \"frames\": [[\"BLOCKED\", 2]]}, {\"phase\": \"exhausted\", \"registers\": {\"credits\": 2, \"lease\": 1, \"inflight\": [1], \"queue\": [3], \"stale_records\": [], \"sent\": [1, 2]}, \"frames\": [[\"BLOCKED\", 2]]}], \"passed\": true}, {\"check\": \"empty input\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"unknown event\", \"actual\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"reject\", [1, 2, 3]]]}], \"expected\": [{\"phase\": \"none\", \"registers\": {\"credits\": 0, \"lease\": 1, \"inflight\": [1], \"queue\": [1, 2, 3], \"stale_records\": [], \"sent\": []}, \"frames\": [[\"reject\", [1, 2, 3]]]}], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}