#!/usr/bin/env bash
# misc_verify_json_progress — `verify --output json` must STREAM, not batch.
#
# The output is newline-delimited JSON: a `header` line, per-check lines,
# LTS-generation `progress` events emitted as the BFS runs (even when piped /
# non-TTY — the daemon's case), and a closing `summary` line. The model has a
# large state space (two wide subints) so LTS generation runs long enough to
# emit progress.
set -euo pipefail

model="$MODEL_DIR/big.dzn"
out=$("$NUCLEOS" --output json verify -m big_state "$model" 2>/dev/null)

# Header and summary frame the stream.
grep -q '"kind": "header"'  <<<"$out" || { echo "FAIL: missing header line";  printf '%s\n' "$out" | head; exit 1; }
grep -q '"kind": "summary"' <<<"$out" || { echo "FAIL: missing summary line"; printf '%s\n' "$out" | tail; exit 1; }

# At least one LTS-gen progress event, carrying a numeric state count.
progress=$(grep -c '"kind": "progress"' <<<"$out" || true)
if [[ "$progress" -lt 1 ]]; then
  echo "FAIL: expected >=1 progress event in the JSON stream, got $progress"
  printf '%s\n' "$out" | head -20
  exit 1
fi
grep -Eq '"kind": "progress".*"states": [0-9]+' <<<"$out" \
  || { echo "FAIL: progress event missing numeric 'states' field"; exit 1; }

# Every line must be a complete JSON object (NDJSON), not a pretty-printed doc.
while IFS= read -r line; do
  [[ -z "$line" ]] && continue
  [[ "$line" == "{"*"}" ]] || { echo "FAIL: non-NDJSON line: $line"; exit 1; }
done <<<"$out"

echo "ok: verify --output json streams header + $progress progress events + summary (NDJSON)"
