#!/usr/bin/env bash
# misc_lts_diagnose — smoke test for `nucleos lts-diagnose`, the
# per-state verbose LTS-exploration tracer used to localise
# weak-failures divergences (task #128; see memory
# project_external_real_bug + the `external_spont_reply_split`
# lts test-model).
#
# Fixture: an `external` requires port with a request/response
# (doit -> done) plus a synchronous nondet bool `status` called in
# a reply-gated chain while `done` is pending — the same shape that
# exercises the external-spontaneous (`__fire__`) pre-call path.
#
# The post-trigger state id (where the `on p.go` body enumerate
# starts) is discovered from the generated .aut so the test is
# robust to state-numbering changes. Asserts the expected `[dbg]`
# trace kinds: the enumerate header, emitted edges, the
# AwaitingExternalSpontaneous fire/no-fire path tags,
# commit_requires_call replies, dedup NEW/MERGE records, and the
# trailing outgoing-edges dump. Pins the diagnostic's contract so
# refactors of the step_frontier hooks don't silently break it.
set -euo pipefail

F="$NUCTEST_TMPDIR/diag.dzn"
cat > "$F" <<'EOF'
interface Iext {
  in void doit();
  in bool status();
  out void done();
  behavior {
    enum S { Idle, Busy };
    S s = S.Idle;
    [s.Idle] on doit: s = S.Busy;
    [s.Busy] on inevitable: { done; s = S.Idle; }
    on status: reply(true);
    on status: reply(false);
  }
}
interface Iprov { in void go(); behavior { on go: {} } }
component diag {
  provides Iprov p;
  requires external Iext e;
  behavior {
    enum W { Free, Wait };
    W w = W.Free;
    [w.Free] on p.go(): {
      e.doit();
      bool b = e.status();
      if (b) b = e.status();
      w = W.Wait;
    }
    [w.Wait] on p.go(): {}
    on e.done(): { w = W.Free; }
  }
}
EOF

# Discover the post-trigger state: the target of the first `p.go`
# edge is where the handler body enumerate starts.
"$NUCLEOS" lts -m diag --queue-size-external 2 "$F" > "$NUCTEST_TMPDIR/diag.aut"
state=$(grep -oE '^\([0-9]+,"p\.go",[0-9]+\)' "$NUCTEST_TMPDIR/diag.aut" \
        | head -1 | sed -E 's/^\([0-9]+,"p\.go",([0-9]+)\)/\1/')
if [[ -z "$state" ]]; then
  echo "FAIL: no p.go edge in generated LTS" >&2
  cat "$NUCTEST_TMPDIR/diag.aut" >&2
  exit 1
fi
echo "discovered post-trigger state = $state"

out=$("$NUCLEOS" lts-diagnose -m diag --state "$state" --queue-size-external 2 "$F" 2>&1)

fail() { echo "MISSING: $1" >&2; echo "--- output ---" >&2; echo "$out" >&2; exit 1; }

echo "$out" | grep -q "enumerate start: post-trigger state $state" || fail "enumerate-start header"
echo "$out" | grep -qE '\[dbg\] +emit  [0-9]+ --e\.doit--> '      || fail "emit edge (e.doit)"
echo "$out" | grep -q 'AwaitingExternalSpontaneous: __no_fire__'  || fail "no_fire path tag"
echo "$out" | grep -q 'AwaitingExternalSpontaneous: __fire__'     || fail "fire path tag"
echo "$out" | grep -q 'commit_requires_call e.status external=true' || fail "commit_requires_call line"
echo "$out" | grep -qE 'record (NEW|MERGE)'                       || fail "dedup record line"
echo "$out" | grep -q -- "--- outgoing edges of state $state ---" || fail "outgoing-edges dump"

# Negative control: gating on a non-existent state emits no
# enumerate trace (only the lts-diagnose banner).
out2=$("$NUCLEOS" lts-diagnose -m diag --state 999999 --queue-size-external 2 "$F" 2>&1)
if echo "$out2" | grep -q 'enumerate start'; then
  echo "FAIL: gating leaked — enumerate trace fired for a non-target state" >&2
  exit 1
fi

echo "ok: lts-diagnose streamed the expected [dbg] trace for state $state"
