#!/usr/bin/env bash
# misc_verify_no_keepgoing — `nucleos verify` WITHOUT `-k` must
# stop at the FIRST failing check within a model. dzn does this
# by default. nucleos historically only honoured `-k` BETWEEN
# models (the outer loop break); within a single model, all
# checks ran regardless of earlier failures.
#
# Reuses test-models/compliance_determinism_optional — its main
# component has TWO failing checks on its own:
#   1. check: deterministic: fail   (component is non-deterministic)
#   2. check: compliance:    fail   (component non-compliant)
#
# With -k:    both fail lines appear (existing baseline/verify ↔).
# Without -k: only deterministic fail; subsequent check lines
#             (illegal/deadlock/unreachable/livelock/compliance)
#             must NOT appear. dzn-compat.
#
# This test FAILED on the codebase before the dzn-compat fix
# (nucleos would emit all six check lines unconditionally) — a
# regression now means someone restored the always-run-all-checks
# behavior.
set -euo pipefail

SISTER="$MODEL_DIR/../compliance_determinism_optional/compliance_determinism_optional.dzn"

set +e
"$NUCLEOS" -v verify -m compliance_determinism_optional "$SISTER" \
    > "$NUCTEST_TMPDIR/stdout.txt" 2> "$NUCTEST_TMPDIR/stderr.txt"
exit_code=$?
set -e

# Verify must exit non-zero on any failure (basic sanity).
if [ "$exit_code" = 0 ]; then
    echo "FAIL: verify exited 0 despite the model having a failing check" >&2
    cat "$NUCTEST_TMPDIR/stderr.txt" >&2
    exit 1
fi

# The first failing check (deterministic) MUST appear.
if ! grep -q "deterministic: fail" "$NUCTEST_TMPDIR/stderr.txt"; then
    echo "FAIL: expected 'deterministic: fail' line in stderr" >&2
    cat "$NUCTEST_TMPDIR/stderr.txt" >&2
    exit 1
fi

# Subsequent check lines for this same model must NOT appear
# without -k. Probe each one we KNOW would otherwise be emitted.
for forbidden in \
    "compliance_determinism_optional: check: illegal" \
    "compliance_determinism_optional: check: deadlock" \
    "compliance_determinism_optional: check: unreachable" \
    "compliance_determinism_optional: check: livelock" \
    "compliance_determinism_optional: check: compliance"; do
    if grep -qF "$forbidden" "$NUCTEST_TMPDIR/stderr.txt"; then
        echo "FAIL: '$forbidden' appeared without -k — nucleos continued past first failure" >&2
        echo "      dzn-compat semantics require stopping at the first failing check." >&2
        echo "      stderr was:" >&2
        cat "$NUCTEST_TMPDIR/stderr.txt" >&2
        exit 1
    fi
done

# Sanity: the same model WITH -k SHOULD show the additional checks.
# (Inverse gate — keeps this from being a one-sided assertion that
# could pass spuriously if the verify subcommand started silently
# eating all output.)
"$NUCLEOS" -v verify -k -m compliance_determinism_optional "$SISTER" \
    > "$NUCTEST_TMPDIR/stdout.k.txt" 2> "$NUCTEST_TMPDIR/stderr.k.txt" || true

if ! grep -q "compliance_determinism_optional: check: compliance" "$NUCTEST_TMPDIR/stderr.k.txt"; then
    echo "FAIL: with -k, 'check: compliance' line was missing — verify is broken in a different way" >&2
    cat "$NUCTEST_TMPDIR/stderr.k.txt" >&2
    exit 1
fi
