#!/usr/bin/env bash
# misc_verify_failfast — fail-fast is the verify default (no CLI flag); it must
# produce byte-identical output to a full (non-fail-fast) exploration.
#
# `verify` without `-k` stops at the first failing check, so it may truncate
# LTS exploration at the first error edge. The dev knob NUC_VERIFY_NO_FAILFAST=1
# forces full exploration. This test pins the invariant
#
#     verify  ==  NUC_VERIFY_NO_FAILFAST=1 verify        (byte-for-byte)
#
# across the three code paths fail-fast can take, using committed sibling
# models so the assertion stays meaningful even as their verdicts evolve:
#
#   1. report     — error edge IS the verdict; truncate + report it, and the
#                   unexplored BFS frontier must not be mistaken for deadlocks.
#   2. nondet     — non-determinism must NOT truncate (later checks need the
#                   full graph), so output matches full exploration.
#   3. fallback   — error edge is dedup'd / not reported; the speculative
#                   truncation is a red herring, so verify rebuilds the full
#                   LTS before running compliance.
#
# nuctest's own verify category always passes -k (fail-fast gates off there),
# so THIS test is the only automated coverage of the no-`k` fail-fast path.
set -euo pipefail

ROOT="$MODEL_DIR/.."

# assert_identical <label> <model-dir-name> [extra verify args...]
assert_identical() {
    local label="$1" name="$2"; shift 2
    local dir="$ROOT/$name" dzn="$ROOT/$name/$name.dzn"
    if [ ! -f "$dzn" ]; then
        echo "FAIL[$label]: fixture model '$name' not found at $dzn" >&2
        exit 1
    fi
    local base=(-v verify -I "$dir" -m "$name" "$@")
    # Fail-fast (default) vs full exploration (--full-lts). Must be identical.
    "$NUCLEOS" "${base[@]}"            "$dzn" > "$NUCTEST_TMPDIR/$name.ff"   2>&1 || true
    "$NUCLEOS" "${base[@]}" --full-lts "$dzn" > "$NUCTEST_TMPDIR/$name.full" 2>&1 || true
    if ! diff -q "$NUCTEST_TMPDIR/$name.full" "$NUCTEST_TMPDIR/$name.ff" > /dev/null; then
        echo "FAIL[$label]: fail-fast output differs from full exploration for '$name'" >&2
        diff -u "$NUCTEST_TMPDIR/$name.full" "$NUCTEST_TMPDIR/$name.ff" >&2 || true
        exit 1
    fi
    # Positive evidence the run actually produced verify output (guards against
    # both sides being empty due to a crash — diff would pass vacuously).
    if ! grep -q "^verify: " "$NUCTEST_TMPDIR/$name.ff"; then
        echo "FAIL[$label]: no verify output for '$name' (crash?)" >&2
        cat "$NUCTEST_TMPDIR/$name.ff" >&2
        exit 1
    fi
}

# 1. report: illegal action — truncates at the <illegal> edge and reports it.
assert_identical report   compliance_provides_illegal

# 2. nondet: non-deterministic component with reachable deadlock — fail-fast
#    must keep exploring past the non-determinism so the deadlock still shows.
assert_identical nondet   determinism_deadlock

# 3. fallback: external out-events whose error edges are dedup'd; compliance
#    must see the full LTS (queue-size-external from this model's META).
assert_identical fallback external_multiple_out1 --queue-size-external 2

# ── `lts` consistency ────────────────────────────────────────────────────
# `lts` is fail-fast by default (the same graph verify consumes) with the same
# fallback; `--full-lts` forces complete exploration.

# lts_aut <out> <model> [extra args...] — capture an .aut, fail if it's not a
# well-formed Aldebaran graph.
lts_aut() {
    local out="$1" name="$2"; shift 2
    local dir="$ROOT/$name"
    "$NUCLEOS" lts "$@" -I "$dir" -m "$name" "$dir/$name.dzn" > "$out" 2>/dev/null || true
    if ! head -1 "$out" | grep -q '^des ('; then
        echo "FAIL[lts]: '$name' ($*) produced no .aut header" >&2
        head -5 "$out" >&2
        exit 1
    fi
}

# The fallback model: a dedup'd error edge triggers speculative truncation that
# is then discarded, so default `lts` must equal `lts --full-lts` (the fallback
# rebuilt the full graph — exactly what verify did above).
lts_aut "$NUCTEST_TMPDIR/emo1.ff"   external_multiple_out1 --queue-size-external 2
lts_aut "$NUCTEST_TMPDIR/emo1.full" external_multiple_out1 --queue-size-external 2 --full-lts
if ! diff -q "$NUCTEST_TMPDIR/emo1.full" "$NUCTEST_TMPDIR/emo1.ff" > /dev/null; then
    echo "FAIL[lts]: default lts != --full-lts for external_multiple_out1 (fallback didn't rebuild)" >&2
    diff -u "$NUCTEST_TMPDIR/emo1.full" "$NUCTEST_TMPDIR/emo1.ff" >&2 || true
    exit 1
fi

# Sanity: --full-lts is still accepted on a plain model and yields a graph.
lts_aut "$NUCTEST_TMPDIR/illegal.full" compliance_provides_illegal --full-lts

echo "ok: fail-fast verify output byte-identical to full exploration; lts consistent"
